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

Goal state before:
pp: case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : -p = -C ↑u * X ^ k + -(C ↑v * X ^ m) + -(C ↑w * X ^ n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
← neg_mul,

Goal state after:
case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : -p = -C ↑u * X ^ k + -C ↑v * X ^ m + -(C ↑w * X ^ n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : -p = -C ↑u * X ^ k + -C ↑v * X ^ m + -(C ↑w * X ^ n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
← neg_mul,

Goal state after:
case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : -p = -C ↑u * X ^ k + -C ↑v * X ^ m + -C ↑w * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : AddZeroClass R
x y : R
⊢ QuadraticAlgebra.C (x + y) = QuadraticAlgebra.C x + QuadraticAlgebra.C y

Tactic:
by
  ext <;> simp

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : NegZeroClass R
x : R
⊢ QuadraticAlgebra.C (-x) = -QuadraticAlgebra.C x

Tactic:
by
  ext <;> simp

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ ω * ω = { re := a, im := b }

Tactic:
by
  ext <;> simp

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ ω * ω = a • 1 + b • ω

Tactic:
by
  ext <;> simp

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

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

Tactic:
by
  ext <;> simp

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

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

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP : P ≠ 0
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
generalize hd : P.natDegree = d

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP : P ≠ 0
d : ℕ
hd : P.natDegree = d
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ QuadraticAlgebra.C r * x = r • x

Tactic:
by
  ext <;> simp

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ QuadraticAlgebra.C (x * y) = QuadraticAlgebra.C x * QuadraticAlgebra.C y

Tactic:
by
  ext <;> simp

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : NonAssocSemiring R
n : ℕ
x y : R
⊢ ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }

Tactic:
by
  ext <;> simp

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : CommRing R
n : ℤ
x y : R
⊢ ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }

Tactic:
by
  ext <;> simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝ : AddCommMonoid k
f : G ≃ H
a : G
b : k
⊢ (equivMapDomain f (single a b)).coeff = (single (f a) b).coeff

Tactic:
simp_rw [coeff_equivMapDomain, single, Finsupp.equivMapDomain_single]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ ↑0 = 0

Tactic:
simp +instances [instNatCast, natCast, ← zero_quot]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝¹ : R → R → Prop
inst✝ : Algebra S R
r✝ : R → R → Prop
r : S
⊢ ∀ (x : RingQuot r✝),
    r • x =
      { toFun := fun r ↦ { toQuot := Quot.mk (Rel r✝) ((algebraMap S R) r) }, map_one' := ⋯, map_mul' := ⋯,
            map_zero' := ⋯, map_add' := ⋯ }
          r *
        x

Tactic:
by
    rintro ⟨⟨a⟩⟩
    simp [smul_quot, Algebra.smul_def, mul_quot]

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

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
⊢ ∀ (a b : FreeAlgebra R X),
    MulOpposite.unop (y (MulOpposite.unop (y a))) = a →
      MulOpposite.unop (y (MulOpposite.unop (y b))) = b → MulOpposite.unop (y (MulOpposite.unop (y (a + b)))) = a + b

Tactic:
· intros
      simp only [*, map_add, MulOpposite.unop_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
ha : a ≠ 0
⊢ (if a = 0 then p.support.erase n else insert n p.support) = insert n p.support

Tactic:
if_neg ha

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
ha : a ≠ 0
⊢ insert n p.support = insert n p.support
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)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : ↑v = 0
⊢ u = 1 • v

Tactic:
by ext; simp [this, huv] at huv ⊢

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) = ∑ p ∈ f.support ×ˢ g.support, F p

Tactic:
Finset.sum_product

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) = ∑ x ∈ f.support, ∑ y ∈ g.support, F (x, y)
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ a * (b + c) = a * b + a * c

Tactic:
by
      rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
      congr 2
      rw [mul_add]
      abel

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) = ∑ p ∈ f.support ×ˢ g.support, F p

Tactic:
Finset.sum_product

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) = ∑ x ∈ f.support, ∑ y ∈ g.support, F (x, y)
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ (a + b) * c = a * c + b * c

Tactic:
by
      rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
      congr 2
      rw [mul_add]
      abel

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

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
⊢ ∀ (x_1 : x ∈ U), ¬IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x ⋯)) 0)

Tactic:
intro hx

Goal state after:
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
hx : x ∈ U
⊢ ¬IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x ⋯)) 0)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap e.inv ((ConcreteCategory.hom e.hom.base) x) ≫ Hom.stalkMap e.hom x = X.presheaf.stalkSpecializes ⋯

Tactic:
rw [← stalkMap_comp, LocallyRingedSpace.stalkMap_congr_hom (e.hom ≫ e.inv) (𝟙 _) (by simp)]
  simp

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

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ (eqToHom ⋯ ≫ (Presheaf.pushforward C X.toRestrictTop.base).map (X.ofRestrict ⋯).c).app (op U✝) =
    (𝟙 (X.restrict ⋯)).c.app (op U✝)

Tactic:
ofRestrict_top_c,

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ (eqToHom ⋯ ≫ (Presheaf.pushforward C X.toRestrictTop.base).map (eqToHom ⋯)).app (op U✝) =
    (𝟙 (X.restrict ⋯)).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ (((X.ofRestrict ⋯).c ≫ (Presheaf.pushforward C (X.ofRestrict ⋯).base).map X.toRestrictTop.c) ≫
          whiskerRight (eqToHom ⋯) X.presheaf).app
      (op U✝) =
    (𝟙 X).c.app (op U✝)

Tactic:
ofRestrict_top_c,

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ ((eqToHom ⋯ ≫ (Presheaf.pushforward C (X.ofRestrict ⋯).base).map X.toRestrictTop.c) ≫
          whiskerRight (eqToHom ⋯) X.presheaf).app
      (op U✝) =
    (𝟙 X).c.app (op U✝)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X ≅ Y
x : ↥X
⊢ e.inv (e.hom x) = x

Tactic:
by
  change (e.hom ≫ e.inv) x = 𝟙 X.toPresheafedSpace x
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
⊢ E.Small

Tactic:
by
    choose i y hy using ofArrows_mem_jointlySurjectivePrecoverage_iff.mp E.mem₀
    refine ⟨X, i, ?_⟩
    rw [ofArrows_mem_jointlySurjectivePrecoverage_iff]
    intro x
    use x, y x, hy x

Goal state after:
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ Presieve.singleton f ∈ P.precoverage.coverings Y ↔ P f

Tactic:
by
  simp [← Presieve.ofArrows_pUnit.{0}]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P✝ Q P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
Z : C
g : Z ⟶ Y
W : C
a : W ⟶ X
h : S a
⊢ P (pullback.snd a f)

Tactic:
have := S.hasPullback f h

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P✝ Q P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ P.precoverage.coverings X
this✝ : S.HasPullbacks f
Z : C
g : Z ⟶ Y
W : C
a : W ⟶ X
h : S a
this : HasPullback a f
⊢ P (pullback.snd a f)
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:
← limit.w (cospan f g) WalkingCospan.Hom.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 ≫ (cospan f g).map WalkingCospan.Hom.inl)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (X Y S : Scheme) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    IsOpenImmersion g → IsOpenImmersion (pullback.fst f g)

Tactic:
intro X Y Z f g _ H; infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

Tactic:
inf_eq_right.mpr _

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r
⊢ X.basicOpen r ≤ f ⁻¹ᵁ f ''ᵁ U
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
x : ↑↑s.pt.toPresheafedSpace
this :
  PresheafedSpace.Hom.stalkMap
      (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯) ≫
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd)
      x =
    eqToHom ⋯ ≫ s.snd.stalkMap x
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
        x))

Tactic:
rw [PresheafedSpace.stalkMap.comp, ← IsIso.eq_inv_comp] at this

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
x : ↑↑s.pt.toPresheafedSpace
this :
  PresheafedSpace.Hom.stalkMap
      (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
        (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
      x =
    inv
        (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd
          ((ConcreteCategory.hom
              (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                  (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)).base)
            x)) ≫
      eqToHom ⋯ ≫ s.snd.stalkMap x
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
        x))
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:
← limit.w (cospan f g) WalkingCospan.Hom.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 ≫ (cospan f g).map WalkingCospan.Hom.inl)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
⊢ const (g i • f j) (g i * g j) (basicOpen (g i * g j)) ⋯ =
    (ConcreteCategory.hom ((structureSheafInType R M).obj.map (homOfLE ?m.192).op)) s

Tactic:
refine .trans (Subtype.ext <| funext fun a ↦ ?_) congr((structureSheafInType R M).obj.map
        (homOfLE ((PrimeSpectrum.basicOpen_mul (g i) (g j)).trans_le inf_le_right)).op $(H j))

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
a : ↥(unop (op (basicOpen (g i * g j))))
⊢ ↑(const (g i • f j) (g i * g j) (basicOpen (g i * g j)) ⋯) a =
    ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map (homOfLE ⋯).op))
          (const (f j) (g j) (basicOpen (g j)) ⋯))
      a
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ pullback.snd (f ≫ g) (Scheme.Opens.ι U) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)

Tactic:
← pullbackRightPullbackFstIso_inv_snd_snd

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.snd g (Scheme.Opens.ι U) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_1
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ resLE iY (f ⁻¹ᵁ US) (g ⁻¹ᵁ UX) ⋯ ⁻¹ᵁ opensRange (T.homOfLE hUST) = opensRange (Y.homOfLE ⋯)

Tactic:
simp only [Scheme.opensRange_homOfLE, ← Scheme.Hom.comp_preimage, Scheme.Hom.resLE_comp_ι]

Goal state after:
case refine_1
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ ((g ⁻¹ᵁ UX).ι ≫ iY) ⁻¹ᵁ UT = (g ⁻¹ᵁ UX).ι ⁻¹ᵁ UY
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑hU.fromSpec = ↑U

Tactic:
by
  delta IsAffineOpen.fromSpec; dsimp [IsAffineOpen.isoSpec_inv]
  rw [Set.range_comp, Set.range_eq_univ.mpr, Set.image_univ]
  · exact Subtype.range_coe
  rw [← TopCat.coe_comp, ← TopCat.epi_iff_surjective]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ f ≫ s.inl = g ≫ s.inl

Tactic:
have H₁ : f ≫ s.inl = s.inr := by simpa using congr(coprod.inl ≫ $s.condition)

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
H₁ : f ≫ s.inl = s.inr
⊢ f ≫ s.inl = g ≫ s.inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ s ≫ 𝟙 S = g ≫ t

Tactic:
by simp [hg]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ s ≫ 𝟙 S = g ≫ t

Tactic:
by simp [hg]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
i : 𝒰.I₀
⊢ s ≫ 𝟙 S = g ≫ t

Tactic:
by simp [hg]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op W))
⊢ ↑((comap (g.comp f) U W ⋯) s) p = ↑(((comap g V W hVW).comp (comap f U V hUV)) s) p

Tactic:
rw [comap_apply, Localization.localRingHom_comp _ (PrimeSpectrum.comap g p.1).asIdeal] <;>
        simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e_a
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ IsOpenImmersion.lift U.ι f ⋯ ≫ hU.isoSpec.hom = IsOpenImmersion.lift U.ι g ⋯ ≫ hU.isoSpec.hom

Tactic:
← Spec.homEquiv.injective.eq_iff,

Goal state after:
case e_a
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ Spec.homEquiv (IsOpenImmersion.lift U.ι f ⋯ ≫ hU.isoSpec.hom) =
    Spec.homEquiv (IsOpenImmersion.lift U.ι g ⋯ ≫ hU.isoSpec.hom)