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

Goal state before:
pp: 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
p q : Fq[X]
hp : p = 0
hq : ¬q = 0
⊢ 0 < ↑(Fintype.card Fq) ^ q.natDegree ↔ p.degree < q.degree

pp: 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
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ ↑(Fintype.card Fq) ^ p.natDegree < 0 ↔ p.degree < q.degree

pp: 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
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(Fintype.card Fq) ^ p.natDegree < ↑(Fintype.card Fq) ^ q.natDegree ↔ p.degree < q.degree

Tactic:
· simp only [hp, hq, degree_zero, Ne, bot_lt_iff_ne_bot, degree_eq_bot, pow_pos,
          not_false_iff]

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
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ ↑(Fintype.card Fq) ^ p.natDegree < 0 ↔ p.degree < q.degree

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
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(Fintype.card Fq) ^ p.natDegree < ↑(Fintype.card Fq) ^ q.natDegree ↔ p.degree < q.degree
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case neg
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
⊢ 1 ^ deg(p) * p.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
exact Submodule.mul_mem_mul (Submodule.pow_mem_pow Mq hq' _) (hp i)

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ ↑1 ≤ ↑|ev|

Tactic:
Int.cast_le

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ |ev|
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (a : ℕ) → a ∈ Finset.range (p.natDegree + 1) → p.mirror.coeff a ≠ 0 → ℕ

pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ (a : ℕ) (h₁ : a ∈ Finset.range (p.natDegree + 1)) (h₂ : p.mirror.coeff a ≠ 0),
    ?refine_1 a h₁ h₂ ∈ Finset.range (p.natDegree + 1)

pp: case refine_3
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ (a₁ : ℕ) (h₁₁ : a₁ ∈ Finset.range (p.natDegree + 1)) (h₁₂ : p.mirror.coeff a₁ ≠ 0) (a₂ : ℕ)
    (h₂₁ : a₂ ∈ Finset.range (p.natDegree + 1)) (h₂₂ : p.mirror.coeff a₂ ≠ 0),
    ?refine_1 a₁ h₁₁ h₁₂ = ?refine_1 a₂ h₂₁ h₂₂ → a₁ = a₂

pp: case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 → ∃ a, ∃ (h₁ : a ∈ Finset.range (p.natDegree + 1)) (h₂ : p.mirror.coeff a ≠ 0), ?refine_1 a h₁ h₂ = b

pp: case refine_5
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ (a : ℕ) (h₁ : a ∈ Finset.range (p.natDegree + 1)) (h₂ : p.mirror.coeff a ≠ 0),
    p.mirror.coeff a = p.coeff (?refine_1 a h₁ h₂)

Tactic:
· exact fun n _ _ => revAt (p.natDegree + p.natTrailingDegree) n

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → (revAt (p.natDegree + p.natTrailingDegree)) a ∈ Finset.range (p.natDegree + 1)

case refine_3
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a₁ ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a₁ ≠ 0 →
      ∀ a₂ ∈ Finset.range (p.natDegree + 1),
        p.mirror.coeff a₂ ≠ 0 →
          (revAt (p.natDegree + p.natTrailingDegree)) a₁ = (revAt (p.natDegree + p.natTrailingDegree)) a₂ → a₁ = a₂

case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 →
      ∃ a,
        ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
          (revAt (p.natDegree + p.natTrailingDegree)) a = b

case refine_5
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) a)
Module: Mathlib.Algebra.Polynomial.Mirror

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

Tactic:
by
  rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror,
    revAt_le (Nat.le_add_left _ _), add_tsub_cancel_right]

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

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (p.toTupleMvPolynomial ((fun i ↦ i) ⟨0, ⋯⟩)).IsHomogeneous p.natDegree

pp: case «1»
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (p.toTupleMvPolynomial ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous p.natDegree

Tactic:
· simp [toTupleMvPolynomial]

Goal state after:
case «1»
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (p.toTupleMvPolynomial ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous p.natDegree
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: 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
hqr : r₁ + g * q₁ = r₂ + g * q₂
hrs : rs₁ = rs₂
⊢ r₁.degree < g.degree

Tactic:
by simpa using hr₁ (Fin.last n)

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
⊢ Irreducible p

Tactic:
rw [Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three hdeg2 hdeg.2]

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
⊢ p.roots = 0
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

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

Tactic:
have hsl : SignType.sign (leadingCoeff P) ≠ 0 := by simp_all

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
⊢ P.signVariations =
    P.eraseLead.signVariations + if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0
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]
⊢ (-P).signVariations = P.signVariations

Tactic:
by
  rw [signVariations, signVariations, coeffList_neg]
  simp only [List.map_map, List.filter_map]
  have hsc : SignType.sign ∘ (fun (x : R) => -x) = (fun x => -x) ∘ SignType.sign := by
    grind [Left.sign_neg]
  have h_neg_destutter (l : List SignType) :
      (l.destutter (¬· = ·)).map (- ·) = (l.map (- ·)).destutter (¬· = ·) := by
    grind [List.map_destutter, neg_inj]
  rw [hsc, List.comp_map, ← h_neg_destutter, List.length_map]
  congr 5
  funext
  simp [SignType.sign]

Goal state after:
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 : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] :=
  fun p ↦
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff) }
h : C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) = f (q * q.mirror)
⊢ q = p ∨ q = p.mirror

Tactic:
replace h := h.trans (irreducible_aux1 hkm' hmn' u v w hq).symm

Goal state after:
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
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] :=
  fun p ↦
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff) }
h :
  C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) = C ↑v * (C ↑u * X ^ (m' + n) + C ↑w * X ^ (n - m' + k + n))
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
⊢ range q = range (q - 1 + 1)

Tactic:
rw [tsub_add_cancel_of_le (Nat.one_le_of_lt hq)]

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✝ : ((X - C η) * P).eraseLead.eraseLead = ((X - C η) * P.eraseLead).eraseLead
this : ((X - C η) * P).leadingCoeff :: ((X - C η) * P).eraseLead.coeffList = ((X - C η) * P).coeffList
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)

Tactic:
have := coeffList_eraseLead (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₉)

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₃ : 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✝¹ : ((X - C η) * P).eraseLead.eraseLead = ((X - C η) * P.eraseLead).eraseLead
this✝ : ((X - C η) * P).leadingCoeff :: ((X - C η) * P).eraseLead.coeffList = ((X - C η) * P).coeffList
this :
  ((X - C η) * P).eraseLead.coeffList =
    ((X - C η) * P).eraseLead.leadingCoeff ::
      (List.replicate (((X - C η) * P).eraseLead.natDegree - ((X - C η) * P).eraseLead.eraseLead.degree.succ) 0 ++
        ((X - C η) * P).eraseLead.eraseLead.coeffList)
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
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:
Int.cast_neg,

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ (c₂ • c₃) • 1 - q.k * q.j = (c₂ * c₃) • 1 - c₃ • q.i

Tactic:
k_mul_j

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ (c₂ • c₃) • 1 - c₃ • q.i = (c₂ * c₃) • 1 - c₃ • q.i
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]
              exact congrArg (@Zero.zero R) h_zero'

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

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocSemiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : inst₁.toMulZeroOneClass.toOne = inst₂.toMulZeroOneClass.toOne
h_one : One.one = One.one
this✝ : inst₁.toAddCommMonoidWithOne = inst₂.toAddCommMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
⊢ inst₁ = inst₂

Tactic:
cases inst₁

Goal state after:
case mk
R : Type u
inst₂ : NonAssocSemiring R
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
        mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toNonUnitalNonAssocSemiring =
    inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
          mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
          natCast_succ := natCast_succ✝ }.toMulZeroOneClass.toOne =
    inst₂.toMulZeroOneClass.toOne
h_one : One.one = One.one
this✝ :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
        mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toAddCommMonoidWithOne =
    inst₂.toAddCommMonoidWithOne
this :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
        mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toNatCast =
    inst₂.toNatCast
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
      mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ } =
    inst₂
Module: Mathlib.Algebra.Ring.Ext

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

Tactic:
cases inst₁

Goal state after:
case mk
R : Type u
inst₂ : NonUnitalRing R
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
this :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_assoc := mul_assoc✝ }.toNonUnitalNonAssocRing =
    inst₂.toNonUnitalNonAssocRing
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_assoc := mul_assoc✝ } = inst₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing
h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring
h₃ : inst₁.toAddCommGroupWithOne = inst₂.toAddCommGroupWithOne
⊢ inst₁ = inst₂

Tactic:
cases inst₁

Goal state after:
case mk
R : Type u
inst₂ : NonAssocRing R
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
toIntCast✝ : IntCast R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonUnitalNonAssocRing =
    inst₂.toNonUnitalNonAssocRing
h₂ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonAssocSemiring =
    inst₂.toNonAssocSemiring
h₃ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroupWithOne =
    inst₂.toAddCommGroupWithOne
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
      toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
      intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ } =
    inst₂
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid
h₁ : inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring
h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring
h₃ : inst₁.toMonoidWithZero.toMonoid = inst₂.toMonoidWithZero.toMonoid
⊢ inst₁ = inst₂

Tactic:
cases inst₁

Goal state after:
case mk
R : Type u
inst₂ : Semiring R
toAddCommMonoid✝ : AddCommMonoid R
toMonoid✝ : Monoid R
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
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
toNatCast✝ : NatCast R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₀ :
  { toAddCommMonoid := toAddCommMonoid✝, toMonoid := toMonoid✝, zero_mul := zero_mul✝, mul_zero := mul_zero✝,
        left_distrib := left_distrib✝, right_distrib := right_distrib✝, toNatCast := toNatCast✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ }.toAddCommMonoid =
    inst₂.toAddCommMonoid
h₁ :
  { toAddCommMonoid := toAddCommMonoid✝, toMonoid := toMonoid✝, zero_mul := zero_mul✝, mul_zero := mul_zero✝,
        left_distrib := left_distrib✝, right_distrib := right_distrib✝, toNatCast := toNatCast✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ }.toNonUnitalSemiring =
    inst₂.toNonUnitalSemiring
h₂ :
  { toAddCommMonoid := toAddCommMonoid✝, toMonoid := toMonoid✝, zero_mul := zero_mul✝, mul_zero := mul_zero✝,
        left_distrib := left_distrib✝, right_distrib := right_distrib✝, toNatCast := toNatCast✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ }.toNonAssocSemiring =
    inst₂.toNonAssocSemiring
h₃ :
  { toAddCommMonoid := toAddCommMonoid✝, toMonoid := toMonoid✝, zero_mul := zero_mul✝, mul_zero := mul_zero✝,
          left_distrib := left_distrib✝, right_distrib := right_distrib✝, toNatCast := toNatCast✝,
          natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ }.toMonoidWithZero.toMonoid =
    inst₂.toMonoidWithZero.toMonoid
⊢ { toAddCommMonoid := toAddCommMonoid✝, toMonoid := toMonoid✝, zero_mul := zero_mul✝, mul_zero := mul_zero✝,
      left_distrib := left_distrib✝, right_distrib := right_distrib✝, toNatCast := toNatCast✝,
      natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ } =
    inst₂
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq_add.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
rcases eq_or_ne s 0 with (rfl | ne_s)

Goal state after:
case sq_add.inr.inl
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s a : R
ne_a : a ≠ 0
hs✝ : IsSumSq 0
ih : 0 ≠ 0 → IsSumNonzeroSq 0
hs : a * a + 0 ≠ 0
⊢ IsSumNonzeroSq (a * a + 0)

case sq_add.inr.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
ne_s : s ≠ 0
⊢ IsSumNonzeroSq (a * a + s)