awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y z : M
r : ℝ≥0∞
hr : riemannianEDist I x y + riemannianEDist I y z < r
u : ℝ≥0∞
hu : u > riemannianEDist I x y
v : ℝ≥0∞
hv : v > riemannianEDist I y z
huv : u + v < r
γ₁ : ℝ → M
hγ₁0 : γ₁ 0 = x
hγ₁1 : γ₁ 1 = y
hγ₁_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₁
hγ₁ : pathELength I γ₁ 0 1 < u
hγ₁_const : γ₁ =ᶠ[𝓝 1] fun (x : ℝ) ↦ y
γ₂ : ℝ → M
hγ₂1 : γ₂ 1 = y
hγ₂2 : γ₂ 2 = z
hγ₂_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₂
hγ₂ : pathELength I γ₂ 1 2 < v
hγ₂_const : γ₂ =ᶠ[𝓝 1] fun (x : ℝ) ↦ y
γ : (i : ℝ) → M := piecewise (β := fun (i : ℝ) ↦ M) (Iic 1) γ₁ γ₂
this : riemannianEDist I x z ≤ pathELength I γ 0 2
⊢ pathELength I γ 0 1 + pathELength I γ 1 2 < u + v
have xz : pathELength I γ 0 1 < u
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y z : M
r : ℝ≥0∞
hr : riemannianEDist I x y + riemannianEDist I y z < r
u : ℝ≥0∞
hu : u > riemannianEDist I x y
v : ℝ≥0∞
hv : v > riemannianEDist I y z
huv : u + v < r
γ₁ : ℝ → M
hγ₁0 : γ₁ 0 = x
hγ₁1 : γ₁ 1 = y
hγ₁_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₁
hγ₁ : pathELength I γ₁ 0 1 < u
hγ₁_const : γ₁ =ᶠ[𝓝 1] fun (x : ℝ) ↦ y
γ₂ : ℝ → M
hγ₂1 : γ₂ 1 = y
hγ₂2 : γ₂ 2 = z
hγ₂_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₂
hγ₂ : pathELength I γ₂ 1 2 < v
hγ₂_const : γ₂ =ᶠ[𝓝 1] fun (x : ℝ) ↦ y
γ : (i : ℝ) → M := piecewise (β := fun (i : ℝ) ↦ M) (Iic 1) γ₁ γ₂
this : riemannianEDist I x z ≤ pathELength I γ 0 2
xz : pathELength I γ 0 1 < u
⊢ pathELength I γ 0 1 + pathELength I γ 1 2 < u + v
have yw : pathELength I γ 1 2 < v
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y z : M
r : ℝ≥0∞
hr : riemannianEDist I x y + riemannianEDist I y z < r
u : ℝ≥0∞
hu : u > riemannianEDist I x y
v : ℝ≥0∞
hv : v > riemannianEDist I y z
huv : u + v < r
γ₁ : ℝ → M
hγ₁0 : γ₁ 0 = x
hγ₁1 : γ₁ 1 = y
hγ₁_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₁
hγ₁ : pathELength I γ₁ 0 1 < u
hγ₁_const : γ₁ =ᶠ[𝓝 1] fun (x : ℝ) ↦ y
γ₂ : ℝ → M
hγ₂1 : γ₂ 1 = y
hγ₂2 : γ₂ 2 = z
hγ₂_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₂
hγ₂ : pathELength I γ₂ 1 2 < v
hγ₂_const : γ₂ =ᶠ[𝓝 1] fun (x : ℝ) ↦ y
γ : (i : ℝ) → M := piecewise (β := fun (i : ℝ) ↦ M) (Iic 1) γ₁ γ₂
this : riemannianEDist I x z ≤ pathELength I γ 0 2
⊢ pathELength I γ 0 1 < u
have h : WithTop NNReal = ℝ≥0∞ → pathELength I γ 0 1 = pathELength I γ₁ 0 1
Tactic: convert! hγ₁ using 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y z : M
r : ℝ≥0∞
hr : riemannianEDist I x y + riemannianEDist I y z < r
u : ℝ≥0∞
hu : u > riemannianEDist I x y
v : ℝ≥0∞
hv : v > riemannianEDist I y z
huv : u + v < r
γ₁ : ℝ → M
hγ₁0 : γ₁ 0 = x
hγ₁1 : γ₁ 1 = y
hγ₁_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₁
hγ₁ : pathELength I γ₁ 0 1 < u
hγ₁_const : γ₁ =ᶠ[𝓝 1] fun (x : ℝ) ↦ y
γ₂ : ℝ → M
hγ₂1 : γ₂ 1 = y
hγ₂2 : γ₂ 2 = z
hγ₂_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₂
hγ₂ : pathELength I γ₂ 1 2 < v
hγ₂_const : γ₂ =ᶠ[𝓝 1] fun (x : ℝ) ↦ y
γ : (i : ℝ) → M := piecewise (β := fun (i : ℝ) ↦ M) (Iic 1) γ₁ γ₂
this : riemannianEDist I x z ≤ pathELength I γ 0 2
e_1 : WithTop NNReal = ℝ≥0∞
⊢ pathELength I γ 0 1 = pathELength I γ₁ 0 1
have h : EqOn γ γ₁ (Icc 0 1)
Tactic: apply pathELength_congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y z : M
r : ℝ≥0∞
hr : riemannianEDist I x y + riemannianEDist I y z < r
u : ℝ≥0∞
hu : u > riemannianEDist I x y
v : ℝ≥0∞
hv : v > riemannianEDist I y z
huv : u + v < r
γ₁ : ℝ → M
hγ₁0 : γ₁ 0 = x
hγ₁1 : γ₁ 1 = y
hγ₁_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₁
hγ₁ : pathELength I γ₁ 0 1 < u
hγ₁_const : γ₁ =ᶠ[𝓝 1] fun (x : ℝ) ↦ y
γ₂ : ℝ → M
hγ₂1 : γ₂ 1 = y
hγ₂2 : γ₂ 2 = z
hγ₂_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₂
hγ₂ : pathELength I γ₂ 1 2 < v
hγ₂_const : γ₂ =ᶠ[𝓝 1] fun (x : ℝ) ↦ y
γ : (i : ℝ) → M := piecewise (β := fun (i : ℝ) ↦ M) (Iic 1) γ₁ γ₂
this : riemannianEDist I x z ≤ pathELength I γ 0 2
⊢ pathELength I γ 1 2 < v
have h : WithTop NNReal = ℝ≥0∞ → pathELength I γ 1 2 = pathELength I γ₂ 1 2
Tactic: convert! hγ₂ using 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y z : M
r : ℝ≥0∞
hr : riemannianEDist I x y + riemannianEDist I y z < r
u : ℝ≥0∞
hu : u > riemannianEDist I x y
v : ℝ≥0∞
hv : v > riemannianEDist I y z
huv : u + v < r
γ₁ : ℝ → M
hγ₁0 : γ₁ 0 = x
hγ₁1 : γ₁ 1 = y
hγ₁_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₁
hγ₁ : pathELength I γ₁ 0 1 < u
hγ₁_const : γ₁ =ᶠ[𝓝 1] fun (x : ℝ) ↦ y
γ₂ : ℝ → M
hγ₂1 : γ₂ 1 = y
hγ₂2 : γ₂ 2 = z
hγ₂_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₂
hγ₂ : pathELength I γ₂ 1 2 < v
hγ₂_const : γ₂ =ᶠ[𝓝 1] fun (x : ℝ) ↦ y
γ : (i : ℝ) → M := piecewise (β := fun (i : ℝ) ↦ M) (Iic 1) γ₁ γ₂
this : riemannianEDist I x z ≤ pathELength I γ 0 2
e_1 : WithTop NNReal = ℝ≥0∞
⊢ pathELength I γ 1 2 = pathELength I γ₂ 1 2
have h : EqOn γ γ₂ (Ioo 1 2)
Tactic: apply pathELength_congr_Ioo
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.Basic (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens (↑(TopCat.of M) : Type u)
i : U ⟶ V
f : (x : ↥V) → M'
h : ChartedSpace.LiftProp P f
x : ↥U
⊢ ChartedSpace.LiftPropAt (M' := M') P (fun (x : ↥U) ↦ f ((i : (a : ↥U) → ↥V) x)) x
have hUV : U ≤ V
Tactic: have hUV : U ≤ V := CategoryTheory.leOfHom i
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.Basic (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens (↑(TopCat.of M) : Type u)
i : U ⟶ V
f : (x : ↥V) → M'
h : ChartedSpace.LiftProp P f
x : ↥U
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt (M' := M') P (fun (x : ↥U) ↦ f ((i : (a : ↥U) → ↥V) x)) x
have change : ChartedSpace.LiftPropAt P (f ∘ Opens.inclusion hUV) x
Tactic: change ChartedSpace.LiftPropAt P (f ∘ Opens.inclusion hUV) x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.Basic (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens (↑(TopCat.of M) : Type u)
i : U ⟶ V
f : (x : ↥V) → M'
h : ChartedSpace.LiftProp P f
x : ↥U
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P (f ∘ Opens.inclusion hUV) x
have rw : ChartedSpace.LiftPropAt P f
  (inclusion (s := (↑U : Set (↑(TopCat.of M) : Type u))) (t := (↑V : Set (↑(TopCat.of M) : Type u))) hUV x)
Tactic: rw [← hG.liftPropAt_iff_comp_inclusion hUV]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.Basic (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens (↑(TopCat.of M) : Type u)
f : (x : ↥V) → M'
h :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑(TopCat.of M) : Type u)) (_ : (↑x : (↑(TopCat.of M) : Type u)) ∈ V_1) (i : V_1 ⟶ V),
      ChartedSpace.LiftProp (M' := M') P fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥V) x)
x : ↥V
⊢ ChartedSpace.LiftPropAt P f x
have obtain : ∀ (U : Opens (↑(TopCat.of M) : Type u)) (hxU : (↑x : (↑(TopCat.of M) : Type u)) ∈ U) (i : U ⟶ V)
  (hU : ChartedSpace.LiftProp (M := ↥U) P (f ∘ (⇑i : (a : ↥U) → ↥V))), ChartedSpace.LiftPropAt P f x
Tactic: obtain ⟨U, hxU, i, hU : ChartedSpace.LiftProp P (f ∘ _)⟩ := h x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.Basic (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens (↑(TopCat.of M) : Type u)
f : (x : ↥V) → M'
h :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑(TopCat.of M) : Type u)) (_ : (↑x : (↑(TopCat.of M) : Type u)) ∈ V_1) (i : V_1 ⟶ V),
      ChartedSpace.LiftProp (M' := M') P fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥V) x)
x : ↥V
U : Opens (↑(TopCat.of M) : Type u)
hxU : (↑x : (↑(TopCat.of M) : Type u)) ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp (M := ↥U) P (f ∘ (⇑i : (a : ↥U) → ↥V))
x' : ↥U := Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ U) (↑x : (↑(TopCat.of M) : Type u)) hxU
⊢ ChartedSpace.LiftPropAt P f x
have hUV : U ≤ V
Tactic: have hUV : U ≤ V := CategoryTheory.leOfHom i
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.Basic (goal)
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens (↑(TopCat.of M) : Type u)
f : (x : ↥V) → M'
h :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑(TopCat.of M) : Type u)) (_ : (↑x : (↑(TopCat.of M) : Type u)) ∈ V_1) (i : V_1 ⟶ V),
      ChartedSpace.LiftProp (M' := M') P fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥V) x)
x : ↥V
U : Opens (↑(TopCat.of M) : Type u)
hxU : (↑x : (↑(TopCat.of M) : Type u)) ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp (M := ↥U) P (f ∘ (⇑i : (a : ↥U) → ↥V))
x' : ↥U := Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ U) (↑x : (↑(TopCat.of M) : Type u)) hxU
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P f (Opens.inclusion hUV x')
have rw : ChartedSpace.LiftPropAt P
  (f ∘ inclusion (s := (↑U : Set (↑(TopCat.of M) : Type u))) (t := (↑V : Set (↑(TopCat.of M) : Type u))) hUV) x'
Tactic: rw [hG.liftPropAt_iff_comp_inclusion hUV]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.Basic (hypothesis)
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens (↑(TopCat.of M) : Type u)
f : (x : ↥V) → M'
h :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑(TopCat.of M) : Type u)) (_ : (↑x : (↑(TopCat.of M) : Type u)) ∈ V_1) (i : V_1 ⟶ V),
      ChartedSpace.LiftProp (M' := M') P fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥V) x)
x : ↥V
U : Opens (↑(TopCat.of M) : Type u)
hxU : (↑x : (↑(TopCat.of M) : Type u)) ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp (M := ↥U) P (f ∘ (⇑i : (a : ↥U) → ↥V))
x' : ↥U := Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ U) (↑x : (↑(TopCat.of M) : Type u)) hxU
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P f x
have this : ChartedSpace.LiftPropAt P f (Opens.inclusion hUV x')
Tactic: have : ChartedSpace.LiftPropAt P f (Opens.inclusion hUV x') := by
      rw [hG.liftPropAt_iff_comp_inclusion hUV]
      exact hU x'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
EM : Type u_1
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_2
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace HM M
x : M
f :
  (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) : Type u)
⊢ IsUnit f ↔
    f ∉
      RingHom.ker (F :=
        (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
            Type u) →+*
          𝕜)
        (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)
have mp : IsUnit f →
  f ∉
    RingHom.ker (F :=
      (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
          Type u) →+*
        𝕜)
      (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
EM : Type u_1
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_2
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace HM M
x : M
f :
  (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) : Type u)
mp :
  IsUnit f →
    f ∉
      RingHom.ker (F :=
        (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
            Type u) →+*
          𝕜)
        (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)
⊢ IsUnit f ↔
    f ∉
      RingHom.ker (F :=
        (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
            Type u) →+*
          𝕜)
        (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)
have mpr : f ∉
    RingHom.ker (F :=
      (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
          Type u) →+*
        𝕜)
      (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) →
  IsUnit f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
EM : Type u_1
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_2
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace HM M
x : M
f :
  (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) : Type u)
