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

Goal state before:
pp: α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map id ⟨s, al⟩) = ↑⟨s, al⟩

Tactic:
;

Goal state after:
α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map id ⟨s, al⟩) = ↑⟨s, al⟩
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ map id ⟨s, al⟩ = ⟨s, al⟩

Tactic:
apply Subtype.ext; dsimp [map]
    rw [Option.map_id, Stream'.map_id]

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
⊢ ∃ b, b ∈ cb ∧ R a b

Tactic:
;

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
⊢ ∃ b, b ∈ cb ∧ R a b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map f (tail ⟨s, al⟩)) = ↑(map f ⟨s, al⟩).tail

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map f (tail ⟨s, al⟩)) = ↑(map f ⟨s, al⟩).tail
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map (g ∘ f) ⟨s, al⟩) = ↑(map g (map f ⟨s, al⟩))

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map (g ∘ f) ⟨s, al⟩) = ↑(map g (map f ⟨s, al⟩))
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ ∃ a, a ∈ ca ∧ R a b

Tactic:
;

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ ∃ a, a ∈ ca ∧ R a b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ pure a
⊢ ∃ b, b ∈ cb ∧ R a b

Tactic:
;

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ pure a
⊢ ∃ b, b ∈ cb ∧ R a b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ R a b

Tactic:
;

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ R a b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel (swap R) cb.think ca ↔ LiftRel (swap R) cb ca

Tactic:
;

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel (swap R) cb.think ca ↔ LiftRel (swap R) cb ca
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ LiftRel S (s1.bind (pure ∘ f1)) (s2.bind (pure ∘ f2))

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ LiftRel S (s1.bind (pure ∘ f1)) (s2.bind (pure ∘ f2))
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ ∀ {a : α} {b : β}, R a b → LiftRel S ((pure ∘ f1) a) ((pure ∘ f2) b)

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ ∀ {a : α} {b : β}, R a b → LiftRel S ((pure ∘ f1) a) ((pure ∘ f2) b)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
x✝ : ∃ b_1, b_1 ∈ pure b ∧ R a b_1
b' : β
mb : b' ∈ pure b
h : R a b'
⊢ LiftRelAux R C (Sum.inl a) (pure b').destruct

Tactic:
;

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
x✝ : ∃ b_1, b_1 ∈ pure b ∧ R a b_1
b' : β
mb : b' ∈ pure b
h : R a b'
⊢ LiftRelAux R C (Sum.inl a) (pure b').destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case some
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ g
h' : f a = b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b

Tactic:
;

Goal state after:
case some
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ g
h' : f a = b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: case inl
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
i j : ι
hij : i ≤ j
x : G i
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) (FreeCommRing.of ⟨j, f i j hij x⟩ - FreeCommRing.of ⟨i, x⟩) = 0

Tactic:
simp only [map_sub, lift_of, Hg, map_one, map_add, map_mul,
          (g i).map_one, (g i).map_add, (g i).map_mul, sub_self]

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

Goal state before:
pp: case inr.inl
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
i : ι
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) (FreeCommRing.of ⟨i, 1⟩ - 1) = 0

Tactic:
simp only [map_sub, lift_of, Hg, map_one, map_add, map_mul,
          (g i).map_one, (g i).map_add, (g i).map_mul, sub_self]

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

Goal state before:
pp: case inr.inr.inl
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
i : ι
x y : G i
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd)
      (FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩)) =
    0

Tactic:
simp only [map_sub, lift_of, Hg, map_one, map_add, map_mul,
          (g i).map_one, (g i).map_add, (g i).map_mul, sub_self]

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

Goal state before:
pp: case inr.inr.inr
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
i : ι
x y : G i
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd)
      (FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩) =
    0

Tactic:
simp only [map_sub, lift_of, Hg, map_one, map_add, map_mul,
          (g i).map_one, (g i).map_add, (g i).map_mul, sub_self]

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

Goal state before:
pp: case nil
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) nil.destruct
    nil.destruct

pp: case cons
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons x✝ s✝).destruct (cons x✝ s✝).destruct

Tactic:
;

Goal state after:
case nil
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) nil.destruct
    nil.destruct

case cons
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons x✝ s✝).destruct (cons x✝ s✝).destruct
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
F : DirectLimit G f →+* P
i✝ : ι
x✝ : G i✝
⊢ ((lift G f P (fun i ↦ F.comp (of G f i)) ⋯).comp (of G f i✝)) x✝ = (F.comp (of G f i✝)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
F : DirectLimit G f →+* P
i✝ : ι
x✝ : G i✝
⊢ ((lift G f P (fun i ↦ F.comp (of G f i)) ⋯).comp (of G f i✝)) x✝ = (F.comp (of G f i✝)) x✝
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
i✝ : ι
x✝ : G i✝
⊢ ((lift G f (DirectLimit G f) (of G f) ⋯).comp (of G f i✝)) x✝ = ((RingHom.id (DirectLimit G f)).comp (of G f i✝)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝¹ : Preorder ι
G : ι → Type u_2
inst✝ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
i✝ : ι
x✝ : G i✝
⊢ ((lift G f (DirectLimit G f) (of G f) ⋯).comp (of G f i✝)) x✝ = ((RingHom.id (DirectLimit G f)).comp (of G f i✝)) x✝
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case zero
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
H : (IntFractPair.of v).fr = Int.fract v
⊢ IntFractPair.stream v (0 + 1) = IntFractPair.stream (Int.fract v)⁻¹ 0

Tactic:
rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H h), H]

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

Goal state before:
pp: case ih
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g✝ : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) (f i j hij x) = (g✝ i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0
i✝ : ι
g : G i✝
hz : (g✝ i✝) g = 0
⊢ (of G f i✝) g = 0

Tactic:
;

Goal state after:
case ih
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g✝ : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) (f i j hij x) = (g✝ i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0
i✝ : ι
g : G i✝
hz : (g✝ i✝) g = 0
⊢ (of G f i✝) g = 0
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Preorder ι
G : ι → Type u_2
inst✝⁴ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝³ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝¹ : IsDirectedOrder ι
inst✝ : Nonempty ι
i✝ : ι
x✝ : G i✝
⊢ (((lift G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (_root_.DirectLimit G f') (Ring.of G f') ⋯).comp
            (Ring.lift G f' (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (of G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ⋯)).comp
        (Ring.of G f' i✝))
      x✝ =
    ((RingHom.id (_root_.DirectLimit G f')).comp (Ring.of G f' i✝)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝⁵ : Preorder ι
G : ι → Type u_2
inst✝⁴ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝³ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝¹ : IsDirectedOrder ι
inst✝ : Nonempty ι
i✝ : ι
x✝ : G i✝
⊢ (((lift G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (_root_.DirectLimit G f') (Ring.of G f') ⋯).comp
            (Ring.lift G f' (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (of G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ⋯)).comp
        (Ring.of G f' i✝))
      x✝ =
    ((RingHom.id (_root_.DirectLimit G f')).comp (Ring.of G f' i✝)) x✝
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Preorder ι
G : ι → Type u_2
inst✝⁴ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝³ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝¹ : IsDirectedOrder ι
inst✝ : Nonempty ι
i✝ : ι
x✝ : G i✝
⊢ (((Ring.lift G f' (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (of G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ⋯).comp
            (lift G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (_root_.DirectLimit G f') (Ring.of G f') ⋯)).comp
        (of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i✝))
      x✝ =
    ((RingHom.id (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3))).comp (of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i✝)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝⁵ : Preorder ι
G : ι → Type u_2
inst✝⁴ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝³ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝¹ : IsDirectedOrder ι
inst✝ : Nonempty ι
i✝ : ι
x✝ : G i✝
⊢ (((Ring.lift G f' (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (of G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ⋯).comp
            (lift G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (_root_.DirectLimit G f') (Ring.of G f') ⋯)).comp
        (of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i✝))
      x✝ =
    ((RingHom.id (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3))).comp (of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i✝)) x✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)

Tactic:
;

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ s.drop (1 + n) = s.tail.drop n

Tactic:
;

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ s.drop (1 + n) = s.tail.drop n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
⊢ (s.tail.drop n).head = s.tail.get? n

Tactic:
;

Goal state after:
case succ
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
⊢ (s.tail.drop n).head = s.tail.get? n
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
i✝ : ι
x✝ : G i✝
⊢ ((map (fun x ↦ RingHom.id (G x)) ⋯).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝ =
    ((RingHom.id (DirectLimit G fun x x_1 h ↦ ⇑(f x x_1 h))).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
inst✝¹ : Preorder ι
G : ι → Type u_2
inst✝ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i →+* G j
i✝ : ι
x✝ : G i✝
⊢ ((map (fun x ↦ RingHom.id (G x)) ⋯).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝ =
    ((RingHom.id (DirectLimit G fun x x_1 h ↦ ⇑(f x x_1 h))).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝
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
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i✝ : ι
x✝ : G i✝
⊢ (((map g₂ hg₂).comp (map g₁ hg₁)).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝ =
    ((map (fun i ↦ (g₂ i).comp (g₁ i)) ⋯).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝

Tactic:
;

Goal state after:
ι : 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
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i✝ : ι
x✝ : G i✝
⊢ (((map g₂ hg₂).comp (map g₁ hg₁)).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝ =
    ((map (fun i ↦ (g₂ i).comp (g₁ i)) ⋯).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝
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 : ι
H : 0 = (Ring.DirectLimit.of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ?m.64) 1
⊢ False

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 : ι
H : 0 = (Ring.DirectLimit.of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ?m.64) 1
⊢ False
Module: Mathlib.Data.Seq.Basic

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

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'

Tactic:
;

Goal state after:
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'

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: x✝ : ℕ
⊢ fib x✝ = x✝.fastFib

Tactic:
;

Goal state after:
x✝ : ℕ
⊢ fib x✝ = x✝.fastFib
Module: Mathlib.Data.Nat.Fib.Basic

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

Tactic:
;

Goal state after:
case inr
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ (match (Seq.cons b s).destruct with
    | none => (a, S.join)
    | some s' => (a, (Seq.cons s' S).join)) =
    (a, (Seq.cons (b, s) S).join)

Tactic:
;

Goal state after:
α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ (match (Seq.cons b s).destruct with
    | none => (a, S.join)
    | some s' => (a, (Seq.cons s' S).join)) =
    (a, (Seq.cons (b, s) S).join)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct

Tactic:
;

Goal state after:
α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s✝ s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct

Tactic:
;

Goal state after:
α : Type u
s✝ s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct
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 γ
s_2 : Seq (Seq1 γ)
y : γ
t : Seq γ
⊢ (join (((a, Seq.cons x s_1), Seq.cons (y, t) s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons (y, t) 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 γ
s_2 : Seq (Seq1 γ)
y : γ
t : Seq γ
⊢ (join (((a, Seq.cons x s_1), Seq.cons (y, t) s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons (y, t) s_2), Seq.map join SS)
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case h.mk
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
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
a✝ b✝ : ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast { a := a✝, b := b✝ }
⊢ { a := ↑z * (Pair.map Rat.cast pred_conts).a + 1 * (Pair.map Rat.cast { a := a✝, b := b✝ }).a,
      b := ↑z * (Pair.map Rat.cast pred_conts).b + 1 * (Pair.map Rat.cast { a := a✝, b := b✝ }).b } =
    Pair.map Rat.cast (nextConts 1 ↑z { a := a✝, b := b✝ } pred_conts)

Tactic:
;

Goal state after:
case h.mk
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
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
a✝ b✝ : ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast { a := a✝, b := b✝ }
⊢ { a := ↑z * (Pair.map Rat.cast pred_conts).a + 1 * (Pair.map Rat.cast { a := a✝, b := b✝ }).a,
      b := ↑z * (Pair.map Rat.cast pred_conts).b + 1 * (Pair.map Rat.cast { a := a✝, b := b✝ }).b } =
    Pair.map Rat.cast (nextConts 1 ↑z { a := a✝, b := b✝ } pred_conts)