awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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 : 𝕜)
⊢ ∀ᶠ (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'
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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 : 𝕜)
⊢ ∃ (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

Premises used: eventually_nhds_iff
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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
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))
⊢ 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
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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' := ⋯ }
⊢ V ≤ U

Tactic:
have hUV : V ≤ U := Subtype.coe_image_subset (U : Set M) V₀
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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
⊢ {x : (↑(↑U : Set M) : Type u) | (↑x : M) ∈ (↑V : Set M)} =
    Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)

Tactic:
(Set.range_inclusion hUV).symm

Premises used: Set.range_inclusion, Eq.symm
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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
h : Set ↥U = Set (↑(↑U : Set M) : Type u) → V₀ = {x : (↑(↑U : Set M) : Type u) | (↑x : M) ∈ (↑V : Set M)}
⊢ V₀ = Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)

Tactic:
convert! (Set.range_inclusion hUV).symm

Premises used: Set.range_inclusion, Eq.symm
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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)
h : ∀ (y : ↥U), y ∈ V₀ ↔ Membership.mem (γ := Set ↥U) {x : (↑(↑U : Set M) : Type u) | (↑x : M) ∈ (↑V : Set M)} y
⊢ V₀ = {x : (↑(↑U : Set M) : Type u) | (↑x : M) ∈ (↑V : Set M)}

Tactic:
ext y
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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
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
⊢ y ∈ V₀ ↔ Membership.mem (γ := Set ↥U) {x : (↑(↑U : Set M) : Type u) | (↑x : M) ∈ (↑V : Set M)} y

Tactic:
change _ ↔ y ∈ Subtype.val ⁻¹' Subtype.val '' V₀

Premises used: Subtype.val
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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
h h₁ : y ∈ V₀ ↔ y ∈ V₀
⊢ 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:
rw [Set.preimage_image_eq _ Subtype.coe_injective]

Premises used: Subtype.coe_injective, Set.preimage_image_eq
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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)

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]
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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)
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))
⊢ 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
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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)
⊢ ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)

Tactic:
subst hV
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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 : 𝕜)
⊢ IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))

Tactic:
subst hV
-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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))
⊢ 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