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

Goal state before:
pp: case refl
R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) ⟨0 + 3, ⋯⟩ =
    x✝ ⟨0 + 3, ⋯⟩

pp: case step.refl
R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) ⟨0 + 2, ⋯⟩ =
    x✝ ⟨0 + 2, ⋯⟩

pp: case step.step.refl
R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) ⟨0 + 1, ⋯⟩ =
    x✝ ⟨0 + 1, ⋯⟩

pp: case step.step.step.refl
R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) ⟨0, ⋯⟩ =
    x✝ ⟨0, ⋯⟩

Tactic:
<;>

Goal state after:
case refl
R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) ⟨0 + 3, ⋯⟩ =
    x✝ ⟨0 + 3, ⋯⟩

case step.refl
R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) ⟨0 + 2, ⋯⟩ =
    x✝ ⟨0 + 2, ⋯⟩

case step.step.refl
R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) ⟨0 + 1, ⋯⟩ =
    x✝ ⟨0 + 1, ⋯⟩

case step.step.step.refl
R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) ⟨0, ⋯⟩ =
    x✝ ⟨0, ⋯⟩
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ (↑(x + y)).re = (↑x + ↑y).re

pp: case imI
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ (↑(x + y)).imI = (↑x + ↑y).imI

pp: case imJ
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ (↑(x + y)).imJ = (↑x + ↑y).imJ

pp: case imK
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ (↑(x + y)).imK = (↑x + ↑y).imK

Tactic:
<;>

Goal state after:
case re
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ (↑(x + y)).re = (↑x + ↑y).re

case imI
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ (↑(x + y)).imI = (↑x + ↑y).imI

case imJ
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ (↑(x + y)).imJ = (↑x + ↑y).imJ

case imK
R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ (↑(x + y)).imK = (↑x + ↑y).imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ (↑(-x)).re = (-↑x).re

pp: case imI
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ (↑(-x)).imI = (-↑x).imI

pp: case imJ
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ (↑(-x)).imJ = (-↑x).imJ

pp: case imK
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ (↑(-x)).imK = (-↑x).imK

Tactic:
<;>

Goal state after:
case re
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ (↑(-x)).re = (-↑x).re

case imI
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ (↑(-x)).imI = (-↑x).imI

case imJ
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ (↑(-x)).imJ = (-↑x).imJ

case imK
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ (↑(-x)).imK = (-↑x).imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).re = (s • t • x).re

pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imI = (s • t • x).imI

pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imJ = (s • t • x).imJ

pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imK = (s • t • x).imK

Tactic:
<;>

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).re = (s • t • x).re

case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imI = (s • t • x).imI

case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imJ = (s • t • x).imJ

case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imK = (s • t • x).imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).re = (t • s • x).re

pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).imI = (t • s • x).imI

pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).imJ = (t • s • x).imJ

pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).imK = (t • s • x).imK

Tactic:
<;>

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).re = (t • s • x).re

case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).imI = (t • s • x).imI

case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).imJ = (t • s • x).imJ

case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : SMul S R
inst✝¹ : SMul T R
s✝ : S
inst✝ : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).imK = (t • s • x).imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case zero
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ (equivProd c₁ c₂ c₃) 0 = 0

pp: case add
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x y : ℍ[R,c₁,c₂,c₃]), (equivProd c₁ c₂ c₃) (x + y) = (equivProd c₁ c₂ c₃) x + (equivProd c₁ c₂ c₃) y

pp: case neg
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x : ℍ[R,c₁,c₂,c₃]), (equivProd c₁ c₂ c₃) (-x) = -(equivProd c₁ c₂ c₃) x

pp: case sub
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x y : ℍ[R,c₁,c₂,c₃]), (equivProd c₁ c₂ c₃) (x - y) = (equivProd c₁ c₂ c₃) x - (equivProd c₁ c₂ c₃) y

pp: case nsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x : ℍ[R,c₁,c₂,c₃]) (n : ℕ), (equivProd c₁ c₂ c₃) (n • x) = n • (equivProd c₁ c₂ c₃) x

pp: case zsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x : ℍ[R,c₁,c₂,c₃]) (n : ℤ), (equivProd c₁ c₂ c₃) (n • x) = n • (equivProd c₁ c₂ c₃) x

Tactic:
<;>

Goal state after:
case zero
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ (equivProd c₁ c₂ c₃) 0 = 0

case add
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x y : ℍ[R,c₁,c₂,c₃]), (equivProd c₁ c₂ c₃) (x + y) = (equivProd c₁ c₂ c₃) x + (equivProd c₁ c₂ c₃) y

case neg
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x : ℍ[R,c₁,c₂,c₃]), (equivProd c₁ c₂ c₃) (-x) = -(equivProd c₁ c₂ c₃) x

case sub
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x y : ℍ[R,c₁,c₂,c₃]), (equivProd c₁ c₂ c₃) (x - y) = (equivProd c₁ c₂ c₃) x - (equivProd c₁ c₂ c₃) y

case nsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x : ℍ[R,c₁,c₂,c₃]) (n : ℕ), (equivProd c₁ c₂ c₃) (n • x) = n • (equivProd c₁ c₂ c₃) x

case zsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ ∀ (x : ℍ[R,c₁,c₂,c₃]) (n : ℤ), (equivProd c₁ c₂ c₃) (n • x) = n • (equivProd c₁ c₂ c₃) x
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)

Tactic:
have map_dvd_pow_q :
      g.map (algebraMap R K) ∣ q.map (algebraMap R K) ^ p := by
    rw [← IsUnit.dvd_mul_left _, ← hfmodP]
    · exact Polynomial.map_dvd _ hg_div
    · simp_all

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case zero
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ (equivProd c₁ c₂ c₃) 0 = 0

pp: case add
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ y✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (x✝ + y✝) = (equivProd c₁ c₂ c₃) x✝ + (equivProd c₁ c₂ c₃) y✝

pp: case neg
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (-x✝) = -(equivProd c₁ c₂ c₃) x✝

pp: case sub
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ y✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (x✝ - y✝) = (equivProd c₁ c₂ c₃) x✝ - (equivProd c₁ c₂ c₃) y✝

pp: case nsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
n✝ : ℕ
⊢ (equivProd c₁ c₂ c₃) (n✝ • x✝) = n✝ • (equivProd c₁ c₂ c₃) x✝

pp: case zsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
n✝ : ℤ
⊢ (equivProd c₁ c₂ c₃) (n✝ • x✝) = n✝ • (equivProd c₁ c₂ c₃) x✝

Tactic:
<;>

Goal state after:
case zero
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ (equivProd c₁ c₂ c₃) 0 = 0

case add
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ y✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (x✝ + y✝) = (equivProd c₁ c₂ c₃) x✝ + (equivProd c₁ c₂ c₃) y✝

case neg
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (-x✝) = -(equivProd c₁ c₂ c₃) x✝

case sub
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ y✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (x✝ - y✝) = (equivProd c₁ c₂ c₃) x✝ - (equivProd c₁ c₂ c₃) y✝

case nsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
n✝ : ℕ
⊢ (equivProd c₁ c₂ c₃) (n✝ • x✝) = n✝ • (equivProd c₁ c₂ c₃) x✝

case zsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
n✝ : ℤ
⊢ (equivProd c₁ c₂ c₃) (n✝ • x✝) = n✝ • (equivProd c₁ c₂ c₃) x✝
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * x✝¹ * x✝).re = (x✝² * (x✝¹ * x✝)).re

pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * x✝¹ * x✝).imI = (x✝² * (x✝¹ * x✝)).imI

pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * x✝¹ * x✝).imJ = (x✝² * (x✝¹ * x✝)).imJ

pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * x✝¹ * x✝).imK = (x✝² * (x✝¹ * x✝)).imK

Tactic:
<;>

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * x✝¹ * x✝).re = (x✝² * (x✝¹ * x✝)).re

case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * x✝¹ * x✝).imI = (x✝² * (x✝¹ * x✝)).imI

case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * x✝¹ * x✝).imJ = (x✝² * (x✝¹ * x✝)).imJ

case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * x✝¹ * x✝).imK = (x✝² * (x✝¹ * x✝)).imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x✝).re = x✝.re

pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x✝).imI = x✝.imI

pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x✝).imJ = x✝.imJ

pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x✝).imK = x✝.imK

Tactic:
<;>

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x✝).re = x✝.re

case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x✝).imI = x✝.imI

case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x✝).imJ = x✝.imJ

case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x✝).imK = x✝.imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 1).re = x✝.re

pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 1).imI = x✝.imI

pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 1).imJ = x✝.imJ

pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 1).imK = x✝.imK

Tactic:
<;>

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 1).re = x✝.re

case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 1).imI = x✝.imI

case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 1).imJ = x✝.imJ

case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 1).imK = x✝.imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x✝).re = re 0

pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x✝).imI = imI 0

pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x✝).imJ = imJ 0

pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x✝).imK = imK 0

Tactic:
<;>

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x✝).re = re 0

case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x✝).imI = imI 0

case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x✝).imJ = imJ 0

case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x✝).imK = imK 0
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 0).re = re 0

pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 0).imI = imI 0

pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 0).imJ = imJ 0

pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 0).imK = imK 0

Tactic:
<;>

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 0).re = re 0

case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 0).imI = imI 0

case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 0).imJ = imJ 0

case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝ * 0).imK = imK 0
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * (x✝¹ + x✝)).re = (x✝² * x✝¹ + x✝² * x✝).re

pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * (x✝¹ + x✝)).imI = (x✝² * x✝¹ + x✝² * x✝).imI

pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * (x✝¹ + x✝)).imJ = (x✝² * x✝¹ + x✝² * x✝).imJ

pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * (x✝¹ + x✝)).imK = (x✝² * x✝¹ + x✝² * x✝).imK

Tactic:
<;>

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * (x✝¹ + x✝)).re = (x✝² * x✝¹ + x✝² * x✝).re

case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * (x✝¹ + x✝)).imI = (x✝² * x✝¹ + x✝² * x✝).imI

case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * (x✝¹ + x✝)).imJ = (x✝² * x✝¹ + x✝² * x✝).imJ

case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² * (x✝¹ + x✝)).imK = (x✝² * x✝¹ + x✝² * x✝).imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((x✝² + x✝¹) * x✝).re = (x✝² * x✝ + x✝¹ * x✝).re

pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((x✝² + x✝¹) * x✝).imI = (x✝² * x✝ + x✝¹ * x✝).imI

pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((x✝² + x✝¹) * x✝).imJ = (x✝² * x✝ + x✝¹ * x✝).imJ

pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((x✝² + x✝¹) * x✝).imK = (x✝² * x✝ + x✝¹ * x✝).imK

Tactic:
<;>

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((x✝² + x✝¹) * x✝).re = (x✝² * x✝ + x✝¹ * x✝).re

case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((x✝² + x✝¹) * x✝).imI = (x✝² * x✝ + x✝¹ * x✝).imI

case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((x✝² + x✝¹) * x✝).imJ = (x✝² * x✝ + x✝¹ * x✝).imJ

case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((x✝² + x✝¹) * x✝).imK = (x✝² * x✝ + x✝¹ * x✝).imK
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
⊢ ∀ (i : ℕ), (Polynomial.map (algebraMap R S) f).natDegree ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
suffices x ^ (f.map (algebraMap R S)).natDegree ∈ 𝓟.map (algebraMap R S) by
    intro i hi
    obtain ⟨k, hk⟩ := exists_add_of_le hi
    rw [hk, pow_add]
    exact mul_mem_right _ _ this
  rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def] at hx
  exact pow_natDegree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le

Goal state after: