mathlib-initiative/mathlib-tactics huggingface dataset:
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✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.re +
            c₁ *
                (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                  c₃ * x✝².imK * x✝¹.imJ) *
              x✝.imI +
          c₃ *
              (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
                c₁ * x✝².imK * x✝¹.imI) *
            x✝.imJ +
        c₂ * c₃ *
            (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
          x✝.imK -
      c₁ * c₃ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) *
        x✝.imK =
    x✝².re *
              (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
                c₁ * c₃ * x✝¹.imK * x✝.imK) +
            c₁ * x✝².imI *
              (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK +
                c₃ * x✝¹.imK * x✝.imJ) +
          c₃ * x✝².imJ *
            (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI -
              c₁ * x✝¹.imK * x✝.imI) +
        c₂ * c₃ * x✝².imJ *
          (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) -
      c₁ * c₃ * x✝².imK *
        (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.imI +
            (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
              x✝.re +
          c₂ *
              (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
            x✝.imI -
        c₃ *
            (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
          x✝.imK +
      c₃ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) *
        x✝.imJ =
    x✝².re *
              (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK +
                c₃ * x✝¹.imK * x✝.imJ) +
            x✝².imI *
              (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
                c₁ * c₃ * x✝¹.imK * x✝.imK) +
          c₂ * x✝².imI *
            (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK +
              c₃ * x✝¹.imK * x✝.imJ) -
        c₃ * x✝².imJ *
          (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
      c₃ * x✝².imK *
        (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI - c₁ * x✝¹.imK * x✝.imI)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.imJ +
            c₁ *
                (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                  c₃ * x✝².imK * x✝¹.imJ) *
              x✝.imK +
          (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
            x✝.re +
        c₂ *
            (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
          x✝.imI -
      c₁ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) *
        x✝.imI =
    x✝².re *
              (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI -
                c₁ * x✝¹.imK * x✝.imI) +
            c₁ * x✝².imI *
              (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
          x✝².imJ *
            (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
              c₁ * c₃ * x✝¹.imK * x✝.imK) +
        c₂ * x✝².imJ *
          (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ) -
      c₁ * x✝².imK *
        (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.imK +
            (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
              x✝.imJ +
          c₂ *
              (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
            x✝.imK -
        (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
            c₁ * x✝².imK * x✝¹.imI) *
          x✝.imI +
      (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) * x✝.re =
    x✝².re * (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
            x✝².imI *
              (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI -
                c₁ * x✝¹.imK * x✝.imI) +
          c₂ * x✝².imI *
            (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) -
        x✝².imJ *
          (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ) +
      x✝².imK *
        (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
          c₁ * c₃ * x✝¹.imK * x✝.imK)

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : ℕ → R
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = -1 * ((algebraMap R S) p * ∑ i, (algebraMap R S) (φ ↑i) * x ^ ↑i)

Tactic:
← mul_assoc (-1 : S),

Goal state after:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : ℕ → R
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = -1 * (algebraMap R S) p * ∑ i, (algebraMap R S) (φ ↑i) * x ^ ↑i
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✝².re * (x✝¹.re + x✝.re) + c₁ * x✝².imI * (x✝¹.imI + x✝.imI) + c₃ * x✝².imJ * (x✝¹.imJ + x✝.imJ) +
        c₂ * c₃ * x✝².imJ * (x✝¹.imK + x✝.imK) -
      c₁ * c₃ * x✝².imK * (x✝¹.imK + x✝.imK) =
    x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
        c₁ * c₃ * x✝².imK * x✝¹.imK +
      (x✝².re * x✝.re + c₁ * x✝².imI * x✝.imI + c₃ * x✝².imJ * x✝.imJ + c₂ * c₃ * x✝².imJ * x✝.imK -
        c₁ * c₃ * x✝².imK * x✝.imK)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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✝².re * (x✝¹.imI + x✝.imI) + x✝².imI * (x✝¹.re + x✝.re) + c₂ * x✝².imI * (x✝¹.imI + x✝.imI) -
        c₃ * x✝².imJ * (x✝¹.imK + x✝.imK) +
      c₃ * x✝².imK * (x✝¹.imJ + x✝.imJ) =
    x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK + c₃ * x✝².imK * x✝¹.imJ +
      (x✝².re * x✝.imI + x✝².imI * x✝.re + c₂ * x✝².imI * x✝.imI - c₃ * x✝².imJ * x✝.imK + c₃ * x✝².imK * x✝.imJ)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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✝².re * (x✝¹.imJ + x✝.imJ) + c₁ * x✝².imI * (x✝¹.imK + x✝.imK) + x✝².imJ * (x✝¹.re + x✝.re) +
        c₂ * x✝².imJ * (x✝¹.imI + x✝.imI) -
      c₁ * x✝².imK * (x✝¹.imI + x✝.imI) =
    x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI - c₁ * x✝².imK * x✝¹.imI +
      (x✝².re * x✝.imJ + c₁ * x✝².imI * x✝.imK + x✝².imJ * x✝.re + c₂ * x✝².imJ * x✝.imI - c₁ * x✝².imK * x✝.imI)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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✝².re * (x✝¹.imK + x✝.imK) + x✝².imI * (x✝¹.imJ + x✝.imJ) + c₂ * x✝².imI * (x✝¹.imK + x✝.imK) -
        x✝².imJ * (x✝¹.imI + x✝.imI) +
      x✝².imK * (x✝¹.re + x✝.re) =
    x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re +
      (x✝².re * x✝.imK + x✝².imI * x✝.imJ + c₂ * x✝².imI * x✝.imK - x✝².imJ * x✝.imI + x✝².imK * x✝.re)

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
inst✝ : IsFractionRing (↥S) A
⊢ IsIntegrallyClosed ↥S ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
rw [isIntegrallyClosed_iff A]

Goal state after:
A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
inst✝ : IsFractionRing (↥S) A
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ y, (algebraMap (↥S) A) y = x) ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
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✝².re + x✝¹.re) * x✝.re + c₁ * (x✝².imI + x✝¹.imI) * x✝.imI + c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imJ +
        c₂ * c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imK -
      c₁ * c₃ * (x✝².imK + x✝¹.imK) * x✝.imK =
    x✝².re * x✝.re + c₁ * x✝².imI * x✝.imI + c₃ * x✝².imJ * x✝.imJ + c₂ * c₃ * x✝².imJ * x✝.imK -
        c₁ * c₃ * x✝².imK * x✝.imK +
      (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
        c₁ * c₃ * x✝¹.imK * x✝.imK)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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✝².re + x✝¹.re) * x✝.imI + (x✝².imI + x✝¹.imI) * x✝.re + c₂ * (x✝².imI + x✝¹.imI) * x✝.imI -
        c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imK +
      c₃ * (x✝².imK + x✝¹.imK) * x✝.imJ =
    x✝².re * x✝.imI + x✝².imI * x✝.re + c₂ * x✝².imI * x✝.imI - c₃ * x✝².imJ * x✝.imK + c₃ * x✝².imK * x✝.imJ +
      (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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✝².re + x✝¹.re) * x✝.imJ + c₁ * (x✝².imI + x✝¹.imI) * x✝.imK + (x✝².imJ + x✝¹.imJ) * x✝.re +
        c₂ * (x✝².imJ + x✝¹.imJ) * x✝.imI -
      c₁ * (x✝².imK + x✝¹.imK) * x✝.imI =
    x✝².re * x✝.imJ + c₁ * x✝².imI * x✝.imK + x✝².imJ * x✝.re + c₂ * x✝².imJ * x✝.imI - c₁ * x✝².imK * x✝.imI +
      (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI - c₁ * x✝¹.imK * x✝.imI)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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✝².re + x✝¹.re) * x✝.imK + (x✝².imI + x✝¹.imI) * x✝.imJ + c₂ * (x✝².imI + x✝¹.imI) * x✝.imK -
        (x✝².imJ + x✝¹.imJ) * x✝.imI +
      (x✝².imK + x✝¹.imK) * x✝.re =
    x✝².re * x✝.imK + x✝².imI * x✝.imJ + c₂ * x✝².imI * x✝.imK - x✝².imJ * x✝.imI + x✝².imK * x✝.re +
      (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re)

Tactic:
ring

Goal state after:
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✝ : ℍ[R,c₁,c₃]
⊢ x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ - c₁ * c₃ * x✝¹.imK * x✝.imK =
    x✝¹.re * x✝.re + c₃ * x✝¹.imJ * x✝.imJ + c₁ * x✝¹.imI * x✝.imI - c₃ * c₁ * x✝¹.imK * x✝.imK

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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✝ : ℍ[R,c₁,c₃]
⊢ x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re - c₁ * x✝¹.imK * x✝.imI =
    x✝¹.re * x✝.imJ + x✝¹.imJ * x✝.re + c₁ * x✝¹.imI * x✝.imK + -(c₁ * x✝¹.imK * x✝.imI)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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✝ : ℍ[R,c₁,c₃]
⊢ x✝¹.re * x✝.imI + x✝¹.imI * x✝.re - c₃ * x✝¹.imJ * x✝.imK =
    x✝¹.re * x✝.imI + -(c₃ * x✝¹.imJ * x✝.imK) + x✝¹.imI * x✝.re

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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✝ : ℍ[R,c₁,c₃]
⊢ -(x✝¹.imK * x✝.re) + (x✝¹.imJ * x✝.imI - (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ)) =
    -(x✝¹.re * x✝.imK) + x✝¹.imJ * x✝.imI - x✝¹.imI * x✝.imJ + -(x✝¹.imK * x✝.re)

Tactic:
ring

Goal state after:
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
a b : ℍ[R,c₁,c₂,c₃]
⊢ a.re * b.re + c₁ * a.imI * b.imI + c₃ * a.imJ * b.imJ + c₂ * c₃ * a.imJ * b.imK - c₁ * c₃ * a.imK * b.imK +
      c₂ * (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI - c₃ * a.imJ * b.imK + c₃ * a.imK * b.imJ) =
    (b.re + c₂ * b.imI) * (a.re + c₂ * a.imI) + c₁ * b.imI * a.imI + c₃ * b.imJ * a.imJ + c₂ * c₃ * b.imJ * a.imK -
      c₁ * c₃ * b.imK * a.imK

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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
a b : ℍ[R,c₁,c₂,c₃]
⊢ -(c₃ * a.imK * b.imJ) + (c₃ * a.imJ * b.imK - (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI)) =
    -((b.re + c₂ * b.imI) * a.imI) + -(b.imI * (a.re + c₂ * a.imI)) + c₂ * b.imI * a.imI - c₃ * b.imJ * a.imK +
      c₃ * b.imK * a.imJ

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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
a b : ℍ[R,c₁,c₂,c₃]
⊢ c₁ * a.imK * b.imI - (a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re + c₂ * a.imJ * b.imI) =
    -((b.re + c₂ * b.imI) * a.imJ) + c₁ * b.imI * a.imK + -(b.imJ * (a.re + c₂ * a.imI)) + c₂ * b.imJ * a.imI -
      c₁ * b.imK * a.imI

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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
a b : ℍ[R,c₁,c₂,c₃]
⊢ -(a.imK * b.re) + (a.imJ * b.imI - (a.re * b.imK + a.imI * b.imJ + c₂ * a.imI * b.imK)) =
    -((b.re + c₂ * b.imI) * a.imK) + b.imI * a.imJ + c₂ * b.imI * a.imK - b.imJ * a.imI + -(b.imK * (a.re + c₂ * a.imI))

Tactic:
ring

Goal state after:
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
a b : ℍ[R,c₁,c₂,c₃]
⊢ a.re + b.re + c₂ * (a.imI + b.imI) = a.re + c₂ * a.imI + (b.re + c₂ * b.imI)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a.re + (a.re + c₂ * a.imI) = a.re + a.re + c₂ * a.imI

Tactic:
ring

Goal state after:
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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.re = a.re * (2 * a.re + c₂ * a.imI - a.re)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imI + -(a.imI * a.re) = -(a.re * a.imI) + a.imI * (2 * a.re + c₂ * a.imI - a.re)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) =
    -(a.re * a.imJ) + -(c₁ * a.imI * a.imK) + a.imJ * (2 * a.re + c₂ * a.imI - a.re)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) =
    -(a.re * a.imK) + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + a.imK * (2 * a.re + c₂ * a.imI - a.re)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imI + -(a.imI * a.re) + -(c₂ * a.imI * a.imI) + c₃ * a.imJ * a.imK + -(c₃ * a.imK * a.imJ) = 0

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) + -(c₂ * a.imJ * a.imI) + c₁ * a.imK * a.imI = 0

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) = 0

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.imI + a.imI * b.re + 0 * a.imI * b.imI - -1 * a.imJ * b.imK + -1 * a.imK * b.imJ =
    a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.imJ + -1 * a.imI * b.imK + a.imJ * b.re + 0 * a.imJ * b.imI - -1 * a.imK * b.imI =
    a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.imK + a.imI * b.imJ + 0 * a.imI * b.imK - a.imJ * b.imI + a.imK * b.re =
    a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
⊢ (normSq 0)⁻¹ • 0 = 0

Tactic:
smul_zero

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
⊢ 0 = 0
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝¹ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a✝ b a : ℍ[R]
ha : a ≠ 0
⊢ ↑1 = 1

Tactic:
coe_one

Goal state after:
R : Type u_1
inst✝² : Field R
a✝¹ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a✝ b a : ℍ[R]
ha : a ≠ 0
⊢ 1 = 1
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
⊢ #R * (#R * (#R * #R)) = #R ^ 4

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: m k : ℕ
hmn : m < m + k + 1
⊢ m + k + 1 = k + 1 + m

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : PartialOrder α
inst✝³ : DecidableEq α
inst✝² : MulLeftStrictMono α
inst✝¹ : MulRightStrictMono α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ ↑(Icc a b * Ico c d) ⊆ ↑(Ico (a * c) (b * d))

Tactic:
by simpa using Set.Icc_mul_Ico_subset' _ _ _ _

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
b : C
hb : b ∈ x
c : C
hc : c ∈ y
haz : b * c ∈ z
⊢ b * c ∈ x ⊔ y ⊓ z

Tactic:
rw [mem_sup]

Goal state after:
C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
b : C
hb : b ∈ x
c : C
hc : c ∈ y
haz : b * c ∈ z
⊢ ∃ y_1 ∈ x, ∃ z_1 ∈ y ⊓ z, y_1 * z_1 = b * c
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
⊢ False

Tactic:
rcases hv_t k with hk' | hk'

Goal state after:
case inl
ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k ∈ t
⊢ False

case inr
ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k⁻¹ ∈ t
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : GroupWithZero G
inst✝ : GroupWithZero H
f : G →*₀ H
⊢ ∀ (a : ↥(MonoidHom.mrange f)), a ≠ 0 → a * ⟨(↑a)⁻¹, ⋯⟩ = 1

Tactic:
rintro ⟨a, ha⟩ h

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : GroupWithZero G
inst✝ : GroupWithZero H
f : G →*₀ H
a : H
ha : a ∈ MonoidHom.mrange f
h : ⟨a, ha⟩ ≠ 0
⊢ ⟨a, ha⟩ * ⟨(↑⟨a, ha⟩)⁻¹, ⋯⟩ = 1