S : TopCat.Presheaf CommRingCat (TopCat.of M) := TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)
hf :
  Ne (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜) f : 𝕜)
    (0 : 𝕜)
⊢ IsUnit f
have mpr : ∀ (U : Opens M) (hxU : x ∈ U) (f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯)
  (hf :
    Ne (α := 𝕜)
      ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
          ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                  (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
                (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
              f :
            (↑(S.stalk x) : Type u)) :
        𝕜)
      (0 : 𝕜)),
  IsUnit (M :=
    (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
      Type u))
    ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
          (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
        f :
      (↑(S.stalk x) : Type u))
Tactic: obtain ⟨U : Opens M, hxU, f : C^∞⟮IM, U; 𝓘(𝕜), 𝕜⟯, rfl⟩ := S.exists_germ_eq f
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
EM : Type u_1
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_2
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf :
  Ne (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)
    (0 : 𝕜)
⊢ Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
have h : Eq (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜)
  ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
      ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
            (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
          f :
        (↑(S.stalk x) : Type u)) :
    𝕜)
Tactic: convert! hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
EM : Type u_1
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_2
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf :
  Ne (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)
    (0 : 𝕜)
⊢ IsUnit (M :=
    (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
      Type u))
    ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
          (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
        f :
      (↑(S.stalk x) : Type u))
have hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
Tactic: have hf' : f ⟨x, hxU⟩ ≠ 0 := by
      convert! hf
      exact (smoothSheafCommRing.eval_germ U x hxU f).symm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
EM : Type u_1
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_2
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf :
  Ne (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)
    (0 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
⊢ IsUnit (M :=
    (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
      Type u))
    ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
          (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
        f :
      (↑(S.stalk x) : Type u))
have H : ∀ᶠ (z : ↥U) in 𝓝 (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) z : 𝕜) (0 : 𝕜)
Tactic: have H : ∀ᶠ (z : U) in 𝓝 ⟨x, hxU⟩, f z ≠ 0 := f.2.continuous.continuousAt.eventually_ne hf'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
EM : Type u_1
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_2
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf :
  Ne (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)
    (0 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
H : ∀ᶠ (z : ↥U) in 𝓝 (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) z : 𝕜) (0 : 𝕜)
⊢ IsUnit (M :=
    (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
      Type u))
    ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
          (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
        f :
      (↑(S.stalk x) : Type u))
have H₁ : ∃ (t : Set ↥U),
  (∀ y ∈ t, Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)) ∧
    IsOpen[instTopologicalSpaceSubtype] t ∧ Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ t
Tactic: rw [eventually_nhds_iff] at H
Cleared hypotheses: H