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

Goal state before:
pp: case a
α : Type u
s : Computation α
h : s.Terminates
⊢ (s.think.val s.think.length).isSome = true → s.length + 1 ≤ s.think.length

Tactic:
rcases length (think s) with - | n <;> intro this

Goal state after:
case a.zero
α : Type u
s : Computation α
h : s.Terminates
this : (s.think.val 0).isSome = true
⊢ s.length + 1 ≤ 0

case a.succ
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (s.think.val (n + 1)).isSome = true
⊢ s.length + 1 ≤ n + 1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

pp: case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

Tactic:
· simpa [length'_of_terminates h] using length_le_iff

Goal state after:
case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
δ : Type w
m n : ℕ
x y : List α
a✝ b : Stream' α
a : α
⊢ [a] ≠ []

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s
s : Stream' α
⊢ s.inits.get (n + 1) = take (n + 1).succ s

Tactic:
rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ}, k < n → s.get? k = some x → x ∈ take n s
s : Seq α
n : ℕ
h_mn : k + 1 < n
h_get : s.get? (k + 1) = some x
⊢ x ∈ take n s

Tactic:
| succ k ih =>

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
l : List α
⊢ ↑((↑l).toList ⋯) = ↑l

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredB predB : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_den_eq : g.dens n = ppredB
succ_nth_den_eq : g.dens (n + 1) = predB
⊢ g.dens (n + 2) = gp.b * predB + gp.a * ppredB

Tactic:
obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.conts n = conts ∧ conts.b = ppredB :=
    exists_conts_b_of_den nth_den_eq

Goal state after:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predB : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
succ_nth_den_eq : g.dens (n + 1) = predB
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
⊢ g.dens (n + 2) = gp.b * predB + gp.a * ppredConts.b
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: K : Type u_1
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
n_le_m : n ≤ m
terminatedAt_n : s.TerminatedAt n
⊢ convs'Aux s m = convs'Aux s n

Tactic:
induction n_le_m with
  | refl => rfl
  | step n_le_m IH =>
    refine (convs'Aux_stable_step_of_terminated (?_)).trans IH
    exact s.terminated_stable n_le_m terminatedAt_n

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s t u✝ : Seq α
x✝ : α
u : Seq α
⊢ u = (nil.append nil).append u

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s t u✝ : Seq α
x✝ : α
u : Seq α
⊢ u = nil.append (nil.append u)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s t✝ u✝ u : Seq α
x✝ : α
t : Seq α
⊢ t.append u = (nil.append t).append u

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s t✝ u✝ u : Seq α
x✝ : α
t : Seq α
⊢ t.append u = nil.append (t.append u)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s t✝ : Seq α
x✝ : α
t : Seq α
⊢ map f t = map f (nil.append t)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s t✝ : Seq α
x✝ : α
t : Seq α
⊢ map f t = (map f nil).append (map f t)

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ IntFractPair.stream v (n + 1) = none ↔
    IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0

Tactic:
rw [IntFractPair.stream]
  cases IntFractPair.stream v n <;> simp [imp_false]

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
F : DirectLimit G f →+* P
i j : ι
hij : i ≤ j
x : G i
⊢ (F.comp (of G f j)) (f i j hij x) = (F.comp (of G f i)) x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
i j : ι
hij : i ≤ j
x : G i
⊢ (of G f j) (f i j hij x) = (of G f i) x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
S T✝ T : Seq (Seq1 α)
a : α
s : Seq α
⊢ s.append T.join = s.append (nil.append T).join

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
S T✝ T : Seq (Seq1 α)
a : α
s : Seq α
⊢ s.append T.join = s.append (nil.join.append T.join)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
S T : Seq (Seq1 α)
⊢ (S.append T).join = nil.append (S.append T).join

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
S T : Seq (Seq1 α)
⊢ S.join.append T.join = nil.append (S.join.append T.join)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
⊢ (s.drop (k + 1)).get? m = s.get? (k + 1 + m)

Tactic:
| succ k ih =>

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

Goal state before:
pp: case succ
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
n✝ : ℕ
a✝ : (of ↑a).convs' n✝ = ↑a
⊢ (of ↑a).convs' (n✝ + 1) = ↑a

Tactic:
convs',

Goal state after:
case succ
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
n✝ : ℕ
a✝ : (of ↑a).convs' n✝ = ↑a
⊢ (of ↑a).h + convs'Aux (of ↑a).s (n✝ + 1) = ↑a
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ (of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

Tactic:
convs',

Goal state after:
case inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ (of v).h + convs'Aux (of v).s (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convs'Aux (of v).s.tail n = (of (fract v)⁻¹).convs' n

Tactic:
convs',

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convs'Aux (of v).s.tail n = (of (fract v)⁻¹).h + convs'Aux (of (fract v)⁻¹).s n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
t : Seq α
ih : motive t
⊢ motive t.tail

Tactic:
cases t

Goal state after:
case succ.nil
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
ih : motive nil
⊢ motive nil.tail

case succ.cons
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
x✝ : α
s✝ : Seq α
ih : motive (cons x✝ s✝)
⊢ motive (cons x✝ s✝).tail
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
⊢ fib m < fib 0 ↔ m < 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
⊢ fib m < fib 1 ↔ m < 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ n + 2 ∈ Set.Ici 2

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α}, s.get? n = some x → s.get? (n + 1) = some y → R x y
i : ℕ
x : α
hx : x ∈ s.get? i
k : ℕ
ih : ∀ y ∈ s.get? (i + k + 1), R x y
y : α
hy : y ∈ s.get? (i + (k + 1) + 1)
⊢ R x y

Tactic:
| succ k ih =>

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ.cons
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
m : ℕ
tb_hd : β
tb_tl : Seq β
ih : cons tb_hd tb_tl ≠ nil → motive (a.drop m) (cons tb_hd tb_tl)
hb : (cons tb_hd tb_tl).tail ≠ nil
⊢ motive (a.drop m).tail (cons tb_hd tb_tl).tail

Tactic:
| cons tb_hd tb_tl =>

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: m n : ℕ
⊢ (fib m).gcd (fib (n + 0 * m)) = (fib m).gcd (fib n)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x✝ x : α
s : Seq α
⊢ Seq.cons x (s.append (S.join.append SS.join.join)) = (Seq.cons x (s.append S.join)).append SS.join.join

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x✝ x : α
s : Seq α
⊢ Seq.cons x (s.append (S.join.append (Seq.map join SS).join)) =
    (Seq.cons x (s.append S.join)).append (Seq.map join SS).join

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ SS.join.join = nil.append SS.join.join

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ (Seq.map join SS).join = nil.append (Seq.map join SS).join

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

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

Tactic:
cases t

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.Computation.TerminatesIffRat

Goal state before:
pp: case succ.zero
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
⊢ ∃ conts, (of v).contsAux (0 + 1) = Pair.map Rat.cast conts

Tactic:
suffices ∃ conts : Pair ℚ, Pair.mk g.h 1 = conts.map (↑) by simpa [contsAux]

Goal state after:
case succ.zero
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
⊢ ∃ conts, { a := g.h, b := 1 } = Pair.map Rat.cast conts
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.some.inr
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 : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
· have : (fr : K)⁻¹ = ((fr⁻¹ : ℚ) : K) := by norm_cast
        have coe_of_fr := coe_of_rat_eq this
        simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]

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
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p ↦ { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    Option.map (fun p ↦ { a := 1, b := ↑p.b }) (IntFractPair.stream v (n + 1))

Tactic:
← IntFractPair.coe_stream'_rat_eq v_eq_q

Goal state after:
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 : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p ↦ { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    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.ConvergentsEquiv

Goal state before:
pp: case inr.succ
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := g'.contsAux (n' + 1)
succ_n'th_contsAux_eq' : pred_conts' = g'.contsAux (n' + 1)
ppred_conts' : Pair K := g'.contsAux n'
n'th_contsAux_eq' : ppred_conts' = g'.contsAux n'
pA' : K := pred_conts'.a
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)

Tactic:
let pB' := pred_conts'.b

Goal state after:
case inr.succ
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := g'.contsAux (n' + 1)
succ_n'th_contsAux_eq' : pred_conts' = g'.contsAux (n' + 1)
ppred_conts' : Pair K := g'.contsAux n'
n'th_contsAux_eq' : ppred_conts' = g'.contsAux n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)
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
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
⊢ gp.a = 1 ∧ ∃ z, gp.b = ↑z

Tactic:
obtain ⟨ifp, stream_succ_nth_eq, -⟩ : ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ _ :=
    IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq
  have : gp = ⟨1, ifp.b⟩ := by
    have : (of v).s.get? n = some ⟨1, ifp.b⟩ :=
      get?_of_eq_some_of_succ_get?_intFractPair_stream stream_succ_nth_eq
    have : some gp = some ⟨1, ifp.b⟩ := by rwa [nth_s_eq] at this
    injection this
  simp [this]

Goal state after:
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.leadingCoeff = P.d

Tactic:
rw [of_c_eq_zero ha hb hc, leadingCoeff_C]

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

Goal state before:
pp: case succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
rcases Decidable.em <| g.TerminatedAt (n - 1) with terminated | not_terminated
    · -- terminating case
      rcases n with - | n
      · simp
      · have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
          contsAux_stable_step_of_terminated terminated
        simp only [g, this, IH]
    · -- non-terminating case
      calc
        (0 : K) ≤ fib (n + 1) := mod_cast (n + 1).fib.zero_le
        _ ≤ ((of v).contsAux (n + 1)).b := fib_le_of_contsAux_b (Or.inr not_terminated)

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
i : I
s : Finset I
h : i ∈ s
⊢ e i * ∑ j ∈ s, e j = e i

Tactic:
by
  classical
  simp [Finset.mul_sum, he.mul_eq, h]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
i : I
s : Finset I
h : i ∉ s
⊢ e i * ∑ j ∈ s, e j = 0

Tactic:
by
  classical
  simp [Finset.mul_sum, he.mul_eq, h]

Goal state after:
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
x : A ⊗[R] M
⊢ (basisAux A b) (a • 0) = a • (basisAux A b) 0

Tactic:
by simp

Goal state after:
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 * f 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : Nonempty n
I J : RingCon R
eq : matrix n I = matrix n J
r s : R
⊢ I r s ↔ J r s

Tactic:
have := congr_fun (DFunLike.congr_fun eq (Matrix.of fun _ _ ↦ r)) (Matrix.of fun _ _ ↦ s)

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : Nonempty n
I J : RingCon R
eq : matrix n I = matrix n J
r s : R
this :
  (matrix n I) (Matrix.of fun x x_1 ↦ r) (Matrix.of fun x x_1 ↦ s) =
    (matrix n J) (Matrix.of fun x x_1 ↦ r) (Matrix.of fun x x_1 ↦ s)
⊢ I r s ↔ J r s
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Fintype n
x✝⁴ x✝³ : Matrix n n R
x✝² : ⊤ x✝⁴ x✝³
x✝¹ x✝ : n
⊢ ⊤ (x✝⁴ x✝¹ x✝) (x✝³ x✝¹ x✝)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s : Finset I
⊢ (∏ i ∈ ∅, (1 - e i)) * x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents fun x ↦ 1 - e x
⊢ ∀ (x : I), 1 - (1 - e x) = e x

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ False

Tactic:
refine hv.2 ((LinearMap.ker_eq_bot'.mp f'.ker) v (?_ : μ • v - f v = 0))

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ μ • v - f v = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
h : r ∈ ↑(equivMatrix.symm I)
⊢ single i j r i j = r

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
n : ℕ∞
k : ℕ
ih : ∀ ⦃x : M⦄, ↑k ≤ n → ((f - μ • 1) ^ k) x = 0 → ((f - μ • 1) ^ k) (f x) = 0
x : M
hk : ↑(k + 1) ≤ n
hx : ((f - μ • 1) ^ k) ((f - μ • 1) x) = 0
⊢ ↑k ≤ ↑(k + 1)

Tactic:
by simp

Goal state after: