mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.AList

Goal state before:
pp: case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
⊢ insertRec H0 IH (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }) =
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })

Tactic:
apply eq_of_heq

Goal state after:
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
⊢ insertRec H0 IH (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }) ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ (∀ (l : List (Sigma β)), l ∈ L → Pairwise (fun s s' ↦ s.fst ≠ s'.fst) l) ∧
      Pairwise (fun l₁ l₂ ↦ ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L ↔
    (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys) ∧ Pairwise (fun a b ↦ a.keys.Disjoint b.keys) L

Tactic:
refine and_congr (forall₂_congr fun l _ => by simp [nodupKeys_iff_pairwise]) ?_

Goal state after:
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ Pairwise (fun l₁ l₂ ↦ ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L ↔
    Pairwise (fun a b ↦ a.keys.Disjoint b.keys) L
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
f : β✝ → β✝
hf : ∃ a ∈ s, const α✝ id a = f
ha : ∃ a_1 ∈ t, f a_1 = a
⊢ a ∈ t

Tactic:
obtain ⟨b, hb, rfl⟩ := ha

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
f : β✝ → β✝
hf : ∃ a ∈ s, const α✝ id a = f
b : β✝
hb : b ∈ t
⊢ f b ∈ t
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
f : α✝ → β✝
s : Finset α✝
⊢ pure f <*> s = f <$> s

Tactic:
by simp only [pure_def, seq_def, sup_singleton, fmap_def]

Goal state after:
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ (s.sum id).support ⊆ s.sup Finsupp.support

Tactic:
by
  convert! Multiset.support_sum_subset s.1; simp

Goal state after:
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f + g) = neLocus 0 g

Tactic:
← neLocus_add_left f 0 g,

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f + g) = (f + 0).neLocus (f + g)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n k : ℕ
⊢ (↑n).lnot.testBit k = !(↑n).testBit k

Tactic:
by simp [lnot, testBit]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n k : ℕ
⊢ -[n+1].lnot.testBit k = !-[n+1].testBit k

Tactic:
by simp [lnot, testBit]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m x✝ : ℕ
⊢ Nat.shiftLeft' false m x✝ = m * 2 ^ x✝

Tactic:
simp [Nat.shiftLeft_eq]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n : ℕ
⊢ Nat.shiftLeft' false 1 n = 2 ^ n

Tactic:
simp [Nat.shiftLeft_eq]

Goal state after:
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
⊢ (drop l₂.length (l₁ ++ l₂).reverse).reverse = l₁

Tactic:
← length_reverse,

Goal state after:
α : Type u_1
l₁ l₂ : List α
⊢ (drop l₂.reverse.length (l₁ ++ l₂).reverse).reverse = l₁
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (hd :: tl ++ [a]) r = r.toListAppend (go f (hd :: tl ++ [a]) #[])

Tactic:
| cons hd tl =>

Goal state after:
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons
α : Type u_1
f : α → α
l₁ : List α
hd : α
tl : List α
x✝ : hd :: tl ≠ []
⊢ modifyLast f (l₁ ++ hd :: tl) = l₁ ++ modifyLast f (hd :: tl)

Tactic:
| cons hd tl =>

Goal state after:
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
⊢ q ≤ (drop q w).length

Tactic:
rw [length_drop]

Goal state after:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
⊢ q ≤ w.length - q
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₁ - Y₂) + Z₂

Tactic:
add_left_inj,

Goal state after:
case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₂ = X₁ ∩ X₂ + (Z₁ - Y₂)
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ (y : α), y ∈ Y → y < a
⊢ M.IsDershowitzMannaLT N

Tactic:
use X, Y, {a}, by simp, M_def, N_def

Goal state after:
case right
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ (y : α), y ∈ Y → y < a
⊢ ∀ (y : α), y ∈ Y → ∃ z, z ∈ {a} ∧ y < z
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: a : ℚ≥0
n : ℕ
h : 0 ≤ a
⊢ n ≤ ⌊↑a⌋₊ ↔ ↑↑n ≤ ↑a

Tactic:
Nat.le_floor_iff

Goal state after:
a : ℚ≥0
n : ℕ
h : 0 ≤ a
⊢ ↑n ≤ ↑a ↔ ↑↑n ≤ ↑a

a : ℚ≥0
n : ℕ
h : 0 ≤ a
⊢ 0 ≤ ↑a
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: case mpr
m n : ℕ
hm : m ≠ 1
p : ℕ
hp : Prime p
hdvd : p ∣ m
hdvd' : p ∣ n !
⊢ m.minFac ≤ n

Tactic:
exact le_trans (minFac_le_of_dvd hp.two_le hdvd) (hp.dvd_factorial.mp hdvd')

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = (k % p, k / p).1 + p * (k % p, k / p).2

Tactic:
mod_add_div

Goal state after:
case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = k
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : ¬(k % p, k / p).1 < n % p + 1 ∨ ¬(k % p, k / p).2 < n / p + 1
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
Nat.lt_succ_iff,

Goal state after:
case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : ¬(k % p, k / p).1 ≤ n % p ∨ ¬(k % p, k / p).2 < n / p + 1
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inl.inl
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : n < k + 1
ha : p (nth p n)
hk : k + 1 < #hf.toFinset
⊢ nth p n ≤ nth p k

Tactic:
Nat.lt_succ_iff,

Goal state after:
case inl.inl
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : n ≤ k
ha : p (nth p n)
hk : k + 1 < #hf.toFinset
⊢ nth p n ≤ nth p k
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Infinite
n : ℕ
h : n < k + 1
ha : p (nth p n)
⊢ nth p n ≤ nth p k

Tactic:
Nat.lt_succ_iff,

Goal state after:
case inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Infinite
n : ℕ
h : n ≤ k
ha : p (nth p n)
⊢ nth p n ≤ nth p k
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil
α : 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₂
hm : Valid' (↑x) nil ↑y
Hm : 0 < nil.size
H :
  l.size = 0 ∧ nil.size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ nil.size ∧
        delta * l.size ≤ nil.size + r.size ∧ 3 * (nil.size + r.size) ≤ 16 * l.size + 9 ∧ nil.size ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x nil y r) o₂

Tactic:
cases Hm

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑↑b + -↑↑a = -↑↑a + ↑↑b

Tactic:
← Int.cast_neg,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑↑b + ↑(-↑a) = ↑(-↑a) + ↑↑b
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
a✝ b✝ c✝ : ZNum
⊢ ↑c✝ * (↑a✝ + ↑b✝) = ↑a✝ * ↑c✝ + ↑b✝ * ↑c✝

Tactic:
simp [mul_add, _root_.mul_comm]

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

Goal state before:
pp: a✝ b✝ : Num
⊢ (↑a✝ * ↑b✝).size ≤ (↑a✝).size + (↑b✝).size

Tactic:
Nat.size_le,

Goal state after:
a✝ b✝ : Num
⊢ ↑a✝ * ↑b✝ < 2 ^ ((↑a✝).size + (↑b✝).size)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl.refl.refl.refl.refl.hrec
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a, f₂⟩) = iselect ps (M.mk ⟨a, f₁⟩)
i : F.B a
ps : Path F
h : n = length ps
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)

Tactic:
specialize hrec (⟨_, i⟩ :: ps) (congr_arg _ h)

Goal state after:
case succ.step.step.f.f.refl.refl.refl.refl.refl.hrec
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
i : F.B a
ps : Path F
hrec : iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f₂⟩) = iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f₁⟩)
h : n = length ps
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t₁ t₂ : Ordnode α
h₁ : t₁.Sized
h₂ : t₂.Sized
h : t₁.toList = t₂.toList
⊢ t₁.size = t₂.size

Tactic:
by rw [← length_toList h₁, h, length_toList h₂]

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| (g ::: fun x ↦ g <$$> x) <$$> dest P ⟨a, f⟩

Tactic:
M.dest,

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| (g ::: fun x ↦ g <$$> x) <$$> dest' P ⋯ ⟨a, f⟩.snd
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: p : Nat.Primes
⊢ factorMultisetEquiv.symm (↑p).factorMultiset = factorMultisetEquiv.symm (PrimeMultiset.ofPrime p)

Tactic:
change (p : ℕ+).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod

Goal state after:
p : Nat.Primes
⊢ (↑p).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: case succ
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
m : ℕ+
a✝ : m < PNat.find h₂ + 1 → ¬p m
hm : ∀ (m_1 : ℕ+), m_1 ≤ m → ¬p (m_1 + 1)
⊢ ¬p (m + 1)

Tactic:
exact hm _ le_rfl

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

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
⊢ lrl.size = 0 ∧ lrr.size = 0

Tactic:
have := balancedSz_zero.1 hl.1.symm

Goal state after:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : (node lrs lrl lrx lrr).size ≤ 1
⊢ lrl.size = 0 ∧ lrr.size = 0
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
⊢ let d := a.gcdD b;
  let w := a.gcdW b;
  let x := a.gcdX b;
  let 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:
intro d w x y z a' b'

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
a' : ℕ+ := a.gcdA' b
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.Ordmap.Ordset

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ l✝ a₂ → Valid' (Option.map f a₁) (map f l✝) (Option.map f a₂) ∧ (map f l✝).size = l✝.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ r✝ a₂ → Valid' (Option.map f a₁) (map f r✝) (Option.map f a₂) ∧ (map f r✝).size = r✝.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_ih_l' : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝) ∧ (map f l✝).size = l✝.size
t_ih_r' : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂) ∧ (map f r✝).size = r✝.size
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    (map f (Ordnode.node size✝ l✝ x✝ r✝)).size = (Ordnode.node size✝ l✝ x✝ r✝).size

Tactic:
clear t_ih_l t_ih_r

Goal state after:
case node
α : 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_ih_l' : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝) ∧ (map f l✝).size = l✝.size
t_ih_r' : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂) ∧ (map f r✝).size = r✝.size
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    (map f (Ordnode.node size✝ l✝ x✝ r✝)).size = (Ordnode.node size✝ l✝ x✝ r✝).size
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
⊢ (∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u) ↔ ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)

Tactic:
constructor <;> intros

Goal state after:
case mp.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
a✝ : ∀ (i : Fin2 n) (u : α i) (x : (P F).B a i), f i x = u → p u
i✝ : Fin2 n
x✝ : (P F).B a i✝
⊢ p (f i✝ x✝)

case mp.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(P F) α), supp (abs x) = supp x
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
h' : IsUniform
a✝¹ : ∀ (i : Fin2 n) (x : (P F).B a i), p (f i x)
i✝ : Fin2 n
u✝ : α i✝
x✝ : (P F).B a i✝
a✝ : f i✝ x✝ = u✝
⊢ p u✝
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_l a₂ → Valid' a₁ (erase x t_l) a₂ ∧ Raised (erase x t_l).size t_l.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ t_r a₂ → Valid' a₁ (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (erase x t_l).size t_l.size
t_ih_r' : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      size✝

Tactic:
clear t_ih_l t_ih_r

Goal state after:
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) ↑t_x ∧ Raised (erase x t_l).size t_l.size
t_ih_r' : Valid' (↑t_x) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (match cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
      size✝
Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma

Goal state before:
pp: n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(Sigma.P F) α), Sigma.abs F (f <$$> p) = f <$$> Sigma.abs F p

Tactic:
rintro α β f ⟨x, g⟩

Goal state after:
n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
α β : TypeVec.{u} n
f : α ⟹ β
x : (Sigma.P F).A
g : (Sigma.P F).B x ⟹ α
⊢ Sigma.abs F (f <$$> ⟨x, g⟩) = f <$$> Sigma.abs F ⟨x, g⟩
Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma

Goal state before:
pp: n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(Pi.P F) α), Pi.abs F (f <$$> p) = f <$$> Pi.abs F p

Tactic:
rintro α β f ⟨x, g⟩

Goal state after:
n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
α β : TypeVec.{u} n
f : α ⟹ β
x : (Pi.P F).A
g : (Pi.P F).B x ⟹ α
⊢ Pi.abs F (f <$$> ⟨x, g⟩) = f <$$> Pi.abs F ⟨x, g⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l : ∀ {a₁ : WithBot α} {a₂ : WithTop α}, Valid' a₁ t_l a₂ → x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r : ∀ {a₁ : WithBot α} {a₂ : WithTop α}, Valid' a₁ t_r a₂ → x ∈ t_r → (erase x t_r).size = t_r.size - 1
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : x ∈ node size✝ t_l t_x t_r
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
⊢ (erase x (node size✝ t_l t_x t_r)).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
clear t_ih_l t_ih_r

Goal state after:
case node
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : x ∈ node size✝ t_l t_x t_r
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
⊢ (erase x (node size✝ t_l t_x t_r)).size = (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ g₁ ⟦WType.mk a f⟧ = g₂ ⟦WType.mk a f⟧

Tactic:
rw [← Fix.ind_aux a f]

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ g₁ (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩)) = g₂ (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩))
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR (α.RelLast r) x✝.dest y✝.dest

Tactic:
← LiftR_RelLast_iff

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR' (α.RelLast' r) x✝.dest y✝.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid) (f a))
⊢ p ⟦WType.mk a f⟧

Tactic:
rw [← Fix.ind_aux a f]

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid) (f a))
⊢ p (mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩))
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h₀.fz
n : ℕ
ι ι' : Type u
n✝ : ℕ
α : TypeVec.{u} (n✝ + 1)
x : (α ::: ι).drop Fin2.fz
⊢ subtypeVal α.repeatEq Fin2.fz (diagSub Fin2.fz x) = prod.diag Fin2.fz x

Tactic:
| fz =>

Goal state after: