mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
⊢ (∑ k ∈ range (n % p + 1), ∑ k' ∈ range (n / p + 1), X ^ (k + p * k') * ↑((n % p).choose k * (n / p).choose k')).coeff
      k =
    (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)))

Tactic:
have h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1),
      k = x.1 + p * x.2 ↔ (k % p, k / p) = x := by
    intro ⟨x₁, x₂⟩ hx
    rw [Prod.mk.injEq]
    constructor <;> intro h
    · simp only [mem_product, mem_range] at hx
      have h' : x₁ < p := lt_of_lt_of_le hx.left <| mod_lt _ Fin.pos'
      rw [h, add_mul_mod_self_left, add_mul_div_left _ _ Fin.pos', eq_comm (b := x₂)]
      exact ⟨mod_eq_of_lt h', right_eq_add.mpr (div_eq_of_lt h')⟩
    · rw [← h.left, ← h.right, mod_add_div]

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
⊢ (∑ k ∈ range (n % p + 1), ∑ k' ∈ range (n / p + 1), X ^ (k + p * k') * ↑((n % p).choose k * (n / p).choose k')).coeff
      k =
    (Int.castRingHom (ZMod p)) (↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)))
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
⊢ n.minFac ^ 1 ∣ (Icc 1 (n - 1)).gcd n.choose

Tactic:
simpa using minFac_dvd_gcd_choose_of_isPrimePow h

Goal state after:
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit0
a✝ : PosNum
⊢ ↑a✝.bit0.minFac = (↑a✝.bit0).minFac

Tactic:
rw [minFac, Nat.minFac_eq, if_pos]

Goal state after:
case bit0
a✝ : PosNum
⊢ ↑2 = 2

case bit0.hc
a✝ : PosNum
⊢ 2 ∣ ↑a✝.bit0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit0 = ↑(pos p) + ↑(pos p)

Tactic:
cast_pos

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit0 = ↑p + ↑p
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit1 = ↑(pos p) + ↑(pos p) + 1

Tactic:
cast_pos

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit1 = ↑p + ↑p + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = Num.zero.succ'
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑p + -↑p + 1

Tactic:
conv at ep => change p = 1
      subst p
      simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocRing α
m n : ZNum
⊢ ↑↑m * ↑↑n = ↑m * ↑n

Tactic:
cast_to_int,

Goal state after:
α : Type u_1
inst✝ : NonAssocRing α
m n : ZNum
⊢ ↑m * ↑↑n = ↑m * ↑n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocRing α
m n : ZNum
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
by
  rw [← cast_to_int, mul_to_int, Int.cast_mul, cast_to_int, cast_to_int]

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.balance' x r).Sized

Tactic:
unfold Ordnode.balance'

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (if l.size + r.size ≤ 1 then l.node' x r
    else
      if r.size > delta * l.size then l.rotateL x r
      else if l.size > delta * r.size then l.rotateR x r else l.node' x r).Sized
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
x : α
⊢ findMax' x t.dual = t.findMin' x

Tactic:
← findMin'_dual,

Goal state after:
α : Type u_1
t : Ordnode α
x : α
⊢ t.dual.dual.findMin' x = t.findMin' x
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset

Tactic:
PrimeMultiset.factorMultiset_prod

Goal state after:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ u + v = u.prod.factorMultiset + v.prod.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ u + v = u.prod.factorMultiset + v.prod.factorMultiset

Tactic:
PrimeMultiset.factorMultiset_prod

Goal state after:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ u + v = u + v.prod.factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ u + v = u + v.prod.factorMultiset

Tactic:
PrimeMultiset.factorMultiset_prod

Goal state after:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ u + v = u + v
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (m • u).prod.factorMultiset = m • u.prod.factorMultiset

Tactic:
PrimeMultiset.factorMultiset_prod

Goal state after:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ m • u = m • u.prod.factorMultiset
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.nil
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ nil o₂
sep : All (fun x ↦ All (fun y ↦ x < y) nil) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size nil.size
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).glue nil) o₂ ∧
    ((Ordnode.node ls ll lx lr).glue nil).size = (Ordnode.node ls ll lx lr).size + nil.size

Tactic:
exact ⟨hl, rfl⟩

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

Goal state before:
pp: n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ m • u = m • u.prod.factorMultiset

Tactic:
PrimeMultiset.factorMultiset_prod

Goal state after:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ m • u = m • u
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }

Tactic:
by
  have : ∃ (n' : ℕ) (n : ℕ+) (_ : n' = n), p n := Exists.elim h fun n hn => ⟨n, n, rfl, hn⟩
  have n := Nat.findX this
  refine ⟨⟨n, ?_⟩, ?_, fun m hm pm => ?_⟩
  · obtain ⟨n', hn', -⟩ := n.prop.1
    rw [hn']
    exact n'.prop
  · obtain ⟨n', hn', pn'⟩ := n.prop.1
    simpa [hn', Subtype.coe_eta] using! pn'
  · exact n.prop.2 m hm ⟨m, rfl, pm⟩

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

Goal state before:
pp: m : ℕ+
v : PrimeMultiset
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Tactic:
by
  let h := @factorMultiset_le_iff m v.prod
  rw [v.factorMultiset_prod] at h
  exact h

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

Goal state before:
pp: case node.nil
α : Type u_1
inst✝ : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih✝ :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ ll o₂ →
      Valid' o₁ r o₂ →
        All (fun x ↦ All (fun y ↦ x < y) r) ll → Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ lr o₂ →
      Valid' o₁ r o₂ →
        All (fun x ↦ All (fun y ↦ x < y) r) lr → Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ nil o₂
sep : All (fun x ↦ All (fun y ↦ x < y) nil) (Ordnode.node ls ll lx lr)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge nil) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge nil).size = (Ordnode.node ls ll lx lr).size + nil.size

Tactic:
exact ⟨hl, rfl⟩

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

Goal state before:
pp: u : XgcdType
_h : ¬u.r = 0
⊢ sizeOf u.step < sizeOf u

Tactic:
apply u.step_wf _h

Goal state after:
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ico a b) = ∏ i, #(Icc (a i) (b i)) - 1

Tactic:
by
  rw [card_Ico_eq_card_Icc_sub_one, card_Icc]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr x y
| (TypeVec.id ::: Quot.factor r Mcongr this ∘ Quot.mk r) <$$> abs (M.dest (P F) x)

Tactic:
rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map,
          ← appendFun_comp_id]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M α), r x y → Mcongr x y
| (TypeVec.id ::: Quot.factor r Mcongr this ∘ Quot.mk r) <$$> abs (M.dest (P F) y)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
| (corec g x).dest

Tactic:
Cofix.dest,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
| Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯ (corec g x)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
⊢ r' a b →
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
      MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)

Tactic:
r'ab

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
⊢ MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) a) =
    MvQPF.abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ abs ((P F).objAppend1 a₀ (g ⊚ f'₀) fun x ↦ (P F).wMap g (f₀ x)) =
    abs ((P F).objAppend1 a₁ (g ⊚ f'₁) fun x ↦ (P F).wMap g (f₁ x))

Tactic:
rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]

Goal state after:
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
g : α ⟹ β
x y : (P F).W α
⊢ WEquiv x y → WEquiv (g <$$> x) (g <$$> y)

Tactic:
by
  intro h; induction h with
  | ind a f' f₀ f₁ h ih => rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.ind; exact ih
  | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h =>
    rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.abs
    change
      abs (q.P.objAppend1 a₀ (g ⊚ f'₀) fun x => q.P.wMap g (f₀ x)) =
        abs (q.P.objAppend1 a₁ (g ⊚ f'₁) fun x => q.P.wMap g (f₁ x))
    rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
  | trans x y z _ _ ih₁ ih₂ =>
    apply MvQPF.WEquiv.trans
    · apply ih₁
    · apply ih₂

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
⊢ ∀ (x y : Cofix F α), r x y → x = y

Tactic:
intro x y rxy

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x y : Cofix F α
rxy : r x y
⊢ x = y
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) <$$> (TypeVec.id ::: Quot.mk r) <$$> x.dest =
    (TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) <$$> (TypeVec.id ::: Quot.mk r) <$$> y.dest

Tactic:
h _ _ r'xy

Goal state after:
case h.inr
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r x y
this : ∀ (x y : Cofix F α), r x y → r' x y
⊢ (TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) <$$> (TypeVec.id ::: Quot.mk r) <$$> y.dest =
    (TypeVec.id ::: Quot.factor r (fun x y ↦ x = y ∨ r x y) this) <$$> (TypeVec.id ::: Quot.mk r) <$$> y.dest
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
⊢ ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest

Tactic:
intro x y rxy

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
⊢ (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
| (corec g x).dest

Tactic:
Cofix.dest,

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
| Quot.lift (fun x ↦ Quot.mk Mcongr <$> abs x.dest) ⋯ (corec g x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M
⊢ r' a b → abs ((P F).map (Quot.mk r') a.dest) = abs ((P F).map (Quot.mk r') b.dest)

Tactic:
r'ab

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
y : (P F).M
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M → (P F).M → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M
r'ab : r' a b
⊢ abs ((P F).map (Quot.mk r') a.dest) = abs ((P F).map (Quot.mk r') b.dest)
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
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' =
    (TypeVec.id ::: _root_.id) <$$> x'
⊢ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) (mk x')).fst = _root_.id (mk x')

Tactic:
rw [Fix.rec_eq]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' =
    (TypeVec.id ::: _root_.id) <$$> x'
⊢ ⟨mk
          ((TypeVec.id ::: Sigma.fst) <$$>
            (TypeVec.id ::: rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x'),
        g ((TypeVec.id ::: rec fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) <$$> x')⟩.fst =
    _root_.id (mk x')
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
⊢ ∀ (x y : Cofix F), r x y → x = y

Tactic:
intro x y rxy

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ x = y
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
    Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest

Tactic:
h _ _ r'xy

Goal state after:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest =
    Quot.factor r (fun x y ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
⊢ ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest

Tactic:
intro x y rxy

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
⊢ Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
ha : none ∈ s.destruct
t1 : LiftRelO R (LiftRel R) none b
c : α × WSeq α
hc : some c ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b (some c)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)

Tactic:
cases b
    · cases t2
    · cases t1

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

Goal state before:
pp: α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
⊢ a ∈ s

Tactic:
have := @IH (tail s)

Goal state after:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
this : some a ∈ s.tail.get? n → a ∈ s.tail
⊢ a ∈ s
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case3
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c } { s := ofList (c :: s₂.s.toList), i := s₂.i + c } = true

Tactic:
rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_neg (by simpa using h₂)]

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

Goal state before:
pp: s₁ s₂ : List Char
⊢ ltb (Legacy.iter (ofList s₁)) (Legacy.iter (ofList s₂)) = true ↔ ofList s₁ < ofList s₂

Tactic:
simp only [lt_iff_toList_lt, String.Legacy.iter, String.Legacy.mkIterator, String.toList_ofList]

Goal state after:
s₁ s₂ : List Char
⊢ ltb { s := ofList s₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ s₁ < s₂
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ ltb { s := ofList [], i := 0 } { s := ofList (c₂ :: cs₂), i := 0 } = true

pp: case nil.cons.hb
c₂ : Char
cs₂ : List Char
⊢ [] < c₂ :: cs₂

Tactic:
· unfold ltb
      simp [Legacy.Iterator.hasNext, Char.utf8Size_pos]

Goal state after:
case nil.cons.hb
c₂ : Char
cs₂ : List Char
⊢ [] < c₂ :: cs₂
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case right.ST
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
b : Option (β × WSeq β)
mb : b ∈ T.join.destruct
⊢ LiftRel (LiftRel (swap R)) ?m.340 S

Tactic:
rw [← LiftRel.swap R, ← LiftRel.swap]

Goal state after:
case right.ST
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
b : Option (β × WSeq β)
mb : b ∈ T.join.destruct
⊢ swap (LiftRel (LiftRel R)) ?m.340 S
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inl
α : Type u_1
k : ℕ
h✝ : Finite α
val✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ Fintype.card (Sym α k) = (Fintype.card α).multichoose k

Tactic:
exact card_sym_eq_multichoose _ _

Goal state after: