mathlib-initiative/mathlib-tactics huggingface dataset:
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 ∈ s, p x

Tactic:
simp only [mem_iff_exists_get?]
  grind

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

Goal state before:
pp: 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

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

Tactic:
·

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
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: 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

Tactic:
·

Goal state after:
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.Seq.Basic

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

pp: case refine_2
α β : Type u
f : α → β
p : β → Prop
s : Seq α
x✝¹ : ∀ x ∈ s, (p ∘ f) x
x✝ : β
hx : x✝ ∈ map f s
⊢ p x✝

Tactic:
·

Goal state after:
case refine_1
α β : Type u
f : α → β
p : β → Prop
s : Seq α
x✝¹ : ∀ x ∈ map f s, p x
x✝ : α
hx : x✝ ∈ s
⊢ (p ∘ f) x✝
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
⊢ p x✝

Tactic:
·

Goal state after:
case refine_2
α β : Type u
f : α → β
p : β → Prop
s : Seq α
x✝¹ : ∀ x ∈ s, (p ∘ f) x
x✝ : β
hx : x✝ ∈ map f s
⊢ p x✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case inl
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
⊢ p y

pp: case inr
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = (s.set n x).get? m
h_nm : n ≠ m
⊢ p y

Tactic:
·

Goal state after:
case inl
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
⊢ p y
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
h_term : s.TerminatedAt n
⊢ p y

pp: case neg
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
h_term : ¬s.TerminatedAt n
⊢ p y

Tactic:
·

Goal state after:
case pos
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
h_term : s.TerminatedAt n
⊢ p y
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
h_term : ¬s.TerminatedAt n
⊢ p y

Tactic:
·

Goal state after:
case neg
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
h_term : ¬s.TerminatedAt n
⊢ p y
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case inr
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = (s.set n x).get? m
h_nm : n ≠ m
⊢ p y

Tactic:
·

Goal state after:
case inr
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = (s.set n x).get? m
h_nm : n ≠ m
⊢ p y
Module: Mathlib.Data.Nat.Fib.Basic

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

Tactic:
simp [pos_iff_ne_zero]

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 ≠ (Ring.DirectLimit.of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ?m.64) 1

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 : ι
⊢ ι

Tactic:
·

Goal state after:
ι : 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 ≠ (Ring.DirectLimit.of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ?m.64) 1
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 lia

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 lia

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 lia

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

Goal state before:
pp: case zero
⊢ fib (2 * 0) = fib 0 * (2 * fib (0 + 1) - fib 0)

pp: case succ
n✝ : ℕ
⊢ fib (2 * (n✝ + 1)) = fib (n✝ + 1) * (2 * fib (n✝ + 1 + 1) - fib (n✝ + 1))

Tactic:
·

Goal state after:
case zero
⊢ fib (2 * 0) = fib 0 * (2 * fib (0 + 1) - fib 0)
Module: Mathlib.Data.Nat.Fib.Basic

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

Tactic:
·

Goal state after:
case succ
n✝ : ℕ
⊢ fib (2 * (n✝ + 1)) = fib (n✝ + 1) * (2 * fib (n✝ + 1 + 1) - fib (n✝ + 1))
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case h
n : ℕ
⊢ (if false = true then
        ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → false = true)

Tactic:
·

Goal state after:
case h
n : ℕ
⊢ (if false = true then
        ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → false = true)
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 lia

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

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

pp: case cons
α : Type u
R : α → α → Prop
x✝ : α
s✝ : Seq α
h : Pairwise R (cons x✝ s✝)
⊢ Pairwise R (cons x✝ s✝).tail

Tactic:
·

Goal state after:
case nil
α : Type u
R : α → α → Prop
h : Pairwise R nil
⊢ Pairwise R nil.tail
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons
α : Type u
R : α → α → Prop
x✝ : α
s✝ : Seq α
h : Pairwise R (cons x✝ s✝)
⊢ Pairwise R (cons x✝ s✝).tail

Tactic:
·

Goal state after:
case cons
α : Type u
R : α → α → Prop
x✝ : α
s✝ : Seq α
h : Pairwise R (cons x✝ s✝)
⊢ Pairwise R (cons x✝ s✝).tail
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
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

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

Tactic:
·

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

Tactic:
·

Goal state after:
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.Data.Seq.Basic

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

pp: case pos
α : 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
⊢ b.length' ≤ a.length'

Tactic:
·

Goal state after:
case neg
α : 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
⊢ b.length' ≤ a.length'
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case h
n : ℕ
⊢ (if false = true then
        ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → true = true)

Tactic:
·

Goal state after:
case h
n : ℕ
⊢ (if false = true then
        ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → true = true)
Module: Mathlib.Data.Nat.Fib.Basic

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

pp: case refine_2
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), n.fastFibAux = (fib n, fib (n + 1)) → (bit b n).fastFibAux = (fib (bit b n), fib (bit b n + 1))

Tactic:
·

Goal state after:
case refine_1
n : ℕ
⊢ fastFibAux 0 = (fib 0, fib (0 + 1))
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case refine_2
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), n.fastFibAux = (fib n, fib (n + 1)) → (bit b n).fastFibAux = (fib (bit b n), fib (bit b n + 1))

Tactic:
·

Goal state after:
case refine_2
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), n.fastFibAux = (fib n, fib (n + 1)) → (bit b n).fastFibAux = (fib (bit b n), fib (bit b n + 1))
Module: Mathlib.Data.Nat.Fib.Basic

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

pp: case inr
m n : ℕ
h : n > 0
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)

Tactic:
·

Goal state after:
case inl
m : ℕ
⊢ (fib m).gcd (fib (0 + m)) = (fib m).gcd (fib 0)
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
  rcases Nat.eq_zero_or_pos n with rfl | h
  · simp
  replace h := Nat.succ_pred_eq_of_pos h; rw [← h, succ_eq_add_one]
  calc
    gcd (fib m) (fib (n.pred + 1 + m)) =
        gcd (fib m) (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) := by
        rw [← fib_add n.pred _]
        ring_nf
    _ = gcd (fib m) (fib (n.pred + 1) * fib (m + 1)) := by
        rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
    _ = gcd (fib m) (fib (n.pred + 1)) :=
      Coprime.gcd_mul_right_cancel_right (fib (n.pred + 1)) (Coprime.symm (fib_coprime_fib_succ m))

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

Goal state before:
pp: case bisim
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ Seq.IsBisimulation fun s1 s2 ↦ ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join

pp: case r
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ ∃ s S_1,
    Seq.map f S.join = s.append (Seq.map f S_1.join) ∧ (Seq.map (map f) S).join = s.append (Seq.map (map f) S_1).join

Tactic:
·

Goal state after:
case bisim
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ Seq.IsBisimulation fun s1 s2 ↦ ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case r
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ ∃ s S_1,
    Seq.map f S.join = s.append (Seq.map f S_1.join) ∧ (Seq.map (map f) S).join = s.append (Seq.map (map f) S_1).join

Tactic:
·

Goal state after:
case r
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ ∃ s S_1,
    Seq.map f S.join = s.append (Seq.map f S_1.join) ∧ (Seq.map (map f) S).join = s.append (Seq.map (map f) S_1).join
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ Seq.IsBisimulation fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join

pp: case r
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ ∃ s SS_1, SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join

Tactic:
·

Goal state after:
case bisim
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ Seq.IsBisimulation fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case r
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ ∃ s SS_1, SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join

Tactic:
·

Goal state after:
case r
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ ∃ s SS_1, SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join
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)

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

Tactic:
·

Goal state after:
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)
Module: Mathlib.Data.Seq.Basic

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

Tactic:
·

Goal state after:
case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, Seq.cons x s_1), Seq.cons x_1 s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons x_1 s_2), Seq.map join SS)
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

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

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

pp: case succ.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
·

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

pp: case succ.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
·

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, (of v).contsAux (0 + 1) = Pair.map Rat.cast conts
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
·

Goal state after:
case succ.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.succ.none
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : g.s.get? n = none
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

pp: case succ.succ.some
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
·

Goal state after:
case succ.succ.none
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : g.s.get? n = none
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.succ.some
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
·

Goal state after:
case succ.succ.some
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

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

pp: case some.inr
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
·

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