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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

Tactic:
by
  by_cases hdp : P.natDegree = 0
  · rw [eq_C_of_natDegree_eq_zero hdp] at h ⊢
    simp [coeffList_C (C_ne_zero.mp h)]
  by_cases hep : P.eraseLead = 0
  · have h₂ : .monomial P.natDegree P.leadingCoeff = P := by
      simpa [hep] using P.eraseLead_add_monomial_natDegree_leadingCoeff
    nth_rewrite 1 [← h₂]
    simp [coeffList_monomial (Polynomial.leadingCoeff_ne_zero.mpr h), hep]
  have h₁ := withBotSucc_degree_eq_natDegree_add_one h
  have h₂ := withBotSucc_degree_eq_natDegree_add_one hep
  obtain ⟨n, hn, hn2⟩ : ∃ d, P.natDegree = P.eraseLead.natDegree + 1 + d ∧
      d = P.natDegree - P.eraseLead.degree.succ := by
    use P.natDegree - P.eraseLead.natDegree - 1
    have := eraseLead_natDegree_le P
    lia
  rw [← hn2]; clear hn2
  apply List.ext_getElem?
  rintro (_ | k)
  · obtain ⟨w, h⟩ := (coeffList_eq_cons_leadingCoeff h)
    simp_all
  simp only [coeffList, List.map_reverse]
  by_cases! hkd : P.natDegree + 1 ≤ k + 1
  · rw [List.getElem?_eq_none]
      <;> simp <;> lia
  obtain ⟨dk, hdk⟩ := exists_add_of_le (Nat.le_of_lt_succ hkd)
  rw [List.getElem?_reverse (by simpa [withBotSucc_degree_eq_natDegree_add_one h] using hkd),
    List.getElem?_cons_succ, List.length_map, List.length_range, List.getElem?_map,
    List.getElem?_range (by lia), Option.map_some]
  conv_lhs => arg 1; equals P.eraseLead.coeff dk =>
    rw [eraseLead_coeff_of_ne (f := P) dk (by lia)]
    congr
    lia
  by_cases! hkn : k < n
  · simpa [List.getElem?_append, hkn] using coeff_eq_zero_of_natDegree_lt (by lia)
  · rw [List.getElem?_append_right (List.length_replicate ▸ hkn),
      List.length_replicate, List.getElem?_reverse, List.getElem?_map]
    · rw [List.length_map, List.length_range,
        List.getElem?_range (by lia), Option.map_some]
      congr 2
      lia
    · simp
      lia

Goal state after:
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 q : Fq[X]
⊢ (if p * q = 0 then 0 else ↑(Fintype.card Fq) ^ (p * q).natDegree) =
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) * if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
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 q : Fq[X]
hp : p = 0
⊢ (if p * q = 0 then 0 else ↑(Fintype.card Fq) ^ (p * q).natDegree) =
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) * if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree

case neg
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 q : Fq[X]
hp : ¬p = 0
⊢ (if p * q = 0 then 0 else ↑(Fintype.card Fq) ^ (p * q).natDegree) =
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) * if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree
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 q : Fq[X]
⊢ (if p + q = 0 then 0 else ↑(Fintype.card Fq) ^ (p + q).natDegree) ≤
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) + if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
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 q : Fq[X]
hp : p = 0
⊢ (if p + q = 0 then 0 else ↑(Fintype.card Fq) ^ (p + q).natDegree) ≤
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) + if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree

case neg
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 q : Fq[X]
hp : ¬p = 0
⊢ (if p + q = 0 then 0 else ↑(Fintype.card Fq) ^ (p + q).natDegree) ≤
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) + if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.mirror.natDegree = p.natDegree

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ p.mirror.natDegree = p.natDegree

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.mirror.natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Mirror

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

Tactic:
rw [← tsub_add_eq_add_tsub h2, ← tsub_tsub_assoc h2 h3, mirror, coeff_mul_X_pow', if_pos h3,
      coeff_reverse, revAt_le (tsub_le_self.trans h2)]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * q).mirror = p.mirror * q.mirror

case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * q).mirror = p.mirror * q.mirror
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * q.reverse * (X ^ p.natTrailingDegree * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Tactic:
rw [mul_assoc, ← mul_assoc q.reverse, ← X_pow_mul (p := reverse q)]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * q.reverse * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)
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
n : ℕ
⊢ (X * (X ^ n * p)).smeval x = x ^ (1 + n) * p.smeval x

Tactic:
smeval_X_mul,

Goal state after:
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
n : ℕ
⊢ x * (X ^ n * p).smeval x = x ^ (1 + n) * p.smeval x
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ AddGroup (QuadraticAlgebra R a b)

Tactic:
refine (equivProd a b).injective.addGroup _ rfl ?_ ?_ ?_ ?_ ?_ <;> intros

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ + y✝) = (equivProd a b) x✝ + (equivProd a b) y✝

case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (-x✝) = -(equivProd a b) x✝

case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ - y✝) = (equivProd a b) x✝ - (equivProd a b) y✝

case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ : QuadraticAlgebra R a b
n✝ : ℕ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝

case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ : QuadraticAlgebra R a b
n✝ : ℤ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommGroupWithOne R
n : ℕ
⊢ QuadraticAlgebra.C ↑↑n = ↑n

Tactic:
norm_cast

Goal state after:
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:
← List.destutter_cons',

Goal state after:
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
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommGroupWithOne R
n : ℕ
⊢ -QuadraticAlgebra.C ↑(↑n + 1) = -↑(n + 1)

Tactic:
norm_cast

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:
symm
        calc
          (z.re • (1 : A) + z.im • ↑u) * (w.re • 1 + w.im • ↑u) =
            (z.re * w.re) • (1 : A) + (z.re * w.im) • u +
              (z.im * w.re) • u + (z.im * w.im) • (u * u) := by
              simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]
              apply add_add_add_comm'
          _ = (z.re * w.re) • (1 : A) + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (u * u) := by
              congr 1
              simp only [add_assoc]
              rw [← add_smul]
          _ = (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (a • 1 + b • u) := by
              simp [u.prop]
          _ = (z.re * w.re + a * z.im * w.im) • 1 +
                (z.re * w.im + z.im * w.re + b * z.im * w.im) • u := by
              simp only [smul_add]
              module
            _ = (z * w).re • 1 + (z * w).im • u := by
              simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
i : Fin 2
⊢ ((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) i =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec (⇑((basis a b).repr w)) i

Tactic:
fin_cases i
    <;> simp

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ z.re * w.re + a * z.im * w.im = w.re * z.re + w.im * (a * z.im)

case «1»
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ z.re * w.im + z.im * w.re + b * z.im * w.im = w.re * z.im + w.im * (z.re + b * z.im)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case neg
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
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
have : signVariations ((X - C η) * P).eraseLead + 1 =
          signVariations ((X - C η) * P) := by
        simp [-leadingCoeff_mul, ← sign_ne_zero,
          signVariations_eq_eraseLead_add_ite h_mul, leadingCoeff_eraseLead_eq_nextCoeff,
          hs_nC_mul, h_mul_lC]

Goal state after:
case neg
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
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
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) (r i j.rev * g i ^ ↑j.rev) * ∏ x ∈ s.erase i, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x) =
    (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
Finset.prod_congr rfl fun x hx => hc x (Finset.mem_of_mem_erase hx),

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) (r i j.rev * g i ^ ↑j.rev) * ∏ x ∈ s.erase i, 1) =
    (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonUnitalNonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
rcases inst₁ with @⟨_, ⟨⟩⟩

Goal state after:
R : Type u
inst₂ : NonUnitalNonAssocSemiring R
toAddCommMonoid✝ : AddCommMonoid R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ { toAddCommMonoid := toAddCommMonoid✝, mul := mul✝, left_distrib := left_distrib✝, right_distrib := right_distrib✝,
      zero_mul := zero_mul✝, mul_zero := mul_zero✝ } =
    inst₂
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case a.refine_1
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ (algebraMap R A) y.re ∈ R[B.i, B.j, B.k]

pp: case a.refine_2
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ y.imI • B.i ∈ R[B.i, B.j, B.k]

pp: case a.refine_3
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ y.imJ • B.j ∈ R[B.i, B.j, B.k]

pp: case a.refine_4
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ y.imK • B.k ∈ R[B.i, B.j, B.k]

Tactic:
· exact algebraMap_mem _ _

Goal state after:
case a.refine_2
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ y.imI • B.i ∈ R[B.i, B.j, B.k]

case a.refine_3
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ y.imJ • B.j ∈ R[B.i, B.j, B.k]

case a.refine_4
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ y.imK • B.k ∈ R[B.i, B.j, B.k]
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonUnitalNonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
rcases inst₁ with @⟨_, ⟨⟩⟩

Goal state after:
R : Type u
inst₂ : NonUnitalNonAssocRing R
toAddCommGroup✝ : AddCommGroup R
mul✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ { toAddCommGroup := toAddCommGroup✝, mul := mul✝, left_distrib := left_distrib✝, right_distrib := right_distrib✝,
      zero_mul := zero_mul✝, mul_zero := mul_zero✝ } =
    inst₂
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
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime✝ : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf : ↑q₁ + ↑r₁₁ / ↑g₁ + ↑r₂₁ / ↑g₂ = ↑q₂ + ↑r₁₂ / ↑g₁ + ↑r₂₂ / ↑g₂
g : Bool → R[X] := fun t ↦ Bool.rec g₂ g₁ t
r₁ : Bool → R[X] := fun t ↦ Bool.rec r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun t ↦ Bool.rec r₂₂ r₁₂ t
hg : ∀ i ∈ Finset.univ, (g i).Monic
hcoprime : (↑Finset.univ).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : ∀ i ∈ Finset.univ, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ Finset.univ, (r₂ i).degree < (g i).degree
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂

Tactic:
refine (quo_add_sum_rem_div_unique K hg hcoprime hr₁ hr₂ ?_).imp_right fun h =>
    ⟨h true (Finset.mem_univ true), h false (Finset.mem_univ false)⟩

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime✝ : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf : ↑q₁ + ↑r₁₁ / ↑g₁ + ↑r₂₁ / ↑g₂ = ↑q₂ + ↑r₁₂ / ↑g₁ + ↑r₂₂ / ↑g₂
g : Bool → R[X] := fun t ↦ Bool.rec g₂ g₁ t
r₁ : Bool → R[X] := fun t ↦ Bool.rec r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun t ↦ Bool.rec r₂₂ r₁₂ t
hg : ∀ i ∈ Finset.univ, (g i).Monic
hcoprime : (↑Finset.univ).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : ∀ i ∈ Finset.univ, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ Finset.univ, (r₂ i).degree < (g i).degree
⊢ ↑q₁ + ∑ i, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i, ↑(r₂ i) / ↑(g i)
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel
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
a b x✝ y✝ : R
hab : Rel r x✝ y✝
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x✝ * c) (y✝ * d)

Tactic:
refine (Relation.EqvGen.rel _ _ hab.mul_left).trans _ _ _ ?_
      induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
⊢ ∀ (c : SkewMonoidAlgebra k G) {x : V}, x ∈ ↑W → c • x ∈ ↑W

Tactic:
intro f v hv
    rw [← sum_single f, sum_def, Finsupp.sum, Finset.sum_smul]
    simp_rw [← smul_of, smul_assoc]
    exact Submodule.sum_smul_mem W _ fun g _ ↦ h g v hv

Goal state after: