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

Goal state before:
pp: 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 : ℕ
⊢ (p.divModByMonicAux hq).1.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (p.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
rw [divModByMonicAux]
    have H₀ (i) : p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) := by
      refine SetLike.le_def.mp ?_ <| subset_span <| mem_range_self i
      calc
        span R coeffs(p)
        _ = 1 ^ deg(p) * span R coeffs(p) := by simp
        _ ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) := by gcongr; exacts [le_sup_left, le_sup_right]
    split_ifs with hpq; swap
    · simpa using H₀ _
    simp only [coeff_add, coeff_C_mul, coeff_X_pow]
    generalize hr : (p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q)))) = r
    by_cases hr' : r = 0
    · simp only [mul_ite, mul_one, mul_zero, hr', divModByMonicAux, degree_zero, le_bot_iff,
        degree_eq_bot, ne_eq, not_true_eq_false, and_false, ↓reduceDIte, coeff_zero, add_zero,
        Submodule.zero_mem, and_true]
      split_ifs
      exacts [H₀ _, zero_mem _]
    have H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p) := by
      rw [span_le, ← hr]
      rintro _ ⟨i, rfl⟩
      rw [coeff_sub, ← mul_assoc, coeff_mul_X_pow', coeff_mul_C]
      apply sub_mem
      · exact SetLike.le_def.mp le_sup_left (subset_span (mem_range_self _))
      · split_ifs
        · refine SetLike.le_def.mp le_sup_right (mul_mem_mul ?_ ?_) <;> exact subset_span ⟨_, rfl⟩
        · exact zero_mem _
    have deg_r_lt_deg_p : deg(r) < deg(p) := natDegree_lt_natDegree hr' (hr ▸ div_wf_lemma hpq hq)
    have H'' := calc
      spanCoeffs(q) ^ deg(r) * spanCoeffs(r)
      _ ≤ spanCoeffs(q) ^ deg(r) *
          (1 ⊔ (span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p))) := by gcongr
      _ ≤ spanCoeffs(q) ^ deg(r) * (spanCoeffs(q) * spanCoeffs(p)) := by
        gcongr
        simp only [sup_le_iff]
        refine ⟨one_le_mul le_sup_left le_sup_left, ?_, mul_le_mul' le_sup_right le_sup_right⟩
        rw [Submodule.sup_mul, one_mul]
        exact le_sup_of_le_left le_sup_right
      _ = spanCoeffs(q) ^ (deg(r) + 1) * spanCoeffs(p) := by rw [pow_succ, mul_assoc]
      _ ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) := by gcongr; exacts [le_sup_left, deg_r_lt_deg_p]
    refine ⟨add_mem ?_ ?_, ?_⟩
    · split_ifs <;> simp only [mul_one, mul_zero]
      exacts [H₀ _, zero_mem _]
    · exact H'' (coeff_divModByMonicAux_mem_span_pow_mul_span r _ hq i).1
    · exact H'' (coeff_divModByMonicAux_mem_span_pow_mul_span _ _ hq i).2

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

Goal state before:
pp: case isUnit_or_isUnit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g : R[X]
⊢ ∀ ⦃b : R[X]⦄, f = g * b → IsUnit g ∨ IsUnit b

Tactic:
h

Goal state after:
case isUnit_or_isUnit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
⊢ f = g * h → IsUnit g ∨ IsUnit h
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hb : ∀ {a : α}, IsChain R (a :: l) → destutter' R a l = a :: l
a : α
h : IsChain R (a :: b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l

Tactic:
obtain ⟨h, hc⟩ := isChain_cons_cons.mp h

Goal state after:
case cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hb : ∀ {a : α}, IsChain R (a :: l) → destutter' R a l = a :: l
a : α
h✝ : IsChain R (a :: b :: l)
h : R a b
hc : IsChain R (b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ p.coeff k * (((fun₀ | 0 => k).prod fun n e ↦ x n ^ e) * (fun₀ | 1 => n - k).prod fun n e ↦ x n ^ e) =
    p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n

pp: case h_zero
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2), x a ^ 0 = 1

pp: case h_add
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2) (b₁ b₂ : ℕ), x a ^ (b₁ + b₂) = x a ^ b₁ * x a ^ b₂

pp: case h
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ (fun₀ | 0 => k) 1 = 0

Tactic:
Finsupp.prod_single_index,

Goal state after:
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ p.coeff k * (x 0 ^ k * (fun₀ | 1 => n - k).prod fun n e ↦ x n ^ e) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n

K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ x 0 ^ 0 = 1

case h_zero
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2), x a ^ 0 = 1

case h_add
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2) (b₁ b₂ : ℕ), x a ^ (b₁ + b₂) = x a ^ b₁ * x a ^ b₂

case h
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ (fun₀ | 0 => k) 1 = 0
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ p.coeff k * (x 0 ^ k * (fun₀ | 1 => n - k).prod fun n e ↦ x n ^ e) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n

pp: K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ x 0 ^ 0 = 1

pp: case h_zero
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2), x a ^ 0 = 1

pp: case h_add
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2) (b₁ b₂ : ℕ), x a ^ (b₁ + b₂) = x a ^ b₁ * x a ^ b₂

pp: case h
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ (fun₀ | 0 => k) 1 = 0

Tactic:
Finsupp.prod_single_index,

Goal state after:
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ p.coeff k * (x 0 ^ k * x 1 ^ (n - k)) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n

K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ x 1 ^ 0 = 1

K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ x 0 ^ 0 = 1

case h_zero
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2), x a ^ 0 = 1

case h_add
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2) (b₁ b₂ : ℕ), x a ^ (b₁ + b₂) = x a ^ b₁ * x a ^ b₂

case h
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ (fun₀ | 0 => k) 1 = 0
Module: Mathlib.Algebra.Polynomial.PartialFractions

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

Tactic:
induction n generalizing q₁ q₂ with

Goal state after:
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.comp q).smeval x = p.smeval (q.smeval x)

Tactic:
induction p using Polynomial.induction_on' with
  | add r s hr hs => simp [add_comp, hr, hs, smeval_add]
  | monomial n a => simp [smeval_monomial, smeval_C_mul, smeval_pow]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
⊢ P.eraseLead.signVariations = P.signVariations

Tactic:
by
  by_cases hpz : P = 0
  · simp_all
  · have h₂ : nextCoeff P ≠ 0 := by intro; simp_all
    obtain ⟨_, hl⟩ := coeffList_eq_cons_leadingCoeff (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₂)
    simp [signVariations, List.destutter, leadingCoeff_eraseLead_eq_nextCoeff h₂, hl, h, h₂,
      coeffList_eraseLead hpz]

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

Goal state before:
pp: p q : ℤ[X]
h : p * p.mirror = q * q.mirror
⊢ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3 ↔
    (q * q.mirror).coeff (((q * q.mirror).natDegree + (q * q.mirror).natTrailingDegree) / 2) = 3

Tactic:
h

Goal state after:
p q : ℤ[X]
h : p * p.mirror = q * q.mirror
⊢ (q * q.mirror).coeff (((q * q.mirror).natDegree + (q * q.mirror).natTrailingDegree) / 2) = 3 ↔
    (q * q.mirror).coeff (((q * q.mirror).natDegree + (q * q.mirror).natTrailingDegree) / 2) = 3
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

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

Tactic:
rcases hadd with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)

Goal state after:
case inl
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q * q.mirror
hq : q = trinomial k m' n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑w * ↑u
⊢ q = p ∨ q = p.mirror

case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q * q.mirror
hq : q = trinomial k m' n ↑w ↑v ↑u
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
⊢ ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0

Tactic:
z

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
⊢ z * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → z = 0
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y' → y = y'

pp: case mpr
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ y = y' → x ◃⁻¹ y = x ◃⁻¹ y'

Tactic:
· apply (act' x).symm.injective

Goal state after:
case mpr
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ y = y' → x ◃⁻¹ y = x ◃⁻¹ y'
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : Rᵐᵒᵖ
⊢ ∀ {z : Rᵐᵒᵖ},
    op (unop x ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) = op (unop (op (unop x ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop x ◃⁻¹ unop z)))

Tactic:
z

Goal state after:
R : Type u_1
inst✝ : Rack R
x y z : Rᵐᵒᵖ
⊢ op (unop x ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) = op (unop (op (unop x ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop x ◃⁻¹ unop z)))
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ ∀ {z : Conj G}, (MulAut.conj x) ((MulAut.conj y) z) = (MulAut.conj ((MulAut.conj x) y)) ((MulAut.conj x) z)

Tactic:
z

Goal state after:
Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y z : Conj G
⊢ (MulAut.conj x) ((MulAut.conj y) z) = (MulAut.conj ((MulAut.conj x) y)) ((MulAut.conj x) z)
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x y : Dihedral n
⊢ ∀ {z : Dihedral n}, dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)

Tactic:
z

Goal state after:
Q : Type u_1
inst✝ : Quandle Q
n : ℕ
x y z : Dihedral n
⊢ dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ n i * (algebraMap R[X] K) (g i) ^ ↑j.rev = gi i ^ (↑j + 1) * (gi i * (algebraMap R[X] K) (g i)) ^ ↑j.rev

Tactic:
mul_pow,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ n i * (algebraMap R[X] K) (g i) ^ ↑j.rev =
    gi i ^ (↑j + 1) * (gi i ^ ↑j.rev * (algebraMap R[X] K) (g i) ^ ↑j.rev)
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
⊢ a₁✝.toDistrib = a₂✝.toDistrib → a₁✝ = a₂✝

Tactic:
h

Goal state after:
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : a₁✝.toDistrib = a₂✝.toDistrib
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ (↑j.rev + 1) * (gi i * (algebraMap R[X] K) (g i)) ^ ↑j * (algebraMap R[X] K) (g i) ^ n i =
    (algebraMap R[X] K) (g i) ^ ↑j

Tactic:
mul_pow,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ (↑j.rev + 1) * (gi i ^ ↑j * (algebraMap R[X] K) (g i) ^ ↑j) * (algebraMap R[X] K) (g i) ^ n i =
    (algebraMap R[X] K) (g i) ^ ↑j
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
⊢ a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring → a₁✝ = a₂✝

Tactic:
h

Goal state after:
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
h : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonUnitalRing R
⊢ a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring → a₁✝ = a₂✝

Tactic:
h

Goal state after:
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonAssocRing R
⊢ a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring → a₁✝ = a₂✝

Tactic:
h

Goal state after:
R : Type u
a₁✝ a₂✝ : NonAssocRing R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₁ : IsSumNonzeroSq s₁
h₂ : IsSumNonzeroSq s₂
⊢ IsSumNonzeroSq (s₁ + s₂)

Tactic:
induction h₁

Goal state after:
case sq
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₂ : IsSumNonzeroSq s₂
a✝ : R
ha✝ : a✝ ≠ 0
⊢ IsSumNonzeroSq (a✝ * a✝ + s₂)

case sq_add
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₂ : IsSumNonzeroSq s₂
a✝ s✝ : R
ha✝ : a✝ ≠ 0
hs✝ : IsSumNonzeroSq s✝
hs_ih✝ : IsSumNonzeroSq (s✝ + s₂)
⊢ IsSumNonzeroSq (a✝ * a✝ + s✝ + s₂)
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s : R
hs : s ≠ 0
h : IsSumSq s
⊢ IsSumNonzeroSq s

Tactic:
induction h with

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

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : Semiring R
⊢ a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring → a₁✝ = a₂✝

Tactic:
h

Goal state after:
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : Semiring R
⊢ a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring → a₁✝ = a₂✝

Tactic:
h

Goal state after:
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.IsFormallyReal

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

Tactic:
exact not_isSumNonzeroSq_zero (h ▸ IsSumNonzeroSq.add hs₁ hs₂)

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

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : Ring R
⊢ toNonUnitalRing = toNonUnitalRing → a₁✝ = a₂✝

Tactic:
h

Goal state after:
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : Ring R
⊢ toNonAssocRing = toNonAssocRing → a₁✝ = a₂✝

Tactic:
h

Goal state after:
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : Ring R
⊢ a₁✝.toSemiring = a₂✝.toSemiring → a₁✝ = a₂✝

Tactic:
h

Goal state after:
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
x : G
lx : IsLeftRegular x
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
y : G
yf : y ∈ f.support
hy : x * y ∈ image (fun x_1 ↦ x * x_1) f.support
⊢ x * y ∈ (single x r * f).support

Tactic:
simp [coeff_mul, mem_support_iff.mp yf, hrx, mem_support_iff, sum_single_index, Ne,
    zero_mul, ite_self, sum_zero, lx.eq_iff]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mp.rel
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
h : Rel r x✝ y✝
⊢ RingConGen.Rel r x✝ y✝

Tactic:
induction h with

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mp
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
h : Relation.EqvGen (Rel r) x₁ x₂
⊢ RingConGen.Rel r x₁ x₂

Tactic:
induction h with

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mpr
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
h : RingConGen.Rel r x₁ x₂
⊢ Relation.EqvGen (Rel r) x₁ x₂

Tactic:
induction h with

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
⊢ { toQuot := Quot.mk (Rel r) ((algebraMap S R) 0) } = 0

Tactic:
simp [← 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 → R → Prop
⊢ { toQuot := Quot.mk (Rel r) 0 } = 0

Tactic:
simp [← 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✝² : 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 y : RingQuot s), Quot.lift ⇑f ⋯ (x + y).toQuot = Quot.lift ⇑f ⋯ x.toQuot + Quot.lift ⇑f ⋯ y.toQuot

Tactic:
by
    rintro ⟨⟨x⟩⟩ ⟨⟨y⟩⟩
    simp only [add_quot, map_add _ x y]

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

Goal state before:
pp: R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
S T : StarSubsemiring R
h : S.toSubsemiring = T.toSubsemiring
x : R
⊢ x ∈ S.toSubsemiring ↔ x ∈ T.toSubsemiring

Tactic:
h

Goal state after:
R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
S T : StarSubsemiring R
h : S.toSubsemiring = T.toSubsemiring
x : R
⊢ x ∈ T.toSubsemiring ↔ x ∈ T.toSubsemiring
Module: Mathlib.Algebra.Star.RingQuot

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b : R
h : Rel r a b
⊢ Rel r (Star.star a) (Star.star b)

Tactic:
induction h with

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
⊢ (a.sum fun a b_1 ↦ b.sum fun a_1 b ↦ ↑f (b_1 * a • b) * g (a * a_1)) =
    a.sum fun a c ↦ b.sum fun a_1 c_1 ↦ ↑f c * g a * (↑f c_1 * g a_1)

Tactic:
refine sum_congr fun y hy ↦ sum_congr fun x _hx ↦ ?_

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ ↑f (a.coeff y * y • b.coeff x) * g (y * x) = ↑f (a.coeff y) * g y * (↑f (b.coeff x) * g x)