mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
⊢ ContinuousAt (⇑((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))))
    1

Tactic:
ContinuousAt,

Goal state after:
case pos
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
⊢ Filter.Tendsto
    (⇑((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L)))) (nhds 1)
    (nhds (((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))) 1))
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case ha
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ 1 ≤ ↑p

pp: case a
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ k ≤ k + 1

Tactic:
<;>

Goal state after:
case ha
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ 1 ≤ ↑p

case a
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ k ≤ k + 1
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
r : R
⊢ (lift f_compat) r - ↑((f n) r).val ∈ RingHom.ker (toZModPow n)

Tactic:
ker_toZModPow

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
r : R
⊢ (lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
⊢ ((traceMatrix K ⇑B.basis).updateCol i fun i ↦ (trace K L) (z * B.basis i)).det ∈ ⊥

Tactic:
det_apply

Goal state after:
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
⊢ ∑ σ,
      Equiv.Perm.sign σ •
        ∏ i_1, (traceMatrix K ⇑B.basis).updateCol i (fun i ↦ (trace K L) (z * B.basis i)) (σ i_1) i_1 ∈
    ⊥
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case re
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 1)).re = (pellZd a1 n * { re := ↑a, im := 1 }).re

pp: case im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 1)).im = (pellZd a1 n * { re := ↑a, im := 1 }).im

Tactic:
<;>

Goal state after:
case re
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 1)).re = (pellZd a1 n * { re := ↑a, im := 1 }).re

case im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 1)).im = (pellZd a1 n * { re := ↑a, im := 1 }).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1
d : ℤ
⊢ ∀ (a b c : ℤ√d), a + b + c = a + (b + c)

pp: case refine_2
d : ℤ
⊢ ∀ (a : ℤ√d), 0 + a = a

pp: case refine_3
d : ℤ
⊢ ∀ (a : ℤ√d), a + 0 = a

pp: case refine_4
d : ℤ
⊢ ∀ (a : ℤ√d), -a + a = 0

pp: case refine_5
d : ℤ
⊢ ∀ (a b : ℤ√d), a + b = b + a

Tactic:
<;>

Goal state after:
case refine_1
d : ℤ
⊢ ∀ (a b c : ℤ√d), a + b + c = a + (b + c)

case refine_2
d : ℤ
⊢ ∀ (a : ℤ√d), 0 + a = a

case refine_3
d : ℤ
⊢ ∀ (a : ℤ√d), a + 0 = a

case refine_4
d : ℤ
⊢ ∀ (a : ℤ√d), -a + a = 0

case refine_5
d : ℤ
⊢ ∀ (a b : ℤ√d), a + b = b + a
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)

pp: case refine_2
d : ℤ
a✝ : ℤ√d
⊢ 0 + a✝ = a✝

pp: case refine_3
d : ℤ
a✝ : ℤ√d
⊢ a✝ + 0 = a✝

pp: case refine_4
d : ℤ
a✝ : ℤ√d
⊢ -a✝ + a✝ = 0

pp: case refine_5
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝ + b✝ = b✝ + a✝

Tactic:
<;>

Goal state after:
case refine_1
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)

case refine_2
d : ℤ
a✝ : ℤ√d
⊢ 0 + a✝ = a✝

case refine_3
d : ℤ
a✝ : ℤ√d
⊢ a✝ + 0 = a✝

case refine_4
d : ℤ
a✝ : ℤ√d
⊢ -a✝ + a✝ = 0

case refine_5
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝ + b✝ = b✝ + a✝
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝ + c✝).re = (a✝ + (b✝ + c✝)).re

pp: case refine_1.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝ + c✝).im = (a✝ + (b✝ + c✝)).im

pp: case refine_2.re
d : ℤ
a✝ : ℤ√d
⊢ (0 + a✝).re = a✝.re

pp: case refine_2.im
d : ℤ
a✝ : ℤ√d
⊢ (0 + a✝).im = a✝.im

pp: case refine_3.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ + 0).re = a✝.re

pp: case refine_3.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ + 0).im = a✝.im

pp: case refine_4.re
d : ℤ
a✝ : ℤ√d
⊢ (-a✝ + a✝).re = re 0

pp: case refine_4.im
d : ℤ
a✝ : ℤ√d
⊢ (-a✝ + a✝).im = im 0

pp: case refine_5.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).re = (b✝ + a✝).re

pp: case refine_5.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).im = (b✝ + a✝).im

Tactic:
<;>

Goal state after:
case refine_1.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝ + c✝).re = (a✝ + (b✝ + c✝)).re

case refine_1.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝ + c✝).im = (a✝ + (b✝ + c✝)).im

case refine_2.re
d : ℤ
a✝ : ℤ√d
⊢ (0 + a✝).re = a✝.re

case refine_2.im
d : ℤ
a✝ : ℤ√d
⊢ (0 + a✝).im = a✝.im

case refine_3.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ + 0).re = a✝.re

case refine_3.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ + 0).im = a✝.im

case refine_4.re
d : ℤ
a✝ : ℤ√d
⊢ (-a✝ + a✝).re = re 0

case refine_4.im
d : ℤ
a✝ : ℤ√d
⊢ (-a✝ + a✝).im = im 0

case refine_5.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).re = (b✝ + a✝).re

case refine_5.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).im = (b✝ + a✝).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1
d : ℤ
⊢ ∀ (a b : ℤ√d), a + b = b + a

pp: case refine_2
d : ℤ
⊢ ∀ (a b c : ℤ√d), a * b * c = a * (b * c)

pp: case refine_3
d : ℤ
⊢ ∀ (a : ℤ√d), 1 * a = a

pp: case refine_4
d : ℤ
⊢ ∀ (a : ℤ√d), a * 1 = a

pp: case refine_5
d : ℤ
⊢ ∀ (a : ℤ√d), 0 * a = 0

pp: case refine_6
d : ℤ
⊢ ∀ (a : ℤ√d), a * 0 = 0

pp: case refine_7
d : ℤ
⊢ ∀ (a b c : ℤ√d), a * (b + c) = a * b + a * c

pp: case refine_8
d : ℤ
⊢ ∀ (a b c : ℤ√d), (a + b) * c = a * c + b * c

pp: case refine_9
d : ℤ
⊢ ∀ (a b : ℤ√d), a * b = b * a

Tactic:
<;>

Goal state after:
case refine_1
d : ℤ
⊢ ∀ (a b : ℤ√d), a + b = b + a

case refine_2
d : ℤ
⊢ ∀ (a b c : ℤ√d), a * b * c = a * (b * c)

case refine_3
d : ℤ
⊢ ∀ (a : ℤ√d), 1 * a = a

case refine_4
d : ℤ
⊢ ∀ (a : ℤ√d), a * 1 = a

case refine_5
d : ℤ
⊢ ∀ (a : ℤ√d), 0 * a = 0

case refine_6
d : ℤ
⊢ ∀ (a : ℤ√d), a * 0 = 0

case refine_7
d : ℤ
⊢ ∀ (a b c : ℤ√d), a * (b + c) = a * b + a * c

case refine_8
d : ℤ
⊢ ∀ (a b c : ℤ√d), (a + b) * c = a * c + b * c

case refine_9
d : ℤ
⊢ ∀ (a b : ℤ√d), a * b = b * a
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝ + b✝ = b✝ + a✝

pp: case refine_2
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)

pp: case refine_3
d : ℤ
a✝ : ℤ√d
⊢ 1 * a✝ = a✝

pp: case refine_4
d : ℤ
a✝ : ℤ√d
⊢ a✝ * 1 = a✝

pp: case refine_5
d : ℤ
a✝ : ℤ√d
⊢ 0 * a✝ = 0

pp: case refine_6
d : ℤ
a✝ : ℤ√d
⊢ a✝ * 0 = 0

pp: case refine_7
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝

pp: case refine_8
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝

pp: case refine_9
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝ * b✝ = b✝ * a✝

Tactic:
<;>

Goal state after:
case refine_1
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝ + b✝ = b✝ + a✝

case refine_2
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)

case refine_3
d : ℤ
a✝ : ℤ√d
⊢ 1 * a✝ = a✝

case refine_4
d : ℤ
a✝ : ℤ√d
⊢ a✝ * 1 = a✝

case refine_5
d : ℤ
a✝ : ℤ√d
⊢ 0 * a✝ = 0

case refine_6
d : ℤ
a✝ : ℤ√d
⊢ a✝ * 0 = 0

case refine_7
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝

case refine_8
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝

case refine_9
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝ * b✝ = b✝ * a✝
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).re = (b✝ + a✝).re

pp: case refine_1.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).im = (b✝ + a✝).im

pp: case refine_2.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * b✝ * c✝).re = (a✝ * (b✝ * c✝)).re

pp: case refine_2.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * b✝ * c✝).im = (a✝ * (b✝ * c✝)).im

pp: case refine_3.re
d : ℤ
a✝ : ℤ√d
⊢ (1 * a✝).re = a✝.re

pp: case refine_3.im
d : ℤ
a✝ : ℤ√d
⊢ (1 * a✝).im = a✝.im

pp: case refine_4.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 1).re = a✝.re

pp: case refine_4.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 1).im = a✝.im

pp: case refine_5.re
d : ℤ
a✝ : ℤ√d
⊢ (0 * a✝).re = re 0

pp: case refine_5.im
d : ℤ
a✝ : ℤ√d
⊢ (0 * a✝).im = im 0

pp: case refine_6.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 0).re = re 0

pp: case refine_6.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 0).im = im 0

pp: case refine_7.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * (b✝ + c✝)).re = (a✝ * b✝ + a✝ * c✝).re

pp: case refine_7.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * (b✝ + c✝)).im = (a✝ * b✝ + a✝ * c✝).im

pp: case refine_8.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ ((a✝ + b✝) * c✝).re = (a✝ * c✝ + b✝ * c✝).re

pp: case refine_8.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ ((a✝ + b✝) * c✝).im = (a✝ * c✝ + b✝ * c✝).im

pp: case refine_9.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ * b✝).re = (b✝ * a✝).re

pp: case refine_9.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ * b✝).im = (b✝ * a✝).im

Tactic:
<;>

Goal state after:
case refine_1.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).re = (b✝ + a✝).re

case refine_1.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).im = (b✝ + a✝).im

case refine_2.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * b✝ * c✝).re = (a✝ * (b✝ * c✝)).re

case refine_2.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * b✝ * c✝).im = (a✝ * (b✝ * c✝)).im

case refine_3.re
d : ℤ
a✝ : ℤ√d
⊢ (1 * a✝).re = a✝.re

case refine_3.im
d : ℤ
a✝ : ℤ√d
⊢ (1 * a✝).im = a✝.im

case refine_4.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 1).re = a✝.re

case refine_4.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 1).im = a✝.im

case refine_5.re
d : ℤ
a✝ : ℤ√d
⊢ (0 * a✝).re = re 0

case refine_5.im
d : ℤ
a✝ : ℤ√d
⊢ (0 * a✝).im = im 0

case refine_6.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 0).re = re 0

case refine_6.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 0).im = im 0

case refine_7.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * (b✝ + c✝)).re = (a✝ * b✝ + a✝ * c✝).re

case refine_7.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * (b✝ + c✝)).im = (a✝ * b✝ + a✝ * c✝).im

case refine_8.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ ((a✝ + b✝) * c✝).re = (a✝ * c✝ + b✝ * c✝).re

case refine_8.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ ((a✝ + b✝) * c✝).im = (a✝ * c✝ + b✝ * c✝).im

case refine_9.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ * b✝).re = (b✝ * a✝).re

case refine_9.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ * b✝).im = (b✝ * a✝).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.re + b✝.re = b✝.re + a✝.re

pp: case refine_1.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.im + b✝.im = b✝.im + a✝.im

pp: case refine_2.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re * b✝.re + d * a✝.im * b✝.im) * c✝.re + d * (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.im =
    a✝.re * (b✝.re * c✝.re + d * b✝.im * c✝.im) + d * a✝.im * (b✝.re * c✝.im + b✝.im * c✝.re)

pp: case refine_2.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re * b✝.re + d * a✝.im * b✝.im) * c✝.im + (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.re =
    a✝.re * (b✝.re * c✝.im + b✝.im * c✝.re) + a✝.im * (b✝.re * c✝.re + d * b✝.im * c✝.im)

pp: case refine_7.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝.re * (b✝.re + c✝.re) + d * a✝.im * (b✝.im + c✝.im) =
    a✝.re * b✝.re + d * a✝.im * b✝.im + (a✝.re * c✝.re + d * a✝.im * c✝.im)

pp: case refine_7.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝.re * (b✝.im + c✝.im) + a✝.im * (b✝.re + c✝.re) = a✝.re * b✝.im + a✝.im * b✝.re + (a✝.re * c✝.im + a✝.im * c✝.re)

pp: case refine_8.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re + b✝.re) * c✝.re + d * (a✝.im + b✝.im) * c✝.im =
    a✝.re * c✝.re + d * a✝.im * c✝.im + (b✝.re * c✝.re + d * b✝.im * c✝.im)

pp: case refine_8.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re + b✝.re) * c✝.im + (a✝.im + b✝.im) * c✝.re = a✝.re * c✝.im + a✝.im * c✝.re + (b✝.re * c✝.im + b✝.im * c✝.re)

pp: case refine_9.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.re * b✝.re + d * a✝.im * b✝.im = b✝.re * a✝.re + d * b✝.im * a✝.im

pp: case refine_9.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.re * b✝.im + a✝.im * b✝.re = b✝.re * a✝.im + b✝.im * a✝.re

Tactic:
<;>

Goal state after:
case refine_1.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.re + b✝.re = b✝.re + a✝.re

case refine_1.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.im + b✝.im = b✝.im + a✝.im

case refine_2.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re * b✝.re + d * a✝.im * b✝.im) * c✝.re + d * (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.im =
    a✝.re * (b✝.re * c✝.re + d * b✝.im * c✝.im) + d * a✝.im * (b✝.re * c✝.im + b✝.im * c✝.re)

case refine_2.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re * b✝.re + d * a✝.im * b✝.im) * c✝.im + (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.re =
    a✝.re * (b✝.re * c✝.im + b✝.im * c✝.re) + a✝.im * (b✝.re * c✝.re + d * b✝.im * c✝.im)

case refine_7.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝.re * (b✝.re + c✝.re) + d * a✝.im * (b✝.im + c✝.im) =
    a✝.re * b✝.re + d * a✝.im * b✝.im + (a✝.re * c✝.re + d * a✝.im * c✝.im)

case refine_7.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝.re * (b✝.im + c✝.im) + a✝.im * (b✝.re + c✝.re) = a✝.re * b✝.im + a✝.im * b✝.re + (a✝.re * c✝.im + a✝.im * c✝.re)

case refine_8.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re + b✝.re) * c✝.re + d * (a✝.im + b✝.im) * c✝.im =
    a✝.re * c✝.re + d * a✝.im * c✝.im + (b✝.re * c✝.re + d * b✝.im * c✝.im)

case refine_8.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re + b✝.re) * c✝.im + (a✝.im + b✝.im) * c✝.re = a✝.re * c✝.im + a✝.im * c✝.re + (b✝.re * c✝.im + b✝.im * c✝.re)

case refine_9.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.re * b✝.re + d * a✝.im * b✝.im = b✝.re * a✝.re + d * b✝.im * a✝.im

case refine_9.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.re * b✝.im + a✝.im * b✝.re = b✝.re * a✝.im + b✝.im * a✝.re
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case re
d : ℤ
a b : ℤ√d
⊢ (star (a * b)).re = (star b * star a).re

pp: case im
d : ℤ
a b : ℤ√d
⊢ (star (a * b)).im = (star b * star a).im

Tactic:
<;>

Goal state after:
case re
d : ℤ
a b : ℤ√d
⊢ (star (a * b)).re = (star b * star a).re

case im
d : ℤ
a b : ℤ√d
⊢ (star (a * b)).im = (star b * star a).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case re
d : ℤ
a b : ℤ√d
⊢ a.re * b.re + d * a.im * b.im = b.re * a.re + d * b.im * a.im

pp: case im
d : ℤ
a b : ℤ√d
⊢ -(a.im * b.re) + -(a.re * b.im) = -(b.re * a.im) + -(b.im * a.re)

Tactic:
<;>

Goal state after:
case re
d : ℤ
a b : ℤ√d
⊢ a.re * b.re + d * a.im * b.im = b.re * a.re + d * b.im * a.im

case im
d : ℤ
a b : ℤ√d
⊢ -(a.im * b.re) + -(a.re * b.im) = -(b.re * a.im) + -(b.im * a.re)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case ofNat
d : ℤ
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).re = Int.ofNat a✝

pp: case negSucc
d : ℤ
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).re = Int.negSucc a✝

Tactic:
<;>

Goal state after:
case ofNat
d : ℤ
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).re = Int.ofNat a✝

case negSucc
d : ℤ
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).re = Int.negSucc a✝
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case ofNat
d : ℤ
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).im = 0

pp: case negSucc
d : ℤ
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).im = 0

Tactic:
<;>

Goal state after:
case ofNat
d : ℤ
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).im = 0

case negSucc
d : ℤ
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).im = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case re
d n : ℤ
⊢ (↑n).re = { re := n, im := 0 }.re

pp: case im
d n : ℤ
⊢ (↑n).im = { re := n, im := 0 }.im

Tactic:
<;>

Goal state after:
case re
d n : ℤ
⊢ (↑n).re = { re := n, im := 0 }.re

case im
d n : ℤ
⊢ (↑n).im = { re := n, im := 0 }.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case re
d n : ℤ
⊢ (ofInt n).re = (↑n).re

pp: case im
d n : ℤ
⊢ (ofInt n).im = (↑n).im

Tactic:
<;>

Goal state after:
case re
d n : ℤ
⊢ (ofInt n).re = (↑n).re

case im
d n : ℤ
⊢ (ofInt n).im = (↑n).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case re
d : ℤ
n : ℕ
x y : ℤ
⊢ (↑n * { re := x, im := y }).re = { re := ↑n * x, im := ↑n * y }.re

pp: case im
d : ℤ
n : ℕ
x y : ℤ
⊢ (↑n * { re := x, im := y }).im = { re := ↑n * x, im := ↑n * y }.im

Tactic:
<;>

Goal state after:
case re
d : ℤ
n : ℕ
x y : ℤ
⊢ (↑n * { re := x, im := y }).re = { re := ↑n * x, im := ↑n * y }.re

case im
d : ℤ
n : ℕ
x y : ℤ
⊢ (↑n * { re := x, im := y }).im = { re := ↑n * x, im := ↑n * y }.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case re
d n x y : ℤ
⊢ (↑n * { re := x, im := y }).re = { re := n * x, im := n * y }.re

pp: case im
d n x y : ℤ
⊢ (↑n * { re := x, im := y }).im = { re := n * x, im := n * y }.im

Tactic:
<;>

Goal state after:
case re
d n x y : ℤ
⊢ (↑n * { re := x, im := y }).re = { re := n * x, im := n * y }.re

case im
d n x y : ℤ
⊢ (↑n * { re := x, im := y }).im = { re := n * x, im := n * y }.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case re
d x y : ℤ
⊢ (sqrtd * { re := x, im := y }).re = { re := d * y, im := x }.re

pp: case im
d x y : ℤ
⊢ (sqrtd * { re := x, im := y }).im = { re := d * y, im := x }.im

Tactic:
<;>

Goal state after:
case re
d x y : ℤ
⊢ (sqrtd * { re := x, im := y }).re = { re := d * y, im := x }.re

case im
d x y : ℤ
⊢ (sqrtd * { re := x, im := y }).im = { re := d * y, im := x }.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case re
d : ℤ
⊢ (sqrtd * sqrtd).re = (↑d).re

pp: case im
d : ℤ
⊢ (sqrtd * sqrtd).im = (↑d).im

Tactic:
<;>

Goal state after:
case re
d : ℤ
⊢ (sqrtd * sqrtd).re = (↑d).re

case im
d : ℤ
⊢ (sqrtd * sqrtd).im = (↑d).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case re
d n x y : ℤ
⊢ (sqrtd * ↑n * { re := x, im := y }).re = { re := d * n * y, im := n * x }.re

pp: case im
d n x y : ℤ
⊢ (sqrtd * ↑n * { re := x, im := y }).im = { re := d * n * y, im := n * x }.im

Tactic:
<;>

Goal state after:
case re
d n x y : ℤ
⊢ (sqrtd * ↑n * { re := x, im := y }).re = { re := d * n * y, im := n * x }.re

case im
d n x y : ℤ
⊢ (sqrtd * ↑n * { re := x, im := y }).im = { re := d * n * y, im := n * x }.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case re
d x y : ℤ
⊢ { re := x, im := y }.re = (↑x + sqrtd * ↑y).re

pp: case im
d x y : ℤ
⊢ { re := x, im := y }.im = (↑x + sqrtd * ↑y).im

Tactic:
<;>

Goal state after:
case re
d x y : ℤ
⊢ { re := x, im := y }.re = (↑x + sqrtd * ↑y).re

case im
d x y : ℤ
⊢ { re := x, im := y }.im = (↑x + sqrtd * ↑y).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case re
d x y : ℤ
⊢ ({ re := x, im := y } * star { re := x, im := y }).re = (↑x * ↑x - ↑d * ↑y * ↑y).re

pp: case im
d x y : ℤ
⊢ ({ re := x, im := y } * star { re := x, im := y }).im = (↑x * ↑x - ↑d * ↑y * ↑y).im

Tactic:
<;>

Goal state after:
case re
d x y : ℤ
⊢ ({ re := x, im := y } * star { re := x, im := y }).re = (↑x * ↑x - ↑d * ↑y * ↑y).re

case im
d x y : ℤ
⊢ ({ re := x, im := y } * star { re := x, im := y }).im = (↑x * ↑x - ↑d * ↑y * ↑y).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ (↑a * b).re = (↑a * c).re → b.re = c.re

pp: d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ (↑a * b).im = (↑a * c).im → b.im = c.im

Tactic:
<;>

Goal state after:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ (↑a * b).re = (↑a * c).re → b.re = c.re

d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ (↑a * b).im = (↑a * c).im → b.im = c.im
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case refine_1
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : ∃ t, p (v ⊗ t) = 0
⊢ ∃ t, p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0

pp: case refine_2
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : ∃ t, p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
⊢ ∃ t, p (v ⊗ t) = 0

Tactic:
<;>

Goal state after:
case refine_1
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : ∃ t, p (v ⊗ t) = 0
⊢ ∃ t, p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0

case refine_2
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : ∃ t, p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
⊢ ∃ t, p (v ⊗ t) = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1

pp: case refine_2
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d

pp: case refine_3
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d

pp: case refine_4
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
<;>

Goal state after:
case refine_1
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1

case refine_2
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d

case refine_3
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d

case refine_4
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inl
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
a : α
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) (inl a) = (v ⊗ t) (inl a)

pp: case inr
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
b : β
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) (inr b) = (v ⊗ t) (inr b)

Tactic:
<;>

Goal state after:
case inl
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
a : α
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) (inl a) = (v ⊗ t) (inl a)

case inr
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
b : β
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) (inr b) = (v ⊗ t) (inr b)