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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
h₁✝ : 0 < ((monomial n) x).coeffList.length
h₁ : 0 < (x :: List.replicate n 0).length
⊢ ∀ (w : List R),
    ((monomial n) x).coeffList = ((monomial n) x).leadingCoeff :: w →
      ((monomial n) x).coeffList.get ⟨0, h₁✝⟩ = (x :: List.replicate n 0).get ⟨0, h₁⟩

Tactic:
by simp_all

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
q p✝ q✝ : A[X]
a✝¹ :
  (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm (p✝ * q)) =
    p✝ • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm q) +
      q • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm p✝)
a✝ :
  (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm (q✝ * q)) =
    q✝ • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm q) +
      q • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm q✝)
⊢ (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((p✝ + q✝) * q)) =
    (p✝ + q✝) • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm q) +
      q • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm (p✝ + q✝))

Tactic:
simp only [add_mul, map_add, add_smul, smul_add, add_add_add_comm, *]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ k - n < (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length

Tactic:
simp
      lia

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

Goal state before:
pp: case neg.refine_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
split_ifs <;> simp only [mul_one, mul_zero]

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]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
h✝ : i = deg(p) - deg(q)
⊢ p.leadingCoeff ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
h✝ : ¬i = deg(p) - deg(q)
⊢ 0 ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)

Tactic:
revAt_le (h2.trans (Nat.le_add_right _ _))

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : q₁ * g ^ (n + 1) + (∑ x, rs₁ x * g ^ ↑x + r₁ * g ^ n) = q₂ * g ^ (n + 1) + (∑ x, rs₂ x * g ^ ↑x + r₂ * g ^ n)
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂

Tactic:
rw [← add_rotate' (r₁ * g ^ n), ← add_rotate' (r₂ * g ^ n), pow_succ', ← mul_assoc, ← mul_assoc,
      ← add_assoc, ← add_assoc, ← add_mul, ← add_mul, ← mul_comm g, ← mul_comm g] at hf

Goal state after:
case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : (r₁ + g * q₁) * g ^ n + ∑ x, rs₁ x * g ^ ↑x = (r₂ + g * q₂) * g ^ n + ∑ x, rs₂ x * g ^ ↑x
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ (trinomial k m n u v w).coeff k ≠ 0

Tactic:
by rwa [trinomial_trailing_coeff' hkm hmn]

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

Goal state before:
pp: case cons.refine_1
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ i ∉ s

pp: case cons.refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ (↑(Finset.cons i s ?cons.refine_1)).Pairwise fun i j ↦ IsCoprime (g i) (g j)

Tactic:
· exact mt Finset.mem_cons_of_mem hi

Goal state after:
case cons.refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ (↑(Finset.cons i s ⋯)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
⊢ P.signVariations =
    P.eraseLead.signVariations + if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

Tactic:
by
  by_cases hpz : P = 0
  · simp_all
  have hsl : SignType.sign (leadingCoeff P) ≠ 0 := by simp_all
  rw [signVariations, signVariations, coeffList_eraseLead hpz]
  rw [List.map_cons, List.map_append, List.map_replicate]
  rcases h_eL : P.eraseLead.coeffList with _ | ⟨c, cs⟩
  · simp [coeffList_eq_nil.mp h_eL, h]
  simp only [List.filter_append, List.filter_replicate, List.map_cons, List.filter, ne_eq, hsl]
  have h₁ : SignType.sign c ≠ 0 := by
    by_contra h₂
    suffices eraseLead P = 0 by grind [coeffList_zero]
    by_contra h
    have := coeffList_eq_cons_leadingCoeff h
    grind [leadingCoeff_eq_zero, sign_eq_zero_iff]
  simp only [decide_not, sign_zero, List.destutter, Bool.false_eq_true, reduceIte, h₁,
    decide_false, Bool.not_false, List.nil_append, List.destutter', decide_true, Bool.not_true]
  obtain rfl : c = leadingCoeff P.eraseLead := by
    have h_eL : eraseLead P ≠ 0 := by simp [← coeffList_eq_nil, h_eL]
    obtain ⟨ls, hls⟩ := coeffList_eq_cons_leadingCoeff h_eL
    grind
  by_cases h₄ : SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
  · grind [SignType.neg_eq_self_iff]
  rw [if_pos h₄, if_pos ?_]
  · grind [Nat.sub_add_cancel, List.length_pos_of_ne_nil, List.destutter'_ne_nil]
  cases _ : SignType.sign P.leadingCoeff
  <;> cases _ : SignType.sign P.eraseLead.leadingCoeff
  <;> grind [= SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one,
      SignType.neg_eq_neg_one, neg_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₂ : 0 < P.nextCoeff
⊢ ((X - C η) * P.eraseLead).signVariations ≤ ((X - C η) * P).signVariations

Tactic:
obtain ⟨c₀, cs, ⟨hcs, hecs⟩⟩ := exists_cons_of_leadingCoeff_pos η h h₂.ne'

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
⊢ ((X - C η) * P.eraseLead).signVariations ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case isTrue.isTrue.cons
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs✝ : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : 1 ≠ SignType.sign c₀
r : SignType
rs : List SignType
hcs : List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs) = r :: rs
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1 (r :: rs)).length ≤
    (1 :: List.destutter' (fun x1 x2 ↦ x1 ≠ x2) (SignType.sign c₀) (r :: rs)).length

Tactic:
· rw [← List.destutter_cons', ← List.destutter_cons']
    grind [List.destutter_cons_cons]

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
u : { u // u * u = a • 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ (z + w).re • 1 + (z + w).im • ↑u = z.re • 1 + z.im • ↑u + (w.re • 1 + w.im • ↑u)

Tactic:
by
        simp only [re_add, im_add, add_smul, ← add_assoc]
        congr 1
        simp only [add_assoc]
        congr 1
        rw [add_comm]

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

Goal state before:
pp: case zero
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
⊢ ↑0 = ↑0

Tactic:
rewrite [inst₁.natCast_zero, inst₂.natCast_zero]

Goal state after:
case zero
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
⊢ 0 = 0
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F (q.j * q.j) = c₃ • 1

Tactic:
q.j_mul_j,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F (c₃ • 1) = c₃ • 1
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)

Tactic:
have : Nontrivial R :=
    have : Nontrivial R[X] := Module.nontrivial R[X] K
    Module.nontrivial R R[X]
  have hgi (i : ι) (hi : i ∈ s) : (algebraMap R[X] K (g i))⁻¹ * algebraMap R[X] K (g i) = 1 :=
    inv_mul_cancel₀ (by simpa using (hg i hi).ne_zero)
  obtain ⟨q, r, hr, hf⟩ := mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse
    f hg hcop (fun _ => 1) hgi
  refine ⟨q, fun i => r i 0, fun i hi => hr i hi 0, ?_⟩
  simp_rw [Fin.sum_univ_one, Fin.val_zero, zero_add, pow_one, Finset.prod_inv_distrib] at hf
  simp_rw [Algebra.cast, div_eq_mul_inv]
  exact hf

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
⊢ IsReduced R

Tactic:
isReduced_iff_pow_one_lt 2 (by lia)

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
⊢ ∀ (x : R), x ^ 2 = 0 → x = 0
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
hc : s₂ = 0
⊢ False

Tactic:
by simp_all

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
⊢ 0 ≤ P

Tactic:
have idem : P * P = 4 * P := CHSH_id T.A₀_inv T.A₁_inv T.B₀_inv T.B₁_inv

Goal state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
⊢ 0 ≤ P
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
⊢ IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a

Tactic:
by
  inhabit G
  refine ⟨IsSMulRegular.skewMonoidAlgebra, fun ha b₁ b₂ inj ↦ ?_⟩
  rw [← (single_injective _).eq_iff, ← smul_single, ← smul_single] at inj
  exact single_injective default (ha inj)

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
zero : p 0
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ ∀ x ∈ f.support, p (SkewMonoidAlgebra.single x (f.coeff x))

Tactic:
by simp_all

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddGroup k
a : G
b : k
⊢ single a (-b) = -single a b

Tactic:
simp [← ofCoeff_single]

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : x ≤ y
⊢ untrop (x + y) = untrop x

Tactic:
by simpa using h

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : y ≤ x
⊢ untrop (x + y) = untrop y

Tactic:
by simpa using h

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ trop (min (untrop x) (untrop y)) = x ↔ x ≤ y

Tactic:
trop_eq_iff_eq_untrop,

Goal state after:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ min (untrop x) (untrop y) = untrop x ↔ x ≤ y
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ trop (min (untrop x) (untrop y)) = y ↔ y ≤ x

Tactic:
trop_eq_iff_eq_untrop,

Goal state after:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ min (untrop x) (untrop y) = untrop y ↔ y ≤ x
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
p : G × G
hps : p ∈ s
hp : p ∉ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
by
        simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : f.coeff p.1 = 0 <;> simp_all

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
p : G × G
hps : p ∈ s
hp : p ∉ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
by
        simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : f.coeff p.1 = 0 <;> simp_all

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ untrop (∑ i ∈ s, f i) = s.inf (untrop ∘ f)

Tactic:
convert! Multiset.untrop_sum (s.val.map f)

Goal state after:
case e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ s.inf (untrop ∘ f) = (Multiset.map untrop (Multiset.map f s.val)).inf
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1.refine_2
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
⊢ (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            U))
        ⟨fU, hU⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩ ∧
    (ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            V))
        ⟨fV, hV⟩ =
      (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop (op W))) x ⋯)) ⟨fun w ↦ fU (iU w), ⋯⟩

Tactic:
exact ⟨colimit_sound iU.op (Subtype.ext rfl), colimit_sound iV.op (Subtype.ext (funext w).symm)⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case inl
X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : ↑Γ(X, U)
hx : x ∈ X.basicOpen f
hn : f ^ 0 ∈ I
⊢ False

Tactic:
exact H f (by simpa using I.mul_mem_left f hn) hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ f ⁻¹ᵁ f ''ᵁ U ≤ U'

Tactic:
← preimage_image_eq f U'

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ f ⁻¹ᵁ f ''ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ U'
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ } ≫ f = Y.ofRestrict ⋯ ≫ g

Tactic:
· exact LocallyRingedSpace.Hom.ext'
        (PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition _ _)

Goal state after:
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' := ⋯ }
x : Y.α
⊢ ↑(ConcreteCategory.hom (⟨↑e_Ring.symm, ⋯⟩ ≫ f)) x = ↑(ConcreteCategory.hom (𝟙 Y)) x

Tactic:
exact e_Ring.right_inv x

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case h.h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : (toBasicOpenₗ R M f) (LocalizedModule.mk a b) = (toBasicOpenₗ R M f) (LocalizedModule.mk c d)
⊢ LocalizedModule.mk a b = LocalizedModule.mk c d

Tactic:
suffices f ∈ ((⊥ : Submodule R M).colon {d • a - b • c}).radical by
    rw [LocalizedModule.mk_eq]
    obtain ⟨n, hn⟩ := this
    exact ⟨⟨f ^ n, n, rfl⟩, by simpa [sub_eq_zero, smul_sub] using! Submodule.mem_colon.mp hn _ rfl⟩

Goal state after:
case h.h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : (toBasicOpenₗ R M f) (LocalizedModule.mk a b) = (toBasicOpenₗ R M f) (LocalizedModule.mk c d)
⊢ f ∈ (⊥.colon {d • a - b • c}).radical
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ ∀ {X_1 Y : X.Opensᵒᵖ} (f : X_1 ⟶ Y),
    (X.restrictFunctor.op ⋙ (Over.forget X).op ⋙ Γ).map f ≫ (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom =
      (Functor.mapIso X.presheaf (eqToIso ⋯).symm.op).hom ≫ X.presheaf.map f

Tactic:
by
      intro U V i
      dsimp
      rw [X.homOfLE_appTop, ← Functor.map_comp, ← Functor.map_comp]
      congr 1

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
rw [← cancel_mono U.ι, morphismRestrict_ι, Category.comp_id, Category.id_comp]

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

Goal state before:
pp: X : LocallyRingedSpace
⊢ Continuous X.toΓSpecFun

Tactic:
by
  rw [isTopologicalBasis_basic_opens.continuous_iff]
  rintro _ ⟨r, rfl⟩
  rw [X.toΓSpec_preimage_basicOpen_eq r]
  exact (X.toRingedSpace.basicOpen r).2

Goal state after: