mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : Commute (x ^ n) (q.smeval y)
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)

Tactic:
commute_iff_eq (x ^ n) (q.smeval y)

Goal state after:
case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit ((x * 0 + y * if n = m then 1 else 0) + z)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
if_neg hmn.ne'

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (x * 0 + y * 0 + z)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : (↑v + (↑w + ↑u)) ^ 2 = (↑v + ↑z + ↑x) ^ 2
⊢ q = p ∨ q = p.mirror

Tactic:
add_assoc

Goal state after:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : (↑v + (↑w + ↑u)) ^ 2 = (↑v + (↑z + ↑x)) ^ 2
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
n x y : R
⊢ ω * (algebraMap R (QuadraticAlgebra R a b)) n * { re := x, im := y } = { re := a * n * y, im := n * x + n * b * y }

Tactic:
ext <;> simp; ring

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ (algebraMap R (QuadraticAlgebra R a b)) (norm z) = z * star z

Tactic:
ext <;> simp [norm, star, mul_comm] <;> ring

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x : mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) x = F ⟦x⟧
ih_y : mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) y = F ⟦y⟧
hm : ⟦x.mul y⟧ = Mul.mul ⟦x⟧ ⟦y⟧
this : ∀ (x y : EnvelGroup R), F (Mul.mul x y) = F x * F y
⊢ mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) = F ⟦x⟧ * F ⟦y⟧

Tactic:
rw [← ih_x, ← ih_y, mapAux]

Goal state after:
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ (f * g) (a✝ * (r * ((f * g) a✝ - (g * f) a✝))) = (g * f) (a✝ * (r * ((f * g) a✝ - (g * f) a✝)))

Tactic:
coe_mul,

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ (⇑f ∘ ⇑g) (a✝ * (r * ((⇑f ∘ ⇑g) a✝ - (g * f) a✝))) = (g * f) (a✝ * (r * ((⇑f ∘ ⇑g) a✝ - (g * f) a✝)))
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ (⇑f ∘ ⇑g) (a✝ * (r * ((⇑f ∘ ⇑g) a✝ - (g * f) a✝))) = (g * f) (a✝ * (r * ((⇑f ∘ ⇑g) a✝ - (g * f) a✝)))

Tactic:
coe_mul,

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ (⇑f ∘ ⇑g) (a✝ * (r * ((⇑f ∘ ⇑g) a✝ - (⇑g ∘ ⇑f) a✝))) = (⇑g ∘ ⇑f) (a✝ * (r * ((⇑f ∘ ⇑g) a✝ - (⇑g ∘ ⇑f) a✝)))
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
a : G
⊢ image₂ (fun x1 x2 ↦ x1 * x2) f.support {a} ⊆ image (fun x ↦ x * a) f.support

Tactic:
rw [Finset.image₂_singleton_right]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
x : R
⊢ (lift ⟨f, w⟩) ((mkRingHom r) x) = f x

Tactic:
simp_rw [lift_def, preLift_def, mkRingHom_def]

Goal state after:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
x : R
⊢ ({
          toFun := fun f ↦
            { toFun := fun x ↦ Quot.lift ⇑↑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ },
          invFun := fun F ↦
            ⟨F.comp
                { toFun := fun x ↦ { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯ },
              ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨f, w⟩)
      ({ toFun := fun x ↦ { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
        x) =
    f x
Module: Mathlib.Algebra.Star.Subsemiring

Goal state before:
pp: R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
S : StarSubsemiring R
s : Set R
hs : s = ↑S
a : R
ha : a ∈ (S.copy s hs).carrier
⊢ a ∈ S.carrier

Tactic:
by simpa [hs] using ha

Goal state after:
Module: Mathlib.Algebra.Star.Subsemiring

Goal state before:
pp: R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
S : StarSubsemiring R
a : R
hs : ↑S = ↑S
__Subsemiring✝ : Subsemiring R := S.copy (↑S) hs
ha : a ∈ (S.copy (↑S) hs).carrier
⊢ a ∈ S.carrier

Tactic:
by simpa [hs] using ha

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ coeff 1 n = if 0 = n then 1 else 0

Tactic:
have : (1 : SkewPolynomial R) = monomial 0 1 := by simp [← CRingHom_eq_C]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
this : 1 = (monomial 0) 1
⊢ coeff 1 n = if 0 = n then 1 else 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
c : R
h : c ≠ 0
⊢ (C c * X).support = {1}

Tactic:
C_mul_X_eq_monomial,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
c : R
h : c ≠ 0
⊢ ((monomial 1) c).support = {1}
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
⊢ (monomial n) (-a) = -(monomial n) a

Tactic:
by
  rw [eq_neg_iff_add_eq_zero, ← monomial_add, neg_add_cancel, monomial_zero_right]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case refine_1
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ ∀ a ∈ f.support ∪ g.support, (h.sum fun a₂ b₂ ↦ single (a * a₂) (0 * a • b₂)) = 0

Tactic:
simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case refine_2
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ ∀ a ∈ f.support ∪ g.support,
    ∀ (b₁ b₂ : k),
      (h.sum fun a₂ b₂_1 ↦ single (a * a₂) ((b₁ + b₂) * a • b₂_1)) =
        (h.sum fun a₂ b₂ ↦ single (a * a₂) (b₁ * a • b₂)) + h.sum fun a₂ b₂_1 ↦ single (a * a₂) (b₂ * a • b₂_1)

Tactic:
simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case refine_3
k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ ((f.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) +
      g.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    (f.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) +
      g.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)

Tactic:
simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]

Goal state after:
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∀ (a : R), a * (↑(toUnits v)⁻¹ * ↑(toUnits u)) = ↑(toUnits v)⁻¹ * (↑(toUnits u) * a)) ↔
    ∃ α, ↑(toUnits u) = α • ↑(toUnits v)

Tactic:
← mul_assoc (((toUnits v)⁻¹ : Rˣ) : R),

Goal state after:
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∀ (a : R), a * (↑(toUnits v)⁻¹ * ↑(toUnits u)) = ↑(toUnits v)⁻¹ * ↑(toUnits u) * a) ↔
    ∃ α, ↑(toUnits u) = α • ↑(toUnits v)
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∀ (a : R), a * (↑(toUnits v)⁻¹ * ↑(toUnits u)) = ↑(toUnits v)⁻¹ * (↑(toUnits u) * a)) ↔ ∃ α, u = α • v

Tactic:
← mul_assoc (((toUnits v)⁻¹ : Rˣ) : R),

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
⊢ (∀ (a : R), a * (↑(toUnits v)⁻¹ * ↑(toUnits u)) = ↑(toUnits v)⁻¹ * ↑(toUnits u) * a) ↔ ∃ α, u = α • v
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S k
inst✝¹ : SMulZeroClass Sᵐᵒᵖ k
inst✝ : IsCentralScalar S k
x✝¹ : S
x✝ : SkewMonoidAlgebra k G
coeff✝ : G →₀ k
⊢ MulOpposite.op x✝¹ • { coeff := coeff✝ } = x✝¹ • { coeff := coeff✝ }

Tactic:
simp_rw [← ofCoeff_smul, op_smul_eq_smul]

Goal state after:
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case mp
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a → a = 0 ∧ b = 0

Tactic:
rintro (⟨rfl, h⟩ | ⟨rfl, h⟩)
    · exact ⟨rfl, le_antisymm (le_zero _) h⟩
    · exact ⟨le_antisymm (le_zero _) h, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym 0 * unsym x✝ + unsym x✝ * unsym 0)) = 0

Tactic:
unsym_zero,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (0 * unsym x✝ + unsym x✝ * 0)) = 0
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym x✝ * unsym 0 + unsym 0 * unsym x✝)) = 0

Tactic:
unsym_zero,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym x✝ * 0 + 0 * unsym x✝)) = 0
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' ↑s)

Tactic:
by
  rcases s.eq_empty_or_nonempty with (rfl | h)
  · simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, untrop_zero]
  · rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, Finset.untrop_sum']

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case refine_1
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j : Jᵒᵖ
⊢ ((Functor.const Jᵒᵖ).obj (s.pt.presheaf.obj U)).obj j ⟶
    ((pushforwardDiagramToColimit F).leftOp ⋙
          (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
            ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).op.obj U)).obj
      j

pp: case refine_2
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
⊢ ((Functor.const Jᵒᵖ).obj (s.pt.presheaf.obj U)).map f ≫ ?refine_1 =
    ?refine_1 ≫
      ((pushforwardDiagramToColimit F).leftOp ⋙
            (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
              ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).op.obj U)).map
        f

Tactic:
· refine (s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ?_)
    dsimp
    rw [← Opens.map_comp_obj]
    simp

Goal state after:
case refine_2
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
⊢ ((Functor.const Jᵒᵖ).obj (s.pt.presheaf.obj U)).map f ≫
      (s.ι.app (unop j')).c.app U ≫ (F.obj (unop j')).presheaf.map (eqToHom ⋯) =
    ((s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      ((pushforwardDiagramToColimit F).leftOp ⋙
            (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
              ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).op.obj U)).map
        f
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_3
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
⊢ ∀ (y : ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))),
    (fun s ↦ (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf s) y → y = ⟨gl, ⋯⟩

Tactic:
intro gl' hgl'

Goal state after:
case refine_3
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
gl' : ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))
hgl' : (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf gl'
⊢ gl' = ⟨gl, ⋯⟩
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
⊢ ∃ R f, IsOpenImmersion f ∧ x ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑U

Tactic:
obtain ⟨⟨V, hxV⟩, R, ⟨e⟩⟩ := X.2 x

Goal state after:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
⊢ ∃ R f, IsOpenImmersion f ∧ x ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑U
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↥X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : X.Opens
W : (X.restrict h).Opens
e : W ≤ X.ofRestrict h ⁻¹ᵁ V
⊢ X.ofRestrict h ''ᵁ unop (op W) ≤ V

Tactic:
exact Set.image_subset_iff.mpr e

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) WalkingCospan.one)

Tactic:
rw [← limit.w (cospan f g) WalkingCospan.Hom.inl, cospan_map_inl]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) WalkingCospan.left ≫ f)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) WalkingCospan.one)

Tactic:
rw [← limit.w (cospan f g) WalkingCospan.Hom.inl, cospan_map_inl]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) WalkingCospan.left ≫ f)
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let __src := ↑f;
  let __src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  { toFun := (↑↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ ⟨↑e_Ring.symm, ⋯⟩ ≫ f = 𝟙 Y

Tactic:
by
            ext x
            exact e_Ring.right_inv x

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ U.ι ''ᵁ (↑U).basicOpen ((ConcreteCategory.hom U.topIso.inv) r) = X.basicOpen r

Tactic:
ι_image_basicOpen',

Goal state after:
X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) ((ConcreteCategory.hom U.topIso.inv) r)) =
    X.basicOpen r
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ 𝟙 X ∣_ U ≫ U.ι = 𝟙 ↑(𝟙 X ⁻¹ᵁ U) ≫ U.ι

Tactic:
morphismRestrict_ι,

Goal state after:
X : Scheme
U : X.Opens
⊢ (𝟙 X ⁻¹ᵁ U).ι ≫ 𝟙 X = 𝟙 ↑(𝟙 X ⁻¹ᵁ U) ≫ U.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.fst f g ≫ f

Tactic:
morphismRestrict_ι,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ (f ⁻¹ᵁ Scheme.Hom.opensRange g).ι ≫ f = pullback.fst f g ≫ f
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
R : CommRingCat
f : Spec R ⟶ X
hf : IsOpenImmersion f ∧ x ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑U
⊢ ∃ W, IsAffineOpen W ∧ x ∈ W ∧ W.carrier ⊆ ↑U

Tactic:
exact ⟨Scheme.Hom.opensRange f (H := hf.1),
    ⟨AlgebraicGeometry.isAffineOpen_opensRange f (H := hf.1), hf.2.1, hf.2.2⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, U)
n : ℕ
⊢ IsUnit ↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) ↑Γ(X, X.basicOpen f)) ⟨(fun x ↦ f ^ x) n, ⋯⟩)

Tactic:
exact
    Submonoid.leftInv_le_isUnit _
      (IsLocalization.toInvSubmonoid (Submonoid.powers f) (Γ(X, X.basicOpen f))
        _).prop

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case e
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ ↾⇑(ConcreteCategory.hom f.base) ≫ ↾⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) =
    ↾⇑(ConcreteCategory.hom g.base) ≫ ↾⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base)

pp: case h
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsColimit (Cofork.ofπ (↾⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base)) ?e)

pp: case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ ⇑(ConcreteCategory.hom (↾⇑(ConcreteCategory.hom f.base))) ⁻¹' (imageBasicOpen f g U s).carrier =
    ⇑(ConcreteCategory.hom (↾⇑(ConcreteCategory.hom g.base))) ⁻¹' (imageBasicOpen f g U s).carrier

Tactic:
· ext
    simp only [TypeCat.Fun.toFun_apply, comp_apply, ConcreteCategory.hom_ofHom,
      TypeCat.Fun.coe_mk, ← TopCat.comp_app, ← PresheafedSpace.comp_base]
    congr 3
    exact SheafedSpace.forgetToPresheafedSpace.congr_map
      (coequalizer.condition f.toShHom g.toShHom)

Goal state after:
case h
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsColimit (Cofork.ofπ (↾⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base)) ⋯)

case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ ⇑(ConcreteCategory.hom (↾⇑(ConcreteCategory.hom f.base))) ⁻¹' (imageBasicOpen f g U s).carrier =
    ⇑(ConcreteCategory.hom (↾⇑(ConcreteCategory.hom g.base))) ⁻¹' (imageBasicOpen f g U s).carrier