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

Goal state before:
pp: case zero.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
⊢ (Corec.f f (some b)).fst = none → (Corec.f f (Corec.f f (some b)).snd).fst = none

Tactic:
intro h

Goal state after:
case zero.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h : (Corec.f f (some b)).fst = none
⊢ (Corec.f f (Corec.f f (some b)).snd).fst = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero.some.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h₁ : f b = none
⊢ (match none with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
      none →
    (match
          (match none with
            | none => (none, none)
            | some (a, b') => (some a, some b')).snd with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')).fst =
      none

Tactic:
intro h

Goal state after:
case zero.some.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h₁ : f b = none
h :
  (match none with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (match
        (match none with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd with
      | none => (none, none)
      | some b =>
        match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero.some.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
s : α × β
h₁ : f b = some s
⊢ (match some s with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
      none →
    (match
          (match some s with
            | none => (none, none)
            | some (a, b') => (some a, some b')).snd with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')).fst =
      none

Tactic:
intro h

Goal state after:
case zero.some.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
s : α × β
h₁ : f b = some s
h :
  (match some s with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (match
        (match some s with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd with
      | none => (none, none)
      | some b =>
        match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    none
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n : ℕ
h : (fun b ↦ a = b) ((b :: s).get n)
⊢ a = b ∨ a ∈ s

Tactic:
rcases n with - | n'

Goal state after:
case zero
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b ∨ a ∈ s

case succ
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a = b ∨ a ∈ s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s : Computation α
a : α
f0 : s.val 0 = none
⊢ (match none with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inl a →
    s = pure a

Tactic:
intro h

Goal state after:
case none
α : Type u
s : Computation α
a : α
f0 : s.val 0 = none
h :
  (match none with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
this : (a :: const a).tail = const a
⊢ (const a).tail = const a

Tactic:
by rwa [← const_eq] at this

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

Goal state before:
pp: case some
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
⊢ (match some val✝ with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inl a →
    s = pure a

Tactic:
intro h

Goal state after:
case some
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s s' : Computation α
f0 : s.val 0 = none
⊢ (match none with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inr s' →
    s = s'.think

Tactic:
intro h

Goal state after:
case none
α : Type u
s s' : Computation α
f0 : s.val 0 = none
h :
  (match none with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case some
α : Type u
s s' : Computation α
a' : α
f0 : s.val 0 = some a'
⊢ (match some a' with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inr s' →
    s = s'.think

Tactic:
intro h

Goal state after:
case some
α : Type u
s s' : Computation α
a' : α
f0 : s.val 0 = some a'
h :
  (match some a' with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero.inl
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' val✝ : α
⊢ (Corec.f f (Sum.inl val✝)).fst = some a' → (Corec.f f (Corec.f f (Sum.inl val✝)).snd).fst = some a'

Tactic:
intro h

Goal state after:
case zero.inl
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' val✝ : α
h : (Corec.f f (Sum.inl val✝)).fst = some a'
⊢ (Corec.f f (Corec.f f (Sum.inl val✝)).snd).fst = some a'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero.inr
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b✝ : β
a' : α
b : β
⊢ (Corec.f f (Sum.inr b)).fst = some a' → (Corec.f f (Corec.f f (Sum.inr b)).snd).fst = some a'

Tactic:
intro h

Goal state after:
case zero.inr
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b✝ : β
a' : α
b : β
h : (Corec.f f (Sum.inr b)).fst = some a'
⊢ (Corec.f f (Corec.f f (Sum.inr b)).snd).fst = some a'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case inl
α : Type u
s₁✝ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
⊢ s₁ = nil ∧ s₁ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

pp: case inr
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive s₁ s₂
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
· cases s₁ <;> grind

Goal state after:
case inr
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive s₁ s₂
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case inr.inl
α : Type u
s₁✝ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
ih : motive s₁ s₁
⊢ s₁ = nil ∧ s₁ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

pp: case inr.inr
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive s₁ s₂
hd : α
s₁' s₂' : Seq α
h✝ : s₁ = cons hd s₁' ∧ s₂ = cons hd s₂' ∧ motive s₁' s₂'
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
· cases s₁ <;> grind

Goal state after:
case inr.inr
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive s₁ s₂
hd : α
s₁' s₂' : Seq α
h✝ : s₁ = cons hd s₁' ∧ s₂ = cons hd s₂' ∧ motive s₁' s₂'
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
⊢ s.TerminatedAt 0 → s = nil

Tactic:
intro h

Goal state after:
case refine_1
α : Type u
s : Seq α
h : s.TerminatedAt 0
⊢ s = nil
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
this : ∀ (i : ℕ), Function.update (↑s) n (Option.map f (s.get? n)) i = none ↔ s.get? i = none
⊢ ∀ {n : ℕ}, s.get? n = none → s.get? (n + 1) = none

Tactic:
exact @s.prop

Goal state after:
Module: Mathlib.Tactic.ENatToNat

Goal state before:
pp: x : ℕ∞
⊢ ¬⊤ < x

Tactic:
cases x

Goal state after:
case top
⊢ ¬⊤ < ⊤

case coe
a✝ : ℕ
⊢ ¬⊤ < ↑a✝
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : (fun b ↦ some a = b) (s.think.val.get n)
⊢ a ∈ s

Tactic:
rcases n with - | n'

Goal state after:
case zero
α : Type u
s : Computation α
a : α
h : some a = s.think.val.get 0
⊢ a ∈ s

case succ
α : Type u
s : Computation α
a : α
n' : ℕ
h : some a = s.think.val.get (n' + 1)
⊢ a ∈ s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
h : s.Terminates
a : α
⊢ s.get = a → a ∈ s

Tactic:
intro h

Goal state after:
α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ a ∈ s
Module: Mathlib.Data.Seq.Computation

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

Tactic:
intro h

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
e : s n = none
h : Option.rec none (fun val ↦ some (f val)) none = some b
⊢ Option.rec none (fun val ↦ some (f val)) (s (n + 1)) = some b
Module: Mathlib.Data.Seq.Computation

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

Tactic:
intro h

Goal state after:
case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
a : α
e : s n = some a
h : Option.rec none (fun val ↦ some (f val)) (some a) = some b
⊢ Option.rec none (fun val ↦ some (f val)) (s (n + 1)) = some b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
n : ℕ
⊢ (∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none) → ¬s.get? n = none

Tactic:
intro h

Goal state after:
case refine_1
α : Type u
s : Seq α
n : ℕ
h : ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none
⊢ ¬s.get? n = none
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: ⊢ nats = 0 :: map succ nats

Tactic:
by
  apply Stream'.ext; intro n
  cases n
  · rfl
  rw [get_succ]; rfl

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
⊢ ∀ (h : s.tail.Terminates), n ≤ s.tail.length h

Tactic:
intro h

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
⊢ n ≤ s.tail.length h
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case pure
α : 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 : α
fs : Computation β
⊢ match (fs.bind g).destruct, (fs.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:
induction fs using recOn with

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

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
n : ℕ
k : α
⊢ s.get? n = some k → ∀ m ≤ n, ¬s.get? m = none

Tactic:
intro h

Goal state after:
α : Type u
s : Seq α
h✝ : s.Terminates
n : ℕ
k : α
h : s.get? n = some k
⊢ ∀ m ≤ n, ¬s.get? m = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
i✝ : ℕ
a✝ : α
⊢ (nil.toList ⋯)[i✝]? = some a✝ ↔ [][i✝]? = some a✝

Tactic:
simp [nil, toList, const]

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

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

Tactic:
intro h

Goal state after:
case zero.pure
α : Type u
β : Type v
f : α → Computation β
b : β
a : α
h : ((pure a).bind f).Results b 0
⊢ ∃ a_1 m n, (pure a).Results a_1 m ∧ (f a_1).Results b n ∧ 0 = n + m
Module: Mathlib.Data.Seq.Computation

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

Tactic:
intro h

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

Goal state before:
pp: case succ.pure
α : 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
a : α
⊢ ((pure a).bind f).Results b (n + 1) → ∃ a_2 m n_1, (pure a).Results a_2 m ∧ (f a_2).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
intro h

Goal state after:
case succ.pure
α : 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
a : α
h : ((pure a).bind f).Results b (n + 1)
⊢ ∃ a_1 m n_1, (pure a).Results a_1 m ∧ (f a_1).Results b n_1 ∧ n + 1 = n_1 + m
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ.think
α : 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'.think.bind f).Results b (n + 1) → ∃ a m n_1, s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
intro h

Goal state after:
case succ.think
α : 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 α
h : (s'.think.bind f).Results b (n + 1)
⊢ ∃ a m n_1, s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
⊢ a ∈ ss → a ∈ s₁ ∨ a ∈ s₂

Tactic:
intro h

Goal state after:
α : Type u
s₁ s₂ : Seq α
a : α
h✝ : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
h : a ∈ ss
⊢ a ∈ s₁ ∨ a ∈ s₂
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ (of v).s.get? 0 = (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })

Tactic:
rw [of, IntFractPair.seq1]

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
          | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p ↦ { a := 1, b := ↑p.b }) s }).s.get?
      0 =
    (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })
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✝

Tactic:
solve_by_elim [mem_map f hx]

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

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

Tactic:
by decide

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

Goal state before:
pp: x✝ : ℕ
⊢ fib x✝ = x✝.fastFib

Tactic:
rw [fastFib_eq]

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

Goal state before:
pp: case some.zero
K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (0 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : (squashSeq s 0).head = some { a := gp_head.a, b := gp_head.b + gp_succ_n.a / gp_succ_n.b }
⊢ convs'Aux s (0 + 2) = convs'Aux (squashSeq s 0) (0 + 1)

Tactic:
simp_all [convs'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]

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

Goal state before:
pp: case succ
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ m < m' + 1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
m_le_n : m' + 1 ≤ n
⊢ g.contsAux (m' + 1) = (g.squashGCF n).contsAux (m' + 1)

Tactic:
rcases n with - | n'

Goal state after:
case succ.zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ m < m' + 1, m ≤ 0 → g.contsAux m = (g.squashGCF 0).contsAux m
m_le_n : m' + 1 ≤ 0
⊢ g.contsAux (m' + 1) = (g.squashGCF 0).contsAux (m' + 1)

case succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
m' n' : ℕ
IH : ∀ m < m' + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m' + 1 ≤ n' + 1
⊢ g.contsAux (m' + 1) = (g.squashGCF (n' + 1)).contsAux (m' + 1)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
b✝ : ℤ
ifp_n_fr : K
nth_stream_eq : IntFractPair.stream v n = some { b := b✝, fr := ifp_n_fr }
this : ↑⌊{ b := b✝, fr := ifp_n_fr }.fr⁻¹⌋ ≤ { b := b✝, fr := ifp_n_fr }.fr⁻¹
⊢ ifp_n_fr ≠ 0

Tactic:
intro h

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
b✝ : ℤ
ifp_n_fr : K
nth_stream_eq : IntFractPair.stream v n = some { b := b✝, fr := ifp_n_fr }
this : ↑⌊{ b := b✝, fr := ifp_n_fr }.fr⁻¹⌋ ≤ { b := b✝, fr := ifp_n_fr }.fr⁻¹
h : ifp_n_fr = 0
⊢ False
Module: Mathlib.Algebra.DirectSum.Idempotents

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i : I
⊢ ((decompose V) (∑ i, idempotent V i)) i = ((decompose V) 1) i

Tactic:
decompose_sum,

Goal state after:
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i : I
⊢ (∑ i, (decompose V) (idempotent V i)) i = ((decompose V) 1) i
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_eq_zero : ifp.fr = 0
g_finite_correctness : v = g.convs n
⊢ v - g.convs n = 0

Tactic:
exact sub_eq_zero.2 g_finite_correctness

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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ n = 0 ∨ ¬g.TerminatedAt (n - 1)

Tactic:
rcases n with - | n'

Goal state after:
case zero
K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
stream_nth_eq : IntFractPair.stream v 0 = some ifp
conts : Pair K := g.contsAux (0 + 1)
pred_conts : Pair K := g.contsAux 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ 0 = 0 ∨ ¬g.TerminatedAt (0 - 1)

case succ
K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.refine_1.succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ (n + 1) = 0
⊢ f (1 - (1 - a ^ (n + 1)) ^ (n + 1)) = f e₁

Tactic:
simp only [map_sub, map_one, map_pow, ha, he₁.pow_succ_eq,
      he₁.one_sub.pow_succ_eq, sub_sub_cancel]

Goal state after:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
c : Con M
s : Multiset ι
f g : ι → M
h : ∀ x ∈ s, c (f x) (g x)
⊢ c (Multiset.map f s).prod (Multiset.map g s).prod

Tactic:
rcases s; simpa using c.list_prod h

Goal state after: