mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: case root
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
i : Fin2 n
c : P.drop.B a i
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
a' : P.A
g₁' : P.last.B a' → P.last.M
e₁' : x.dest = ⟨a', g₁'⟩
e₁ : dest P ⟨x, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨g₁' x_1, pathDestRight P e₁' f₁ x_1⟩⟩
g₂' : P.last.B a' → P.last.M
e₂' : x.dest = ⟨a', g₂'⟩
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨x, f₂⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩⟩
h'' :
  ∀ (i : (P.B a').last),
    R ((fun x_1 ↦ ⟨g₁' x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 ↦ ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩) i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)

Tactic:
cases h'.symm.trans e₁'

Goal state after:
case root.refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
i : Fin2 n
c : P.drop.B a i
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
g₂' : P.last.B a → P.last.M
e₂' : x.dest = ⟨a, g₂'⟩
e₁' : x.dest = ⟨a, f⟩
e₁ : dest P ⟨x, f₁⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩⟩
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨x, f₂⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩⟩
h'' :
  ∀ (i : (P.B a).last),
    R ((fun x_1 ↦ ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 ↦ ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩) i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: case child
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
i : P.last.B a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : P.mp.B (f i) ⟹ α), R ⟨f i, f₁⟩ ⟨f i, f₂⟩ → f₁ c p = f₂ c p
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
a' : P.A
g₁' : P.last.B a' → P.last.M
e₁' : x.dest = ⟨a', g₁'⟩
e₁ : dest P ⟨x, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨g₁' x_1, pathDestRight P e₁' f₁ x_1⟩⟩
g₂' : P.last.B a' → P.last.M
e₂' : x.dest = ⟨a', g₂'⟩
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨x, f₂⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩⟩
h'' :
  ∀ (i : (P.B a').last),
    R ((fun x_1 ↦ ⟨g₁' x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 ↦ ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩) i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)

Tactic:
cases h'.symm.trans e₁'

Goal state after:
case child.refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁ : P.mp.A
i✝ : Fin2 n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h' : x.dest = ⟨a, f⟩
i : P.last.B a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : P.mp.B (f i) ⟹ α), R ⟨f i, f₁⟩ ⟨f i, f₂⟩ → f₁ c p = f₂ c p
f₁ f₂ : P.mp.B x ⟹ α
r : R ⟨x, f₁⟩ ⟨x, f₂⟩
g₂' : P.last.B a → P.last.M
e₂' : x.dest = ⟨a, g₂'⟩
e₁' : x.dest = ⟨a, f⟩
e₁ : dest P ⟨x, f₁⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩⟩
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨x, f₂⟩ = ⟨a, splitFun (pathDestLeft P e₁' f₁) fun x_1 ↦ ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩⟩
h'' :
  ∀ (i : (P.B a).last),
    R ((fun x_1 ↦ ⟨f x_1, pathDestRight P e₁' f₁ x_1⟩) i) ((fun x_1 ↦ ⟨g₂' x_1, pathDestRight P e₂' f₂ x_1⟩) i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (l.rotateR x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
rw [← all_dual, dual_rotateR, all_rotateL]; simp [all_dual, and_comm, and_left_comm, and_assoc]

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

Goal state before:
pp: case head
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
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₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ : a = a''
h₁ : a' = a''
⊢ a = a'

Tactic:
rw [h₀, h₁]

Goal state after:
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

pp: case node.node
α : 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
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)) o₂ ∧
    ((Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)).size =
      (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size

Tactic:
· exact ⟨hl, rfl⟩

Goal state after:
case node.node
α : 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
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)) o₂ ∧
    ((Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)).size =
      (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size
Module: Mathlib.Data.PNat.Xgcd

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

Tactic:
decreasing_by apply u.step_wf _h

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

Goal state before:
pp: x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.flip.IsReduced

Tactic:
flip_isReduced

Goal state after:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.IsReduced
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ supp x i
a' : Fin2 n
⊢ ∀ (a'_1 : (P F).A) (f' : (P F).B a'_1 ⟹ α), abs ⟨a'_1, f'⟩ = x → f a' '' univ ⊆ f' a' '' univ

Tactic:
f'

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ supp x i
a' : Fin2 n
f' : (P F).A
⊢ ∀ (f'_1 : (P F).B f' ⟹ α), abs ⟨f', f'_1⟩ = x → f a' '' univ ⊆ f'_1 a' '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mpr.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs ⟨a, f⟩ = x
h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
j : Fin2 n
y : (P F).B a j
a' : (P F).A
⊢ ∀ (f_1 : (P F).B a' ⟹ α), abs ⟨a', f_1⟩ = x → f j y ∈ f_1 j '' univ

Tactic:
f'

Goal state after:
case mpr.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs ⟨a, f⟩ = x
h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
j : Fin2 n
y : (P F).B a j
a' : (P F).A
f' : (P F).B a' ⟹ α
⊢ abs ⟨a', f'⟩ = x → f j y ∈ f' j '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i✝ : Fin2 n
u : α i✝
h' : u ∈ f i✝ '' univ
a' : (P F).A
⊢ ∀ (f_1 : (P F).B a' ⟹ α), abs ⟨a', f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ

Tactic:
f'

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i✝ : Fin2 n
u : α i✝
h' : u ∈ f i✝ '' univ
a' : (P F).A
f' : (P F).B a' ⟹ α
⊢ abs ⟨a', f'⟩ = abs ⟨a, f⟩ → u ∈ f' i✝ '' univ
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' (Option.map f a₁) nil (Option.map f a₂)

Tactic:
apply valid'_nil

Goal state after:
case nil
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ nil.Bounded (Option.map f a₁) (Option.map f a₂)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
⊢ ∀ (f' : (P F).B a' ⟹ α), abs ⟨a, f⟩ = abs ⟨a', f'⟩ → ∀ (i : Fin2 n), f i '' univ = f' i '' univ

Tactic:
f'

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
⊢ abs ⟨a, f⟩ = abs ⟨a', f'⟩ → ∀ (i : Fin2 n), f i '' univ = f' i '' univ
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case refine_1
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₁)
a : (P F).A
⊢ ∀ (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α),
    (∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)) →
      (∀ (x : (P F).last.B a), recF u (f₀ x) = recF u (f₁ x)) → recF u ((P F).wMk a f' f₀) = recF u ((P F).wMk a f' f₁)

Tactic:
f'

Goal state after:
case refine_1
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₁)
a : (P F).A
f' : (P F).drop.B a ⟹ α
⊢ ∀ (f₀ f₁ : (P F).last.B a → (P F).W α),
    (∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)) →
      (∀ (x : (P F).last.B a), recF u (f₀ x) = recF u (f₁ x)) → recF u ((P F).wMk a f' f₀) = recF u ((P F).wMk a f' f₁)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case sz.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
⊢ size✝ = l✝.size + (map f r✝).size + 1

Tactic:
t_r_size

Goal state after:
case sz.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
⊢ size✝ = l✝.size + r✝.size + 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.bal.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
⊢ BalancedSz l✝.size (map f r✝).size

Tactic:
t_r_size

Goal state after:
case node.bal.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
⊢ BalancedSz l✝.size r✝.size
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'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
⊢ ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v

Tactic:
intro u

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
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
u : (P F).M α
⊢ ∀ (v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
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'ab : r' a b
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs a.dest = Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest
⊢ ∀ (u v : (P F).M), Mcongr u v → Quot.mk r' u = Quot.mk r' v

Tactic:
intro u

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
h₀ : Quot.mk r <$> Quot.mk Mcongr <$> abs a.dest = Quot.mk r <$> Quot.mk Mcongr <$> abs b.dest
u : (P F).M
⊢ ∀ (v : (P F).M), Mcongr u v → Quot.mk r' u = Quot.mk r' v
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
hr : r ≠ 0
⊢ 0 < r.sign * r

Tactic:
refine lt_of_le_of_ne (sign_mul_nonneg r) fun h => hr ?_
  have hs0 := (zero_eq_mul.mp h).resolve_right hr
  exact sign_eq_zero_iff.mp hs0

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

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
⊢ ↑((P F₂).comp (P F₁)) α → Functor.Comp F₂ F₁ α

Tactic:
dsimp [Functor.Comp]

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
⊢ ↑((P F₂).comp (P F₁)) α → F₂ (F₁ α)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
⊢ Functor.Comp F₂ F₁ α → ↑((P F₂).comp (P F₁)) α

Tactic:
dsimp [Functor.Comp]

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
⊢ F₂ (F₁ α) → ↑((P F₂).comp (P F₁)) α
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
⊢ ∀ (x : Functor.Comp F₂ F₁ α),
    id (fun p ↦ abs ⟨p.fst.fst, fun x ↦ abs ⟨p.fst.snd x, fun y ↦ p.snd ⟨x, y⟩⟩⟩)
        (id
          (fun y ↦
            ⟨⟨(repr y).fst, fun u ↦ (repr ((repr y).snd u)).fst⟩, id fun x ↦ (repr ((repr y).snd x.fst)).snd x.snd⟩)
          x) =
      x

Tactic:
dsimp [Functor.Comp]

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
⊢ ∀ (x : F₂ (F₁ α)),
    abs ⟨(repr x).fst, fun x_1 ↦ abs ⟨(repr ((repr x).snd x_1)).fst, fun y ↦ (repr ((repr x).snd x_1)).snd y⟩⟩ = x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
⊢ ∀ u ∈ supp x, u ∈ supp x

Tactic:
intro u

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
u : α
⊢ u ∈ supp x → u ∈ supp x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : (P F).A
⊢ ∀ (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ

Tactic:
f'

Goal state after:
case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : (P F).A
f' : (P F).B a' → α
⊢ abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr.mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ u ∈ supp x, p u
i : (P F).B a
a' : (P F).A
⊢ ∀ (f_1 : (P F).B a' → α), abs ⟨a', f_1⟩ = x → f i ∈ f_1 '' univ

Tactic:
f'

Goal state after:
case mpr.mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ u ∈ supp x, p u
i : (P F).B a
a' : (P F).A
f' : (P F).B a' → α
⊢ abs ⟨a', f'⟩ = x → f i ∈ f' '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
h' : u ∈ f '' univ
a' : (P F).A
⊢ ∀ (f_1 : (P F).B a' → α), abs ⟨a', f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ

Tactic:
f'

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
h' : u ∈ f '' univ
a' : (P F).A
f' : (P F).B a' → α
⊢ abs ⟨a', f'⟩ = abs ⟨a, f⟩ → u ∈ f' '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
a a' : (P F).A
f : (P F).B a → α
⊢ ∀ (f' : (P F).B a' → α), abs ⟨a, f⟩ = abs ⟨a', f'⟩ → f '' univ = f' '' univ

Tactic:
f'

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
a a' : (P F).A
f : (P F).B a → α
f' : (P F).B a' → α
⊢ abs ⟨a, f⟩ = abs ⟨a', f'⟩ → f '' univ = f' '' univ
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 (α ::: (Cofix F α ⊕ β))
x : β
⊢ (corec' g x).dest = (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x

Tactic:
rw [Cofix.corec', Cofix.dest_corec]; dsimp
  congr!; ext (i | i) <;> erw [corec_roll] <;> dsimp [Cofix.corec']
  · mv_bisim i with R a b x Ha Hb
    rw [Ha, Hb, Cofix.dest_corec]
    dsimp [Function.comp_def]
    repeat rw [MvFunctor.map_map, ← appendFun_comp_id]
    apply liftR_map_last'
    dsimp [Function.comp_def]
    intros
    exact ⟨_, rfl, rfl⟩
  · congr 1 with y
    erw [appendFun_id_id]
    simp [MvFunctor.id_map, Sum.elim]

Goal state after:
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
⊢ enumerate sel s m = none

Tactic:
by
    cases hs : sel s
    · exact enumerate_eq_none_of_sel sel hs
    · cases m with
      | zero => contradiction
      | succ m' =>
        simp only [enumerate, hs] at h ⊢
        have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
        exact enumerate_eq_none h hm

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

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

Tactic:
let ⟨a', h'⟩ := head_some_of_head_tail_some h
      exact IH h'

Goal state after:
Module: Mathlib.Data.Set.FiniteExhaustion

Goal state before:
pp: case pos.refine_3
α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty ↑s
f : ℕ → ↑s
hf : Function.Surjective f
⊢ ⋃ n, Subtype.val ∘ f '' {i | i ≤ n} = s

Tactic:
simp [← image_image, ← image_iUnion, iUnion_le_nat, range_eq_univ.mpr hf]

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

Goal state before:
pp: case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Prod.fst <$> some a ∈ t.head

Tactic:
· obtain ⟨a, s'⟩ := a
    obtain ⟨b, t'⟩ := b
    rw [dst.left]
    exact @Computation.mem_map _ _ (@Functor.map _ _ (α × WSeq α) _ Prod.fst)
      (some (b, t')) (destruct t) dtm

Goal state after: