awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
x₀ : (↑(↑V : Set M) : Type u)
hxx₀ : Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV x₀ = Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU
⊢ x ∈ (↑V : Set M)
have h : x = (↑x₀ : M)
Tactic: convert! x₀.2
-- 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 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
hxV₀ :
  Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
⊢ 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 hxV : x ∈ (↑V : Set M)
Tactic: have hxV : x ∈ (V : Set M) := by
      obtain ⟨x₀, hxx₀⟩ := hxV₀
      convert! x₀.2
      exact congr_arg Subtype.val hxx₀.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 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
hxV₀ :
  Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
hxV : x ∈ (↑V : Set M)
⊢ 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 hVf : ∀ (y : ↥V), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV y) : 𝕜) (0 : 𝕜)
Tactic: have hVf : ∀ y : V, f (Set.inclusion hUV y) ≠ 0 :=
      fun y ↦ hV₀f (Set.inclusion hUV y) (Set.mem_range_self y)
-- 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 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
hxV₀ :
  Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
hxV : x ∈ (↑V : Set M)
hVf :
  ∀ (y : ↥V), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV y) : 𝕜) (0 : 𝕜)
mpr :
  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))
⊢ 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 mpr₁ : ContMDiff IM 𝓘(𝕜, 𝕜) (M' := 𝕜) ∞ ((⇑f : (a : ↥U) → 𝕜) ∘ Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)⁻¹
Tactic: let g : C^∞⟮IM, V; 𝓘(𝕜), 𝕜⟯ := ⟨(f ∘ Set.inclusion hUV)⁻¹, ?_⟩
-- 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 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
hxV₀ :
  Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
hxV : x ∈ (↑V : Set M)
hVf :
  ∀ (y : ↥V), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV y) : 𝕜) (0 : 𝕜)
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ :=
  Subtype.mk (p := fun (f : ↥V → 𝕜) ↦ ContMDiff IM 𝓘(𝕜, 𝕜) ∞ f)
    ((⇑f : (a : ↥U) → 𝕜) ∘ Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)⁻¹ ⋯
⊢ Eq (α :=
    (↑(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 V x hxV) :
          (a : (↑(S.obj (Opposite.op V)) : Type u)) →
            (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u))
        (HMul.hMul (α := (↑(S.obj (Opposite.op V)) : Type u))
          ((ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV : (a : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯) f :
            C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯)
          g) :
      (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
        Type u))
    (1 :
      (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
        Type u))
have h : HMul.hMul (α := (↑(S.obj (Opposite.op V)) : Type u))
    ((ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV : (a : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯) f :
      C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯)
    g =
  1
Tactic: convert! RingHom.map_one _
-- 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 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
hxV₀ :
  Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
hxV : x ∈ (↑V : Set M)
hVf :
  ∀ (y : ↥V), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV y) : 𝕜) (0 : 𝕜)
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ :=
  Subtype.mk (p := fun (f : ↥V → 𝕜) ↦ ContMDiff IM 𝓘(𝕜, 𝕜) ∞ f)
    ((⇑f : (a : ↥U) → 𝕜) ∘ Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)⁻¹ ⋯
⊢ HMul.hMul (α := (↑(S.obj (Opposite.op V)) : Type u))
      ((ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV : (a : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯) f :
        C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯)
      g =
    1
have h : (↑(HMul.hMul (α := (↑(S.obj (Opposite.op V)) : Type u))
        ((ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV : (a : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯) f :
          C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯)
        g) :
    (x : ↥(Opposite.unop (Opposite.op V))) →
      (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of M) : Type u))) =
  (↑1 :
    (x : ↥(Opposite.unop (Opposite.op V))) → (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of M) : Type u)))
Tactic: apply Subtype.ext
-- 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 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
hxV₀ :
  Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
hxV : x ∈ (↑V : Set M)
hVf :
  ∀ (y : ↥V), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV y) : 𝕜) (0 : 𝕜)
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ :=
  Subtype.mk (p := fun (f : ↥V → 𝕜) ↦ ContMDiff IM 𝓘(𝕜, 𝕜) ∞ f)
    ((⇑f : (a : ↥U) → 𝕜) ∘ Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)⁻¹ ⋯
⊢ (↑(HMul.hMul (α := (↑(S.obj (Opposite.op V)) : Type u))
          ((ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV : (a : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯) f :
            C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯)
          g) :
      (x : ↥(Opposite.unop (Opposite.op V))) →
        (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of M) : Type u))) =
    (↑1 :
      (x : ↥(Opposite.unop (Opposite.op V))) →
        (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of M) : Type u)))
have h : ∀ (y : ↥(Opposite.unop (Opposite.op V))),
  (↑(HMul.hMul (α := (↑(S.obj (Opposite.op V)) : Type u))
            ((ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV : (a : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯)
                f :
              C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯)
            g) :
        (x : ↥(Opposite.unop (Opposite.op V))) →
          (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of M) : Type u)))
      y =
    (↑1 :
        (x : ↥(Opposite.unop (Opposite.op V))) →
          (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of M) : Type u)))
      y
Tactic: ext y
-- 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 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
hxV₀ :
  Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
hxV : x ∈ (↑V : Set M)
hVf :
  ∀ (y : ↥V), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV y) : 𝕜) (0 : 𝕜)
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ :=
  Subtype.mk (p := fun (f : ↥V → 𝕜) ↦ ContMDiff IM 𝓘(𝕜, 𝕜) ∞ f)
    ((⇑f : (a : ↥U) → 𝕜) ∘ Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)⁻¹ ⋯
y : ↥(Opposite.unop (Opposite.op V))
⊢ (↑(HMul.hMul (α := (↑(S.obj (Opposite.op V)) : Type u))
            ((ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV : (a : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯)
                f :
              C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯)
            g) :
        (x : ↥(Opposite.unop (Opposite.op V))) →
          (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of M) : Type u)))
      y =
    (↑1 :
        (x : ↥(Opposite.unop (Opposite.op V))) →
          (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of M) : Type u)))
      y
have h : Ne (α := (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑y : (↑(TopCat.of M) : Type u)))
  ((((ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV : (a : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯) f :
          C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯) :
        (a : ↥(Opposite.unop (Opposite.op V))) → 𝕜)
      y :
    𝕜)
  (0 : (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑y : (↑(TopCat.of M) : Type u)))
Tactic: apply mul_inv_cancel₀
-- 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 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
hxV₀ :
  Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
hxV : x ∈ (↑V : Set M)
hVf :
  ∀ (y : ↥V), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV y) : 𝕜) (0 : 𝕜)
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ :=
  Subtype.mk (p := fun (f : ↥V → 𝕜) ↦ ContMDiff IM 𝓘(𝕜, 𝕜) ∞ f)
    ((⇑f : (a : ↥U) → 𝕜) ∘ Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)⁻¹ ⋯
⊢ Eq (α :=
    (↑(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 V x hxV) :
          (a : (↑(S.obj (Opposite.op V)) : Type u)) →
            (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u))
        (HMul.hMul (β := (↑(S.obj (Opposite.op V)) : Type u)) g
          ((ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV : (a : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯) f :
            C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
      (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
        Type u))
    (1 :
      (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
        Type u))
have h : HMul.hMul (β := (↑(S.obj (Opposite.op V)) : Type u)) g
    ((ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV : (a : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯) f :
      C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯) =
  1
Tactic: convert! RingHom.map_one _