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

Goal state before:
pp: case neg.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 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
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 : ¬0 < ratio * rr.size
rl0 : rl.size = 0
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂

Tactic:
not_lt,

Goal state after:
case neg.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 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
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 : ratio * rr.size ≤ 0
rl0 : rl.size = 0
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).Sized

pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized

Tactic:
· exact hl.rotateR hr

Goal state after:
case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: case refine_2.rel
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.factor R (Relation.EqvGen R) this) <$$> (TypeVec.id ::: Quot.mk R) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.factor R (Relation.EqvGen R) this) <$$> (TypeVec.id ::: Quot.mk R) <$$> dest P y✝

Tactic:
h

Goal state after:
case refine_2.rel
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.factor R (Relation.EqvGen R) this) <$$> (TypeVec.id ::: Quot.mk R) <$$> dest P ?refine_2.rel.y =
    (TypeVec.id ::: Quot.factor R (Relation.EqvGen R) this) <$$> (TypeVec.id ::: Quot.mk R) <$$> dest P y✝

case refine_2.rel.y
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : R x✝ y✝
⊢ P.M α

case refine_2.rel.a
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : R x✝ y✝
⊢ R x✝ ?refine_2.rel.y
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
by
  rw [← findMin_dual, dual_dual]

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

Goal state before:
pp: u v : PrimeMultiset
⊢ u.prod ∣ v.prod ↔ u ≤ v

Tactic:
let h := @PNat.factorMultiset_le_iff' u.prod v
  rw [u.factorMultiset_prod] at h
  exact h.symm

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

Goal state before:
pp: case e'_3.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
⊢ q ∈ k • PrimeMultiset.ofPrime p → q = p

Tactic:
h

Goal state after:
case e'_3.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • PrimeMultiset.ofPrime p
⊢ q = p
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊓ v).prod = n.gcd m

Tactic:
have : u = n.factorMultiset := u.factorMultiset_prod.symm

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

Goal state before:
pp: u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊔ v).prod = n.lcm m

Tactic:
have : u = n.factorMultiset := u.factorMultiset_prod.symm

Goal state after:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (u ⊔ v).prod = n.lcm m
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.nil.nil.node.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs nil lrx lrr)).Balanced
sl : (node ls nil lx (node lrs nil lrx lrr)).Sized
this : nil.size = 0 ∧ lrr.size = 0
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (nil.node' lx (node lrs nil lrx lrr)).node' x nil
    else (nil.node' lx (node lrs nil lrx lrr)).rotateR x nil

Tactic:
cases sl.2.2.2.2.size_eq_zero.1 this.2

Goal state after:
case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrx : α
hl : (nil.node' lx (node lrs nil lrx nil)).Balanced
sl : (node ls nil lx (node lrs nil lrx nil)).Sized
this : nil.size = 0 ∧ nil.size = 0
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (nil.node' lx (node lrs nil lrx nil)).node' x nil
    else (nil.node' lx (node lrs nil lrx nil)).rotateR x nil
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
⊢ let z := a.gcdZ b;
  let a' := a.gcdA' b;
  let b' := a.gcdB' b;
  w * z = (x * y).succPNat ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
z

Goal state after:
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
⊢ let a' := a.gcdA' b;
  let b' := a.gcdB' b;
  w * z = (x * y).succPNat ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
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)
⊢ (fun i t ↦ (↑t).1) <$$> abs ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = x

Tactic:
xeq,

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)
⊢ (fun i t ↦ (↑t).1) <$$> abs ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = abs ⟨a, f₀⟩
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case inr
k n : ℕ
⊢ Raised (k + n) (k + (n + 1))

Tactic:
· exact Or.inr rfl

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

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

Tactic:
· exact Or.inr rfl

Goal state after:
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
⊢ LiftP (fun i u ↦ u ∈ supp x i) x

Tactic:
h

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.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:
h

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 y : (P F).M α
h : r x y
⊢ Mcongr x y
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 <$$> x) i = g i '' supp x i

Tactic:
by
  rw [← abs_repr x]; obtain ⟨a, f⟩ := repr x; rw [← abs_map, MvPFunctor.map_eq]
  rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, ← image_comp]
  rfl

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ recF g ((P F).wMk a f' f) = g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)

Tactic:
rw [recF, MvPFunctor.wRec_eq]; rfl

Goal state after:
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' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ supp (abs ⟨a', f'⟩) i = supp ⟨a', f'⟩ i

Tactic:
h

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' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ supp ⟨a', f'⟩ i = supp ⟨a', f'⟩ i
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
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : SuppPreservation
⊢ LiftP p (abs ⟨a, f⟩) ↔ LiftP p ⟨a, f⟩

Tactic:
suppPreservation_iff_isUniform

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ LiftP p (abs ⟨a, f⟩) ↔ LiftP p ⟨a, f⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation ↔ IsUniform

Tactic:
suppPreservation_iff_isUniform

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ IsUniform ↔ IsUniform
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case refine_2
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₀ : (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 α
⊢ abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩ →
    recF u ((P F).wMk a₀ f'₀ f₀) = recF u ((P F).wMk a₁ f'₁ f₁)

Tactic:
h

Goal state after:
case refine_2
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₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ recF u ((P F).wMk a₀ f'₀ f₀) = recF u ((P F).wMk a₁ f'₁ f₁)
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₁)
x y : (P F).W α
⊢ ∀ (w : (P F).W α), WEquiv x y → WEquiv y w → recF u x = recF u y → recF u y = recF u w → recF u x = recF u w

Tactic:
z

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 y z : (P F).W α
⊢ WEquiv x y → WEquiv y z → recF u x = recF u y → recF u y = recF u z → recF u x = recF u z
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 y : (P F).W α
h : WEquiv x y
⊢ WEquiv y x

Tactic:
induction h with

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

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

Tactic:
h

Goal state after:
case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ (g ::: (P F).wMap g) <$$> abs ⟨a₁, (P F).appendContents f'₁ f₁⟩ =
    (g ::: (P F).wMap g) <$$> abs ((P F).objAppend1 a₁ f'₁ f₁)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
h : WEquiv x y
⊢ WEquiv (g <$$> x) (g <$$> y)

Tactic:
induction h with

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : 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:
by
  intro x
  rcases x; clear x; rename M (P F) α => x
  intro y
  rcases y; clear y; rename M (P F) α => y
  intro rxy
  apply Quot.sound
  let r' := fun x y => r (Quot.mk _ x) (Quot.mk _ y)
  have hr' : r' = fun x y => r (Quot.mk _ x) (Quot.mk _ y) := rfl
  have : IsPrecongr r' := by
    intro a b r'ab
    have h₀ :
      appendFun id (Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest q.P a) =
        appendFun id (Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest q.P b) := by
      rw [appendFun_comp_id, comp_map, comp_map]; exact h _ _ r'ab
    have h₁ : ∀ u v : q.P.M α, Mcongr u v → Quot.mk r' u = Quot.mk r' v := by
      intro u v cuv
      apply Quot.sound
      dsimp [r', hr']
      rw [Quot.sound cuv]
      apply h'
    let f : Quot r → Quot r' :=
      Quot.lift (Quot.lift (Quot.mk r') h₁)
        (by
          intro c
          apply Quot.inductionOn
            (motive := fun c =>
              ∀ b, r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b) c
          clear c
          intro c d
          apply Quot.inductionOn
            (motive := fun d => r (Quot.mk Mcongr c) d →
              Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d) d
          clear d
          intro d rcd; apply Quot.sound; apply rcd)
    have : f ∘ Quot.mk r ∘ Quot.mk Mcongr = Quot.mk r' := rfl
    rw [← this, appendFun_comp_id, q.P.comp_map, q.P.comp_map, abs_map, abs_map, abs_map, abs_map,
      h₀]
  exact ⟨r', this, rxy⟩

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

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → 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 : (P F).B a), r (f₀ i) (f₁ i)
⊢ (fun t ↦ (↑t).1) <$> abs ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = x

Tactic:
xeq,

Goal state after:
case h.left
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → 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 : (P F).B a), r (f₀ i) (f₁ i)
⊢ (fun t ↦ (↑t).1) <$> abs ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = abs ⟨a, f₀⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x y : (P F).W
h : Wequiv x y
⊢ recF u x = recF u y

Tactic:
induction h with

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

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

Tactic:
h

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

Goal state before:
pp: F : Type u → Type v
q : QPF F
x y : (P F).W
h : Wequiv x y
⊢ Wequiv y x

Tactic:
induction h with

Goal state after:
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)
h : mk <$> rec (Functor.map mk) <$> x = x
⊢ mk (mk <$> rec (Functor.map mk) <$> x) = mk x

Tactic:
h

Goal state after:
F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
h : mk <$> rec (Functor.map mk) <$> x = x
⊢ 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:
h

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 y : (P F).M
h : 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
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x
⊢ mk ((TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x) = mk x

Tactic:
h

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x
⊢ mk ((TypeVec.id ::: fun x ↦ x) <$$> x) = mk 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
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧
          (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧
            ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
⊢ LiftR (α.RelLast R) x.dest y.dest

Tactic:
rcases h x' Qx' with ⟨a, f', f₀, f₁, ux'eq, vx'eq, h'⟩
      rw [liftR_iff]
      refine
        ⟨a, q.P.appendContents f' f₀, q.P.appendContents f' f₁, xeq.symm ▸ ux'eq,
          yeq.symm ▸ vx'eq, ?_⟩
      intro i; cases i
      · apply h'
      · intro j
        apply Eq.refl

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✝ 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:
h

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : 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.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : 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:
h

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
⊢ (mk x).dest = x

Tactic:
have : Cofix.mk ∘ Cofix.dest = @_root_.id (Cofix F α) := funext Cofix.mk_dest

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ (mk x).dest = 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
⊢ Liftp (fun x_1 ↦ x_1 ∈ supp x) x

Tactic:
h

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 ∈ 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
h : SuppPreservation
α : Type u
a a' : (P F).A
f : (P F).B a → α
f' : (P F).B a' → α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
⊢ supp (abs ⟨a', f'⟩) = supp ⟨a', f'⟩

Tactic:
h

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' → α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
⊢ supp ⟨a', f'⟩ = supp ⟨a', f'⟩
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
⊢ (fun s1 s2 ↦ flatten (Computation.pure s2) = s1) s' s →
    Seq.BisimO (fun s1 s2 ↦ flatten (Computation.pure s2) = s1) s'.destruct s.destruct

Tactic:
h

Goal state after:
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 ↦ flatten (Computation.pure s2) = s1) s'.destruct s.destruct