mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
by
  classical
  by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
  · simp only [Part.fix_def f h₀]
    constructor <;> intro hh
    · exact ⟨_, hh⟩
    have h₁ := Nat.find_spec h₀
    rw [dom_iff_mem] at h₁
    obtain ⟨y, h₁⟩ := h₁
    replace h₁ := approx_mono' f _ _ h₁
    suffices y = b by
      subst this
      exact h₁
    obtain ⟨i, hh⟩ := hh
    revert h₁; generalize succ (Nat.find h₀) = j; intro h₁
    wlog case : i ≤ j
    · rcases le_total i j with H | H <;> [skip; symm] <;> apply_assumption <;> assumption
    replace hh := approx_mono f case _ _ hh
    apply Part.mem_unique h₁ hh
  · simp only [fix_def' (⇑f) h₀, not_exists, false_iff, notMem_none]
    simp only [dom_iff_mem, not_exists] at h₀
    intro; apply h₀

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ (∑ a ∈ s, f a).toNat = ∑ a ∈ s, (f a).toNat

Tactic:
← natCast_inj,

Goal state after:
α : Type u_1
s : Finset α
f : α → ℕ∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ ↑(∑ a ∈ s, f a).toNat = ↑(∑ a ∈ s, (f a).toNat)
Module: Mathlib.Data.Fin.Tuple.BubbleSortInduction

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ ↦ toLex (f ∘ ⇑σ)
⊢ P (f ∘ ⇑(sort f))

Tactic:
refine
    @WellFounded.induction_bot' _ _ _ (IsWellFounded.wf : WellFounded (· < ·))
      (Equiv.refl _) (sort f) P (fun σ => f ∘ σ) (fun σ hσ hfσ => ?_) hf

Goal state after:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ ↦ toLex (f ∘ ⇑σ)
σ : Fin n ≃ Fin n
hσ : f ∘ ⇑σ ≠ f ∘ ⇑(sort f)
hfσ : P (f ∘ ⇑σ)
⊢ ∃ c < σ, P (f ∘ ⇑c)
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
⊢ k ∈ s₁.keys → k ∈ s₂.keys

Tactic:
hk

Goal state after:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
⊢ k ∈ s₂.keys
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case swap.some.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
b : α
l : List α
d : α
h₂ : f b = some d
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: b :: l)
h₁ : f b = some d
⊢ lookmap f (b :: b :: l) ~ lookmap f (b :: b :: l)

Tactic:
exact Perm.refl _

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ s₄ : AList β
p₁₂ : s₁.entries ~ s₂.entries
p₃₄ : s₃.entries ~ s₄.entries
⊢ (s₁ ∪ s₃).entries ~ (s₂ ∪ s₄).entries

Tactic:
by
  simp [p₁₂.kunion s₃.nodupKeys p₃₄]

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝

Tactic:
right
          refine ⟨?_, h'⟩
          intro h''
          apply h _ h''
          rw [keys, ← List.dlookup_isSome, h']
          exact rfl

Goal state after:
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: n : ℤ
⊢ fib (n + 1) * fib (n - 1) - fib n ^ 2 = (-1) ^ n.natAbs

Tactic:
by
  obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
  · exact fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq n
  · if hn : n = 0 then simp [hn] else
    obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
    simp_rw [show -((i + 1 : ℕ) : ℤ) + 1 = -i by simp, sub_eq_add_neg, ← neg_add, fib_neg,
      natAbs_neg, natAbs_natCast, ← fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq]
    grind

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: ⊢ bitwise or = lor

Tactic:
by
  funext m n
  rcases m with m | m <;> rcases n with n | n <;> try {rfl}
    <;> simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff,
      negSucc.injEq, Bool.true_or]
  · rw [Nat.bitwise_swap, Function.swap]
    congr
    funext x y
    cases x <;> cases y <;> rfl
  · simp
  · congr
    simp

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
⊢ rdropWhile p (l ++ [x]) = if p x = true then rdropWhile p l else l ++ [x]

Tactic:
simp only [rdropWhile, dropWhile, reverse_append, reverse_singleton, singleton_append]

Goal state after:
α : Type u_1
p : α → Bool
l : List α
x : α
⊢ (match p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse).reverse =
    if p x = true then (dropWhile p l.reverse).reverse else l ++ [x]
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]

Tactic:
rtakeWhile_concat,

Goal state after:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ (if p x = true then rtakeWhile p l ++ [x] else []) = rtakeWhile p l ++ [x]
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ rtakeWhile p (l ++ [x]) = []

Tactic:
rtakeWhile_concat,

Goal state after:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ (if p x = true then rtakeWhile p l ++ [x] else []) = []
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m

Tactic:
suffices n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m by simp [Ico, this]

Goal state after:
n m l : ℕ
⊢ n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
⊢ Ico n m ∩ Ico m l = []

Tactic:
by convert! inter_consecutive n m l

Goal state after:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h1 : s₁.length < s₂.length
⊢ s₁.length < (s₂ ++ t).length

Tactic:
List.length_append

Goal state after:
case inl
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h1 : s₁.length < s₂.length
⊢ s₁.length < s₂.length + t.length
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
⊢ s.length + t₁.length < (s ++ t₂).length

Tactic:
List.length_append

Goal state after:
case inl
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
⊢ s.length + t₁.length < s.length + t₂.length
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: case h1
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ fst (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) i✝ j✝ =
    fst ((of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) * (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))) i✝
      j✝

Tactic:
dsimp [mul_apply]

Goal state after:
case h1
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ fst (∑ j, A i✝ j * B j j✝) = ∑ j, fst (A i✝ j) * fst (B j j✝)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑m = ↑n ↔ m = n

Tactic:
to_int_inj

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ m = n ↔ m = n
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : lrs < ratio * lls
⊢ (node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)).dual =
    node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)

Tactic:
repeat simp [add_comm]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case neg
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : ¬lrs < ratio * lls
⊢ (node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx (node (lrr.size + 1) lrr x nil)).dual =
    node (ls + 1) (node (lrr.dual.size + 1) nil x lrr.dual) lrx
      (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))

Tactic:
repeat simp [add_comm]

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁸ : F.A
x✝¹ y✝¹ : F.B a✝⁸ → F.M
a✝⁷ : ∀ (i : F.B a✝⁸), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁶ : F.A
x✝ y✝ : F.B a✝⁶ → F.M
a✝⁵ : ∀ (i : F.B a✝⁶), Agree' n (x✝ i) (y✝ i)
a✝⁴ : F.A
f✝¹ : F.B a✝⁴ → F.M
a✝³ : M.mk ⟨a✝⁴, f✝¹⟩ = M.mk ⟨a✝⁸, y✝¹⟩
a✝² : F.A
f✝ : F.B a✝² → F.M
a✝¹ : M.mk ⟨a✝², f✝⟩ = M.mk ⟨a✝⁶, y✝⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁴, f✝¹⟩) = iselect ps (M.mk ⟨a✝², f✝⟩)
a✝ : M.mk ⟨a✝⁸, x✝¹⟩ = M.mk ⟨a✝⁶, x✝⟩
this : ⟨a✝⁸, x✝¹⟩ = ⟨a✝⁶, x✝⟩
⊢ (M.mk ⟨a✝⁴, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝², f✝⟩).approx (n + 1 + 1)

Tactic:
cases this

Goal state after:
case succ.step.step.f.f.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
this : ⟨a✝⁷, x✝⟩ = ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)

Tactic:
cases this

Goal state after:
case succ.step.step.f.f.refl.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
this : ⟨a✝⁷, x✝⟩ = ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)

Tactic:
cases this

Goal state after:
case succ.step.step.f.f.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : F.B a✝⁷ → F.M
a✝⁶ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk ⟨a✝⁷, x✝⟩ = M.mk ⟨a✝⁷, x✝⟩
⊢ (M.mk ⟨a✝⁵, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝³, f✝⟩).approx (n + 1 + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝¹ : F.A
f✝¹ : F.B a✝¹ → F.M
h₂ : M.mk ⟨a✝¹, f✝¹⟩ = M.mk ⟨a, f₂⟩
a✝ : F.A
f✝ : F.B a✝ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝¹, f✝¹⟩) = iselect ps (M.mk ⟨a✝, f✝⟩)
f₁ : F.B a → F.M
h₁ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₁⟩
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
this : ⟨a✝, f✝⟩ = ⟨a, f₁⟩
⊢ (CofixA.intro a✝¹ fun j ↦ (f✝¹ j).approx (n + 1)) = CofixA.intro a✝ fun j ↦ (f✝ j).approx (n + 1)

Tactic:
cases this

Goal state after:
case succ.step.step.f.f.refl.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝ : F.A
f✝ : F.B a✝ → F.M
h₂ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₂⟩
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝, f✝⟩) = iselect ps (M.mk ⟨a, f₁⟩)
h₁ : M.mk ⟨a, f₁⟩ = M.mk ⟨a, f₁⟩
⊢ (CofixA.intro a✝ fun j ↦ (f✝ j).approx (n + 1)) = CofixA.intro a fun j ↦ (f₁ j).approx (n + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝ : F.A
f✝ : F.B a✝ → F.M
h₂ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₂⟩
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝, f✝⟩) = iselect ps (M.mk ⟨a, f₁⟩)
this : ⟨a✝, f✝⟩ = ⟨a, f₂⟩
⊢ (CofixA.intro a✝ fun j ↦ (f✝ j).approx (n + 1)) = CofixA.intro a fun j ↦ (f₁ j).approx (n + 1)

Tactic:
cases this

Goal state after:
case succ.step.step.f.f.refl.refl.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
h₂ : M.mk ⟨a, f₂⟩ = M.mk ⟨a, f₂⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a, f₂⟩) = iselect ps (M.mk ⟨a, f₁⟩)
⊢ (CofixA.intro a fun j ↦ (f₂ j).approx (n + 1)) = CofixA.intro a fun j ↦ (f₁ j).approx (n + 1)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).size =
    l.size + (l✝.size + r✝.size + 1) + 1

Tactic:
split_ifs <;> simp [node3L_size, node4L_size hm.2.1] <;> abel

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
⊢ (node size✝ l x✝ r).toList.length = (node size✝ l x✝ r).realSize

Tactic:
rw [toList_node, List.length_append, List.length_cons, length_toList' l,
        length_toList' r]; rfl

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
⊢ IsBisimulation R

Tactic:
constructor <;> introv ih <;> rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩

Goal state after:
case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a', f'⟩)
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a', f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ a = a'

case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a, f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a, f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)

Tactic:
simp only [dest_mk] at h₀ h₁
    cases h₀
    cases h₁
    apply h₂

Goal state after:
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ (u.wp + 1) * ↑u.b + ((u.wp + 1) * u.qp + u.x) * ↑u.b = ↑u.w * ↑u.a + u.x * ↑u.b

Tactic:
have : u.wp + 1 = u.w := rfl

Goal state after:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
this : u.wp + 1 = ↑u.w
⊢ (u.wp + 1) * ↑u.b + ((u.wp + 1) * u.qp + u.x) * ↑u.b = ↑u.w * ↑u.a + u.x * ↑u.b
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.finish.v.1 = u.v.1

Tactic:
change (u.wp + 1) * u.b + ((u.wp + 1) * u.qp + u.x) * u.b = u.w * u.a + u.x * u.b
    have : u.wp + 1 = u.w := rfl
    rw [this, ← ha, u.qp_eq hr]
    ring

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a → α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ Liftr r x y

Tactic:
use abs ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩

Goal state after:
case h
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a → α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ (fun t ↦ (↑t).1) <$> abs ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = x ∧
    (fun t ↦ (↑t).2) <$> abs ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = y
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case ind
F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
a : (P F).A
f f' : (P F).B a → (P F).W
a✝ : ∀ (x : (P F).B a), Wequiv (f x) (f' x)
ih : ∀ (x : (P F).B a), recF u (f x) = recF u (f' x)
⊢ recF u (WType.mk a f) = recF u (WType.mk a f')

Tactic:
simp only [recF_eq', PFunctor.map_eq, Function.comp_def, ih]

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x✝ : Fix F
x : F (Fix F)
hyp' : rec g <$> x = h <$> x
⊢ rec g (mk x) = g (rec g <$> x)

Tactic:
Fix.rec_eq

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x✝ : Fix F
x : F (Fix F)
hyp' : rec g <$> x = h <$> x
⊢ g (rec g <$> x) = g (rec g <$> x)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x✝ : Fix F α
x : F (α ::: Fix F α)
hyp' : (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x
⊢ rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)

Tactic:
Fix.rec_eq

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x✝ : Fix F α
x : F (α ::: Fix F α)
hyp' : (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x
⊢ g ((TypeVec.id ::: rec g) <$$> x) = g ((TypeVec.id ::: rec g) <$$> x)