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

Goal state before:
pp: case h.left
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)

Tactic:
have h₇ : natDegree ((X - C η) * P) = P.natDegree + 1 := by
      rw [natDegree_mul h₅ h₃, natDegree_X_sub_C, add_comm]
    have h₈ : ((X - C η) * P.eraseLead).eraseLead =
        (X - C η) * P.eraseLead - monomial P.natDegree P.nextCoeff := by
      simp [← self_sub_monomial_natDegree_leadingCoeff (_ * _), natDegree_mul,
        h₅, h₆, h₂, h₄, add_comm 1]
    have : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length := by
      simp [h₅, h₆, natDegree_mul, add_comm 1]
    have : P.natDegree + 2 = ((X - C η) * P).coeffList.length := by simp [X_sub_C_ne_zero, h₃, h₇]
    have := leadingCoeff_monic_mul (q := P) (monic_X_sub_C η)
    by_cases h₉ : ((X - C η) * P).nextCoeff = 0
    · suffices ((X - C η) * P).eraseLead = ((X - C η) * P.eraseLead).eraseLead by
        have := coeffList_eraseLead (mul_ne_zero (X_sub_C_ne_zero η) h₃)
        #adaptation_note
        /--
        Moving from `nightly-2025-10-13` to `nightly-2025-10-19`
        we now need to provide an intermediate step.
        -/
        have : ((X - C η) * P).natDegree - ((X - C η) * P).eraseLead.degree.succ = n + 1 := by grind
        grind [leadingCoeff_mul, leadingCoeff_X_sub_C]
      suffices C η * monomial P.natDegree P.leadingCoeff = monomial P.natDegree P.nextCoeff by
        grind [X_mul_monomial, sub_mul, mul_sub, self_sub_monomial_natDegree_leadingCoeff]
      grind [leadingCoeff, nextCoeff_of_natDegree_pos, eq_of_sub_eq_zero, coeff_X_sub_C_mul]
    · suffices ((X - C η) * P).eraseLead.eraseLead = ((X - C η) * P.eraseLead).eraseLead by
        have := leadingCoeff_cons_eraseLead h₉
        have := coeffList_eraseLead (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₉)
        grind [leadingCoeff_eraseLead_eq_nextCoeff]
      suffices monomial P.natDegree ((X - C η) * P).nextCoeff =
          monomial P.natDegree P.nextCoeff - C η * monomial P.natDegree P.leadingCoeff by
        grind [X_mul_monomial, sub_mul, mul_sub, self_sub_monomial_natDegree_leadingCoeff,
          natDegree_eraseLead_add_one, leadingCoeff_eraseLead_eq_nextCoeff]
      grind [coeff_X_sub_C_mul, nextCoeff_of_natDegree_pos, leadingCoeff]

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : Zero R
inst✝ : One R
r : R
⊢ QuadraticAlgebra.C r = 1 ↔ r = 1

Tactic:
rw [← C_one, C_inj]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ ω * ω = (algebraMap R (QuadraticAlgebra R a b)) a + (algebraMap R (QuadraticAlgebra R a b)) b * ω

Tactic:
simp [omega_mul_omega_eq_add, Algebra.algebraMap_eq_smul_one]

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
η : R
hη : 0 < η
d : ℕ
ih : ∀ m < d, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
rcases d with _ | d

Goal state after:
case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
ih : ∀ m < 0, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = 0
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : x * (star x * (algebraMap R (QuadraticAlgebra R a b)) r) = 1
hr' : r * norm x = 1
⊢ star x * (algebraMap R (QuadraticAlgebra R a b)) r * x = 1

Tactic:
rw [mul_comm, hr]

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
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 0
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = -1
h✝ : ¬P.eraseLead = 0
this : ((X - C η) * P).eraseLead.signVariations + 1 = ((X - C η) * P).signVariations
⊢ ((X - C η) * P.eraseLead).signVariations ≤ ((X - C η) * P).eraseLead.signVariations

Tactic:
have := signVariations_eraseLead_le (eraseLead ((X - C η) * P))

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 0
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = -1
h✝ : ¬P.eraseLead = 0
this✝ : ((X - C η) * P).eraseLead.signVariations + 1 = ((X - C η) * P).signVariations
this : ((X - C η) * P).eraseLead.eraseLead.signVariations ≤ ((X - C η) * P).eraseLead.signVariations
⊢ ((X - C η) * P.eraseLead).signVariations ≤ ((X - C η) * P).eraseLead.signVariations
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * star z = 0
⊢ star w * star (star z) = 0

Tactic:
← star_mul,

Goal state after:
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * star z = 0
⊢ star (star z * w) = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
x : QuadraticAlgebra K a b
⊢ (q • x).re = (↑q * x).re

Tactic:
simp [Rat.smul_def]

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

Goal state before:
pp: case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
x : QuadraticAlgebra K a b
⊢ (q • x).im = (↑q * x).im

Tactic:
simp [Rat.smul_def]

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 : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (unit.mul a) = mapAux f a

Tactic:
by simp [toEnvelGroup.mapAux]

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 : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (a.mul unit) = mapAux f a

Tactic:
by simp [toEnvelGroup.mapAux]

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 : R →◃ Quandle.Conj G
a : PreEnvelGroup R
⊢ mapAux f (a.inv.mul a) = mapAux f unit

Tactic:
by simp [toEnvelGroup.mapAux]

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 : R →◃ Quandle.Conj G
x y : R
⊢ mapAux f (((incl x).mul (incl y)).mul (incl x).inv) = mapAux f (incl (x ◃ y))

Tactic:
by simp [toEnvelGroup.mapAux]

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

Goal state before:
pp: case succ
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝¹² : NonUnitalNonAssocSemiring α
inst✝¹¹ : Monoid M
inst✝¹⁰ : Monoid N
inst✝⁹ : Semiring R
inst✝⁸ : DistribMulAction M α
inst✝⁷ : SMulCommClass M α α
inst✝⁶ : IsScalarTower M α α
inst✝⁵ : DistribMulAction N α
inst✝⁴ : SMulCommClass N α α
inst✝³ : IsScalarTower N α α
inst✝² : Module R α
inst✝¹ : SMulCommClass R α α
inst✝ : IsScalarTower R α α
f : CentroidHom α
a b : α
n : ℕ
ih :
  let __AddMonoidHom := f.toEnd ^ n;
  (↑(f.toEnd ^ n)).toFun (a * b) = a * (↑(f.toEnd ^ n)).toFun b
__AddMonoidHom✝ : α →+ α := f.toEnd ^ (n + 1)
⊢ (↑(f.toEnd ^ (n + 1))).toFun (a * b) = a * (↑(f.toEnd ^ (n + 1))).toFun b

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝¹² : NonUnitalNonAssocSemiring α
inst✝¹¹ : Monoid M
inst✝¹⁰ : Monoid N
inst✝⁹ : Semiring R
inst✝⁸ : DistribMulAction M α
inst✝⁷ : SMulCommClass M α α
inst✝⁶ : IsScalarTower M α α
inst✝⁵ : DistribMulAction N α
inst✝⁴ : SMulCommClass N α α
inst✝³ : IsScalarTower N α α
inst✝² : Module R α
inst✝¹ : SMulCommClass R α α
inst✝ : IsScalarTower R α α
f : CentroidHom α
a b : α
n : ℕ
ih :
  let __AddMonoidHom := f.toEnd ^ n;
  (↑(f.toEnd ^ n)).toFun (a * b) = (↑(f.toEnd ^ n)).toFun a * b
__AddMonoidHom✝ : α →+ α := f.toEnd ^ (n + 1)
⊢ (↑(f.toEnd ^ (n + 1))).toFun (a * b) = (↑(f.toEnd ^ (n + 1))).toFun a * b

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case succ
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
x✝ : RingQuot r
a✝ : Quot (Rel r)
a b : R
h : Rel r a b
n : ℕ
ih : Quot.mk (Rel r) (a ^ n) = Quot.mk (Rel r) (b ^ n)
⊢ Quot.mk (Rel r) (a ^ (n + 1)) = Quot.mk (Rel r) (b ^ (n + 1))

Tactic:
| succ n ih =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (monomial 0) 1 = X ^ 0

Tactic:
| zero      =>

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = X ^ (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ star ((star g * ↑f) (star a)) = star ((↑f * star g) (star a))

Tactic:
f.property.comm

Goal state after:
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ star ((star g * ↑f) (star a)) = star ((star g * ↑f) (star a))
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
p : SkewPolynomial R
⊢ X ^ 0 * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[0] b)) * X ^ 0

Tactic:
| zero      =>

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ X ^ (n + 1) * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n + 1] b)) * X ^ (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
r : R
⊢ (monomial n) r * X ^ 0 = (monomial (n + 0)) r

Tactic:
| zero      =>

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n✝ : ℕ
r : R
n : ℕ
ih : (monomial n✝) r * X ^ n = (monomial (n✝ + n)) r
⊢ (monomial n✝) r * X ^ (n + 1) = (monomial (n✝ + (n + 1))) r

Tactic:
| succ n ih =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ X ^ 0 = (monomial 0) 1

Tactic:
| zero      =>

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
hn : X ^ n = (monomial n) 1
⊢ X ^ (n + 1) = (monomial (n + 1)) 1

Tactic:
rw [pow_succ', hn, X, monomial_mul_monomial]

Goal state after:
case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
hn : X ^ n = (monomial n) 1
⊢ (monomial (1 + n)) (1 * (⇑φ)^[1] 1) = (monomial (n + 1)) 1
Module: Mathlib.Algebra.Star.RingQuot

Goal state before:
pp: case mk
R✝ : Type u
inst✝³ : Semiring R✝
r✝ : R✝ → R✝ → Prop
inst✝² : StarRing R✝
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ star' r hr (star' r hr { toQuot := Quot.mk (Rel r) a✝ }) = { toQuot := Quot.mk (Rel r) a✝ }

Tactic:
simp [star'_quot]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : AddMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
inhabited_h : Inhabited G
⊢ IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a

Tactic:
refine ⟨IsSMulRegular.skewMonoidAlgebra, fun ha b₁ b₂ inj ↦ ?_⟩

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : AddMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj : (fun x ↦ a • x) b₁ = (fun x ↦ a • x) b₂
⊢ b₁ = b₂
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
⊢ Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c ≫ H.hom.c =
    𝟙 ((Presheaf.pushforward C H.hom.base).obj X.presheaf)

Tactic:
by
    ext U
    dsimp
    rw [NatTrans.id_app]
    simp only [Presheaf.pushforwardToOfIso_app, Iso.symm_inv, mapIso_hom, forget_map,
      Iso.symm_hom, mapIso_inv, eqToHom_map, assoc]
    have eq₁ := congr_app H.hom_inv_id (op ((Opens.map H.hom.base).obj U))
    have eq₂ := H.hom.c.naturality (eqToHom (congr_obj (congr_arg Opens.map
      ((forget C).congr_map H.inv_hom_id.symm)) U)).op
    rw [id_c, NatTrans.id_app, id_comp, eqToHom_map, comp_c_app] at eq₁
    rw [eqToHom_op, eqToHom_map] at eq₂
    erw [eq₂, reassoc_of% eq₁]
    simp

Goal state after:
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)]

Goal state after:
X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ X.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 X) x = X.presheaf.stalkSpecializes ⋯
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ (f ≫ inv f) ⁻¹ᵁ U = U

