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

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
a✝ : γ
⊢ Option.rec none (fun val ↦ some (g (f val))) none = some a✝ ↔
    ((fun o ↦ Option.rec none (fun val ↦ some (g val)) o) ∘ fun o ↦ Option.rec none (fun val ↦ some (f val)) o) none =
      some a✝

pp: case some
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
val✝ : α
a✝ : γ
⊢ Option.rec none (fun val ↦ some (g (f val))) (some val✝) = some a✝ ↔
    ((fun o ↦ Option.rec none (fun val ↦ some (g val)) o) ∘ fun o ↦ Option.rec none (fun val ↦ some (f val)) o)
        (some val✝) =
      some a✝

Tactic:
<;>

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
a✝ : γ
⊢ Option.rec none (fun val ↦ some (g (f val))) none = some a✝ ↔
    ((fun o ↦ Option.rec none (fun val ↦ some (g val)) o) ∘ fun o ↦ Option.rec none (fun val ↦ some (f val)) o) none =
      some a✝

case some
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
val✝ : α
a✝ : γ
⊢ Option.rec none (fun val ↦ some (g (f val))) (some val✝) = some a✝ ↔
    ((fun o ↦ Option.rec none (fun val ↦ some (g val)) o) ∘ fun o ↦ Option.rec none (fun val ↦ some (f val)) o)
        (some val✝) =
      some a✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
⊢ take 0 nil = []

pp: case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ take 0 (cons x✝ s✝) = []

Tactic:
<;>

Goal state after:
case nil
α : Type u
⊢ take 0 nil = []

case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ take 0 (cons x✝ s✝) = []
Module: Mathlib.Data.Seq.Computation

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

pp: case inr
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
cb : Computation β
⊢ match
    match Bind.g (Sum.inr cb) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inr cb with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = corec (Bind.f f) (Sum.inl (pure a)) ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
b : β
⊢ match
    match Bind.g (Sum.inl b) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inl b with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = corec (Bind.f f) (Sum.inl (pure a)) ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False

case inr
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
cb : Computation β
⊢ match
    match Bind.g (Sum.inr cb) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inr cb with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = corec (Bind.f f) (Sum.inl (pure a)) ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False
Module: Mathlib.Data.Seq.Computation

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

pp: case inr
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
c cb : Computation β
⊢ match
    match Bind.g (Sum.inr cb) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inr cb with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
c : Computation β
b : β
⊢ match
    match Bind.g (Sum.inl b) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inl b with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False

case inr
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
c cb : Computation β
⊢ match
    match Bind.g (Sum.inr cb) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inr cb with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: case none
α : Type u_1
g : GenContFract α
n : ℕ
s_nth_eq : g.s.get? n = none
⊢ g.partNums.get? n = none ↔ none = none

pp: case some
α : Type u_1
g : GenContFract α
n : ℕ
val✝ : Pair α
s_nth_eq : g.s.get? n = some val✝
⊢ g.partNums.get? n = none ↔ some val✝ = none

Tactic:
<;>

Goal state after:
case none
α : Type u_1
g : GenContFract α
n : ℕ
s_nth_eq : g.s.get? n = none
⊢ g.partNums.get? n = none ↔ none = none

case some
α : Type u_1
g : GenContFract α
n : ℕ
val✝ : Pair α
s_nth_eq : g.s.get? n = some val✝
⊢ g.partNums.get? n = none ↔ some val✝ = none
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: case none
α : Type u_1
g : GenContFract α
n : ℕ
s_nth_eq : g.s.get? n = none
⊢ g.partDens.get? n = none ↔ none = none

pp: case some
α : Type u_1
g : GenContFract α
n : ℕ
val✝ : Pair α
s_nth_eq : g.s.get? n = some val✝
⊢ g.partDens.get? n = none ↔ some val✝ = none

Tactic:
<;>

Goal state after:
case none
α : Type u_1
g : GenContFract α
n : ℕ
s_nth_eq : g.s.get? n = none
⊢ g.partDens.get? n = none ↔ none = none

case some
α : Type u_1
g : GenContFract α
n : ℕ
val✝ : Pair α
s_nth_eq : g.s.get? n = some val✝
⊢ g.partDens.get? n = none ↔ some val✝ = none
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)

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

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

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

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

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

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

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

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

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

Goal state before:
pp: case zero
α : Type u
β : Type v
f : α → Computation β
b : β
s : Computation α
⊢ (s.bind f).Results b 0 → ∃ a m n, s.Results a m ∧ (f a).Results b n ∧ 0 = n + m

pp: case succ
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s : Computation α
⊢ (s.bind f).Results b (n + 1) → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
<;>

Goal state after:
case zero
α : Type u
β : Type v
f : α → Computation β
b : β
s : Computation α
⊢ (s.bind f).Results b 0 → ∃ a m n, s.Results a m ∧ (f a).Results b n ∧ 0 = n + m

case succ
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s : Computation α
⊢ (s.bind f).Results b (n + 1) → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: case succ
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
obtain ⟨gp, s_nth_eq⟩ : ∃ gp, g.s.get? n = some gp :=
      Option.ne_none_iff_exists'.1 not_terminated_at_n

Goal state after:
case succ
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ (of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₁ i h1) = of G (fun i j h ↦ ⇑(f' i j h)) i₁

pp: case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ (of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₂ i h2) = of G (fun i j h ↦ ⇑(f' i j h)) i₂

Tactic:
<;>

Goal state after:
case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ (of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₁ i h1) = of G (fun i j h ↦ ⇑(f' i j h)) i₁

case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ (of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₂ i h2) = of G (fun i j h ↦ ⇑(f' i j h)) i₂
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
x : G i₁
⊢ ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₁ i h1)) x = (of G (fun i j h ↦ ⇑(f' i j h)) i₁) x

pp: case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
x : G i₂
⊢ ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₂ i h2)) x = (of G (fun i j h ↦ ⇑(f' i j h)) i₂) x

Tactic:
<;>

Goal state after:
case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
x : G i₁
⊢ ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₁ i h1)) x = (of G (fun i j h ↦ ⇑(f' i j h)) i₁) x

case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
x : G i₂
⊢ ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₂ i h2)) x = (of G (fun i j h ↦ ⇑(f' i j h)) i₂) x
Module: Mathlib.Data.Seq.Basic

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

pp: case r
α : Type u
s t u : Seq α
⊢ ∃ s_1 t_1 u_1,
    (s.append t).append u = (s_1.append t_1).append u_1 ∧ s.append (t.append u) = s_1.append (t_1.append u_1)

Tactic:
· rintro _ _ ⟨s, t, u, rfl, rfl⟩
    cases s with
    | nil =>
      cases t with
      | nil =>
        cases u with
        | nil => simp
        | cons _ u => simpa using ⟨nil, nil, u, by simp, by simp⟩
      | cons _ t => simpa using ⟨nil, t, u, by simp, by simp⟩
    | cons _ s => simpa using ⟨s, t, u, rfl, rfl⟩

Goal state after:
case r
α : Type u
s t u : Seq α
⊢ ∃ s_1 t_1 u_1,
    (s.append t).append u = (s_1.append t_1).append u_1 ∧ s.append (t.append u) = s_1.append (t_1.append u_1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
l' : List α
⊢ ↑([] ++ l') = (↑[]).append ↑l'

pp: case cons
α : Type u
l' : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ↑(tail✝ ++ l') = (↑tail✝).append ↑l'
⊢ ↑(head✝ :: tail✝ ++ l') = (↑(head✝ :: tail✝)).append ↑l'

Tactic:
<;>

Goal state after:
case nil
α : Type u
l' : List α
⊢ ↑([] ++ l') = (↑[]).append ↑l'

case cons
α : Type u
l' : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ↑(tail✝ ++ l') = (↑tail✝).append ↑l'
⊢ ↑(head✝ :: tail✝ ++ l') = (↑(head✝ :: tail✝)).append ↑l'
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
s : Stream' α
⊢ ↑([] ++ₛ s) = (↑[]).append ↑s

pp: case cons
α : Type u
s : Stream' α
head✝ : α
tail✝ : List α
tail_ih✝ : ↑(tail✝ ++ₛ s) = (↑tail✝).append ↑s
⊢ ↑(head✝ :: tail✝ ++ₛ s) = (↑(head✝ :: tail✝)).append ↑s

Tactic:
<;>

Goal state after:
case nil
α : Type u
s : Stream' α
⊢ ↑([] ++ₛ s) = (↑[]).append ↑s

case cons
α : Type u
s : Stream' α
head✝ : α
tail✝ : List α
tail_ih✝ : ↑(tail✝ ++ₛ s) = (↑tail✝).append ↑s
⊢ ↑(head✝ :: tail✝ ++ₛ s) = (↑(head✝ :: tail✝)).append ↑s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
⊢ R a b

Tactic:
let ⟨b', mb', ab'⟩ := l ma

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

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
a✝ : γ
⊢ Option.map (g ∘ f) none = some a✝ ↔ (Option.map g ∘ Option.map f) none = some a✝

pp: case some
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
val✝ : α
a✝ : γ
⊢ Option.map (g ∘ f) (some val✝) = some a✝ ↔ (Option.map g ∘ Option.map f) (some val✝) = some a✝

Tactic:
<;>

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
a✝ : γ
⊢ Option.map (g ∘ f) none = some a✝ ↔ (Option.map g ∘ Option.map f) none = some a✝

case some
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
val✝ : α
a✝ : γ
⊢ Option.map (g ∘ f) (some val✝) = some a✝ ↔ (Option.map g ∘ Option.map f) (some val✝) = some a✝
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
b : β
⊢ LiftRel R ca (pure b) ↔ ∃ a, a ∈ ca ∧ R a b

Tactic:
LiftRel.swap,

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
b : β
⊢ LiftRel (fun x y ↦ R y x) (pure b) ca ↔ ∃ a, a ∈ ca ∧ R a b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
b : β
⊢ LiftRel R ca (pure b) ↔ ∃ a, a ∈ ca ∧ R a b

Tactic:
rw [LiftRel.swap, liftRel_pure_left]

Goal state after: