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

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h : ¬p = 0 → ↑(Fintype.card Fq) ^ p.natDegree = 0
⊢ p = 0

Tactic:
contrapose! h

Goal state after:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h : p ≠ 0
⊢ p ≠ 0 ∧ ↑(Fintype.card Fq) ^ p.natDegree ≠ 0
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ (p.divModByMonicAux H).2.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
refine SetLike.le_def.mp ?_ (coeff_divModByMonicAux_mem_span_pow_mul_span (R := R) p q H i).2

Goal state after:
case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ≤ Mq ^ deg(p) * Mp
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
m n : ℕ
⊢ x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)

Tactic:
induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [smeval_add, ph, qh, mul_add]
  | monomial n a => simp only [smeval_monomial, mul_smul_comm, npow_mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p) ↔ p.roots = 0

Tactic:
simp_rw [show p.natDegree / 2 = 1 from
      (Nat.div_le_div_right hp3).antisymm
        (by apply Nat.div_le_div_right (c := 2) hp2),
    show Finset.Ioc 0 1 = {1} from rfl,
    Finset.mem_singleton, Multiset.eq_zero_iff_forall_notMem, mem_roots hp0, ← dvd_iff_isRoot]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree = 1 → ¬q ∣ p) ↔ ∀ (a : R), ¬X - C a ∣ p
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
p q : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
⊢ (p * q).smeval x = p.smeval x * q.smeval x

Tactic:
induction p using Polynomial.induction_on' with
  | add r s hr hs => simp only [hr, hs, smeval_add, add_mul]
  | monomial n a =>
    simp only [smeval_monomial, smeval_monomial_mul, smul_mul_assoc]

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

Goal state before:
pp: p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            (((monomial (k + k)) (↑u * ↑w)).toFinsupp + ((monomial (k + (n - m + k))) (↑u * ↑v)).toFinsupp +
                    ((monomial (k + n)) (↑u * ↑u)).toFinsupp +
                  (((monomial (m + k)) (↑v * ↑w)).toFinsupp + ((monomial (m + (n - m + k))) (↑v * ↑v)).toFinsupp +
                    ((monomial (m + n)) (↑v * ↑u)).toFinsupp) +
                (((monomial (n + k)) (↑w * ↑w)).toFinsupp + ((monomial (n + (n - m + k))) (↑w * ↑v)).toFinsupp +
                  ((monomial (n + n)) (↑w * ↑u)).toFinsupp)).coeff) }

Tactic:
toFinsupp_monomial,

Goal state after:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            (AddMonoidAlgebra.single (k + k) (↑u * ↑w) + AddMonoidAlgebra.single (k + (n - m + k)) (↑u * ↑v) +
                    AddMonoidAlgebra.single (k + n) (↑u * ↑u) +
                  (AddMonoidAlgebra.single (m + k) (↑v * ↑w) + AddMonoidAlgebra.single (m + (n - m + k)) (↑v * ↑v) +
                    AddMonoidAlgebra.single (m + n) (↑v * ↑u)) +
                (AddMonoidAlgebra.single (n + k) (↑w * ↑w) + AddMonoidAlgebra.single (n + (n - m + k)) (↑w * ↑v) +
                  AddMonoidAlgebra.single (n + n) (↑w * ↑u))).coeff) }
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
⊢ (⇑SignType.sign ∘ fun x ↦ -x) = (fun x ↦ -x) ∘ ⇑SignType.sign

Tactic:
grind [Left.sign_neg]

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 < 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)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
this✝² : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length
this✝¹ : P.natDegree + 2 = ((X - C η) * P).coeffList.length
this✝ : ((X - C η) * P).leadingCoeff = P.leadingCoeff
h₉ : ¬((X - C η) * P).nextCoeff = 0
this :
  (monomial P.natDegree) ((X - C η) * P).nextCoeff =
    (monomial P.natDegree) P.nextCoeff - C η * (monomial P.natDegree) P.leadingCoeff
⊢ ((X - C η) * P).eraseLead.eraseLead = ((X - C η) * P.eraseLead).eraseLead

Tactic:
by
        grind [X_mul_monomial, sub_mul, mul_sub, self_sub_monomial_natDegree_leadingCoeff,
          natDegree_eraseLead_add_one, leadingCoeff_eraseLead_eq_nextCoeff]

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

Goal state before:
pp: case inl.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 = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑v ↑z
h1 : ↑y = ↑v
h2 : q = p.mirror
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
exact Or.inr (Or.inr (Or.inl h2))

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

Goal state before:
pp: 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

Tactic:
have hcQ : 0 < coeff P 0 := by grind [leadingCoeff]

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
hcQ : 0 < P.coeff 0
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : CommSemiring R
r1 r2 : R
⊢ r1 • QuadraticAlgebra.C r2 = QuadraticAlgebra.C r1 * QuadraticAlgebra.C r2

Tactic:
C_mul_eq_smul

Goal state after:
R : Type u_1
a b : R
inst✝ : CommSemiring R
r1 r2 : R
⊢ r1 • QuadraticAlgebra.C r2 = r1 • QuadraticAlgebra.C r2
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddCommGroup = inst₂.toAddCommGroup
this : inst₁.toAddGroupWithOne = inst₂.toAddGroupWithOne
⊢ inst₁ = inst₂

Tactic:
injection this with _ h_addMonoidWithOne

Goal state after:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this : inst₁.toAddCommGroup = inst₂.toAddCommGroup
toIntCast_eq✝ : inst₁.toIntCast = inst₂.toIntCast
h_addMonoidWithOne :
  { toNatCast := inst₁.toNatCast, toAddMonoid := inst₁.toAddMonoid, toOne := inst₁.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ } =
    { toNatCast := inst₂.toNatCast, toAddMonoid := inst₂.toAddMonoid, toOne := inst₂.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ a ∉ ((erase a) f).support

Tactic:
rw [support_erase, Finset.mem_erase]
      exact fun H ↦ H.1 rfl

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✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
⊢ ∀ (r : S), Quot.lift ⇑f ⋯ ((algebraMap S (RingQuot s)) r).toQuot = (algebraMap S B) r

Tactic:
rintro x

Goal state after:
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✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
x : S
⊢ Quot.lift ⇑f ⋯ ((algebraMap S (RingQuot s)) x).toQuot = (algebraMap S B) x
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✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : { f // ∀ ⦃x y : A⦄, s x y → f x = f y }
⊢ (fun F ↦ ⟨F.comp (mkAlgHom S s), ⋯⟩) ((fun f' ↦ preLiftAlgHom S ⋯) f) = f

Tactic:
by
      ext
      simp only [preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def,
        AlgHom.coe_comp, AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
        Function.comp_apply]

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

Goal state before:
pp: R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : Star R
p q : StarSubsemiring R
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ p = q

Tactic:
obtain ⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩ := p; cases q; congr

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

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

Tactic:
induction k with

Goal state after:
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✝³ : SMul S₁ S₂
inst✝² : SMulZeroClass S₁ k
inst✝¹ : SMulZeroClass S₂ k
inst✝ : IsScalarTower S₁ S₂ k
x✝² : S₁
x✝¹ : S₂
x✝ : SkewMonoidAlgebra k G
coeff✝ : G →₀ k
⊢ (x✝² • x✝¹) • { coeff := coeff✝ } = x✝² • x✝¹ • { coeff := coeff✝ }

Tactic:
simp_rw [← ofCoeff_smul, smul_assoc]

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

Goal state before:
pp: case inr.inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : z ≤ x
⊢ y ≤ x + z

Tactic:
add_eq_right hx

Goal state after:
case inr.inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : z ≤ x
⊢ y ≤ z
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a)) =
    sym
      (⅟2 *
        (unsym a * unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) +
          unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) * unsym a))

Tactic:
rw [unsym_sym, sym_inj, ← mul_assoc, ← commute_half_left (unsym a), mul_assoc (⅟2) (unsym a),
        mul_assoc (⅟2) _ (unsym a), ← mul_add, ← mul_assoc]

Goal state after:
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
        unsym (a * a) * unsym b * unsym a) =
    ⅟2 * ⅟2 *
      (unsym a * (unsym b * unsym (a * a) + unsym (a * a) * unsym b) +
        (unsym b * unsym (a * a) + unsym (a * a) * unsym b) * unsym a)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ (X.ofRestrict ⋯).c.app (op U✝) = (eqToHom ⋯).app (op U✝)

Tactic:
dsimp [ofRestrict]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ X.presheaf.map (⋯.adjunction.counit.app U✝).op = (eqToHom ⋯).app (op U✝)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
k : ℕ
h : 0 < k + Nat.succ 0
⊢ X.basicOpen (f ^ (k + Nat.succ 0)) = X.basicOpen f

Tactic:
induction k with

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf ≅ (Y.restrict ⋯).presheaf

Tactic:
symm
    fapply NatIso.ofComponents
    · intro U
      refine asIso (f.c.app (op (opensFunctor f |>.obj (unop U)))) ≪≫ X.presheaf.mapIso (eqToIso ?_)
      induction U with | op U => ?_
      cases U
      dsimp only [IsOpenMap.functor, Functor.op, Opens.map_def]
      congr 2
      erw [Set.preimage_image_eq _ H.base_open.injective]
      rfl
    · intro U V i
      dsimp
      simp only [NatTrans.naturality_assoc, TopCat.Presheaf.pushforward_obj_obj,
        TopCat.Presheaf.pushforward_obj_map, Quiver.Hom.unop_op, Category.assoc]
      rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]
      congr 1

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑I.radical = X.zeroLocus ↑I

Tactic:
by
  refine (X.zeroLocus_mono I.le_radical).antisymm ?_
  simp only [Set.subset_def, mem_zeroLocus_iff, SetLike.mem_coe]
  rintro x H f ⟨n, hn⟩ hx
  rcases n.eq_zero_or_pos with rfl | hn'
  · exact H f (by simpa using I.mul_mem_left f hn) hx
  · exact H _ hn (X.basicOpen_pow f hn' ▸ hx)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ (Spec R).zeroLocus s = PrimeSpectrum.zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s)

Tactic:
convert! Spec_zeroLocus_eq_zeroLocus ((Scheme.ΓSpecIso R).inv ⁻¹' s)

Goal state after:
R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ (Spec R).zeroLocus s = PrimeSpectrum.zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s) ↔
    (Spec R).zeroLocus
        (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s) =
      PrimeSpectrum.zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsOpenImmersion g
⊢ opensRange (f ≫ g) = opensRange g

Tactic:
by
  rw [opensRange_comp, opensRange_of_isIso, image_top_eq_opensRange]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ f ⁻¹ᵁ opensRange f = ⊤

Tactic:
simp [Scheme.Hom.opensRange]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover P X
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.f i)) ∧
    ∀ (i : { I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.I₀),
      P ({ I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.f i)

Tactic:
refine ⟨fun x ↦ ?_, 𝒰.map_prop⟩

Goal state after:
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover P X
x : ↥X
⊢ ∃ i, x ∈ Set.range ⇑({ I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.f i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hf : Scheme.Hom.opensRange f = ⊤
⊢ Set.range ⇑f = Set.univ

Tactic:
exact TopologicalSpace.Opens.ext_iff.mp hf

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 : R
⊢ IsUnit ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) f)

Tactic:
by
  have := (isUnit_basicOpen f).map
    (algebraMap _ (Module.End Γ(R, basicOpen f) Γ(M, basicOpen f)))
  rw [Module.End.isUnit_iff] at this ⊢
  convert! this
  ext a
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ app (resLE f U V e) ⊤ = U.topIso.hom ≫ appLE f U V e ≫ V.topIso.inv

Tactic:
by simp [Scheme.Hom.resLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ Opens.IsBasis X.affineOpens

Tactic:
rw [Opens.isBasis_iff_nbhd]
  rintro U x (hU : x ∈ (U : Set X))
  obtain ⟨S, hS, hxS, hSU⟩ := X.affineBasisCover_is_basis.exists_subset_of_mem_open hU U.isOpen
  refine ⟨⟨S, X.affineBasisCover_is_basis.isOpen hS⟩, ?_, hxS, hSU⟩
  rcases hS with ⟨i, rfl⟩
  exact isAffineOpen_opensRange _

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
⊢ (ConcreteCategory.hom (toStalk R x)) f =
    (CommRingCat.Hom.hom ((structurePresheafInCommRingCat R).germ (basicOpen f) x hf))
      ((algebraMap R ((structureSheafInType R R).obj.obj (op (basicOpen f)))) f)

Tactic:
exact ((structurePresheafInCommRingCat R).germ_res_apply (homOfLE (le_top : basicOpen f ≤ ⊤))
    x hf (algebraMap R Γ(R, ⊤) f)).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := ⋯
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) := ⋯
⊢ CommRingCat.Hom.hom
      (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))))
          (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)))))
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r))

Tactic:
apply IsLocalization.ringHom_ext (.powers r)

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := ⋯
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) := ⋯
⊢ (CommRingCat.Hom.hom
          (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r))
            ⋯)).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))))
              (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)))))
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r))).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
          (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
            (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
            (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
        X.presheaf.map (eqToHom ⋯).op)

Tactic:
apply IsLocalization.ringHom_ext (.powers r)

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r))).comp (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom
              (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
                (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r)))
                (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
            X.presheaf.map (eqToHom ⋯).op)).comp
      (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed {↑x}
⊢ (hU.primeIdealOf x).asIdeal.IsMaximal

Tactic:
by
  have hx₀ : IsClosed {x} := by
    simpa [← Set.image_singleton, Set.preimage_image_eq _ Subtype.val_injective]
      using hx.preimage U.isOpenEmbedding'.continuous
  apply (hU.primeIdealOf x).isClosed_singleton_iff_isMaximal.mp
  rw [primeIdealOf, ← Set.image_singleton]
  refine (Topology.IsClosedEmbedding.isClosed_iff_image_isClosed <|
    IsHomeomorph.isClosedEmbedding ?_).mp hx₀
  apply (TopCat.isIso_iff_isHomeomorph _).mp
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
⊢ comap (RingHom.id R) U U ⋯ = RingHom.id ↑((structureSheaf R).obj.obj (op U))

Tactic:
rw [comap_id rfl]; rfl

Goal state after: