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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ (s.drop n).head = s.get? n

Tactic:
by
  induction n generalizing s with
  | zero => rfl
  | succ n IH => rw [← get?_tail, ← dropn_tail]; apply IH

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

Goal state before:
pp: α : Type u
s : Seq α
n m i✝ : ℕ
a✝ : α
⊢ (List.drop m (take n s))[i✝]? = some a✝ ↔ (take (n - m) (s.drop m))[i✝]? = some a✝

Tactic:
grind

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
h : fract v ≠ 0
⊢ (some ∘ fun p ↦ { a := 1, b := ↑p.b }) (IntFractPair.of (IntFractPair.of v).fr⁻¹) =
    some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }

Tactic:
rfl

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

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ (of ↑a).s.get? (n + 1) = (of 0⁻¹).s.get? n

Tactic:
inv_zero,

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

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

Tactic:
inv_zero,

Goal state after:
case inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
h : fract ↑a = 0
⊢ ↑a = ↑⌊↑a⌋ + 1 / (of 0).convs' n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
f : α → α
s : Seq α
n m : ℕ
h_if : ¬m = n
⊢ s.get? m = s.get? m

Tactic:
rfl

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

Goal state before:
pp: α : Type u
hd : α
tl : Seq α
f : α → α
⊢ (cons hd tl).update 0 f = cons (f hd) tl

Tactic:
by
  ext1 n
  cases n <;> simp [get?_update]

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

Goal state before:
pp: α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
⊢ (cons hd tl).update (n + 1) f = cons hd (tl.update n f)

Tactic:
by
  ext1 n
  cases n <;> simp [get?_update]

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

Goal state before:
pp: α : Type u
p : α → Prop
s : Seq α
h : ∀ (n : ℕ) (x : α), s.get? n = some x → p x
⊢ ∀ (x : α), (∃ i, some x = s.get? i) → p x

Tactic:
grind

Goal state after:
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_ne_zero : ifp_succ_n.fr ≠ 0
this : compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr

Tactic:
grind

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

Goal state before:
pp: case refl
n : ℕ
⊢ 5 ≤ fib 5

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
⊢ (if false = true then
      ((binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2 ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1 ^
            2,
        (binaryRec (fib 0, fib 1)
              (fun b x p ↦
                if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
              n).2 *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p ↦
                    if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                  n).1 +
            (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2))
    else
      ((binaryRec (fib 0, fib 1)
              (fun b x p ↦
                if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
              n).1 *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p ↦
                    if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                  n).2 -
            (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1),
        (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2 ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1 ^
            2)) =
    let p := n.fastFibAux;
    (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)

Tactic:
rfl

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
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
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc : (↑⌊ifp_n.fr⁻¹⌋ * pA + ppA) / Int.fract ifp_n.fr⁻¹ + pA = (pA * ifp_n.fr⁻¹ + ppA) / Int.fract ifp_n.fr⁻¹
tmp_calc' : (↑⌊ifp_n.fr⁻¹⌋ * pB + ppB) / Int.fract ifp_n.fr⁻¹ + pB = (pB * ifp_n.fr⁻¹ + ppB) / Int.fract ifp_n.fr⁻¹
f : K := Int.fract (1 / ifp_n.fr)
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) =
    if (IntFractPair.of ifp_n.fr⁻¹).fr = 0 then
      (↑⌊ifp_n.fr⁻¹⌋ * (g.contsAux (n + 1)).a + (g.contsAux n).a) /
        (↑⌊ifp_n.fr⁻¹⌋ * (g.contsAux (n + 1)).b + (g.contsAux n).b)
    else
      ((IntFractPair.of ifp_n.fr⁻¹).fr⁻¹ * (↑⌊ifp_n.fr⁻¹⌋ * (g.contsAux (n + 1)).a + (g.contsAux n).a) +
          (g.contsAux (n + 1)).a) /
        ((IntFractPair.of ifp_n.fr⁻¹).fr⁻¹ * (↑⌊ifp_n.fr⁻¹⌋ * (g.contsAux (n + 1)).b + (g.contsAux n).b) +
          (g.contsAux (n + 1)).b)

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ (if true = true then
      ((binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2 ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1 ^
            2,
        (binaryRec (fib 0, fib 1)
              (fun b x p ↦
                if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
              n).2 *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p ↦
                    if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                  n).1 +
            (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2))
    else
      ((binaryRec (fib 0, fib 1)
              (fun b x p ↦
                if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
              n).1 *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p ↦
                    if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                  n).2 -
            (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1),
        (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2 ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1 ^
            2)) =
    let p := n.fastFibAux;
    (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
ih : fib (n + 1) = ∑ k ∈ Finset.range n, fib k + 1
⊢ fib n + fib (n + 1) = fib n + ∑ k ∈ Finset.range n, fib k + 1

Tactic:
by rw [ih, add_assoc]

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
n : ℕ
⊢ ∃ conts, (of v).contsAux (n + 1) = Pair.map Rat.cast conts

Tactic:
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
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
IH : ∀ m < 0, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
m_le_n : 0 ≤ n
⊢ g.contsAux 0 = (g.squashGCF n).contsAux 0

Tactic:
rfl

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

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

Tactic:
rfl

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 : ℕ
a✝ : Pair K
⊢ (Stream'.Seq.map (Pair.map Rat.cast) (of q).s).get? n = some a✝ ↔
    Option.map (Pair.map Rat.cast) ((of q).s.get? n) = some a✝

Tactic:
rfl

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

Goal state before:
pp: case inr.zero
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? 0 = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt 0
s_nth_eq : g.s.get? 0 = some { a := a, b := b }
⊢ (b * g.h + a) / b = g.h + a / b

Tactic:
grind

Goal state after:
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
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this✝ : g'.convs (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
this : g.convs (n' + 2) = (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)
⊢ ((pb + a / b) * pA + pa * ppA) / ((pb + a / b) * pB + pa * ppB) =
    (b * (pb * pA + pa * ppA) + a * pA) / (b * (pb * pB + pa * ppB) + a * pB)

Tactic:
grind

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GenContFract K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      g.convs m.succ = g.convs' m.succ
s_pos : ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ + 1 → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF m.succ
not_terminatedAt_n : ¬g.TerminatedAt m.succ
this✝ : g.convs (m.succ + 1) = g'.convs m.succ
s_mth_eq' : g'.s.get? m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : g.s.get? (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : g.s.get? m = some gp_m
this : 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
ot : g'.s.get? m = some { a := gp_m.a, b := gp_m.b + gp_succ_m.a / gp_succ_m.b }
⊢ 0 < gp'.a ∧ 0 < gp'.b

Tactic:
grind

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
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

Tactic:
grind

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 = 1
a✝ : Nontrivial R
⊢ P.toPoly.Monic

Tactic:
rw [Monic, leadingCoeff_of_c_ne_zero ha hb (hc ▸ one_ne_zero), hc]

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

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

Tactic:
rfl

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

Goal state before:
pp: case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
this✝¹ : 0 ≤ pB
this✝ : 0 < ifp.fr
this : pB + ifp.fr⁻¹ * B ≠ 0
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
grind

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✝ : 1 / den' ≤ 1 / den
this : 1 / |den'| = 1 / den'
⊢ |(-1) ^ n / den'| = 1 / den'

Tactic:
rwa [abs_div, abs_neg_one_pow n]

Goal state after:
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 : ι'
⊢ (baseChange A ((b'.linearMap b) ij)) ((basis A b') k) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') k)

Tactic:
conv_lhs => simp only [basis_apply, baseChange_tmul]

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] ((b'.linearMap b) ij) (b' k) = (((basis A b').linearMap (basis A b)) ij) ((basis A b') k)
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
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)

Tactic:
rcases (zero_le_of_den (K := K)).eq_or_lt' with
    ((hB : (GenContFract.of v).dens n = 0) | hB)

Goal state after:
case inl
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 : (of v).dens n = 0
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)

case inr
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
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
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 map_multiset_prod c.mk' (s.map f)

Goal state after:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h : (i : ι) → β i →+ M
f : Π₀ (i : ι), β i
⊢ (f.sum fun a b ↦ c.mk' ((h a) b)) = f.sum fun x ↦ ⇑(c.mk'.comp (h x))

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
i j : n
⊢ (M • N) i j ∈ ↑I.toAddSubmonoid

Tactic:
rw [smul_eq_mul, mul_apply]

Goal state after:
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
i j : n
⊢ ∑ j_1, M i j_1 * N j_1 j ∈ ↑I.toAddSubmonoid
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
i j k : n
a✝ : k ∈ Finset.univ
⊢ M i k * N k j ∈ I.toAddSubmonoid

Tactic:
apply I.mul_mem_left _ (hN k j)

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
⊢ M ∈ matrix n I ↔ ∀ (i j : n), M i j ∈ I

Tactic:
rfl

Goal state after: