awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t₁ t₂ : Triangle R P
h :
  Eq.{u_3 + 1} (α := Polygon P 3) ((fun (t : Triangle R P) ↦ { vertices := t.points : Polygon P 3 }) t₁)
    ((fun (t : Triangle R P) ↦ { vertices := t.points : Polygon P 3 }) t₂)
h₁ : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), t₁.points i = t₂.points i
⊢ t₁ = t₂

Tactic:
apply Simplex.ext

Premises used: Affine.Simplex.ext
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t₁ t₂ : Triangle R P
h :
  Eq.{u_3 + 1} (α := Polygon P 3) ((fun (t : Triangle R P) ↦ { vertices := t.points : Polygon P 3 }) t₁)
    ((fun (t : Triangle R P) ↦ { vertices := t.points : Polygon P 3 }) t₂)
⊢ Eq.{u_3 + 1} (α := Fin 3 → P)
    (Polygon.vertices ((fun (t : Triangle R P) ↦ { vertices := t.points : Polygon P 3 }) t₁))
    (Polygon.vertices ((fun (t : Triangle R P) ↦ { vertices := t.points : Polygon P 3 }) t₂))

Tactic:
apply_fun Polygon.vertices at h

Premises used: Polygon.vertices
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t₁ t₂ : Triangle R P
h :
  Eq.{u_3 + 1} (α := Fin 3 → P)
    (Polygon.vertices ((fun (t : Triangle R P) ↦ { vertices := t.points : Polygon P 3 }) t₁))
    (Polygon.vertices ((fun (t : Triangle R P) ↦ { vertices := t.points : Polygon P 3 }) t₂))
⊢ ∀ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), t₁.points i = t₂.points i

Tactic:
simp_all
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
⊢ Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t) = t.points

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
p : Polygon P 3
h : HasNondegenerateVertices R p
⊢ p.vertices = ![p.vertices 0, p.vertices 1, p.vertices 2]

Tactic:
have : p.vertices = ![p.vertices 0, p.vertices 1, p.vertices 2] := List.ofFn_inj.mp rfl
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
p : Polygon P 3
h : HasNondegenerateVertices R p
this : p.vertices = ![p.vertices 0, p.vertices 1, p.vertices 2]
rw : AffineIndependent R ![p.vertices 0, p.vertices 1, p.vertices 2]
⊢ AffineIndependent R p.vertices

Tactic:
rw [this]
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
p : Polygon P 3
h : HasNondegenerateVertices R p
this : p.vertices = ![p.vertices 0, p.vertices 1, p.vertices 2]
⊢ AffineIndependent R ![p.vertices 0, p.vertices 1, p.vertices 2]

Tactic:
apply h
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
p : Polygon P 3
h : HasNondegenerateVertices R p
⊢ (toTriangle R p h).points = p.vertices

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AddTorsor V P
poly : Polygon P 3
h : HasNondegenerateVertices R poly
⊢ (Affine.Triangle.toPolygon : (a : Affine.Triangle R P) → Polygon P 3) (toTriangle R poly h) = poly

Tactic:
rfl
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
⊢ t.points = ![t.points 0, t.points 1, t.points 2]

Tactic:
have ht : t.points = ![t.points 0, t.points 1, t.points 2] := List.ofFn_inj.mp rfl
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 0, t.points 1, t.points 2]

Tactic:
simpa [← ht] using t.independent

Premises used: Affine.Simplex.independent
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 0, t.points 1, t.points 2]

Tactic:
have h : AffineIndependent R ![t.points 0, t.points 1, t.points 2] := by
    simpa [← ht] using t.independent
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
i : Fin 3
0 :
  AffineIndependent.{u_1, u_2, u_3, 0} R (P := P)
    ![Polygon.vertices (n := 3) ((toPolygon : (a : Triangle R P) → Polygon P 3) t) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t)
        (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) 1),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t)
        (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) 2)]
1 :
  AffineIndependent.{u_1, u_2, u_3, 0} R (P := P)
    ![Polygon.vertices (n := 3) ((toPolygon : (a : Triangle R P) → Polygon P 3) t) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t)
        (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) 1),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t)
        (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) 2)]
2 :
  AffineIndependent.{u_1, u_2, u_3, 0} R (P := P)
    ![Polygon.vertices (n := 3) ((toPolygon : (a : Triangle R P) → Polygon P 3) t) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t)
        (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) 1),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t)
        (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) 2)]
⊢ AffineIndependent.{u_1, u_2, u_3, 0} R (P := P)
    ![Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t) i,
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t) (i + 1),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t) (i + 2)]

Tactic:
fin_cases i
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
0 : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent.{u_1, u_2, u_3, 0} R (P := P)
    ![Polygon.vertices (n := 3) ((toPolygon : (a : Triangle R P) → Polygon P 3) t) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t)
        (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) 1),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t)
        (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) 2)]

Tactic:
dsimp
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
1 : AffineIndependent R ![t.points 1, t.points 2, t.points 0]
⊢ AffineIndependent.{u_1, u_2, u_3, 0} R (P := P)
    ![Polygon.vertices (n := 3) ((toPolygon : (a : Triangle R P) → Polygon P 3) t) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t)
        (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) 1),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t)
        (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) 2)]

Tactic:
dsimp
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
2 : AffineIndependent R ![t.points 2, t.points 0, t.points 1]
⊢ AffineIndependent.{u_1, u_2, u_3, 0} R (P := P)
    ![Polygon.vertices (n := 3) ((toPolygon : (a : Triangle R P) → Polygon P 3) t) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t)
        (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) 1),
      Polygon.vertices ((toPolygon : (a : Triangle R P) → Polygon P 3) t)
        (HAdd.hAdd (α := Fin 3) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) 2)]

Tactic:
dsimp
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 0, t.points 1, t.points 2]

Tactic:
h
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 1, t.points 2, t.points 0]

Tactic:
h.comm_left.comm_right

Premises used: AffineIndependent.comm_left, AffineIndependent.comm_right
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 2, t.points 0, t.points 1]

Tactic:
h.comm_right.comm_left

Premises used: AffineIndependent.comm_left, AffineIndependent.comm_right
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 0, t.points 1, t.points 2]

Tactic:
exacts [h, h.comm_left.comm_right, h.comm_right.comm_left]

Premises used: AffineIndependent.comm_left, AffineIndependent.comm_right
-- Module: Mathlib.Geometry.Polygon.Basic
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
t : Triangle R P
⊢ Polygon.toTriangle R ((toPolygon : (a : Triangle R P) → Polygon P 3) t) ⋯ = t

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U V : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hUV : U ≤ V
⊢ Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op U)))
    (restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier) 0 U
      hUV)
    0

Tactic:
map_zero _

Premises used: TopCat.Presheaf.restrict, map_zero
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : ↥U
h :
  Eq (α := (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)))
            (X.presheaf.germ U (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) →
            (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
        f :
      (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
    (0 : (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
⊢ Eq (α := (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)))
            (X.presheaf.germ U (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) →
            (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
        f :
      (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)))
            (X.presheaf.germ U (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) →
            (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
        0 :
      (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))

Tactic:
simpa
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : ↥U
h :
  Eq (α := (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)))
            (X.presheaf.germ U (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) →
            (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
        f :
      (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
    (0 : (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
⊢ Eq (α := (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)))
            (X.presheaf.germ U (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) →
            (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
        f :
      (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)))
            (X.presheaf.germ U (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) →
            (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))
        0 :
      (↑(X.presheaf.stalk (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))) : Type u_1))

Tactic:
have h1 : X.presheaf.germ U x.val x.property f = X.presheaf.germ U x.val x.property 0 := by simpa
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hx : x ∈ U
h :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
obtain :
  ∀ (g' : (↑(X.presheaf.stalk x) : Type u_1))
    (heq :
      HMul.hMul (α := (↑(X.presheaf.stalk x) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
                (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
              f :
            (↑(X.presheaf.stalk x) : Type u_1))
          g' =
        1),
    ∃ (V : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) (i : V ⟶ U) (_ : x ∈ V),
      IsUnit (M := (↑(X.presheaf.obj (op V)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map i.op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
            f :
          (↑(X.presheaf.obj (op V)) : Type u_1))
⊢ ∃ (V : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) (i : V ⟶ U) (_ : x ∈ V),
    IsUnit (M := (↑(X.presheaf.obj (op V)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map i.op) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
          f :
        (↑(X.presheaf.obj (op V)) : Type u_1))

Tactic:
obtain ⟨g', heq⟩ := h.exists_right_inv

Premises used: IsUnit.exists_right_inv
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hx : x ∈ U
h :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        f :
      (↑(X.presheaf.stalk x) : Type u_1))
V : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxV : x ∈ V
g :
  ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
    (X.presheaf.obj (op V))
heq :
  HMul.hMul (α := (↑(X.presheaf.stalk x) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          f :
        (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V x hxV) :
            (a : (↑(X.presheaf.obj (op V)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          g :
        (↑(X.presheaf.stalk x) : Type u_1)) =
    1
W : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1) := U ⊓ V
⊢ x ∈ W

Tactic:
have hxW : x ∈ W := ⟨hx, hxV⟩
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
h :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) (hx : x ∈ U),
    IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          f :
        (↑(X.presheaf.stalk x) : Type u_1))
choose :
  ∀ (V : (x : ↥U) → Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) (iVU : (x : ↥U) → V x ⟶ U)
    (m : ∀ (x : ↥U), (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ∈ V x)
    (h_unit :
      ∀ (x : ↥U),
        IsUnit (M := (↑(X.presheaf.obj (op (V x))) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (iVU x).op) :
                (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op (V x))) : Type u_1))
              f :
            (↑(X.presheaf.obj (op (V x))) : Type u_1))),
    IsUnit f
⊢ IsUnit f

Tactic:
choose V iVU m h_unit using fun x : U => X.isUnit_res_of_isUnit_germ U f x x.2 (h x.1 x.2)

Premises used: AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ, Subtype.val, Subtype.property
-- Module: Mathlib.Geometry.RingedSpace.Basic
Goal:
X : RingedSpace
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
f : (↑(X.presheaf.obj (op U)) : Type u_1)
h :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) (hx : x ∈ U),
    IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          f :
        (↑(X.presheaf.stalk x) : Type u_1))
V : (x : ↥U) → Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), (↑x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) ∈ V x
h_unit :
  ∀ (x : ↥U),
    IsUnit (M := (↑(X.presheaf.obj (op (V x))) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map (iVU x).op) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op (V x))) : Type u_1))
          f :
        (↑(X.presheaf.obj (op (V x))) : Type u_1))
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
hxU : x ∈ U
simp : ∃ (i : ↥U), x ∈ V i
⊢ x ∈ iSup V

Tactic:
simp only [Opens.mem_iSup]

Premises used: TopologicalSpace.Opens.mem_iSup