mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node.refine_2.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩

Goal state after:
case node.node.refine_2.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

case node.node.refine_2.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : Set.ofPred p ⊆ ↑(range n)
⊢ nth p n = 0

Tactic:
rw [nth_of_card_le ((finite_toSet _).subset this)]

Goal state after:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : Set.ofPred p ⊆ ↑(range n)
⊢ #⋯.toFinset ≤ n
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
r0 : r.size ≤ 1
⊢ BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (0 + 0 + 1) (0 + r.size + 1)

Tactic:
revert r0

Goal state after:
case node.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
⊢ r.size ≤ 1 → BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (0 + 0 + 1) (0 + r.size + 1)
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
⊢ Liftp p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)

Tactic:
constructor

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
⊢ Liftp p x → ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)

case mpr
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
⊢ (∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)) → Liftp p x
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)) ↔ ∀ (i : P.B a), p (f i)

Tactic:
constructor

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)) → ∀ (i : P.B a), p (f i)

case mpr
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ (∀ (i : P.B a), p (f i)) → ∃ a_2 f_1, ⟨a, f⟩ = ⟨a_2, f_1⟩ ∧ ∀ (i : P.B a_2), p (f_1 i)
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mpr
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)

Tactic:
constructor

Goal state after:
case mpr.h
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ f_1, ⟨a, f⟩ = ⟨?mpr.w, f_1⟩ ∧ ∀ (i : P.B ?mpr.w), p (f_1 i)

case mpr.w
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ P.A
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mpr.h
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ f_1, ⟨a, f⟩ = ⟨?mpr.w, f_1⟩ ∧ ∀ (i : P.B ?mpr.w), p (f_1 i)

Tactic:
constructor

Goal state after:
case mpr.h.h
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩ ∧ ∀ (i : P.B ?mpr.w), p (?mpr.h.w i)

case mpr.h.w
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ P.B ?mpr.w → α
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mpr.h.h
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩ ∧ ∀ (i : P.B ?mpr.w), p (?mpr.h.w i)

Tactic:
constructor

Goal state after:
case mpr.h.h.left
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩

case mpr.h.h.right
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B ?mpr.w), p (?mpr.h.w i)
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mpr.h.h.left
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩

Tactic:
constructor

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

Goal state before:
pp: case mpr.h.h.right
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B a), p (f i)

Tactic:
constructor

Goal state after:
case mpr.h.h.right
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∀ (i : P.B a), p (f i)
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ Liftr r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)

Tactic:
constructor

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ Liftr r x y → ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)

case mpr
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ (∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)) → Liftr r x y
Module: Mathlib.Data.PFunctor.Univariate.Basic

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

Tactic:
constructor

Goal state after:
case h.left
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⟩

case h.right
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⟩
⊢ y = ⟨a, fun i ↦ (↑(f i)).2⟩ ∧ ∀ (i : P.B a), r (↑(f i)).1 (↑(f i)).2
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case h.right
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⟩
⊢ y = ⟨a, fun i ↦ (↑(f i)).2⟩ ∧ ∀ (i : P.B a), r (↑(f i)).1 (↑(f i)).2

Tactic:
constructor

Goal state after:
case h.right.left
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⟩
⊢ y = ⟨a, fun i ↦ (↑(f i)).2⟩

case h.right.right
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⟩
⊢ ∀ (i : P.B a), r (↑(f i)).1 (↑(f i)).2
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
p : PosNum
⊢ pos p = zero ↔ ZNum.pos p = zero.toZNum

Tactic:
constructor

Goal state after:
case zero.mp
p : PosNum
⊢ pos p = zero → ZNum.pos p = zero.toZNum

case zero.mpr
p : PosNum
⊢ ZNum.pos p = zero.toZNum → pos p = zero
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case pos
p a✝ : PosNum
⊢ pos p = pos a✝ ↔ ZNum.pos p = (pos a✝).toZNum

Tactic:
constructor

Goal state after:
case pos.mp
p a✝ : PosNum
⊢ pos p = pos a✝ → ZNum.pos p = (pos a✝).toZNum

case pos.mpr
p a✝ : PosNum
⊢ ZNum.pos p = (pos a✝).toZNum → pos p = pos a✝
Module: Mathlib.Data.PFunctor.Univariate.Basic

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

Tactic:
constructor

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

case h.right
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = ⟨a, f₀⟩
yeq : y = ⟨a, f₁⟩
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ (fun t ↦ (↑t).2) <$> ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = y
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x) ↔ ∃ y, f y = x

Tactic:
constructor

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x) → ∃ y, f y = x

case mpr
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ (∃ y, f y = x) → ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
⊢ LiftP p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
constructor

Goal state after:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
⊢ LiftP p x → ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
⊢ (∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)) → LiftP p x
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) ↔
    ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

Tactic:
constructor

Goal state after:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) →
    ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ (∀ (i : Fin2 n) (x : P.B a i), p (f i x)) →
    ∃ a_2 f_1, ⟨a, f⟩ = ⟨a_2, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_2 i), p (f_1 i j)
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)

Tactic:
constructor

Goal state after:
case mpr.h
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ f_1, ⟨a, f⟩ = ⟨?mpr.w, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B ?mpr.w i), p (f_1 i j)

case mpr.w
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ P.A
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr.h
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∃ f_1, ⟨a, f⟩ = ⟨?mpr.w, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B ?mpr.w i), p (f_1 i j)

Tactic:
constructor

Goal state after:
case mpr.h.h
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩ ∧ ∀ (i : Fin2 n) (j : P.B ?mpr.w i), p (?mpr.h.w i j)

case mpr.h.w
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ P.B ?mpr.w ⟹ α
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr.h.h
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩ ∧ ∀ (i : Fin2 n) (j : P.B ?mpr.w i), p (?mpr.h.w i j)

Tactic:
constructor

Goal state after:
case mpr.h.h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩

case mpr.h.h.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : P.B ?mpr.w i), p (?mpr.h.w i j)
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr.h.h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ⟨a, f⟩ = ⟨?mpr.w, ?mpr.h.w⟩

Tactic:
constructor

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr.h.h.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
constructor

Goal state after:
case mpr.h.h.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
a✝ : ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
⊢ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
⊢ LiftR r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)

Tactic:
constructor

Goal state after:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
⊢ LiftR r x y → ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)

case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
⊢ (∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)) → LiftR r x y
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case h
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ x = ⟨a, fun i j ↦ (↑(f i j)).1⟩ ∧
    y = ⟨a, fun i j ↦ (↑(f i j)).2⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (↑(f i j)).1 ((fun i j ↦ (↑(f i j)).2) i j)

Tactic:
constructor

Goal state after:
case h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ x = ⟨a, fun i j ↦ (↑(f i j)).1⟩

case h.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ y = ⟨a, fun i j ↦ (↑(f i j)).2⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (↑(f i j)).1 (↑(f i j)).2
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case h.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ y = ⟨a, fun i j ↦ (↑(f i j)).2⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (↑(f i j)).1 (↑(f i j)).2

Tactic:
constructor

Goal state after:
case h.right.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ y = ⟨a, fun i j ↦ (↑(f i j)).2⟩

case h.right.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ ∀ (i : Fin2 n) (j : P.B a i), r (↑(f i j)).1 (↑(f i j)).2
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
⊢ (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x) ↔ ∃ y, f i y = x

Tactic:
constructor

Goal state after:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
⊢ (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x) → ∃ y, f i y = x

case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
⊢ (∃ y, f i y = x) → ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case some
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ + ↑d * (2 * ↑q + 1) = ↑n ∧ ↑r₂ < ↑d

Tactic:
constructor

Goal state after:
case some.left
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ + ↑d * (2 * ↑q + 1) = ↑n

case some.right
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ < ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
x : CofixA F 0
y : CofixA F 1
⊢ Agree x y

Tactic:
constructor

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

Goal state before:
pp: case zero
F : PFunctor.{uA, uB}
X : Type w
f : X → ↑F X
i : X
⊢ Agree (sCorec f i 0) (sCorec f i (succ 0))

Tactic:
constructor

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

Goal state before:
pp: F : PFunctor.{uA, uB}
x : ↑F F.M
⊢ Agree (Approx.sMk x 0) (Approx.sMk x (succ 0))

Tactic:
constructor

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

Goal state before:
pp: F : PFunctor.{uA, uB}
x : ↑F F.M
n : ℕ
⊢ Agree (Approx.sMk x n.succ) (Approx.sMk x n.succ.succ)

Tactic:
constructor

Goal state after:
F : PFunctor.{uA, uB}
x : ↑F F.M
n : ℕ
⊢ ∀ (i : F.B x.fst), Agree ((x.snd i).approx n) ((x.snd i).approx (n + 1))
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case zero.f
F : PFunctor.{uA, uB}
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ Agree' 0 (M.mk ⟨a✝, f✝⟩) (M.mk ⟨a✝, f✝⟩)

Tactic:
constructor

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

Goal state before:
pp: case succ.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝, f✝⟩) (M.mk ⟨a✝, f✝⟩)

Tactic:
constructor

Goal state after:
case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨?succ.f.a✝, ?succ.f.x⟩

case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨?succ.f.a✝, ?succ.f.y⟩

case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ ∀ (i : F.B ?succ.f.a✝), Agree' n✝ (?succ.f.x i) (?succ.f.y i)

case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ F.A

case succ.f.x
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ F.B ?succ.f.a✝ → F.M

case succ.f.y
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ F.B ?succ.f.a✝ → F.M
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree (x.approx n) (y.approx (n + 1)) ↔ Agree' n x y

Tactic:
constructor

Goal state after:
case mp
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree (x.approx n) (y.approx (n + 1)) → Agree' n x y

case mpr
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree' n x y → Agree (x.approx n) (y.approx (n + 1))
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mp.zero
F : PFunctor.{uA, uB}
x y : F.M
h : Agree (x.approx 0) (y.approx (0 + 1))
⊢ Agree' 0 x y

Tactic:
constructor

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

Goal state before:
pp: n d : PosNum
⊢ ↑(n.div' d) = ↑(pos n) / ↑(pos d)

Tactic:
by rw [← Num.to_nat_to_int]; simp

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

Goal state before:
pp: n d : PosNum
⊢ -↑(n.div' d) = ↑(pos n) / ↑(neg d)

Tactic:
by rw [← Num.to_nat_to_int]; simp

Goal state after: