mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
β : Type v
a✝ : α
f : α → Seq1 β
a : β
⊢ join ((a, nil), nil) = (a, nil)

pp: case cons
α : Type u
β : Type v
a✝ : α
f : α → Seq1 β
a x✝ : β
s✝ : Seq β
⊢ join ((a, Seq.cons x✝ s✝), nil) = (a, Seq.cons x✝ s✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
a✝ : α
f : α → Seq1 β
a : β
⊢ join ((a, nil), nil) = (a, nil)

case cons
α : Type u
β : Type v
a✝ : α
f : α → Seq1 β
a x✝ : β
s✝ : Seq β
⊢ join ((a, Seq.cons x✝ s✝), nil) = (a, Seq.cons x✝ s✝)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
β : Type v
f : α → β
a : α
S : Seq (Seq1 α)
⊢ map f (join ((a, nil), S)) = (map (map f) ((a, nil), S)).join

pp: case cons
α : Type u
β : Type v
f : α → β
a : α
S : Seq (Seq1 α)
x✝ : α
s✝ : Seq α
⊢ map f (join ((a, Seq.cons x✝ s✝), S)) = (map (map f) ((a, Seq.cons x✝ s✝), S)).join

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
f : α → β
a : α
S : Seq (Seq1 α)
⊢ map f (join ((a, nil), S)) = (map (map f) ((a, nil), S)).join

case cons
α : Type u
β : Type v
f : α → β
a : α
S : Seq (Seq1 α)
x✝ : α
s✝ : Seq α
⊢ map f (join ((a, Seq.cons x✝ s✝), S)) = (map (map f) ((a, Seq.cons x✝ s✝), S)).join
Module: Mathlib.Data.Seq.Basic

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

pp: case cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a x : γ
s_1 : Seq γ
⊢ (join (((a, Seq.cons x s_1), S), SS)).join = join (join ((a, Seq.cons x s_1), S), Seq.map join SS)

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
⊢ (join (((a, nil), S), SS)).join = join (join ((a, nil), S), Seq.map join SS)

case cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a x : γ
s_1 : Seq γ
⊢ (join (((a, Seq.cons x s_1), S), SS)).join = join (join ((a, Seq.cons x s_1), S), Seq.map join SS)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil.cons.nil
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x : γ
⊢ (join (((a, nil), Seq.cons (x, nil) s_2), SS)).join = join (join ((a, nil), Seq.cons (x, nil) s_2), Seq.map join SS)

pp: case nil.cons.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x x✝ : γ
s✝ : Seq γ
⊢ (join (((a, nil), Seq.cons (x, Seq.cons x✝ s✝) s_2), SS)).join =
    join (join ((a, nil), Seq.cons (x, Seq.cons x✝ s✝) s_2), Seq.map join SS)

Tactic:
<;>

Goal state after:
case nil.cons.nil
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x : γ
⊢ (join (((a, nil), Seq.cons (x, nil) s_2), SS)).join = join (join ((a, nil), Seq.cons (x, nil) s_2), Seq.map join SS)

case nil.cons.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x x✝ : γ
s✝ : Seq γ
⊢ (join (((a, nil), Seq.cons (x, Seq.cons x✝ s✝) s_2), SS)).join =
    join (join ((a, nil), Seq.cons (x, Seq.cons x✝ s✝) s_2), Seq.map join SS)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminatedAt_succ_n : s.get? (n + 1) = none
s_nth_eq : s.get? n = none
⊢ squashSeq s n = s

pp: case some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminatedAt_succ_n : s.get? (n + 1) = none
val✝ : Pair K
s_nth_eq : s.get? n = some val✝
⊢ squashSeq s n = s

Tactic:
<;>

Goal state after:
case none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminatedAt_succ_n : s.get? (n + 1) = none
s_nth_eq : s.get? n = none
⊢ squashSeq s n = s

case some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
terminatedAt_succ_n : s.get? (n + 1) = none
val✝ : Pair K
s_nth_eq : s.get? n = some val✝
⊢ squashSeq s n = s
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case none.none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_succ_nth_eq : s.get? (n + 2) = none
s_succ_nth_eq : s.get? (n + 1) = none
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

pp: case none.some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_succ_nth_eq : s.get? (n + 2) = none
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

Tactic:
<;>

Goal state after:
case none.none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_succ_nth_eq : s.get? (n + 2) = none
s_succ_nth_eq : s.get? (n + 1) = none
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

case none.some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_succ_nth_eq : s.get? (n + 2) = none
val✝ : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val✝
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n
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
n : ℕ
⊢ ∃ conts, (of v).conts n = Pair.map Rat.cast conts

Tactic:
rw [nth_cont_eq_succ_nth_contAux]; exact exists_gcf_pair_rat_eq_of_nth_contsAux v <| n + 1

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

Goal state before:
pp: case zero.none
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
g_s_head_eq : g.s.get? 0 = none
⊢ g.convs' (0 + 1) = (g.squashGCF 0).convs' 0

pp: case zero.some
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
val✝ : Pair K
g_s_head_eq : g.s.get? 0 = some val✝
⊢ g.convs' (0 + 1) = (g.squashGCF 0).convs' 0

Tactic:
<;>

Goal state after:
case zero.none
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
g_s_head_eq : g.s.get? 0 = none
⊢ g.convs' (0 + 1) = (g.squashGCF 0).convs' 0

case zero.some
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
val✝ : Pair K
g_s_head_eq : g.s.get? 0 = some val✝
⊢ g.convs' (0 + 1) = (g.squashGCF 0).convs' 0
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case none
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
succ_nth_stream_eq : IntFractPair.stream q (n + 1) = none
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p ↦ { a := 1, b := ↑p.b }) none) =
    Option.map (fun p ↦ { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))

pp: case some
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
b✝ : ℤ
fr✝ : ℚ
succ_nth_stream_eq : IntFractPair.stream q (n + 1) = some { b := b✝, fr := fr✝ }
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p ↦ { a := 1, b := ↑p.b }) (some { b := b✝, fr := fr✝ })) =
    Option.map (fun p ↦ { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))

Tactic:
<;>

Goal state after:
case none
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
succ_nth_stream_eq : IntFractPair.stream q (n + 1) = none
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p ↦ { a := 1, b := ↑p.b }) none) =
    Option.map (fun p ↦ { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))

case some
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
b✝ : ℤ
fr✝ : ℚ
succ_nth_stream_eq : IntFractPair.stream q (n + 1) = some { b := b✝, fr := fr✝ }
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p ↦ { a := 1, b := ↑p.b }) (some { b := b✝, fr := fr✝ })) =
    Option.map (fun p ↦ { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case none
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : (of q).s.get? n = none
⊢ (of v).s.TerminatedAt n ↔ (of q).s.TerminatedAt n

pp: case some
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
val✝ : Pair ℚ
h : (of q).s.get? n = some val✝
⊢ (of v).s.TerminatedAt n ↔ (of q).s.TerminatedAt n

Tactic:
<;>

Goal state after:
case none
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
h : (of q).s.get? n = none
⊢ (of v).s.TerminatedAt n ↔ (of q).s.TerminatedAt n

case some
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
val✝ : Pair ℚ
h : (of q).s.get? n = some val✝
⊢ (of v).s.TerminatedAt n ↔ (of q).s.TerminatedAt n
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case 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
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).a =
    P.a

pp: case b
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
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).b =
    P.b

pp: case c
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
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).c =
    P.c

pp: case d
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
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).d =
    P.d

Tactic:
<;>

Goal state after:
case 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
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).a =
    P.a

case b
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
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).b =
    P.b

case c
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
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).c =
    P.c

case d
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
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).d =
    P.d
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inl.«0»
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 : 0 ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      0 =
    (↑f).coeff 0

pp: case inl.«1»
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 : 1 ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      1 =
    (↑f).coeff 1

pp: case inl.«2»
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 : 2 ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      2 =
    (↑f).coeff 2

pp: case inl.«3»
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 ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      3 =
    (↑f).coeff 3

Tactic:
<;>

Goal state after:
case inl.«0»
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 : 0 ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      0 =
    (↑f).coeff 0

case inl.«1»
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 : 1 ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      1 =
    (↑f).coeff 1

case inl.«2»
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 : 2 ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      2 =
    (↑f).coeff 2

case inl.«3»
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 ≤ 3
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      3 =
    (↑f).coeff 3
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inl.«0»
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 : 0 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 0 = (↑f).coeff 0

pp: case inl.«1»
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 : 1 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 1 = (↑f).coeff 1

pp: case inl.«2»
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 : 2 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 2 = (↑f).coeff 2

pp: case inl.«3»
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 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 3 = (↑f).coeff 3

Tactic:
<;>

Goal state after:
case inl.«0»
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 : 0 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 0 = (↑f).coeff 0

case inl.«1»
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 : 1 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 1 = (↑f).coeff 1

case inl.«2»
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 : 2 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 2 = (↑f).coeff 2

case inl.«3»
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 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 3 = (↑f).coeff 3
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case none
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
j : Option I
ne : none ≠ j
⊢ none.elim x e * j.elim x e = 0

pp: case some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
j : Option I
i : I
ne : some i ≠ j
⊢ (some i).elim x e * j.elim x e = 0

Tactic:
<;>

Goal state after:
case none
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
j : Option I
ne : none ≠ j
⊢ none.elim x e * j.elim x e = 0

case some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
j : Option I
i : I
ne : some i ≠ j
⊢ (some i).elim x e * j.elim x e = 0
Module: Mathlib.RingTheory.TensorProduct.Free

Goal state before:
pp: R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ 1 ⊗ₜ[R] ((b'.linearMap b) ij) (b' k) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') k)

Tactic:
Basis.linearMap_apply_apply,

Goal state after:
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ (1 ⊗ₜ[R] if ij.2 = k then b ij.1 else 0) = if ij.2 = k then (basis A b) ij.1 else 0
Module: Mathlib.RingTheory.TensorProduct.Free

Goal state before:
pp: case isTrue
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
h✝ : ij.2 = k
⊢ 1 ⊗ₜ[R] b ij.1 = 1 ⊗ₜ[R] b ij.1

pp: case isFalse
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
h✝ : ¬ij.2 = k
⊢ 1 ⊗ₜ[R] 0 = 0

Tactic:
<;>

Goal state after:
case isTrue
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
h✝ : ij.2 = k
⊢ 1 ⊗ₜ[R] b ij.1 = 1 ⊗ₜ[R] b ij.1

case isFalse
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
h✝ : ¬ij.2 = k
⊢ 1 ⊗ₜ[R] 0 = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case succ.none
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i, e' i = 0
h₆ : (∑ i, e' i) * e₀ = 0
⊢ (⇑f ∘ (fun x ↦ x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) ((finSuccEquiv n).symm none) =
    e ((finSuccEquiv n).symm none)

pp: case succ.some
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i, e' i = 0
h₆ : (∑ i, e' i) * e₀ = 0
i : Fin n
⊢ (⇑f ∘ (fun x ↦ x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) ((finSuccEquiv n).symm (some i)) =
    e ((finSuccEquiv n).symm (some i))

Tactic:
<;>

Goal state after:
case succ.none
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i, e' i = 0
h₆ : (∑ i, e' i) * e₀ = 0
⊢ (⇑f ∘ (fun x ↦ x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) ((finSuccEquiv n).symm none) =
    e ((finSuccEquiv n).symm none)

case succ.some
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i, e' i = 0
h₆ : (∑ i, e' i) * e₀ = 0
i : Fin n
⊢ (⇑f ∘ (fun x ↦ x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) ((finSuccEquiv n).symm (some i)) =
    e ((finSuccEquiv n).symm (some i))