Nevanlinna/holomorphic_JensenFormula.lean

@@ -1,13 +1,6 @@
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
 
-lemma int₀
-  {a : ℂ}
-  (ha : a ∈ Metric.ball 0 1)
-  :
-  ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - a‖ = 0 := by
-    sorry
-
 
 theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
@@ -71,32 +64,21 @@ theorem jensen_case_R_eq_one
     exact hz A
 
   have s₁ : ∀ z, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
-    intro z hz
+    sorry
-    rw [s₀ z hz]
-    simp
 
   rw [s₁ 0 h₂f] at t₁
 
-  have h₀ {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by
+  have {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by
-    rw [h₃F]
+    sorry
-    simp
-    constructor
-    · exact h₂F (circleMap 0 1 x)
-    · by_contra h'
-      obtain ⟨s, _, h₂s⟩  := Finset.prod_eq_zero_iff.1 h'
-      have : circleMap 0 1 x = a s := by
-        rw [← sub_zero (circleMap 0 1 x)]
-        nth_rw 2 [← h₂s]
-        simp
-      let A := ha s
-      rw [← this] at A
-      simp at A
 
-  simp_rw [s₁ (circleMap 0 1 _) h₀] at t₁
+  simp_rw [s₁ (circleMap 0 1 _) this] at t₁
   rw [intervalIntegral.integral_sub] at t₁
   rw [intervalIntegral.integral_finset_sum] at t₁
 
-  simp_rw [int₀ (ha _)] at t₁
+  have {i : S} : ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - a i‖ = 0 := by
+    sorry
+
+  simp_rw [this] at t₁
   simp at t₁
   rw [t₁]
   simp
@@ -107,7 +89,7 @@ theorem jensen_case_R_eq_one
   simp
   rfl
   -- ∀ i ∈ Finset.univ, IntervalIntegrable (fun x => Real.log ‖circleMap 0 1 x - a i‖) MeasureTheory.volume 0 (2 * Real.pi)
-  intro i _
+  intro i hi
   apply Continuous.intervalIntegrable
   apply continuous_iff_continuousAt.2
   intro x
@@ -133,7 +115,7 @@ theorem jensen_case_R_eq_one
   rw [this]
   apply ContinuousAt.comp
   simp
-  exact h₀
+  sorry
   apply ContinuousAt.comp
   apply Complex.continuous_abs.continuousAt
   apply ContinuousAt.comp
@@ -143,7 +125,7 @@ theorem jensen_case_R_eq_one
   -- IntervalIntegrable (fun x => ∑ s : { x // x ∈ S }, Real.log ‖circleMap 0 1 x - a s‖) MeasureTheory.volume 0 (2 * Real.pi)
   apply Continuous.intervalIntegrable
   apply continuous_finset_sum
-  intro i _
+  intro i hi
   apply continuous_iff_continuousAt.2
   intro x
   have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) :=

Nevanlinna/holomorphic_primitive2.lean

@@ -1,456 +0,0 @@
-import Mathlib.Analysis.Complex.TaylorSeries
-
-
-noncomputable def primitive
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] :
-  ℂ  → (ℂ → E) → (ℂ → E) := by
-  intro z₀
-  intro f
-  exact fun z ↦ (∫ (x : ℝ) in z₀.re..z.re, f ⟨x, z₀.im⟩) + Complex.I • ∫ (x : ℝ) in z₀.im..z.im, f ⟨z.re, x⟩
-
-
-theorem primitive_zeroAtBasepoint
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E)
-  (z₀ : ℂ) :
-  (primitive z₀ f) z₀ = 0 := by
-  unfold primitive
-  simp
-
-
-theorem primitive_fderivAtBasepointZero
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E)
-  (hf : Continuous f) :
-  HasDerivAt (primitive 0 f) (f 0) 0 := by
-  unfold primitive
-  simp
-  apply hasDerivAt_iff_isLittleO.2
-  simp
-  rw [Asymptotics.isLittleO_iff]
-  intro c hc
-
-  have {z : ℂ} {e : E} : z • e = (∫ (_ : ℝ) in (0)..(z.re), e) + Complex.I • ∫ (_ : ℝ) in (0)..(z.im), e:= by
-    simp
-    rw [smul_comm]
-    rw [← smul_assoc]
-    simp
-    have : z.re • e = (z.re : ℂ) • e := by exact rfl
-    rw [this, ← add_smul]
-    simp
-  conv =>
-    left
-    intro x
-    left
-    arg 1
-    arg 2
-    rw [this]
-  have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
-    abel
-  have t₀ {r : ℝ} : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by
-    apply Continuous.intervalIntegrable
-    apply Continuous.comp
-    exact hf
-    have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl
-    rw [this]
-    continuity
-  have t₁ {r : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
-    apply Continuous.intervalIntegrable
-    apply Continuous.comp
-    exact hf
-    fun_prop
-  have t₂ {a b : ℝ} : IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by
-    apply Continuous.intervalIntegrable
-    apply Continuous.comp hf
-    have : (Complex.mk a) = (fun x => Complex.I • Complex.ofRealCLM x + { re := a, im := 0 }) := by
-      funext x
-      apply Complex.ext
-      rw [Complex.add_re]
-      simp
-      simp
-    rw [this]
-    apply Continuous.add
-    continuity
-    fun_prop
-
-  have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by
-    apply Continuous.intervalIntegrable
-    apply Continuous.comp
-    exact hf
-    fun_prop
-  conv =>
-    left
-    intro x
-    left
-    arg 1
-    rw [this]
-    rw [← smul_sub]
-    rw [← intervalIntegral.integral_sub t₀ t₁]
-    rw [← intervalIntegral.integral_sub t₂ t₃]
-  rw [Filter.eventually_iff_exists_mem]
-
-  let s := f⁻¹' Metric.ball (f 0) (c / (4 : ℝ))
-  have h₁s : IsOpen s := IsOpen.preimage hf Metric.isOpen_ball
-  have h₂s : 0 ∈ s := by
-    apply Set.mem_preimage.mpr
-    apply Metric.mem_ball_self
-    linarith
-
-  obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 h₁s 0 h₂s
-
-  have h₃ε : ∀ y ∈ Metric.ball 0 ε, ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by
-    intro y hy
-    apply mem_ball_iff_norm.mp (h₂ε hy)
-
-  use Metric.ball 0 (ε / (4 : ℝ))
-  constructor
-  · apply Metric.ball_mem_nhds 0
-    linarith
-  · intro y hy
-    have h₁y : |y.re| < ε / 4 := by
-      calc |y.re|
-      _ ≤ Complex.abs y := by apply Complex.abs_re_le_abs
-      _ < ε / 4 := by
-        let A := mem_ball_iff_norm.1 hy
-        simp at A
-        linarith
-    have h₂y : |y.im| < ε / 4 := by
-      calc |y.im|
-      _ ≤ Complex.abs y := by apply Complex.abs_im_le_abs
-      _ < ε / 4 := by
-        let A := mem_ball_iff_norm.1 hy
-        simp at A
-        linarith
-
-    have intervalComputation {x' y' : ℝ} (h : x' ∈ Ι 0 y') : |x'| ≤ |y'| := by
-      let A := h.1
-      let B := h.2
-      rcases le_total 0 y' with hy | hy
-      · simp [hy] at A
-        simp [hy] at B
-        rw [abs_of_nonneg hy]
-        rw [abs_of_nonneg (le_of_lt A)]
-        exact B
-      · simp [hy] at A
-        simp [hy] at B
-        rw [abs_of_nonpos hy]
-        rw [abs_of_nonpos]
-        linarith [h.1]
-        exact B
-
-    have t₁ : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ (c / (4 : ℝ)) * |y.re - 0| := by
-      apply intervalIntegral.norm_integral_le_of_norm_le_const
-      intro x hx
-
-      have h₁x : |x| < ε / 4 := by
-        calc |x|
-          _ ≤ |y.re| := intervalComputation hx
-          _ < ε / 4 := h₁y
-      apply le_of_lt
-      apply h₃ε { re := x, im := 0 }
-      rw [mem_ball_iff_norm]
-      simp
-      have : { re := x, im := 0 } = (x : ℂ) := by rfl
-      rw [this]
-      rw [Complex.abs_ofReal]
-      linarith
-
-    have t₂ : ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ ≤ (c / (4 : ℝ)) * |y.im - 0| := by
-      apply intervalIntegral.norm_integral_le_of_norm_le_const
-      intro x hx
-
-      have h₁x : |x| < ε / 4 := by
-        calc |x|
-          _ ≤ |y.im| := intervalComputation hx
-          _ < ε / 4 := h₂y
-
-      apply le_of_lt
-      apply h₃ε { re := y.re, im := x }
-      simp
-
-      calc Complex.abs { re := y.re, im := x }
-        _ ≤ |y.re| + |x| := by
-          apply Complex.abs_le_abs_re_add_abs_im { re := y.re, im := x }
-        _ < ε := by
-          linarith
-
-    calc ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0) + Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖
-      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
-        apply norm_add_le
-      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
-        simp
-        rw [norm_smul]
-        simp
-      _ ≤ (c / (4 : ℝ)) * |y.re - 0| + (c / (4 : ℝ)) * |y.im - 0| := by
-        apply add_le_add
-        exact t₁
-        exact t₂
-      _ ≤ (c / (4 : ℝ)) * (|y.re| + |y.im|) := by
-        simp
-        rw [mul_add]
-      _ ≤ (c / (4 : ℝ)) * (4 * ‖y‖) := by
-        have : |y.re| + |y.im| ≤ 4 * ‖y‖ := by
-          calc |y.re| + |y.im|
-            _ ≤ ‖y‖ + ‖y‖ := by
-              apply add_le_add
-              apply Complex.abs_re_le_abs
-              apply Complex.abs_im_le_abs
-            _ ≤ 4 * ‖y‖ := by
-              rw [← two_mul]
-              apply mul_le_mul
-              linarith
-              rfl
-              exact norm_nonneg y
-              linarith
-
-        apply mul_le_mul
-        rfl
-        exact this
-        apply add_nonneg
-        apply abs_nonneg
-        apply abs_nonneg
-        linarith
-      _ ≤ c * ‖y‖ := by
-        linarith
-
-
-theorem primitive_translation
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E)
-  (z₀ t : ℂ) :
-  primitive z₀ (f ∘ fun z ↦ (z - t)) = ((primitive (z₀ - t) f) ∘ fun z ↦ (z - t)) := by
-  funext z
-  unfold primitive
-  simp
-
-  let g : ℝ → E := fun x ↦ f ( {re := x, im := z₀.im - t.im} )
-  have {x : ℝ} : f ({ re := x, im := z₀.im } - t) = g (1*x - t.re) := by
-    congr 1
-    apply Complex.ext <;> simp
-  conv =>
-    left
-    left
-    arg 1
-    intro x
-    rw [this]
-  rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.re)]
-  simp
-
-  congr 1
-  let g : ℝ → E := fun x ↦ f ( {re := z.re - t.re, im := x} )
-  have {x : ℝ} : f ({ re := z.re, im := x} - t) = g (1*x - t.im) := by
-    congr 1
-    apply Complex.ext <;> simp
-  conv =>
-    left
-    arg 1
-    intro x
-    rw [this]
-  rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.im)]
-  simp
-
-
-theorem primitive_hasDerivAtBasepoint
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Continuous f)
-  (z₀ : ℂ) :
-  HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
-
-  let g := f ∘ fun z ↦ z + z₀
-  have : Continuous g := by continuity
-  let A := primitive_fderivAtBasepointZero g this
-  simp at A
-
-  let B := primitive_translation g z₀ z₀
-  simp at B
-  have : (g ∘ fun z ↦ (z - z₀)) = f := by
-    funext z
-    dsimp [g]
-    simp
-  rw [this] at B
-  rw [B]
-  have : f z₀ = (1 : ℂ) • (f z₀) := by
-    exact (MulAction.one_smul (f z₀)).symm
-  conv =>
-    arg 2
-    rw [this]
-
-  apply HasDerivAt.scomp
-  simp
-  have : g 0 = f z₀ := by simp [g]
-  rw [← this]
-  exact A
-  apply HasDerivAt.sub_const
-  have : (fun (x : ℂ) ↦ x) = id := by
-    funext x
-    simp
-  rw [this]
-  exact hasDerivAt_id z₀
-
-
-lemma integrability₁
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E)
-  (hf : Differentiable ℂ f)
-  (a₁ a₂ b : ℝ) :
-  IntervalIntegrable (fun x => f { re := x, im := b }) MeasureTheory.volume a₁ a₂ := by
-  apply Continuous.intervalIntegrable
-  apply Continuous.comp
-  exact Differentiable.continuous hf
-  have : ((fun x => { re := x, im := b }) : ℝ → ℂ) = (fun x => Complex.ofRealCLM x + { re := 0, im := b }) := by
-    funext x
-    apply Complex.ext
-    rw [Complex.add_re]
-    simp
-    rw [Complex.add_im]
-    simp
-  rw [this]
-  continuity
-
-
-lemma integrability₂
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E)
-  (hf : Differentiable ℂ f)
-  (a₁ a₂ b : ℝ) :
-  IntervalIntegrable (fun x => f { re := b, im := x }) MeasureTheory.volume a₁ a₂ := by
-  apply Continuous.intervalIntegrable
-  apply Continuous.comp
-  exact Differentiable.continuous hf
-  have : (Complex.mk b) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
-    funext x
-    apply Complex.ext
-    rw [Complex.add_re]
-    simp
-    simp
-  rw [this]
-  apply Continuous.add
-  continuity
-  fun_prop
-
-
-theorem primitive_additivity
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E)
-  (hf : Differentiable ℂ f)
-  (z₀ z₁ : ℂ) :
-  (fun z ↦ (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁)) = 0 := by
-  funext z
-
-
-
-  unfold primitive
-  have : (∫ (x : ℝ) in z₀.re..z.re, f { re := x, im := z₀.im }) = (∫ (x : ℝ) in z₀.re..z₁.re, f { re := x, im := z₀.im }) + (∫ (x : ℝ) in z₁.re..z.re, f { re := x, im := z₀.im }) := by
-    rw [intervalIntegral.integral_add_adjacent_intervals]
-    apply integrability₁ f hf
-    apply integrability₁ f hf
-  rw [this]
-  have : (∫ (x : ℝ) in z₀.im..z.im, f { re := z.re, im := x }) = (∫ (x : ℝ) in z₀.im..z₁.im, f { re := z.re, im := x }) + (∫ (x : ℝ) in z₁.im..z.im, f { re := z.re, im := x }) := by
-    rw [intervalIntegral.integral_add_adjacent_intervals]
-    apply integrability₂ f hf
-    apply integrability₂ f hf
-  rw [this]
-  simp
-
-  have {a b c d e f g h : E} : (a + b) + (c + d) - (e + f) - (g + h) = b + (a - g) - e - f + d  - h + (c) := by
-    abel
-  rw [this]
-  simp
-
-  let A := Complex.integral_boundary_rect_eq_zero_of_differentiableOn f ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ (hf.differentiableOn)
-  have {x : ℝ} {w : ℂ} : ↑x + w.im * Complex.I = { re := x, im := w.im } := by
-    apply Complex.ext
-    · simp
-    · simp
-  simp_rw [this] at A
-  have {x : ℝ} {w : ℂ} : w.re + x * Complex.I = { re := w.re, im := x } := by
-    apply Complex.ext
-    · simp
-    · simp
-  simp_rw [this] at A
-  rw [← A]
-  abel
-
-
-theorem primitive_additivity'
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E)
-  (hf : Differentiable ℂ f)
-  (z₀ z₁ : ℂ) :
-  primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := by
-
-  nth_rw 1 [← sub_zero (primitive z₀ f)]
-  rw [← primitive_additivity f hf z₀ z₁]
-
-  funext z
-  simp
-  abel
-
-
-theorem primitive_hasDerivAt
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ z : ℂ) :
-  HasDerivAt (primitive z₀ f) (f z) z := by
-  rw [primitive_additivity' f hf z₀ z]
-  rw [← add_zero (f z)]
-  apply HasDerivAt.add
-  apply primitive_hasDerivAtBasepoint
-  exact hf.continuous
-  apply hasDerivAt_const
-
-
-theorem primitive_differentiable
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  Differentiable ℂ (primitive z₀ f) := by
-  intro z
-  exact (primitive_hasDerivAt hf z₀ z).differentiableAt
-
-
-theorem primitive_hasFderivAt
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  ∀ z, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ℂ ℂ).flip (f z)) z := by
-  intro z
-  rw [hasFDerivAt_iff_hasDerivAt]
-  simp
-  exact primitive_hasDerivAt hf z₀ z
-
-
-theorem primitive_hasFderivAt'
-  {f : ℂ  → ℂ}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  ∀ z, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by
-  intro z
-  rw [hasFDerivAt_iff_hasDerivAt]
-  simp
-  exact primitive_hasDerivAt hf z₀ z
-
-
-theorem primitive_fderiv
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  ∀ z, (fderiv ℂ (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ℂ ℂ).flip (f z) := by
-  intro z
-  apply HasFDerivAt.fderiv
-  exact primitive_hasFderivAt hf z₀ z
-
-
-theorem primitive_fderiv'
-  {f : ℂ  → ℂ}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  ∀ z, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by
-  intro z
-  apply HasFDerivAt.fderiv
-  exact primitive_hasFderivAt' hf z₀ z

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
+   "rev": "d2b1546c5fc05a06426e3f6ee1cb020e71be5592",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
+   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,27 +35,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.40",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"},
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e7e90d90a62e6d12cbb27cbbfc31c094ee4ecc58",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c96401c7496392a2200dc78c0b334df0561466dc",
+   "rev": "cc495260156b40dcbd55b947c047061e15344000",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.10.0-rc2