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 : 𝕜)
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
⊢ 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 : ∀ (V₀ : Set ↥U) (hV₀f : ∀ y ∈ V₀, Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜))
  (hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀) (hxV₀ : Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ V₀),
  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 ⟨V₀, hV₀f, hV₀, hxV₀⟩ := H
Cleared hypotheses: H
-- 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ V₀
V : Opens M := { carrier := Subtype.val (p := fun (x : M) ↦ x ∈ U) '' V₀, is_open' := ⋯ }
⊢ 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 hUV : V ≤ U
Tactic: have hUV : V ≤ U := Subtype.coe_image_subset (U : Set M) V₀
-- 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ V₀
V : Opens M := { carrier := Subtype.val (p := fun (x : M) ↦ x ∈ U) '' V₀, is_open' := ⋯ }
hUV : V ≤ U
⊢ V₀ = Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
have h : Set ↥U = Set (↑(↑U : Set M) : Type u) → V₀ = {x : (↑(↑U : Set M) : Type u) | (↑x : M) ∈ (↑V : Set M)}
Tactic: convert! (Set.range_inclusion hUV).symm
-- 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ V₀
V : Opens M := { carrier := Subtype.val (p := fun (x : M) ↦ x ∈ U) '' V₀, is_open' := ⋯ }
hUV : V ≤ U
e_1 : Set ↥U = Set (↑(↑U : Set M) : Type u)
⊢ V₀ = {x : (↑(↑U : Set M) : Type u) | (↑x : M) ∈ (↑V : Set M)}
have h : ∀ (y : ↥U), y ∈ V₀ ↔ Membership.mem (γ := Set ↥U) {x : (↑(↑U : Set M) : Type u) | (↑x : M) ∈ (↑V : Set M)} 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ V₀
V : Opens M := { carrier := Subtype.val (p := fun (x : M) ↦ x ∈ U) '' V₀, is_open' := ⋯ }
hUV : V ≤ U
e_1 : Set ↥U = Set (↑(↑U : Set M) : Type u)
y : ↥U
⊢ y ∈ V₀ ↔ Membership.mem (γ := Set ↥U) {x : (↑(↑U : Set M) : Type u) | (↑x : M) ∈ (↑V : Set M)} y
have h : y ∈ V₀ ↔
  Membership.mem (γ := Set ↥U) (Subtype.val (p := fun (x : M) ↦ x ∈ U) ⁻¹' Subtype.val (p := fun (x : M) ↦ x ∈ U) '' V₀)
    y
Tactic: change _ ↔ y ∈ Subtype.val ⁻¹' Subtype.val '' V₀
-- 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ V₀
V : Opens M := { carrier := Subtype.val (p := fun (x : M) ↦ x ∈ U) '' V₀, is_open' := ⋯ }
hUV : V ≤ U
e_1 : Set ↥U = Set (↑(↑U : Set M) : Type u)
y : ↥U
⊢ y ∈ V₀ ↔
    Membership.mem (γ := Set ↥U)
      (Subtype.val (p := fun (x : M) ↦ x ∈ U) ⁻¹' Subtype.val (p := fun (x : M) ↦ x ∈ U) '' V₀) y
have h : y ∈ V₀ ↔ y ∈ V₀
Tactic: rw [Set.preimage_image_eq _ Subtype.coe_injective]
-- 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ V₀
V : Opens M := { carrier := Subtype.val (p := fun (x : M) ↦ x ∈ U) '' V₀, is_open' := ⋯ }
hUV : V ≤ 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 hV : V₀ = Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
Tactic: have hV : V₀ = Set.range (Set.inclusion hUV) := by
      convert! (Set.range_inclusion hUV).symm
      ext y
      change _ ↔ y ∈ Subtype.val ⁻¹' Subtype.val '' V₀
      rw [Set.preimage_image_eq _ Subtype.coe_injective]
-- 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ V₀
V : Opens M := { carrier := Subtype.val (p := fun (x : M) ↦ x ∈ U) '' V₀, is_open' := ⋯ }
hUV : V ≤ U
hV : V₀ = 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 mpr : ∀ (V : Opens M) (hUV : V ≤ U) (hV : V₀ = 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))
Tactic: clear_value V
Cleared hypotheses: V, hUV, hV
-- 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ V₀
V : Opens M
hUV : V ≤ U
hV : V₀ = 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 hV₀f₁ : ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
  Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
Tactic: subst hV
Cleared hypotheses: V₀, hV₀f, hV₀, hxV₀, hV
-- 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ V₀
V : Opens M
hUV : V ≤ U
hV : V₀ = Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
hV₀f₁ :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (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 hV₁ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
Tactic: subst hV
Cleared hypotheses: V₀, hV₀f, hV₀, hxV₀, hV
-- 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ V₀
V : Opens M
hUV : V ≤ U
hV : V₀ = Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
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))
⊢ 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₁ : Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
Tactic: subst hV
Cleared hypotheses: V₀, hV₀f, hV₀, hxV₀, hV
-- 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)
⊢ x ∈ (↑V : Set M)
have obtain : ∀ (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)
Tactic: obtain ⟨x₀, hxx₀⟩ := hxV₀
Cleared hypotheses: hxV₀