mathlib-initiative/mathlib-tactics huggingface dataset:
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
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).1) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₀⟩

Tactic:
;

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).1) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₀⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).2) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₁⟩

Tactic:
;

Goal state after:
case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ abs ((fun i t ↦ (↑t).2) <$$> ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₁⟩
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
⊢ (if delta * rs < ls then
      rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l x_2 r l_ih r_ih ↦
              if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        ll
    else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)) =
    if delta * rs < ls then
      rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l x_2 r l_ih r_ih ↦
              if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        ll
    else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)

Tactic:
;

Goal state after:
case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
⊢ (if delta * rs < ls then
      rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l x_2 r l_ih r_ih ↦
              if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        ll
    else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)) =
    if delta * rs < ls then
      rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l x_2 r l_ih r_ih ↦
              if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        ll
    else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
⊢ u ∈ {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i y} ↔
    ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
⊢ u ∈ {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i y} ↔
    ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
⊢ (∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u) ↔
    ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
⊢ (∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u) ↔
    ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ n.dist m ≤ 1

Tactic:
;

Goal state after:
n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ n.dist m ≤ 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: n m : ℕ
H : Raised n m
⊢ n.dist m ≤ 1

Tactic:
;

Goal state after:
n m : ℕ
H : Raised n m
⊢ n.dist m ≤ 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)

Tactic:
;

Goal state after:
k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)
Module: Mathlib.Data.QPF.Multivariate.Basic

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

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
i : Fin2 n
x : F α
x✝ : α i
⊢ x✝ ∈ supp x i ↔ x✝ ∈ {u | ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ}
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised r₁.size r₂.size
⊢ Raised (l.size + r₁.size + 1) (l.size + r₂.size + 1)

Tactic:
;

Goal state after:
α : Type u_1
l : Ordnode α
x₁ x₂ : α
r₁ r₂ : Ordnode α
H : Raised r₁.size r₂.size
⊢ Raised (l.size + r₁.size + 1) (l.size + r₂.size + 1)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: 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
⊢ ∀ (i : Fin2 n), ∀ u ∈ supp x i, u ∈ supp x i

Tactic:
;

Goal state after:
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
⊢ ∀ (i : Fin2 n), ∀ u ∈ supp x i, u ∈ supp x i
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: 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
i : Fin2 n
u : α i
⊢ u ∈ supp x i → u ∈ supp x i

Tactic:
;

Goal state after:
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
i : Fin2 n
u : α i
⊢ u ∈ supp x i → u ∈ supp x i
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
l0 : l.size = 0
⊢ r.size ≤ 1

Tactic:
;

Goal state after:
case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
l0 : l.size = 0
⊢ r.size ≤ 1
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: 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
h'' : (P F).B f' ⟹ α
hu : abs ⟨f', h''⟩ = x
u : α a'
j : (P F).B a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ f a' j ∈ supp x a'

Tactic:
;

Goal state after:
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
h'' : (P F).B f' ⟹ α
hu : abs ⟨f', h''⟩ = x
u : α a'
j : (P F).B a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ f a' j ∈ supp x a'
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case 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
⊢ LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u

Tactic:
;

Goal state after:
case 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
⊢ LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case 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
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u

Tactic:
;

Goal state after:
case 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
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case H2.inr.inl.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
left✝ : r.size ≤ r'
right✝ : r' ≤ r.size + 1
⊢ r.size ≤ delta * l.size

Tactic:
;

Goal state after:
case H2.inr.inl.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
left✝ : r.size ≤ r'
right✝ : r' ≤ r.size + 1
⊢ r.size ≤ delta * l.size
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case H2.inr.inl.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
left✝ : r.size ≤ r'
right✝ : r' ≤ r.size + 1
⊢ r.size ≤ 3 * l.size

Tactic:
;

Goal state after:
case H2.inr.inl.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
left✝ : r.size ≤ r'
right✝ : r' ≤ r.size + 1
⊢ r.size ≤ 3 * l.size
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
⊢ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)

Tactic:
;

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
⊢ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)
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
⊢ f j y ∈ supp x j

Tactic:
;

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
⊢ f j y ∈ supp x j
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
this : t.dual.dual.Bounded o₁ o₂
⊢ t.Bounded o₁ o₂

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
this : t.dual.dual.Bounded o₁ o₂
⊢ t.Bounded o₁ o₂
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
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
⊢ Quot.mk Mcongr (g <$$> aa₁) = Quot.mk Mcongr (g <$$> aa₂)

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
⊢ Quot.mk Mcongr (g <$$> aa₁) = Quot.mk Mcongr (g <$$> aa₂)
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
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := ⋯
⊢ IsPrecongr r' ∧ r' (g <$$> aa₁) (g <$$> aa₂)

Tactic:
;

Goal state after:
case h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := ⋯
⊢ IsPrecongr r' ∧ r' (g <$$> aa₁) (g <$$> aa₂)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: 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
⊢ supp (abs ⟨a, f⟩) i✝ = f i✝ '' univ

Tactic:
;

Goal state after:
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
⊢ supp (abs ⟨a, f⟩) i✝ = f i✝ '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: 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✝
⊢ u ∈ supp (abs ⟨a, f⟩) i✝ ↔ u ∈ f i✝ '' univ

Tactic:
;

Goal state after:
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✝
⊢ u ∈ supp (abs ⟨a, f⟩) i✝ ↔ u ∈ f i✝ '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: 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✝
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ) ↔ u ∈ f i✝ '' univ

Tactic:
;

Goal state after:
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✝
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ) ↔ u ∈ f i✝ '' 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' : (P F).B a' ⟹ α
e : abs ⟨a', f'⟩ = abs ⟨a, f⟩
⊢ u ∈ f i✝ '' univ

Tactic:
;

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' ⟹ α
e : abs ⟨a', f'⟩ = abs ⟨a, f⟩
⊢ u ∈ f i✝ '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), p i (f_1 i j)) ↔
    ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), p i (f_1 i j)) ↔
    ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.right
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := ⋯
⊢ r' (g <$$> aa₁) (g <$$> aa₂)

Tactic:
;

Goal state after:
case h.right
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := ⋯
⊢ r' (g <$$> aa₁) (g <$$> aa₂)
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
⊢ supp (g <$$> abs (repr x)) i = g i '' supp (abs (repr x)) i

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
⊢ supp (g <$$> abs (repr x)) i = g i '' supp (abs (repr x)) i
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (g <$$> abs ⟨a, f⟩) i = g i '' supp (abs ⟨a, f⟩) i

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (g <$$> abs ⟨a, f⟩) i = g i '' supp (abs ⟨a, f⟩) i
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y with
    | Ordering.lt => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match cmpLE x y with
    | Ordering.lt => (insertWith (fun x_1 ↦ x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 ↦ x) x r)

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y with
    | Ordering.lt => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match cmpLE x y with
    | Ordering.lt => (insertWith (fun x_1 ↦ x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 ↦ x) x r)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith (fun x_1 ↦ x) x t).Valid

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith (fun x_1 ↦ x) x t).Valid
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 (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ g (abs ⟨a, splitFun f' fun i ↦ (P F).wRec (fun a f' _f rec ↦ g (abs ⟨a, splitFun f' rec⟩)) (f i)⟩) =
    g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ g (abs ⟨a, splitFun f' fun i ↦ (P F).wRec (fun a f' _f rec ↦ g (abs ⟨a, splitFun f' rec⟩)) (f i)⟩) =
    g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match cmpLE x y with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match cmpLE x y with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.lt with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match Ordering.lt with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)

Tactic:
simp [insert'_eq_insertWith]

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

Goal state before:
pp: case eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.eq with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match Ordering.eq with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)

Tactic:
simp [insert'_eq_insertWith]

Goal state after: