mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
s_nth_eq : g.s.get? n = some { a := 1, b := ifp_n.fr⁻¹ }
this : v = compExactValue ppconts pconts ifp_n.fr
⊢ v = conts.a / conts.b

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
s_nth_eq : g.s.get? n = some { a := 1, b := ifp_n.fr⁻¹ }
this : v = compExactValue ppconts pconts ifp_n.fr
⊢ v =
    (nextConts 1 ifp_n.fr⁻¹ (g.contsAux n) (g.contsAux (n + 1))).a /
      (nextConts 1 ifp_n.fr⁻¹ (g.contsAux n) (g.contsAux (n + 1))).b
Module: Mathlib.Data.Nat.DvdSequence

Goal state before:
pp: f : ℕ → ℕ
hf : IsStrongDvdSequence f
a b : ℕ
hab : a ∣ b
⊢ f a ∣ f b

Tactic:
simpa using

Goal state after:
f : ℕ → ℕ
hf : IsStrongDvdSequence f
a b : ℕ
hab : a ∣ b
⊢ f a ∣ f b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
x : α
n : ℕ
hx : some x = tl.get? n
⊢ R hd x

Tactic:
simpa using

Goal state after:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
x : α
n : ℕ
hx : some x = tl.get? n
⊢ R hd x
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
hd tl_hd : α
tl_tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (cons hd (cons tl_hd tl_tl)).get? i, ∀ y ∈ (cons hd (cons tl_hd tl_tl)).get? j, R x y
⊢ R hd tl_hd

Tactic:
simpa using

Goal state after:
α : Type u
R : α → α → Prop
hd tl_hd : α
tl_tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (cons hd (cons tl_hd tl_tl)).get? i, ∀ y ∈ (cons hd (cons tl_hd tl_tl)).get? j, R x y
⊢ R hd tl_hd
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ n.fastFib = fib n

Tactic:
fastFib,

Goal state after:
n : ℕ
⊢ n.fastFibAux.1 = fib n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.cons
α : Type u
β : Type v
f : α → β
S✝ S : Seq (Seq1 α)
a : α
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join)
    (nil.append (Seq.map f (Seq.cons (a, s) S).join)).destruct
    (nil.append (Seq.map (map f) (Seq.cons (a, s) S)).join).destruct

Tactic:
simpa using

Goal state after:
case bisim.nil.cons
α : Type u
β : Type v
f : α → β
S✝ S : Seq (Seq1 α)
a : α
s : Seq α
⊢ ∃ s_1 S_1,
    (Seq.map f s).append (Seq.map f S.join) = s_1.append (Seq.map f S_1.join) ∧
      (Seq.map f s).append (Seq.map (map f) S).join = s_1.append (Seq.map (map f) S_1).join
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.cons
α : Type u
β : Type v
f : α → β
S✝ S : Seq (Seq1 α)
x✝ : β
s : Seq β
⊢ BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join)
    ((Seq.cons x✝ s).append (Seq.map f S.join)).destruct ((Seq.cons x✝ s).append (Seq.map (map f) S).join).destruct

Tactic:
simpa using

Goal state after:
case bisim.cons
α : Type u
β : Type v
f : α → β
S✝ S : Seq (Seq1 α)
x✝ : β
s : Seq β
⊢ ∃ s_1 S_1,
    s.append (Seq.map f S.join) = s_1.append (Seq.map f S_1.join) ∧
      s.append (Seq.map (map f) S).join = s_1.append (Seq.map (map f) S_1).join
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case r
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ ∃ s S_1,
    Seq.map f S.join = s.append (Seq.map f S_1.join) ∧ (Seq.map (map f) S).join = s.append (Seq.map (map f) S_1).join

Tactic:
simpa using

Goal state after:
case r
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ ∃ s S_1,
    Seq.map f S.join = s.append (Seq.map f S_1.join) ∧ (Seq.map (map f) S).join = s.append (Seq.map (map f) S_1).join
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.cons.nil
α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
⊢ BisimO (fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join)
    (nil.append (Seq.cons ((x, nil), S) SS).join.join).destruct
    (nil.append (Seq.map join (Seq.cons ((x, nil), S) SS)).join).destruct

Tactic:
simpa using

Goal state after:
case bisim.nil.cons.nil
α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
⊢ ∃ s SS_1,
    S.join.append SS.join.join = s.append SS_1.join.join ∧
      S.join.append (Seq.map join SS).join = s.append (Seq.map join SS_1).join
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.cons.cons
α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x✝ x : α
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join)
    (nil.append (Seq.cons ((x✝, Seq.cons x s), S) SS).join.join).destruct
    (nil.append (Seq.map join (Seq.cons ((x✝, Seq.cons x s), S) SS)).join).destruct

Tactic:
simpa using

Goal state after:
case bisim.nil.cons.cons
α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x✝ x : α
s : Seq α
⊢ ∃ s_1 SS_1,
    Seq.cons x (s.append (S.join.append SS.join.join)) = s_1.append SS_1.join.join ∧
      Seq.cons x (s.append (S.join.append (Seq.map join SS).join)) = s_1.append (Seq.map join SS_1).join
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.cons
α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
x✝ : α
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join)
    ((Seq.cons x✝ s).append SS.join.join).destruct ((Seq.cons x✝ s).append (Seq.map join SS).join).destruct

Tactic:
simpa using

Goal state after:
case bisim.cons
α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
x✝ : α
s : Seq α
⊢ ∃ s_1 SS_1,
    s.append SS.join.join = s_1.append SS_1.join.join ∧
      s.append (Seq.map join SS).join = s_1.append (Seq.map join SS_1).join
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case r
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ ∃ s SS_1, SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join

Tactic:
simpa using

Goal state after:
case r
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ ∃ s SS_1, SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map join (Seq.map (map g ∘ f) s))

Tactic:
generalize Seq.map (map g ∘ f) s = SS

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
⊢ (join (map g (f a), SS)).join = join ((map g (f a)).join, Seq.map join SS)
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < 0, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
this : ∃ gp, { a := 1, b := 0 } = Pair.map Rat.cast gp
⊢ ∃ conts, (of v).contsAux 0 = Pair.map Rat.cast conts

Tactic:
simpa [contsAux]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < 0 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
this : ∃ conts, { a := g.h, b := 1 } = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux (0 + 1) = Pair.map Rat.cast conts

Tactic:
simpa [contsAux]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
gp_n : Pair K
s_nth_eq : s.get? n = some gp_n
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
simp [*, squashSeq, m_lt_n.ne]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case succ.succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)

Tactic:
· -- get some inequalities to instantiate the IH for m'' and m'' + 1
            have m'_lt_n : m'' + 1 < n' + 1 := m_le_n
            have succ_m''th_contsAux_eq := IH (m'' + 1) (lt_add_one (m'' + 1)) m'_lt_n.le
            have : m'' < m'' + 2 := lt_add_of_pos_right m'' zero_lt_two
            have m''th_contsAux_eq := IH m'' this (le_trans this.le m_le_n)
            have : (squashGCF g (n' + 1)).s.get? m'' = g.s.get? m'' :=
              squashGCF_nth_of_lt (Nat.succ_lt_succ_iff.mp m'_lt_n)
            simp [contsAux, succ_m''th_contsAux_eq, m''th_contsAux_eq, this]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: K : Type u_1
v : K
inst✝⁶ : Field K
inst✝⁵ : LinearOrder K
inst✝⁴ : IsStrictOrderedRing K
inst✝³ : FloorRing K
inst✝² : Archimedean K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
⊢ Filter.Tendsto (of v).convs Filter.atTop (𝓝 v)

Tactic:
simpa using

Goal state after:
K : Type u_1
v : K
inst✝⁶ : Field K
inst✝⁵ : LinearOrder K
inst✝⁴ : IsStrictOrderedRing K
inst✝³ : FloorRing K
inst✝² : Archimedean K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
⊢ ∀ (ε : K), 0 < ε → ∃ a, ∀ (b : ℕ), a ≤ b → |v - (of v).convs b| < ε
Module: Mathlib.Algebra.DirectSum.AddChar

Goal state before:
pp: ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (G i)
inst✝ : CommMonoid R
ψ χ : (i : ι) → AddChar (G i) R
h : (fun ψ i ↦ toAddMonoidHomEquiv (ψ i)) ψ = (fun ψ i ↦ toAddMonoidHomEquiv (ψ i)) χ
⊢ ψ = χ

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (G i)
inst✝ : CommMonoid R
ψ χ : (i : ι) → AddChar (G i) R
h : (fun ψ i ↦ toAddMonoidHomEquiv (ψ i)) ψ = (fun ψ i ↦ toAddMonoidHomEquiv (ψ i)) χ
⊢ ∀ (x : ι), ψ x = χ x
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
b✝ : ℤ
ifp_n_fr : K
nth_stream_eq : IntFractPair.stream v n = some { b := b✝, fr := ifp_n_fr }
this✝ : ↑⌊{ b := b✝, fr := ifp_n_fr }.fr⁻¹⌋ ≤ { b := b✝, fr := ifp_n_fr }.fr⁻¹
this : ifp_n_fr ≠ 0
⊢ IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n

Tactic:
simpa using

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
b✝ : ℤ
ifp_n_fr : K
nth_stream_eq : IntFractPair.stream v n = some { b := b✝, fr := ifp_n_fr }
this✝ : ↑⌊{ b := b✝, fr := ifp_n_fr }.fr⁻¹⌋ ≤ { b := b✝, fr := ifp_n_fr }.fr⁻¹
this : ifp_n_fr ≠ 0
⊢ IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inr.a
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 3 < n
⊢ 3 < ↑n

Tactic:
simpa using

Goal state after:
case inr.a
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 3 < n
⊢ 3 < n
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
⊢ P.toPoly.degree ≤ 2

Tactic:
simpa using

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
⊢ (C P.b * X ^ 2 + C P.c * X + C P.d).degree ≤ 2
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
this : 1 ≤ b
⊢ g.dens n ≤ b * g.dens n

Tactic:
simpa using

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
this : 1 ≤ b
⊢ g.dens n ≤ b * g.dens n
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
⊢ P.toPoly.degree ≤ 1

Tactic:
simpa using

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
⊢ (C P.c * X + C P.d).degree ≤ 1
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ P.toPoly.degree ≤ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ (C P.d).degree ≤ 0
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
⊢ P.toPoly.natDegree ≤ 2

Tactic:
simpa using

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
⊢ (C P.b * X ^ 2 + C P.c * X + C P.d).natDegree ≤ 2
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
⊢ P.toPoly.natDegree ≤ 1

Tactic:
simpa using

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
⊢ (C P.c * X + C P.d).natDegree ≤ 1
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (map φ P).toPoly = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)

Tactic:
rw [map_toPoly,
    Splits.eq_prod_roots <|
      (splits_iff_roots_eq_three ha).mpr <| Exists.intro x <| Exists.intro y <| Exists.intro z h3,
    leadingCoeff_map, leadingCoeff_of_a_ne_zero ha, ← map_roots, h3]

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ C (φ P.a) * (Multiset.map (fun x ↦ X - C x) {x, y, z}).prod = C (φ P.a) * (X - C x) * (X - C y) * (X - C z)
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (φ P.a * -(x + y + z)) ^ 2 * (φ P.a * (x * y + x * z + y * z)) ^ 2 -
            4 * φ P.a * (φ P.a * (x * y + x * z + y * z)) ^ 3 -
          4 * (φ P.a * -(x + y + z)) ^ 3 * φ P.d -
        27 * φ P.a ^ 2 * φ P.d ^ 2 +
      18 * φ P.a * (φ P.a * -(x + y + z)) * (φ P.a * (x * y + x * z + y * z)) * φ P.d =
    (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2

Tactic:
d_eq_three_roots ha h3

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (φ P.a * -(x + y + z)) ^ 2 * (φ P.a * (x * y + x * z + y * z)) ^ 2 -
            4 * φ P.a * (φ P.a * (x * y + x * z + y * z)) ^ 3 -
          4 * (φ P.a * -(x + y + z)) ^ 3 * (φ P.a * -(x * y * z)) -
        27 * φ P.a ^ 2 * (φ P.a * -(x * y * z)) ^ 2 +
      18 * φ P.a * (φ P.a * -(x + y + z)) * (φ P.a * (x * y + x * z + y * z)) * (φ P.a * -(x * y * z)) =
    (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
Module: Mathlib.RingTheory.TensorProduct.Free

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
i : ι
⊢ a • (basis A b) i = a ⊗ₜ[R] b i

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
i : ι
⊢ a • 1 ⊗ₜ[R] b i = a ⊗ₜ[R] b i
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Subsingleton V
a✝ : Nontrivial W
⊢ ∃ T, f = conjAlgEquiv K T

Tactic:
simpa using

Goal state after:
K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Subsingleton V
a✝ : Nontrivial W
⊢ ∃ T, f = conjAlgEquiv K T
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →ₗ[K] W := applyₗ z ∘ₗ f.toLinearMap ∘ₗ smulRightₗ v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : End K V) (x : V), T (A x) = (f A) (T x)
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
h_smul : (smulRightₗ v) x = (smulRightₗ v) y
⊢ x = y

Tactic:
simpa using

Goal state after:
K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →ₗ[K] W := applyₗ z ∘ₗ f.toLinearMap ∘ₗ smulRightₗ v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : End K V) (x : V), T (A x) = (f A) (T x)
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
h_smul : (smulRightₗ v) x = (smulRightₗ v) y
⊢ x = y
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
k : Rᵐᵒᵖ
hk : MulOpposite.unop (1 ^ n - MulOpposite.op (1 - a ^ n) ^ n) = MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
⊢ 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
k : Rᵐᵒᵖ
hk : MulOpposite.unop (1 ^ n - MulOpposite.op (1 - a ^ n) ^ n) = MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
⊢ 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : S
he : e ∈ f.range
he' : IsIdempotentElem e
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = e

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : S
he : e ∈ f.range
he' : IsIdempotentElem e
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = e
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
c : Con M
f g : ι → M
h : ∀ x ∈ [], c (f x) (g x)
⊢ c (List.map f []).prod (List.map g []).prod

Tactic:
simpa using

Goal state after:
case nil
ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
c : Con M
f g : ι → M
h : ∀ x ∈ [], c (f x) (g x)
⊢ c 1 1
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Finite I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : OrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
val✝ : Fintype I
e' : Fin (Fintype.card I) → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm.toEmbedding
x : I
⊢ (⇑f ∘ e' ∘ ⇑(Fintype.equivFin I).toEmbedding) x = e x

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Finite I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : OrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
val✝ : Fintype I
e' : Fin (Fintype.card I) → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm.toEmbedding
x : I
⊢ f (e' ((Fintype.equivFin I) x)) = e x
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: case mk
ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
c : Con M
s : Multiset ι
f g : ι → M
a✝ : List ι
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid ι)) a✝, c (f x) (g x)
⊢ c (Multiset.map f (Quot.mk (⇑(List.isSetoid ι)) a✝)).prod (Multiset.map g (Quot.mk (⇑(List.isSetoid ι)) a✝)).prod

Tactic:
simpa using

Goal state after:
case mk
ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
c : Con M
s : Multiset ι
f g : ι → M
a✝ : List ι
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid ι)) a✝, c (f x) (g x)
⊢ c (List.map f a✝).prod (List.map g a✝).prod
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
c : Con M
s : Multiset ι
f : ι → M
⊢ ↑(Multiset.map f s).prod = (Multiset.map (fun i ↦ ↑(f i)) s).prod

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
c : Con M
s : Multiset ι
f : ι → M
⊢ ↑(Multiset.map f s).prod = (Multiset.map (fun i ↦ ↑(f i)) s).prod
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.inr.zero
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
h✝¹ : Nontrivial R
h✝ : Nontrivial S
e : Fin 0 → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin 0), e i ∈ f.range
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
simpa using

Goal state after:
case inr.inr.zero
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
h✝¹ : Nontrivial R
h✝ : Nontrivial S
e : Fin 0 → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin 0), e i ∈ f.range
⊢ CompleteOrthogonalIdempotents ![] ∧ ⇑f ∘ ![] = e