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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² * x✝¹ * x✝).re = (x✝² * (x✝¹ * x✝)).re

Tactic:
simp

Goal state after:
case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝².re * x✝¹.re + a * x✝².im * x✝¹.im) * x✝.re +
      a * (x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im) * x✝.im =
    x✝².re * (x✝¹.re * x✝.re + a * x✝¹.im * x✝.im) + a * x✝².im * (x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case im
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ ({ re := x, im := y } * star { re := x, im := y }).im =
    ((algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) x +
          (algebraMap R (QuadraticAlgebra R a b)) b * (algebraMap R (QuadraticAlgebra R a b)) x *
            (algebraMap R (QuadraticAlgebra R a b)) y -
        (algebraMap R (QuadraticAlgebra R a b)) a * (algebraMap R (QuadraticAlgebra R a b)) y *
          (algebraMap R (QuadraticAlgebra R a b)) y).im

Tactic:
simp

Goal state after:
case im
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ -(x * y) + y * (x + b * y) + -(b * y * y) = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² * x✝¹ * x✝).im = (x✝² * (x✝¹ * x✝)).im

Tactic:
simp

Goal state after:
case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝².re * x✝¹.re + a * x✝².im * x✝¹.im) * x✝.im + (x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im) * x✝.re +
      b * (x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im) * x✝.im =
    x✝².re * (x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im) + x✝².im * (x✝¹.re * x✝.re + a * x✝¹.im * x✝.im) +
      b * x✝².im * (x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝ : CommRing R
x✝ : QuadraticAlgebra R a b
⊢ (star (star x✝)).re = x✝.re

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝¹ * x✝).re = (x✝ * x✝¹).re

Tactic:
simp

Goal state after:
case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹.re * x✝.re + a * x✝¹.im * x✝.im = x✝.re * x✝¹.re + a * x✝.im * x✝¹.im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝¹ * x✝).im = (x✝ * x✝¹).im

Tactic:
simp

Goal state after:
case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im = x✝.re * x✝¹.im + x✝.im * x✝¹.re + b * x✝.im * x✝¹.im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (QuadraticAlgebra.C ((algebraMap S R) 1)).re = re 1

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (QuadraticAlgebra.C ((algebraMap S R) 1)).im = im 1

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ (QuadraticAlgebra.C ((algebraMap S R) (x * y))).re =
    (QuadraticAlgebra.C ((algebraMap S R) x) * QuadraticAlgebra.C ((algebraMap S R) y)).re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ (QuadraticAlgebra.C ((algebraMap S R) (x * y))).im =
    (QuadraticAlgebra.C ((algebraMap S R) x) * QuadraticAlgebra.C ((algebraMap S R) y)).im

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (QuadraticAlgebra.C ((algebraMap S R) 0)).re = re 0

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ (QuadraticAlgebra.C ((algebraMap S R) 0)).im = im 0

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ (z - star z).re = (z.im • (ω - star ω)).re

Tactic:
simp

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ b * z.im = z.im * b
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ (QuadraticAlgebra.C ((algebraMap S R) (x + y))).re =
    (QuadraticAlgebra.C ((algebraMap S R) x) + QuadraticAlgebra.C ((algebraMap S R) y)).re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ (QuadraticAlgebra.C ((algebraMap S R) (x + y))).im =
    (QuadraticAlgebra.C ((algebraMap S R) x) + QuadraticAlgebra.C ((algebraMap S R) y)).im

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ (z - star z).im = (z.im • (ω - star ω)).im

Tactic:
simp

Goal state after:
case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z.im + z.im = z.im * (1 + 1)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝ : CommRing R
⊢ re 1 * re 1 + b * re 1 * im 1 - a * im 1 * im 1 = 1

Tactic:
simp

Goal state after:
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✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
⊢ ∀ (r : S) (m : QuadraticAlgebra R a b), (linearEquivTuple a b) (r • m) = r • (linearEquivTuple a b) m

Tactic:
simp

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

Goal state before:
pp: case mp
R : Type u_1
a b : R
inst✝ : CommSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ r ∣ ((algebraMap R (QuadraticAlgebra R a b)) r * x).re ∧ r ∣ ((algebraMap R (QuadraticAlgebra R a b)) r * x).im

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : CommSemiring R
z w : R
⊢ z ∣ ((algebraMap R (QuadraticAlgebra R a b)) w).re ∧ z ∣ ((algebraMap R (QuadraticAlgebra R a b)) w).im ↔ z ∣ w

Tactic:
simp

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

Goal state before:
pp: case re
R : Type u_1
a b : R
inst✝ : CommRing R
n : ℤ
x y : R
⊢ (↑n * { re := x, im := y }).re = { re := ↑n * x, im := ↑n * y }.re

Tactic:
simp

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

Goal state before:
pp: case im
R : Type u_1
a b : R
inst✝ : CommRing R
n : ℤ
x y : R
⊢ (↑n * { re := x, im := y }).im = { re := ↑n * x, im := ↑n * y }.im

Tactic:
simp

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

Goal state before:
pp: case mp
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
⊢ IsUnit x → IsUnit (norm x)

pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
⊢ IsUnit (norm x) → IsUnit x

Tactic:
· exact IsUnit.map norm

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
⊢ IsUnit (norm x) → IsUnit x
Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant

Goal state before:
pp: 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
⊢ ((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec (⇑((basis a b).repr w)) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
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)
Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant

Goal state before:
pp: 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
⊢ ((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec (⇑((basis a b).repr w)) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

Goal state after:
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.QuadraticAlgebra.NormDeterminant

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
⊢ LinearMap.det (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) = norm z

Tactic:
by
  rw [← LinearMap.det_toMatrix <| basis ..]
  have : !![z.re, a * z.im; z.im, z.re + b * z.im].det = z.norm := by
    simp [norm]
    ring
  convert! this
  apply LinearEquiv.eq_symm_apply _ |>.mp
  ext1 w
  apply basis .. |>.repr.injective
  apply DFunLike.coe_injective
  rw [LinearMap.toMatrix_symm, Matrix.repr_toLin]
  ext i
  fin_cases i
    <;> simp
    <;> ring

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
⊢ w * star z = 0 → w = 0

Tactic:
hw

Goal state after:
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * star z = 0
⊢ w = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mp
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
w : QuadraticAlgebra R a b
⊢ w * z = 0 → w = 0

Tactic:
hw

Goal state after:
case mp
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
⊢ w = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case re
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
⊢ 0⁻¹.re = re 0

Tactic:
simp

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

Goal state before:
pp: case im
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
⊢ 0⁻¹.im = im 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_2
inst✝ : Rack R
x y z : R
⊢ (act' (x ◃ y) * act' x) z = (act' x * act' y) z

Tactic:
apply self_distrib.symm

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
⊢ (fun y ↦ op (unop (op x) ◃ unop y)) ((fun y ↦ op (unop (op x) ◃⁻¹ unop y)) (op y)) = op y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
⊢ (fun y ↦ op (unop (op x) ◃⁻¹ unop y)) ((fun y ↦ op (unop (op x) ◃ unop y)) (op y)) = op y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R✝ : Type u_1
inst✝¹ : Rack R✝
R : Type u_2
inst✝ : Rack R
x : R
⊢ (fun x ↦ x ◃⁻¹ x) ((fun x ↦ x ◃ x) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R✝ : Type u_1
inst✝¹ : Rack R✝
R : Type u_2
inst✝ : Rack R
x : R
⊢ (fun x ↦ x ◃ x) ((fun x ↦ x ◃⁻¹ x) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S₁ : Type u_1
S₂ : Type u_2
S₃ : Type u_3
inst✝³ : Shelf S₁
inst✝² : Shelf S₂
inst✝¹ : Shelf S₃
S : Type u_4
inst✝ : Shelf S
⊢ ∀ {x y : S}, x ◃ y = x ◃ y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S₁ : Type u_1
S₂ : Type u_2
S₃ : Type u_3
inst✝² : Shelf S₁
inst✝¹ : Shelf S₂
inst✝ : Shelf S₃
g : S₂ →◃ S₃
f : S₁ →◃ S₂
⊢ ∀ {x y : S₁}, (g.toFun ∘ f.toFun) (x ◃ y) = (g.toFun ∘ f.toFun) x ◃ (g.toFun ∘ f.toFun) y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
x : Q
⊢ x ◃ x ◃⁻¹ x = x ◃ x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case h
Q : Type u_1
inst✝ : Quandle Q
X✝ : Q
⊢ op X✝ ◃ op X✝ = op X✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝² : Quandle Q
G : Type u_2
H : Type u_3
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ ∀ {x y : Conj G}, f (x ◃ y) = f x ◃ f y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ 2 * a - (2 * a - b) = b

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).re =
    (c₁ • 1 + c₂ • { re := 0, imI := 1, imJ := 0, imK := 0 }).re

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imI =
    (c₁ • 1 + c₂ • { re := 0, imI := 1, imJ := 0, imK := 0 }).imI

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imJ =
    (c₁ • 1 + c₂ • { re := 0, imI := 1, imJ := 0, imK := 0 }).imJ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imK =
    (c₁ • 1 + c₂ • { re := 0, imI := 1, imJ := 0, imK := 0 }).imK

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).re = (c₃ • 1).re

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imI = (c₃ • 1).imI

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imJ = (c₃ • 1).imJ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imK = (c₃ • 1).imK

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).re =
    { re := 0, imI := 0, imJ := 0, imK := 1 }.re

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imI =
    { re := 0, imI := 0, imJ := 0, imK := 1 }.imI

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imJ =
    { re := 0, imI := 0, imJ := 0, imK := 1 }.imJ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 }).imK =
    { re := 0, imI := 0, imJ := 0, imK := 1 }.imK

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).re =
    (c₂ • { re := 0, imI := 0, imJ := 1, imK := 0 } - { re := 0, imI := 0, imJ := 0, imK := 1 }).re

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imI =
    (c₂ • { re := 0, imI := 0, imJ := 1, imK := 0 } - { re := 0, imI := 0, imJ := 0, imK := 1 }).imI

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imJ =
    (c₂ • { re := 0, imI := 0, imJ := 1, imK := 0 } - { re := 0, imI := 0, imJ := 0, imK := 1 }).imJ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ ({ re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 }).imK =
    (c₂ • { re := 0, imI := 0, imJ := 1, imK := 0 } - { re := 0, imI := 0, imJ := 0, imK := 1 }).imK

Tactic:
simp

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

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

Tactic:
simp_rw [add_mul, Finset.sum_mul, map_add, map_sum, map_mul, map_prod, map_pow]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
⊢ (algebraMap R[X] K) q * ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i +
      ∑ x ∈ s, ∑ i, (algebraMap R[X] K) (r x i) * gi x ^ (↑i + 1) * ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
    (algebraMap R[X] K) q * ∏ x ∈ s, (algebraMap R[X] K) (g x) ^ n x +
      ∑ x ∈ s,
        ∑ x_1,
          (algebraMap R[X] K) (r x x_1.rev) * (algebraMap R[X] K) (g x) ^ ↑x_1 *
            ∏ x ∈ s.erase x, (algebraMap R[X] K) (g x) ^ n x
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ B.i ∈ {B.i, B.j, B.k}

Tactic:
simp

Goal state after:
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ B.j ∈ {B.i, B.j, B.k}

Tactic:
simp

Goal state after:
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
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ B.k ∈ {B.i, B.j, B.k}

Tactic:
simp

Goal state after: