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

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
⊢ nth p n ≤ f n

Tactic:
by
  by_cases! hn : (∀ hf : Set.Finite (Set.ofPred p), n < hf.toFinset.card)
  · induction n using Nat.strong_induction_on with | _ n ih =>
    rw [nth_eq_sInf]
    refine csInf_le (by simp) ⟨hmaps hn, fun k hk => ?_⟩
    have : f k < f n := by apply hmono <;> grind
    grind
  · rcases hn with ⟨hf, hn⟩
    rw [nth, dif_pos hf, List.getD_eq_default _ _ (by simp [hn])]
    exact Nat.zero_le _

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

Goal state before:
pp: n : PosNum
⊢ n.bit1.Prime ↔ n.bit1.minFacAux (↑n) 1 = n.bit1

Tactic:
by
        refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans ?_)
        · simp only [cast_bit1]
          have := to_nat_pos n
          lia
        rw [← minFac_to_nat, to_nat_inj]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ -↑b.pred' = ↑1 - ↑b

Tactic:
← neg_sub,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ -↑b.pred' = -(↑b - ↑1)
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mp
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)

Tactic:
use a, fun i => (f i).val.fst, fun i => (f i).val.snd

Goal state after:
case h
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ x = ⟨a, fun i ↦ (↑(f i)).1⟩ ∧ y = ⟨a, fun i ↦ (↑(f i)).2⟩ ∧ ∀ (i : P.B a), r (↑(f i)).1 ((fun i ↦ (↑(f i)).2) i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateL x r).dual = r.dual.rotateR x l.dual

Tactic:
cases r <;> simp [rotateL, rotateR]; split_ifs <;>
    simp [dual_node3L, dual_node4L, node3R]

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

Goal state before:
pp: case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (Ordnode.node rs rl rx rr).size ≤ 9 * l.size + 5 ∨ (Ordnode.node rs rl rx rr).size ≤ 3
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂

Tactic:
hr.2.size_eq

Goal state after:
case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size + 1) ≤ 9 * l.size + 5 ∨ rl.size + rr.size + 1 ≤ 3
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.inl.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz rl.size rr.size
rl0 : rl.size = 0
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) rr.size

Tactic:
rw [rl0] at this ⊢
        rw [le_antisymm (balancedSz_zero.1 this.symm) rr0]
        decide

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
⊢ ∀ (x : α),
    True →
      ∃ a f_1 f',
        (f x).dest = ⟨a, f_1⟩ ∧
          (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', True ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
intro x

Goal state after:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
⊢ True →
    ∃ a f_1 f',
      (f x).dest = ⟨a, f_1⟩ ∧
        (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', True ∧ f_1 i = f x' ∧ f' i = M.corec g x'
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case neg
α : 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₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ¬ls > rs
v : Valid' (↑(rl.findMin' rx)) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
⊢ BalancedSz (Ordnode.node ls ll lx lr).size (rl.node' rx rr).size

Tactic:
hr.2.eq_node'

Goal state after:
case neg
α : 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₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (rl.node' rx rr).size
h✝ : ¬ls > rs
v : Valid' (↑(rl.findMin' rx)) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
⊢ BalancedSz (Ordnode.node ls ll lx lr).size (rl.node' rx rr).size
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case inr.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
⊢ ⟨i, a⟩ ≤ ⟨i, b⟩ ∨ ⟨i, b⟩ ≤ ⟨i, a⟩

Tactic:
obtain hab | hba := le_total a b

Goal state after:
case inr.inl.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
hab : a ≤ b
⊢ ⟨i, a⟩ ≤ ⟨i, b⟩ ∨ ⟨i, b⟩ ≤ ⟨i, a⟩

case inr.inl.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
hba : b ≤ a
⊢ ⟨i, a⟩ ≤ ⟨i, b⟩ ∨ ⟨i, b⟩ ≤ ⟨i, a⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
⊢ (fun i ↦ Subtype.val) <$$> y = abs ⟨a, fun i j ↦ ↑(f i j)⟩

Tactic:
← abs_repr y,

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
⊢ (fun i ↦ Subtype.val) <$$> abs (repr y) = abs ⟨a, fun i j ↦ ↑(f i j)⟩
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
⊢ ∀ (x y : (P F).M α), r x y → Mcongr x y

Tactic:
intro x

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
x : (P F).M α
⊢ ∀ (y : (P F).M α), r x y → Mcongr x 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
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 : Cofix F α), r x y → x = y

Tactic:
intro x

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 : Cofix F α
⊢ ∀ (y : Cofix F α), r x y → x = y
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case sz.right.left
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (map f l✝).Sized

pp: case sz.right.right
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (map f r✝).Sized

Tactic:
· exact t_l_valid.sz

Goal state after:
case sz.right.right
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (map f r✝).Sized
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case refine_3
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
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 : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
⊢ ∀ (u_1 v w : (P F).W α),
    WEquiv u_1 v → WEquiv v w → recF u u_1 = recF u v → recF u v = recF u w → recF u u_1 = recF u w

Tactic:
intro x

Goal state after:
case refine_3
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
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 : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
x : (P F).W α
⊢ ∀ (v w : (P F).W α), WEquiv x v → WEquiv v w → recF u x = recF u v → recF u v = recF u w → recF u x = recF u w
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ Subtype.val <$> y = abs ⟨a, fun i ↦ ↑(f i)⟩

Tactic:
← abs_repr y,

Goal state after:
case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ Subtype.val <$> abs (repr y) = abs ⟨a, fun i ↦ ↑(f i)⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ⟨a, fun i ↦ ↑(f i)⟩ = Subtype.val <$> y

Tactic:
← abs_repr y,

Goal state after:
case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ⟨a, fun i ↦ ↑(f i)⟩ = Subtype.val <$> abs (repr y)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

Tactic:
use a, fun i => (f i).val.fst, fun i => (f i).val.snd

Goal state after:
case h
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ x = abs ⟨a, fun i ↦ (↑(f i)).1⟩ ∧
    y = abs ⟨a, fun i ↦ (↑(f i)).2⟩ ∧ ∀ (i : (P F).B a), r (↑(f i)).1 ((fun i ↦ (↑(f i)).2) i)
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 (α ::: β) → β
x : F (α ::: Fix F α)
⊢ ∀ (a : (P F).W α), (recF g ∘ fixToW) ⟦a⟧ = rec g ⟦a⟧

Tactic:
intro x

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x✝ : F (α ::: Fix F α)
x : (P F).W α
⊢ (recF g ∘ fixToW) ⟦x⟧ = rec 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 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

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 : Cofix F α
⊢ ∀ (y : Cofix F α), r x y → x = y
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h'
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 := ⋯
x y : Cofix F α
rxy : r x y
⊢ ∀ (x : Cofix F α), r' x x

Tactic:
intro x

Goal state after:
case h'
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 : Cofix F α
⊢ r' x x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h
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 := ⋯
x y : Cofix F α
rxy : r x y
⊢ ∀ (x y : Cofix F α), r' x y → (TypeVec.id ::: Quot.mk r') <$$> x.dest = (TypeVec.id ::: Quot.mk r') <$$> y.dest

Tactic:
intro x

Goal state after:
case h
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 : Cofix F α
⊢ ∀ (y : Cofix F α), r' x y → (TypeVec.id ::: Quot.mk r') <$$> x.dest = (TypeVec.id ::: Quot.mk r') <$$> y.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
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (a : (P F).W α), g₁ (Quot.mk (⇑(wSetoid α)) a) = g₂ (Quot.mk (⇑(wSetoid α)) a)

Tactic:
intro x

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : (P F).W α
⊢ g₁ (Quot.mk (⇑(wSetoid α)) x) = g₂ (Quot.mk (⇑(wSetoid α)) 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 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

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 : Cofix F α
⊢ ∀ (y : Cofix F α), 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 α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x : Fix F
⊢ ∀ (x : F (Fix F)), rec g <$> x = h <$> x → rec g (mk x) = h (mk x)

Tactic:
intro x

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)
⊢ rec g <$> x = h <$> x → rec g (mk x) = h (mk 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 α)), (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x → rec g (mk x) = h (mk x)

Tactic:
intro x

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 α)
⊢ (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x → rec g (mk x) = h (mk x)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x : Fix F
⊢ ∀ (x : F (Fix F)), (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)

Tactic:
intro x

Goal state after:
F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk 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
x : Fix F α
⊢ ∀ (x : F (α ::: Fix F α)),
    (TypeVec.id ::: mk ∘ dest) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x → (mk ∘ dest) (mk x) = mk x

Tactic:
intro x

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : Fix F α
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x → (mk ∘ dest) (mk x) = mk x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
⊢ ∀ (x y : (P F).M), r x y → Mcongr x y

Tactic:
intro x

Goal state after:
F : Type u → Type u
q : QPF F
x✝ y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x✝ y
x : (P F).M
⊢ ∀ (y : (P F).M), r x y → Mcongr x y
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
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
⊢ ∀ (a : (P F).W α), p (Quot.mk (⇑(wSetoid α)) a)

Tactic:
intro x

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
x : (P F).W α
⊢ p (Quot.mk (⇑(wSetoid α)) 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
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
⊢ ∀ (x : Fix F α), p x

Tactic:
apply Quot.ind
  intro x
  induction x using q.P.wInd
  case ih a f' f ih =>
    change p ⟦q.P.wMk a f' f⟧
    rw [← Fix.ind_aux a f' f]
    apply h
    rw [MvQPF.liftP_iff]
    refine ⟨_, _, rfl, ?_⟩
    intro i j
    cases i
    · apply ih
    · trivial

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 : Cofix F α
⊢ ∀ (x y : Cofix F α),
    x = mk y.dest →
      (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> x.dest =
        (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> y.dest

Tactic:
intro x

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x : Cofix F α
⊢ ∀ (y : Cofix F α),
    x = mk y.dest →
      (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> x.dest =
        (TypeVec.id ::: Quot.mk fun x y ↦ x = mk y.dest) <$$> 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 → 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

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 : Cofix F
⊢ ∀ (y : Cofix F), r x y → x = y
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h'
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 := ⋯
x y : Cofix F
rxy : r x y
⊢ ∀ (x : Cofix F), r' x x

Tactic:
intro x

Goal state after:
case h'
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 : Cofix F
⊢ r' x x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h
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 := ⋯
x y : Cofix F
rxy : r x y
⊢ ∀ (x y : Cofix F), r' x y → Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest

Tactic:
intro x

Goal state after:
case h
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 : Cofix F
⊢ ∀ (y : Cofix F), r' x y → Quot.mk r' <$> x.dest = 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

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 : Cofix F
⊢ ∀ (y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest