awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (ModelWithCorners.prod (𝓡 1) (𝓡 1)) (E' :=
    EuclideanSpace ℝ (Fin 1)) (𝓡 1) (M' := Circle) ω fun (p : Circle × Circle) ↦ p.1 * p.2
have hf : ContMDiff (E := EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (ModelWithCorners.prod (𝓡 1) (𝓡 1)) 𝓘(ℝ, ℂ) (M' :=
  ℂ) ω fun (p : Circle × Circle) ↦ (↑p.1 : ℂ) * (↑p.2 : ℂ)
Tactic: apply ContMDiff.codRestrict_sphere
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
⊢ ContMDiff (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (z : ℂ × ℂ) ↦ z.1 * z.2
have rw : (Continuous (Y := ℂ) fun (z : ℂ × ℂ) ↦ z.1 * z.2) ∧
  ∀ (x : ℂ × ℂ) (y : ℂ),
    ContDiffOn ℝ ω
      ((↑(extChartAt 𝓘(ℝ, ℂ) y) : ℂ → ℂ) ∘
        (fun (z : ℂ × ℂ) ↦ z.1 * z.2) ∘ (↑(extChartAt (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) x).symm : ℂ × ℂ → ℂ × ℂ))
      ((extChartAt (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) x).target ∩
        (↑(extChartAt (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) x).symm : ℂ × ℂ → ℂ × ℂ) ⁻¹'
          (fun (z : ℂ × ℂ) ↦ z.1 * z.2) ⁻¹' (extChartAt 𝓘(ℝ, ℂ) y).source)
Tactic: rw [contMDiff_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (ModelWithCorners.prod (𝓡 1) (𝓡 1)) 𝓘(ℝ, ℂ)
    (M' := ℂ) ω fun (p : Circle × Circle) ↦ (↑p.1 : ℂ) * (↑p.2 : ℂ)
have h₂ : ContMDiff (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (z : ℂ × ℂ) ↦ z.1 * z.2
Tactic: have h₂ : ContMDiff (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) ω fun z : ℂ × ℂ => z.fst * z.snd := by
      rw [contMDiff_iff]
      exact ⟨continuous_mul, fun x y => contDiff_mul.contDiffOn⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
h₂ : ContMDiff (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (z : ℂ × ℂ) ↦ z.1 * z.2
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (ModelWithCorners.prod (𝓡 1) (𝓡 1)) 𝓘(ℝ, ℂ)
    (M' := ℂ) ω fun (p : Circle × Circle) ↦ (↑p.1 : ℂ) * (↑p.2 : ℂ)
have hf : ContMDiff (E := EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (ModelWithCorners.prod (𝓡 1) (𝓡 1))
  (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) ω (Prod.map c c)
Tactic: suffices h₁ : ContMDiff _ _ _ (Prod.map c c) from
      h₂.comp h₁
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
h₂ : ContMDiff (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (z : ℂ × ℂ) ↦ z.1 * z.2
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (ModelWithCorners.prod (𝓡 1) (𝓡 1))
    (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) ω (Prod.map c c)
have hf : ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) 𝓘(ℝ, ℂ) ω c
Tactic: apply ContMDiff.prodMap
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) (E' := EuclideanSpace ℝ (Fin 1)) (𝓡 1) (M' := Circle) ω
    fun (a : Circle) ↦ a⁻¹
have hf : ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (a : Circle) ↦ (↑a : ℂ)⁻¹
Tactic: apply ContMDiff.codRestrict_sphere
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (a : Circle) ↦ (↑a : ℂ)⁻¹
have hf : ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (a : Circle) ↦
  (starRingEnd ℂ : (a : ℂ) → ℂ) (↑a : ℂ)
Tactic: simp only [← Circle.coe_inv, Circle.coe_inv_eq_conj]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) 𝓘(𝕜, R) (M' := Rˣ) n fun (p : Rˣ × Rˣ) ↦ p.1 * p.2
have apply : ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (M := Rˣ × Rˣ) 𝓘(𝕜, R) (M' := R) n
  (Function.comp (β := Rˣ) val fun (p : Rˣ × Rˣ) ↦ p.1 * p.2)
Tactic: apply ContMDiff.of_comp_isOpenEmbedding Units.isOpenEmbedding_val
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
⊢ Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
have h : ∀ (x : Rˣ × Rˣ),
  Eq (α := R) (Function.comp (β := Rˣ) val (fun (x : Rˣ × Rˣ) ↦ x.1 * x.2) x)
    (((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R))) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (M := Rˣ × Rˣ) 𝓘(𝕜, R) (M' := R) n
    (Function.comp (β := Rˣ) val fun (p : Rˣ × Rˣ) ↦ p.1 * p.2)
have this : Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
  ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
Tactic: have : (val : Rˣ → R) ∘ (fun x : Rˣ × Rˣ => x.1 * x.2) =
      (fun x : R × R => x.1 * x.2) ∘ (fun x : Rˣ × Rˣ => (x.1, x.2)) := by ext; simp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this :
  Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (M := Rˣ × Rˣ) 𝓘(𝕜, R) (M' := R) n
    (Function.comp (β := Rˣ) val fun (p : Rˣ × Rˣ) ↦ p.1 * p.2)
have rw : ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (M := Rˣ × Rˣ) 𝓘(𝕜, R) (M' := R) n
  ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this :
  Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (M := Rˣ × Rˣ) 𝓘(𝕜, R) (M' := R) n
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
have this₁ : ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (E' := R × R) 𝓘(𝕜, R × R) (M' := R × R) n fun (x : Rˣ × Rˣ) ↦
  ((↑x.1 : R), (↑x.2 : R))
Tactic: have : ContMDiff (𝓘(𝕜, R).prod 𝓘(𝕜, R)) 𝓘(𝕜, R × R) n
      (fun x : Rˣ × Rˣ => ((x.1 : R), (x.2 : R))) :=
      (contMDiff_val.comp contMDiff_fst).prodMk_space (contMDiff_val.comp contMDiff_snd)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this_1 :
  Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
this :
  ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (E' := R × R) 𝓘(𝕜, R × R) (M' := R × R) n fun (x : Rˣ × Rˣ) ↦
    ((↑x.1 : R), (↑x.2 : R))
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (M := Rˣ × Rˣ) 𝓘(𝕜, R) (M' := R) n
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
have refine : ContMDiff (E := R × R) 𝓘(𝕜, R × R) 𝓘(𝕜, R) (M' := R) n fun (x : R × R) ↦ x.1 * x.2
Tactic: refine ContMDiff.comp ?_ this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this_1 :
  Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
this :
  ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (E' := R × R) 𝓘(𝕜, R × R) (M' := R × R) n fun (x : Rˣ × Rˣ) ↦
    ((↑x.1 : R), (↑x.2 : R))
⊢ ContMDiff (E := R × R) 𝓘(𝕜, R × R) 𝓘(𝕜, R) (M' := R) n fun (x : R × R) ↦ x.1 * x.2
have rw : ContDiff 𝕜 (F := R) n fun (x : R × R) ↦ x.1 * x.2
Tactic: rw [contMDiff_iff_contDiff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
⊢ ContMDiff 𝓘(𝕜, R) 𝓘(𝕜, R) (M' := Rˣ) n fun (a : Rˣ) ↦ a⁻¹
have apply : ContMDiff 𝓘(𝕜, R) (M := Rˣ) 𝓘(𝕜, R) (M' := R) n (Function.comp (β := Rˣ) val fun (a : Rˣ) ↦ a⁻¹)
Tactic: apply ContMDiff.of_comp_isOpenEmbedding Units.isOpenEmbedding_val
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
⊢ Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)
have h : ∀ (x : Rˣ), Function.comp (β := Rˣ) val (fun (x : Rˣ) ↦ x⁻¹) x = (Ring.inverse ∘ val) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
⊢ ContMDiff 𝓘(𝕜, R) (M := Rˣ) 𝓘(𝕜, R) (M' := R) n (Function.comp (β := Rˣ) val fun (a : Rˣ) ↦ a⁻¹)
have this : Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)
Tactic: have : (val : Rˣ → R) ∘ (fun x : Rˣ => x⁻¹) = Ring.inverse ∘ val := by ext; simp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this : Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)
⊢ ContMDiff 𝓘(𝕜, R) (M := Rˣ) 𝓘(𝕜, R) (M' := R) n (Function.comp (β := Rˣ) val fun (a : Rˣ) ↦ a⁻¹)
have rw : ∀ (x : Rˣ), ContMDiffAt 𝓘(𝕜, R) 𝓘(𝕜, R) n (Ring.inverse ∘ val) x
Tactic: rw [this, ContMDiff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this : Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)
⊢ ∀ (x : Rˣ), ContMDiffAt 𝓘(𝕜, R) 𝓘(𝕜, R) n (Ring.inverse ∘ val) x
have refine : ∀ (x : Rˣ), ContMDiffAt 𝓘(𝕜, R) 𝓘(𝕜, R) n Ring.inverse (↑x : R)
Tactic: refine fun x => ContMDiffAt.comp x ?_ (contMDiff_val x)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this : Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)
x : Rˣ
⊢ ContMDiffAt 𝓘(𝕜, R) 𝓘(𝕜, R) n Ring.inverse (↑x : R)
have rw : ContDiffAt 𝕜 n Ring.inverse (↑x : R)
Tactic: rw [contMDiffAt_iff_contDiffAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
⊢ IsMIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
have mp : IsMIntegralCurveAt γ v t₀ → ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
mp : IsMIntegralCurveAt γ v t₀ → ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
⊢ IsMIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
have mpr : (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) → IsMIntegralCurveAt γ v t₀
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
h : IsMIntegralCurveAt γ v t₀
⊢ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
have h₁ : ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
Tactic: rw [IsMIntegralCurveAt, Filter.eventually_iff_exists_mem] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
h : ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
⊢ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
have mp : ∀ (s : Set ℝ) (hs : s ∈ 𝓝 t₀)
  (h : ∀ y ∈ s, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))),
  ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
Tactic: obtain ⟨s, hs, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
⊢ IsMIntegralCurveAt γ v t₀
have mpr : ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
Tactic: rw [IsMIntegralCurveAt, Filter.eventually_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
have mpr : ∀ (s' : Set ℝ) (h1 : s' ⊆ s) (h2 : IsOpen s') (h3 : t₀ ∈ s'),
  ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
Tactic: obtain ⟨s', h1, h2, h3⟩ := mem_nhds_iff.mp hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
s' : Set ℝ
h1 : s' ⊆ s
h2 : IsOpen s'
h3 : t₀ ∈ s'
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
have mpr : ∀ y ∈ s', HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
Tactic: refine ⟨s', h2.mem_nhds h3, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
s' : Set ℝ
h1 : s' ⊆ s
h2 : IsOpen s'
h3 : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
have mpr : s ∈ 𝓝 t
Tactic: apply (h t (h1 ht)).hasMFDerivAt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
s' : Set ℝ
h1 : s' ⊆ s
h2 : IsOpen s'
h3 : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
⊢ s ∈ 𝓝 t
have mpr : ∃ t_1 ⊆ s, IsOpen t_1 ∧ t ∈ t_1
Tactic: rw [mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
⊢ IsMIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
have rw : (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
Tactic: rw [isMIntegralCurveAt_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
⊢ (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
have mp : (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) → ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
mp : (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) → ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
have mpr : (∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)) → ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
⊢ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
have hs₁ : ∃ ε > 0, Metric.ball t₀ ε ⊆ s
Tactic: rw [Metric.mem_nhds_iff] at hs
Cleared hypotheses: hs, h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : ∃ ε > 0, Metric.ball t₀ ε ⊆ s
h : IsMIntegralCurveOn γ v s
⊢ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
have mp : ∀ (ε : ℝ) (hε : ε > 0) (hε' : Metric.ball t₀ ε ⊆ s), ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
Tactic: obtain ⟨ε, hε, hε'⟩ := hs
Cleared hypotheses: hs