Tactic:
rw [IsIso.hom_inv_id]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ 𝟙 X ⁻¹ᵁ U = U
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
f : R
inst✝ : IsLocalization.Away f S
e :
  (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp
      (algebraMap R (Localization.Away f)) =
    algebraMap R S
H : IsIso (CommRingCat.ofHom (↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).toRingHom)
⊢ IsOpenImmersion
    (Spec.map (CommRingCat.ofHom ↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm) ≫
      Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f))))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, AlgEquiv.toAlgHom_toRingHom] at H ⊢

Goal state after:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
f : R
inst✝ : IsLocalization.Away f S
e :
  (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp
      (algebraMap R (Localization.Away f)) =
    algebraMap R S
H : IsIso (CommRingCat.ofHom ↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm)
⊢ IsOpenImmersion
    (Spec.map (CommRingCat.ofHom ↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm) ≫
      Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f))))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case w
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
⊢ ∀ (j : WalkingCospan),
    (limit.cone (cospan f.base g.base)).π.app j =
      ((forget C).mapCone (pullbackConeOfLeft f g)).π.app j ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app j

Tactic:
rintro (_ | _ | _) <;> symm

Goal state after:
case w.none
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
⊢ ((forget C).mapCone (pullbackConeOfLeft f g)).π.app none ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app none =
    (limit.cone (cospan f.base g.base)).π.app none

case w.some.left
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
⊢ ((forget C).mapCone (pullbackConeOfLeft f g)).π.app (some WalkingPair.left) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.left) =
    (limit.cone (cospan f.base g.base)).π.app (some WalkingPair.left)

case w.some.right
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
⊢ ((forget C).mapCone (pullbackConeOfLeft f g)).π.app (some WalkingPair.right) ≫
      (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app (some WalkingPair.right) =
    (limit.cone (cospan f.base g.base)).π.app (some WalkingPair.right)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = Scheme.Hom.app f V ≫ Y.presheaf.map (𝟙 (op ((Opens.map f.base).obj V)))

Tactic:
CategoryTheory.Functor.map_id,

Goal state after:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = Scheme.Hom.app f V ≫ 𝟙 Γ(Y, f ⁻¹ᵁ V)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

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

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

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case neg
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥Y
hx : x ∉ Set.range ⇑f
⊢ x ∈ ⇑f '' X.zeroLocus s ↔ x ∈ Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑f

Tactic:
simp only [Set.mem_inter_iff, hx, and_false, iff_false]
    exact fun H ↦ hx (Set.image_subset_range _ _ H)

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : M
g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen g₁
hf : f₁ = f₂
hg : g₁ = g₂
⊢ const f₁ g₁ U hu = const f₂ g₂ U ⋯

Tactic:
by subst hf hg; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
V : (↑U).Opens
r : ↑Γ(↑U, V)
x : ↥U
⊢ x ∈ (↑U).basicOpen ((ConcreteCategory.hom ((↑U).presheaf.map (eqToHom ⋯).op)) r) ↔ ↑x ∈ X.basicOpen r

Tactic:
exact congr(x ∈ $(U.ι.preimage_basicOpen r)).to_iff.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: I : Type w
inst✝¹ : Category.{v, w} I
D : I ⥤ Scheme
inst✝ : ∀ (i : I), IsAffine (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this✝ : ∀ (i : I), IsIso (α.app i)
this : IsIso α
⊢ PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp

Tactic:
have := monadicCreatesLimits.{v, w} Scheme.Spec.{u}

Goal state after:
I : Type w
inst✝¹ : Category.{v, w} I
D : I ⥤ Scheme
inst✝ : ∀ (i : I), IsAffine (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this✝¹ : ∀ (i : I), IsIso (α.app i)
this✝ : IsIso α
this : CreatesLimitsOfSize.{v, w, u, u, u + 1, u + 1} Scheme.Spec
⊢ PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen (f ''ᵁ U)

Tactic:
rwa [f.isAffineOpen_iff_of_isOpenImmersion]

Goal state after: