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

Goal state before:
pp: α β : Type u
f : α → β
p : β → Prop
s : Seq α
⊢ (∀ x ∈ map f s, p x) ↔ ∀ x ∈ s, (p ∘ f) x

Tactic:
by

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
G' : ι → Type u_4
inst✝ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
e : (i : ι) → G i ≃+* G' i
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)
i : ι
g : G' i
⊢ (congr e he).symm ((of G' (fun x x_1 h ↦ ⇑(f' x x_1 h)) i) g) = (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i) ((e i).symm g)

Tactic:
by

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

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

Goal state before:
pp: α : Type u
s : Seq α
p : α → Prop
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : x ∈ take n s
⊢ p x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : Nonempty ι
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)
⊢ Nonempty ι

Tactic:
by

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

Goal state before:
pp: α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
⊢ ∀ y ∈ s.set n x, p y

Tactic:
by

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

Goal state before:
pp: α : Type u
R : α → α → Prop
⊢ Pairwise R Seq.nil

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ fib (n + 2) = fib n + fib (n + 1)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ fib n ≤ fib (n + 1)

Tactic:
by

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_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
⊢ ifp_n = ifp_n'

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ fib (n + 2) = 0 ↔ n + 2 = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ fib (n + 2) = 0 ↔ n + 2 = 0

Tactic:
by simp [fib_add_two, fib_eq_zero]

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

Goal state before:
pp: n : ℕ
⊢ 0 < fib n ↔ 0 < n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ fib (n + 2) - fib (n + 1) = fib n

Tactic:
by

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
x y : α
k : ℕ
hy : y ∈ tl.get? k
n : ℕ
hx : x ∈ (Seq.cons hd tl).get? (n + 1)
h_ij : n + 1 < k + 1
⊢ n < k

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ fib n < fib (n + 1)

Tactic:
by

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

Goal state before:
pp: ⊢ StrictMono fun n ↦ fib (n + 2)

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : Pairwise R tl
⊢ Pairwise R (Seq.cons hd tl)

Tactic:
by

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

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

Goal state before:
pp: n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ 2 ≤ 5

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
five_le_n : 5 ≤ n
⊢ n ≤ fib n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (fib n).Coprime (fib (n + 1))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : Pairwise R (Seq.cons hd tl)
⊢ (∀ x ∈ tl, R hd x) ∧ Pairwise R tl

Tactic:
by

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
⊢ Pairwise R (cons hd nil)

Tactic:
by

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd tl_hd : α
tl_tl : Seq α
h : Pairwise R (cons hd (cons tl_hd tl_tl))
⊢ R hd tl_hd

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
hd tl_hd : α
tl_tl : Seq α
h_hd : R hd tl_hd
h_tl : Pairwise R (Seq.cons tl_hd tl_tl)
⊢ Pairwise R (Seq.cons hd (Seq.cons tl_hd tl_tl))

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ fib (2 * n + 1) = fib (n + 1) ^ 2 + fib n ^ 2

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : Nonempty ι
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)
i : ι
⊢ 0 ≠ 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
by

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_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
⊢ compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
i : ι
x : G i
H : (Ring.DirectLimit.of G f i) x ≠ 0
h : x = 0
⊢ (Ring.DirectLimit.of G f i) x = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
i : ι
x : G i
H : (Ring.DirectLimit.of G f i) x ≠ 0
⊢ (Ring.DirectLimit.of G f i) x * (Ring.DirectLimit.of G f i) x⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
⊢ Pairwise R s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
hp : p ≠ 0
⊢ p * inv G f p = 1

Tactic:
by

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

Goal state before:
pp: α : 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
n : ℕ
x y : α
hx : (s.drop n).head = some x
hy : s.get? (n + 1) = some y
this : ∀ (n : ℕ), motive (s.drop n)
⊢ y ∈ (s.drop (n + 1)).head

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
hp : p ≠ 0
⊢ inv G f p * p = 1

Tactic:
by

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

Goal state before:
pp: α : 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
n : ℕ
x y : α
hx : s.get? n = some x
hy : s.get? (n + 1) = some y
⊢ R x y

Tactic:
by

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

Goal state before:
pp: α : 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)
⊢ i + k + 1 ≤ i + (k + 1) + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (bit false n).fastFibAux =
    let p := n.fastFibAux;
    (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)

Tactic:
by

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)
z : α
hz : s.get? (i + k + 1) = some z
⊢ R x y

Tactic:
exact _root_.trans (ih z hz) <| h_succ hz hy

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
⊢ ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) ((of v).contsAux (n + 1)) ifp_n.fr

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ Pairwise R s

Tactic:
by

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

Goal state before:
pp: α : Type u
R : α → α → Prop
s : Seq α
h : Pairwise R s
⊢ Pairwise R s.tail

Tactic:
by

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

Goal state before:
pp: α : Type u
R : α → α → Prop
s : Seq α
h : Pairwise R s
n : ℕ
⊢ Pairwise R (s.drop n)

Tactic:
by

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

Goal state before:
pp: α : 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
n : ℕ
hb : b.drop n ≠ nil
⊢ motive (a.drop n) (b.drop n)

Tactic:
by

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
nth_stream_eq_none : IntFractPair.stream v n = none
⊢ v = (of v).convs (n - 1)

Tactic:
by

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
inst✝ : FloorRing K
terminates : (of v).Terminates
⊢ ∀ᶠ (n : ℕ) in atTop, v = (of v).convs n

Tactic:
by

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

Goal state before:
pp: α : 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
this : ∀ (n : ℕ), b.drop n ≠ nil → motive (a.drop n) (b.drop n)
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
⊢ b.drop (a.length ha) ≠ nil

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (bit true n).fastFibAux =
    let p := n.fastFibAux;
    (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.fastFibAux = (fib n, fib (n + 1))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ fib = fastFib

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ b.length' ≤ a.length'

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
s : Seq α
⊢ map id (a, s) = (a, s)

Tactic:
by

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

Goal state before:
pp: m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1))

Tactic:
by

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

Goal state before:
pp: α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ join ((a, Seq.cons b s), S) = (a, (Seq.cons (b, s) S).join)

Tactic:
by

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

Goal state before:
pp: m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) = (fib m).gcd (fib (n.pred + 1) * fib (m + 1))

Tactic:
by

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

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

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ (Seq.map ret s).join = s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Seq α
⊢ bind (a, s) (ret ∘ f) = map f (a, s)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
a : α
f : α → Seq1 β
⊢ (ret a).bind f = f a

Tactic:
by

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

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

Tactic:
by

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

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

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 = (Seq.map (map f) S).join

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
h1 : fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2
h2 : fib (n + 1 + 1) = ∑ p ∈ Finset.antidiagonal (n + 1), p.1.choose p.2
⊢ fib (n + 2 + 1) = ∑ p ∈ Finset.antidiagonal (n + 2), p.1.choose p.2

Tactic:
by

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

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

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

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 + ∑ k ∈ Finset.range n, fib k + 1 = ∑ k ∈ Finset.range (n + 1), fib k + 1

Tactic:
by

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

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

Tactic:
by

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

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

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

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

Tactic:
by

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 : γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, nil), Seq.cons x_1 s_2), SS)).join = join (join ((a, nil), Seq.cons x_1 s_2), Seq.map join SS)

Tactic:
obtain ⟨x, t⟩ := x_1
    cases t <;> simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq1 α
f : α → Seq1 β
g : β → Seq1 γ
⊢ (s.bind f).bind g = s.bind fun x ↦ (f x).bind g

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
⊢ (of v).convs (n + 1) = ↑⌊v⌋ + 1 / (of (Int.fract v)⁻¹).convs n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_n gp_succ_n : Pair K
s_nth_eq : s.get? n = some gp_n
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
⊢ (squashSeq s n).get? n = some { a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b }

Tactic:
by

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

Goal state before:
pp: K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
by

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

Goal state before:
pp: K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

Tactic:
by

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

Tactic:
by

Goal state after: