mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : QuadraticAlgebra R a b
⊢ s • x =
    { toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        s *
      x

Tactic:
ext

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
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : QuadraticAlgebra R a b
⊢ (s • x).re =
    ({ toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s *
        x).re

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
s : S
x : QuadraticAlgebra R a b
⊢ (s • x).im =
    ({ toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          s *
        x).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

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

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
a b : R
inst✝ : CommSemiring R
r : R
z : QuadraticAlgebra R a b
⊢ (algebraMap R (QuadraticAlgebra R a b)) r ∣ z → r ∣ z.re ∧ r ∣ z.im

case mpr
R : Type u_1
a b : R
inst✝ : CommSemiring R
r : R
z : QuadraticAlgebra R a b
⊢ r ∣ z.re ∧ r ∣ z.im → (algebraMap R (QuadraticAlgebra R a b)) r ∣ z
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ (algebraMap R (QuadraticAlgebra R a b)) (norm z) = z * star z

Tactic:
ext

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (norm z)).re = (z * star z).re

case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (norm z)).im = (z * star z).im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

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

Tactic:
ext

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

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
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
⊢ q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k =
    q * ∏ i ∈ s, g i ^ n i +
      ((∑ i ∈ s, q' i) * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r' i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k)

Tactic:
add_right_inj,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
⊢ ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k =
    (∑ i ∈ s, q' i) * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r' i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

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

Tactic:
constructor

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

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.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
r : R
⊢ (∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0) ↔
    ∀ (x : R), x * r = 0 → x = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
⊢ (∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0) →
    ∀ (x : R), x * r = 0 → x = 0

case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
⊢ (∀ (x : R), x * r = 0 → x = 0) →
    ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ norm z ∈ R⁰ ↔ z ∈ (QuadraticAlgebra R a b)⁰

Tactic:
constructor

Goal state after:
case mp
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ norm z ∈ R⁰ → z ∈ (QuadraticAlgebra R a b)⁰

case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z ∈ (QuadraticAlgebra R a b)⁰ → norm z ∈ R⁰
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
hw : w * z = 0
this : w.re * norm z = 0 ∧ w.im * norm z = 0
⊢ w = 0

Tactic:
ext

Goal state after:
case mp.re
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
this : w.re * norm z = 0 ∧ w.im * norm z = 0
⊢ w.re = re 0

case mp.im
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
this : w.re * norm z = 0 ∧ w.im * norm z = 0
⊢ w.im = im 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : z ∈ (QuadraticAlgebra R a b)⁰
⊢ (algebraMap R (QuadraticAlgebra R ?m.89 ?m.90)) (norm z) ∈ (QuadraticAlgebra R ?m.89 ?m.90)⁰

pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : z ∈ (QuadraticAlgebra R a b)⁰
⊢ R

pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : z ∈ (QuadraticAlgebra R a b)⁰
⊢ R

Tactic:
algebraMap_norm_eq_mul_star

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : z ∈ (QuadraticAlgebra R a b)⁰
⊢ z * star z ∈ (QuadraticAlgebra R a b)⁰
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ (algebraMap R (QuadraticAlgebra R a b)) (trace z) = z + star z

Tactic:
ext

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (trace z)).re = (z + star z).re

case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ ((algebraMap R (QuadraticAlgebra R a b)) (trace z)).im = (z + star z).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z ^ 2 - (z + star z) * z + (algebraMap R (QuadraticAlgebra R a b)) (norm z) = 0

Tactic:
algebraMap_norm_eq_mul_star

Goal state after:
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z ^ 2 - (z + star z) * z + z * star z = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
⊢ norm z = 0 ↔ z = 0

Tactic:
constructor

Goal state after:
case mp
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
⊢ norm z = 0 → z = 0

case mpr
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
⊢ z = 0 → norm z = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: 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⁻¹ = 0

Tactic:
ext

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

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
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: 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)
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
ext

Goal state after:
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)
q : ℚ≥0
⊢ (↑q).re = (↑q.num / ↑q.den).re

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)
q : ℚ≥0
⊢ (↑q).im = (↑q.num / ↑q.den).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: 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)
q : ℚ≥0
x : QuadraticAlgebra K a b
⊢ q • x = ↑q * x

Tactic:
ext

Goal state after:
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)
q : ℚ≥0
x : QuadraticAlgebra K a b
⊢ (q • x).re = (↑q * x).re

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)
q : ℚ≥0
x : QuadraticAlgebra K a b
⊢ (q • x).im = (↑q * x).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: 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)
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
ext

Goal state after:
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)
q : ℚ
⊢ (↑q).re = (↑q.num / ↑q.den).re

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)
q : ℚ
⊢ (↑q).im = (↑q.num / ↑q.den).im
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: 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)
q : ℚ
x : QuadraticAlgebra K a b
⊢ q • x = ↑q * x

Tactic:
ext

Goal state after:
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)
q : ℚ
x : QuadraticAlgebra K a b
⊢ (q • x).re = (↑q * x).re

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)
q : ℚ
x : QuadraticAlgebra K a b
⊢ (q • x).im = (↑q * x).im
Module: Mathlib.Algebra.Polynomial.PartialFractions

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

Tactic:
Finset.prod_const_one,

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

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

Tactic:
add_right_inj,

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

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃ y = x ◃ y' ↔ y = y'

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃ y = x ◃ y' → y = y'

case mpr
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ y = y' → x ◃ y = x ◃ y'
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y' ↔ y = y'

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y' → y = y'

case mpr
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ y = y' → x ◃⁻¹ y = x ◃⁻¹ y'
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y ↔ x = y

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y

case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x = y → x ◃ x = y ◃ y
Module: Mathlib.Algebra.Polynomial.PartialFractions

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

Tactic:
Finset.prod_const_one,

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

Goal state before:
pp: 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 } =
    c₁ • 1 + c₂ • { re := 0, imI := 1, imJ := 0, imK := 0 }

Tactic:
ext

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

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

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

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
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
⊢ Equivalence (PreEnvelGroupRel R)

Tactic:
constructor

Goal state after:
case refl
R : Type u_1
inst✝ : Rack R
⊢ ∀ (x : PreEnvelGroup R), PreEnvelGroupRel R x x

case symm
R : Type u_1
inst✝ : Rack R
⊢ ∀ {x y : PreEnvelGroup R}, PreEnvelGroupRel R x y → PreEnvelGroupRel R y x

case trans
R : Type u_1
inst✝ : Rack R
⊢ ∀ {x y z : PreEnvelGroup R}, PreEnvelGroupRel R x y → PreEnvelGroupRel R y z → PreEnvelGroupRel R x z
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: 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 } = c₃ • 1

Tactic:
ext

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

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

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

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
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: 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 := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
ext

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

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

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

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
Module: Mathlib.Algebra.Polynomial.PartialFractions

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

Tactic:
Nat.add_sub_cancel' (by lia)

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