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

Goal state before:
pp: α : Type u
a : α
s t : Seq α
⊢ (corec
        (fun x ↦
          match x.1.destruct with
          | none =>
            match x.2.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.2))
        (cons a s, t)).destruct =
    some
      (a,
        corec
          (fun x ↦
            match x.1.destruct with
            | none =>
              match x.2.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.2))
          (s, t))

Tactic:
corec_eq

Goal state after:
α : Type u
a : α
s t : Seq α
⊢ omap
      (corec fun x ↦
        match x.1.destruct with
        | none =>
          match x.2.destruct with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', x.2))
      (match (cons a s, t).1.destruct with
      | none =>
        match (cons a s, t).2.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a_1, s₁') => some (a_1, s₁', (cons a s, t).2)) =
    some
      (a,
        corec
          (fun x ↦
            match x.1.destruct with
            | none =>
              match x.2.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.2))
          (s, t))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s✝ s : Seq α
⊢ match
    (corec
        (fun x ↦
          match x.1.destruct with
          | none =>
            match x.2.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.2))
        (nil, s)).destruct,
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Tactic:
corec_eq

Goal state after:
α : Type u
s✝ s : Seq α
⊢ match
    omap
      (corec fun x ↦
        match x.1.destruct with
        | none =>
          match x.2.destruct with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', x.2))
      (match (nil, s).1.destruct with
      | none =>
        match (nil, s).2.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', (nil, s).2)),
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
m : a ∈ nil.append s₂
e✝ : nil.append s₂ = cons b s'
⊢ a ∈ nil ∨ a ∈ s₂

Tactic:
apply Or.inr

Goal state after:
case nil
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
m : a ∈ nil.append s₂
e✝ : nil.append s₂ = cons b s'
⊢ a ∈ s₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
⊢ a ∈ s₁.append s₂

Tactic:
apply mem_rec_on h

Goal state after:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
⊢ ∀ (b : α) (s' : Seq α), a = b ∨ a ∈ s'.append s₂ → a ∈ (cons b s').append s₂
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
b : β
⊢ LiftRel R ca (pure b) ↔ ∃ a, a ∈ ca ∧ R a b

Tactic:
by rw [LiftRel.swap, liftRel_pure_left]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f : β → β'
g : α → β' → γ
⊢ zipWith g s₁ (map f s₂) = zipWith (fun a b ↦ g a (f b)) s₁ s₂

Tactic:
convert! zipWith_map _ _ (@id α) _ _
  simp

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

Goal state before:
pp: case succ.inl
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
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = ↑⌊ifp_n'.fr⁻¹⌋
⊢ v = conts.a / conts.b

Tactic:
obtain rfl : ifp_n = ifp_n' := by injection Eq.trans nth_stream_eq.symm nth_stream_eq'

Goal state after:
case succ.inl
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⁻¹⌋
⊢ v = conts.a / conts.b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
p : α → Prop
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl
n : ℕ
s' : Seq α
this : motive s'
⊢ ∀ (x : α), s'.head = some x → p x

Tactic:
cases s' with
  | nil => simp
  | cons hd tl => simp [(step hd tl this).left]

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

Goal state before:
pp: case refine_2
α β : Type u
f : α → β
p : β → Prop
s : Seq α
x✝¹ : ∀ x ∈ s, (p ∘ f) x
x✝ : β
hx : x✝ ∈ map f s
w✝ : α
left✝ : w✝ ∈ s
hx' : f w✝ = x✝
⊢ p (f w✝)

Tactic:
solve_by_elim

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

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
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_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n'.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n'.fr⁻¹).fr ≠ 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n'.fr⁻¹).fr

Tactic:
obtain rfl : ifp_n = ifp_n' := by injection Eq.trans nth_stream_eq.symm nth_stream_eq'

Goal state after:
case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
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
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
n : ℕ
IH : IntFractPair.stream v n = none → v = (of v).convs (n - 1)
nth_stream_eq_none : IntFractPair.stream v (n + 1) = none
g : GenContFract K := of v
⊢ v = g.convs n

Tactic:
obtain ⟨nth_stream_eq_none⟩ | ⟨ifp_n, nth_stream_eq, nth_stream_fr_eq_zero⟩ :
      IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0 :=
      IntFractPair.succ_nth_stream_eq_none_iff.1 nth_stream_eq_none

Goal state after:
case succ.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
n : ℕ
IH : IntFractPair.stream v n = none → v = (of v).convs (n - 1)
nth_stream_eq_none✝ : IntFractPair.stream v (n + 1) = none
g : GenContFract K := of v
nth_stream_eq_none : IntFractPair.stream v n = none
⊢ v = g.convs n

case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
n : ℕ
IH : IntFractPair.stream v n = none → v = (of v).convs (n - 1)
nth_stream_eq_none : IntFractPair.stream v (n + 1) = none
g : GenContFract K := of v
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_stream_fr_eq_zero : ifp_n.fr = 0
⊢ v = g.convs n
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ ε * ↑N' ≤ ε * (B * nB)

Tactic:
gcongr

Goal state after:
case hbc
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := ⋯
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := ⋯
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := ⋯
nB : K := ⋯
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ ↑N' ≤ B * nB
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
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ ↑(fib (n + 1)) * ↑(fib (n + 1)) ≤ ↑(fib (n + 1)) * ↑(fib (n + 2))

Tactic:
gcongr

Goal state after:
case h₂
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := ⋯
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := ⋯
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := ⋯
nB : K := ⋯
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ 1 ≤ 2
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
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ ↑(fib (n + 1)) * ↑(fib (n + 2)) ≤ B * nB

Tactic:
gcongr

Goal state after:
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_n ifp_succ_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
this : ↑⌊ifp_n.fr⁻¹⌋ ≤ ifp_n.fr⁻¹
⊢ ↑ifp_succ_n.b ≤ ifp_n.fr⁻¹

Tactic:
obtain ⟨_, ifp_n_fr⟩ := ifp_n

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⁻¹
⊢ ↑ifp_succ_n.b ≤ { b := b✝, fr := ifp_n_fr }.fr⁻¹
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
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this✝ : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : ↑(fib n) ≤ ppconts.b
this : ↑(fib (n + 1)) ≤ gp.b * pconts.b
⊢ ↑(fib n) + ↑(fib (n + 1)) ≤ ppconts.b + gp.b * pconts.b

Tactic:
gcongr

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

Goal state before:
pp: case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : ↑(fib n) ≤ ppconts.b
one_le_gp_b : 1 ≤ gp.b
⊢ 1 * ↑(fib (n + 1)) ≤ gp.b * pconts.b

Tactic:
gcongr

Goal state after:
case h₂
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := ⋯
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := ⋯
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := ⋯
ppconts_eq : ppconts = g.contsAux n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : ↑(fib n) ≤ ppconts.b
one_le_gp_b : 1 ≤ gp.b
⊢ ↑(fib (n + 1)) ≤ pconts.b
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
d : R
inst✝ : Semiring R
hd : d ≠ 0
⊢ { a := 0, b := 0, c := 0, d := d }.toPoly.degree = 0

Tactic:
by
  simp [hd]

Goal state after:
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
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : gp.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b
⊢ conts.b * (pred_conts.b + gp.b * conts.b) ≤ conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)

Tactic:
gcongr

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

Goal state before:
pp: case right
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : ↑ifp_succ_n.b ≤ ifp_n.fr⁻¹
⊢ ↑ifp_succ_n.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b

Tactic:
gcongr

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

Goal state before:
pp: case h
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
⊢ b * (of v).dens n * (of v).dens n ≤ (of v).dens (n + 1) * (of v).dens n

Tactic:
gcongr

Goal state after:
case hbc
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
⊢ b * (of v).dens n ≤ (of v).dens (n + 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 congr_fun h₂ (Fintype.equivFin I x)

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
I : Type u_3
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm
x : I
⊢ (⇑f ∘ e' ∘ ⇑(Fintype.equivFin I)) x = e x

Tactic:
simpa using congr_fun h₂ (Fintype.equivFin I x)

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
⊢ (f.genEigenspace μ) 0 = ⊥

Tactic:
ext; apply mem_genEigenspace_zero

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 + 1)) x = 0
⊢ ((f - μ • 1) ^ (k + 1)) (f x) = 0

Tactic:
rw [pow_succ, mul_apply] at hx ⊢

Goal state after:
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
⊢ ((f - μ • 1) ^ k) ((f - μ • 1) (f x)) = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

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

Tactic:
case succ k ih =>
    rw [pow_succ, mul_apply] at hx ⊢
    simpa using ih (le_trans (by simp) hk) hx

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ IsNilpotent (0 f)

Tactic:
exact IsNilpotent.zero

Goal state after: