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

Goal state before:
pp: α : Type u
⊢ nil.length' = 0

Tactic:
by
  simp -implicitDefEqProofs [length']

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

Goal state before:
pp: α : Type u
x : α
s : Seq α
h : s.Terminates
⊢ ¬(cons x s).TerminatedAt 0

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u
⊢ nil.length' = 0 ↔ nil = nil

Tactic:
simp

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

Goal state before:
pp: case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ (cons x✝ s✝).length' = 0 ↔ cons x✝ s✝ = nil

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u
⊢ nil.length' ≠ 0 ↔ ∃ x s', nil = cons x s'

Tactic:
simp

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

Goal state before:
pp: case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ (cons x✝ s✝).length' ≠ 0 ↔ ∃ x s', cons x✝ s✝ = cons x s'

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
δ : Type w
m n : ℕ
x y : List α
a✝ b : Stream' α
a : α
⊢ [a] ≠ []

Tactic:
simp

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

Goal state before:
pp: case pure
α : Type u
β : Type v
f : α → β
a✝ : α
⊢ (map f (pure a✝)).destruct = lmap f (rmap (map f) (pure a✝).destruct)

Tactic:
simp

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

Goal state before:
pp: case think
α : Type u
β : Type v
f : α → β
s✝ : Computation α
⊢ (map f s✝.think).destruct = lmap f (rmap (map f) s✝.think.destruct)

Tactic:
simp

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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ ↑n < s.length' ↔ ∃ a, a ∈ s.get? n

Tactic:
by
  by_cases h : s.Terminates
  · simpa [length'_of_terminates h] using lt_length_iff
  · simp only [length'_of_not_terminates h, ENat.natCast_lt_top, Option.mem_def, true_iff]
    rw [not_terminates_iff] at h
    rw [← Option.isSome_iff_exists]
    exact h n

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

Goal state before:
pp: α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take k r)[0]? =
    if 0 < k + 1 then (cons x r).get? 0 else none

Tactic:
simp

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

Goal state before:
pp: case r
α : Type u
β : Type v
a : α
f : α → Computation β
⊢ (pure a).bind f = (pure a).bind f ∧ f a = f a ∨ (pure a).bind f = corec (Bind.f f) (Sum.inr (f a))

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
n✝¹ n✝ : ℕ
⊢ ((zip appendStream' s.inits s.tails).get n✝¹).get n✝ = ((const s).get n✝¹).get n✝

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
⊢ x ∈
    match (cons x s.tail).destruct with
    | none => []
    | some (x, r) => x :: take l r

Tactic:
simp

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

Goal state before:
pp: α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ}, k < n → s.get? k = some x → x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
⊢ 0 ≤ k + 1

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂✝ : Computation β
h : c₁ = c₂✝ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂✝ = map f s
c₂ : Computation β
b : β
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) (Sum.inl b) (Sum.inl b)

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂✝ : Computation β
h : c₁ = c₂✝ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂✝ = map f s
c₂ cb : Computation β
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) (Sum.inr cb) (Sum.inr cb)

Tactic:
simp

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

Goal state before:
pp: case pure
α : Type u
β : Type v
f : α → β
s✝ : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
s : α
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) ((pure s).bind (pure ∘ f)).destruct
    (map f (pure s)).destruct

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
s : Seq α
⊢ (take 0 s).length ≤ 0

Tactic:
simp

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

Goal state before:
pp: case succ.none
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
⊢ (match none with
      | none => []
      | some (x, r) => x :: take m r).length ≤
    m + 1

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂✝ : Computation γ
h : c₁ = c₂✝ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂✝ = s.bind fun x ↦ (f x).bind g
c₂ : Computation γ
b : γ
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g) (Sum.inl b) (Sum.inl b)

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂✝ : Computation γ
h : c₁ = c₂✝ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂✝ = s.bind fun x ↦ (f x).bind g
c₂ cb : Computation γ
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g) (Sum.inr cb)
    (Sum.inr cb)

Tactic:
simp

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

Goal state before:
pp: case pure.pure.inl
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
s : α
t : β
b : γ
⊢ match Sum.inl b, Sum.inl b with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x ↦ (f x).bind g
  | x, x_1 => False

Tactic:
simp

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

Goal state before:
pp: case pure.pure.inr
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
s : α
t : β
cb : Computation γ
⊢ match Sum.inr cb, Sum.inr cb with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x ↦ (f x).bind g
  | x, x_1 => False

Tactic:
simp

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

Goal state before:
pp: case pure.think
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
s : α
s✝ : Computation β
⊢ match (s✝.think.bind g).destruct, (s✝.think.bind g).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x ↦ (f x).bind g
  | x, x_1 => False

Tactic:
simp

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

Goal state before:
pp: α : Type u
l : List α
⊢ ↑((↑l).toList ⋯) = ↑l

Tactic:
simp

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

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

Tactic:
rw [destruct_cons]
    dsimp
    exact ⟨rfl, _, rfl, rfl⟩

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

Goal state before:
pp: case bisim.nil.nil.nil
α : Type u
s t u : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u))
    ((nil.append nil).append nil).destruct (nil.append (nil.append nil)).destruct

Tactic:
simp

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

Goal state before:
pp: α : Type u
s t u✝ : Seq α
x✝ : α
u : Seq α
⊢ u = (nil.append nil).append u

Tactic:
simp

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

Goal state before:
pp: α : Type u
s t u✝ : Seq α
x✝ : α
u : Seq α
⊢ u = nil.append (nil.append u)

Tactic:
simp

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

Goal state before:
pp: α : Type u
s t✝ u✝ u : Seq α
x✝ : α
t : Seq α
⊢ t.append u = (nil.append t).append u

Tactic:
simp

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

Goal state before:
pp: α : Type u
s t✝ u✝ u : Seq α
x✝ : α
t : Seq α
⊢ t.append u = nil.append (t.append u)

Tactic:
simp

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

Goal state before:
pp: case pure
α : Type u
c s' : Computation α
s : α
h : (empty α <|> pure s) = s'
⊢ BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) (empty α <|> pure s).destruct (pure s).destruct

Tactic:
think_empty

Goal state after:
case pure
α : Type u
c s' : Computation α
s : α
h : (empty α <|> pure s) = s'
⊢ BisimO (fun c₁ c₂ ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> pure s).destruct (pure s).destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case pure
α : Type u
c s' : Computation α
s : α
h : (empty α <|> pure s) = s'
⊢ BisimO (fun c₁ c₂ ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> pure s).destruct (pure s).destruct

Tactic:
simp

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

Goal state before:
pp: case think
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) (empty α <|> s.think).destruct s.think.destruct

Tactic:
think_empty

Goal state after:
case think
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ BisimO (fun c₁ c₂ ↦ ((empty α).think <|> c₂) = c₁) ((empty α).think <|> s.think).destruct s.think.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case pure
α : Type u
c s' : Computation α
s : α
h : (pure s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) (pure s <|> empty α).destruct (pure s).destruct

Tactic:
think_empty

Goal state after:
case pure
α : Type u
c s' : Computation α
s : α
h : (pure s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> (empty α).think) = c₁) (pure s <|> (empty α).think).destruct (pure s).destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case pure
α : Type u
c s' : Computation α
s : α
h : (pure s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> (empty α).think) = c₁) (pure s <|> (empty α).think).destruct (pure s).destruct

Tactic:
simp

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

Goal state before:
pp: case think
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) (s.think <|> empty α).destruct s.think.destruct

Tactic:
think_empty

Goal state after:
case think
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> (empty α).think) = c₁) (s.think <|> (empty α).think).destruct s.think.destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
x✝ : ℕ
⊢ (map f s).TerminatedAt x✝ ↔ s.TerminatedAt x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
⊢ LiftRel R (pure a) (pure b) ↔ R a b

Tactic:
simp

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

Goal state before:
pp: case nil.nil
α : Type u
β : Type v
f : α → β
s t : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s t, s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f (nil.append nil)).destruct ((map f nil).append (map f nil)).destruct

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s t✝ : Seq α
x✝ : α
t : Seq α
⊢ map f t = map f (nil.append t)

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s t✝ : Seq α
x✝ : α
t : Seq α
⊢ map f t = (map f nil).append (map f t)

Tactic:
simp

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
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 : DirectLimit G f →+* P
i j : ι
hij : i ≤ j
x : G i
⊢ (F.comp (of G f j)) (f i j hij x) = (F.comp (of G f i)) x

Tactic:
simp

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

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
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
⊢ (of G f j) (f i j hij x) = (of G f i) x

Tactic:
simp

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

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

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

Tactic:
rcases eq_or_ne (IntFractPair.stream (Int.fract v)⁻¹ n) none with hnone | hsome

Goal state after:
case succ.inl
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

case succ.inr
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
Module: Mathlib.Data.Seq.Basic

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

Tactic:
simp

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

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

Goal state before:
pp: α : Type u
S T✝ T : Seq (Seq1 α)
a : α
s : Seq α
⊢ s.append T.join = s.append (nil.append T).join

Tactic:
simp

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

Goal state before:
pp: α : Type u
S T✝ T : Seq (Seq1 α)
a : α
s : Seq α
⊢ s.append T.join = s.append (nil.join.append T.join)

Tactic:
simp

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

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

Goal state before:
pp: α : Type u
S T : Seq (Seq1 α)
⊢ (S.append T).join = nil.append (S.append T).join

Tactic:
simp

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

Goal state before:
pp: α : Type u
S T : Seq (Seq1 α)
⊢ S.join.append T.join = nil.append (S.join.append T.join)

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
s : Seq α
⊢ (s.drop 0).length' = s.length' - ↑0

Tactic:
simp

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

Goal state before:
pp: case succ.nil
α : Type u
n : ℕ
⊢ (nil.drop (n + 1)).length' = nil.length' - ↑(n + 1)

Tactic:
simp

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

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
x : α
s : Seq α
⊢ (s.drop n).length' = s.length' + 1 - (↑n + 1)

Tactic:
convert! drop_length' using 1

Goal state after:
case e'_3
α : Type u
n : ℕ
x : α
s : Seq α
⊢ s.length' + 1 - (↑n + 1) = s.length' - ↑n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
s : Seq α
n✝ : ℕ
⊢ (zipWith f s nil).get? n✝ = nil.get? n✝

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
⊢ (zipWith f (cons x s) (cons x' s')).get? 0 = (cons (f x x') (zipWith f s s')).get? 0

Tactic:
simp

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

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
n✝ : ℕ
⊢ (zipWith f (cons x s) (cons x' s')).get? (n✝ + 1) = (cons (f x x') (zipWith f s s')).get? (n✝ + 1)

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
s : Seq α
x : α
⊢ (cons x s).enum.get? 0 = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? 0

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case none.some
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝ : β
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ (some val✝)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) none (some val✝)

Tactic:
simp

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

Goal state before:
pp: case some.none
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝ : α
⊢ Option.map₂ g (Option.map f₁ (some val✝)) (Option.map f₂ none) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (some val✝) none

Tactic:
simp

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

Goal state before:
pp: case some.some
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map₂ g (Option.map f₁ (some val✝¹)) (Option.map f₂ (some val✝)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (some val✝¹) (some val✝)

Tactic:
simp

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

Goal state before:
pp: case e'_2.e'_1
α : Type u
β : Type v
γ : Type w
α' : Type u'
s₁ : Seq α
s₂ : Seq β
f : α → α'
g : α' → β → γ
⊢ s₂ = map id s₂

Tactic:
simp

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

Goal state before:
pp: case e'_2.e'_5
α : Type u
β : Type v
γ : Type w
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f : β → β'
g : α → β' → γ
⊢ s₁ = map id s₁

Tactic:
simp

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

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

Goal state before:
pp: α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ ((map f₁ s₁).zip (map f₂ s₂)).get? n = (map (Prod.map f₁ f₂) (s₁.zip s₂)).get? n

Tactic:
simp

Goal state after:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (s₁.get? n) (s₂.get? n))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case none.none
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none none)

Tactic:
simp

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

Goal state before:
pp: case none.some
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝ : β
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (some val✝)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (some val✝))

Tactic:
simp

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

Goal state before:
pp: case some.none
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝ : α
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val✝)) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val✝) none)

Tactic:
simp

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

Goal state before:
pp: case some.some
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val✝¹)) (Option.map f₂ (some val✝)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val✝¹) (some val✝))

Tactic:
simp

Goal state after: