mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: case neg.refine_2
n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∈ ↑n.properDivisors

Tactic:
have : k ∣ n := by
      rw [← h, ← prod_factorization_pow_eq_self hn]
      apply prod_dvd_prod_of_subset_of_dvd <| support_mono hlt.le
      exact fun p _ ↦ Nat.pow_dvd_pow p <| hlt.le p
    refine mem_properDivisors.mpr ⟨this, lt_of_le_of_ne (le_of_dvd (Nat.pos_of_ne_zero hn) this) ?_⟩
    suffices k.factorization = f from (this ▸ hlt.ne <| congrArg _ ·)
    exact h ▸ factorization_prod_pow_eq_self_of_le_factorization hlt.le

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_1
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Finite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x

pp: case refine_2
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Infinite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
· rcases exists_lt_card_finite_nth_eq hf h with ⟨n, hn, hx⟩
    exact ⟨n, fun _ => hn, hx⟩

Goal state after:
case refine_2
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Infinite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
· rcases id rr with _ | rrs
      · rcases rl with _ | ⟨_, _, rlx⟩
        · exact node 2 nil x r
        · exact node 3 (ι x) rlx ι rx
      · rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
        · exact node 3 (ι x) rx rr
        · exact
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else
              node (rs + 1) (node (size rll + 1) nil x rll) rlx
                (node (size rlr + rrs + 1) rlr rx rr)

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit0.sub' b.bit0) = ↑a.bit0 - ↑b.bit0

Tactic:
rw [sub', ZNum.cast_bit0, cast_sub' a b]
    have : ((a + -b + (a + -b) : ℤ) : α) = a + a + (-b + -b) := by simp [add_left_comm]
    simpa [sub_eq_add_neg] using this

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

Goal state before:
pp: case pos.zero
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
⊢ 0 + mr.size ≤ 1 → BalancedSz 1 0 ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + 0 + 1) (mr.size + 1 + 1)

Tactic:
cases size mr

Goal state after:
case pos.zero.zero
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
⊢ 0 + 0 ≤ 1 → BalancedSz 1 0 ∧ BalancedSz 0 1 ∧ BalancedSz (1 + 0 + 1) (0 + 1 + 1)

case pos.zero.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
n✝ : ℕ
⊢ 0 + (n✝ + 1) ≤ 1 → BalancedSz 1 0 ∧ BalancedSz (n✝ + 1) 1 ∧ BalancedSz (1 + 0 + 1) (n✝ + 1 + 1 + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ ZNum.ofInt' (-[n + 1+1] + 1) = ZNum.ofInt' -[n + 1+1] + 1

Tactic:
change ZNum.ofInt' -[n+1] = ZNum.ofInt' -[(n + 1)+1] + 1
    dsimp only [ZNum.ofInt', ZNum.ofInt']
    rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ,
      @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]

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

Goal state before:
pp: case pos.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
n✝ : ℕ
⊢ n✝ + 1 + mr.size ≤ 1 → BalancedSz 1 (n✝ + 1) ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + (n✝ + 1) + 1) (mr.size + 1 + 1)

Tactic:
cases size mr

Goal state after:
case pos.succ.zero
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
n✝ : ℕ
⊢ n✝ + 1 + 0 ≤ 1 → BalancedSz 1 (n✝ + 1) ∧ BalancedSz 0 1 ∧ BalancedSz (1 + (n✝ + 1) + 1) (0 + 1 + 1)

case pos.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
n✝¹ n✝ : ℕ
⊢ n✝¹ + 1 + (n✝ + 1) ≤ 1 →
    BalancedSz 1 (n✝¹ + 1) ∧ BalancedSz (n✝ + 1) 1 ∧ BalancedSz (1 + (n✝¹ + 1) + 1) (n✝ + 1 + 1 + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m : Num
p : PosNum
⊢ pos p = m ↔ ZNum.pos p = m.toZNum

Tactic:
cases m

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

case pos
p a✝ : PosNum
⊢ pos p = pos a✝ ↔ ZNum.pos p = (pos a✝).toZNum
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m : Num
p : PosNum
h : ZNum.neg p = m.toZNum
⊢ m ∈ ofZNum' (ZNum.neg p)

Tactic:
cases m

Goal state after:
case zero
p : PosNum
h : ZNum.neg p = zero.toZNum
⊢ zero ∈ ofZNum' (ZNum.neg p)

case pos
p a✝ : PosNum
h : ZNum.neg p = (pos a✝).toZNum
⊢ pos a✝ ∈ ofZNum' (ZNum.neg p)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocRing α
m n : ZNum
⊢ ↑↑(m * n) = ↑m * ↑n

Tactic:
mul_to_int,

Goal state after:
α : Type u_1
inst✝ : NonAssocRing α
m n : ZNum
⊢ ↑(↑m * ↑n) = ↑m * ↑n
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ 0 < s

Tactic:
by
  rw [h.1]; apply Nat.le_add_left

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node4L x m y r).dual = r.dual.node4R y m.dual x l.dual

Tactic:
cases m

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
⊢ (l.node4L x nil y r).dual = r.dual.node4R y nil.dual x l.dual

case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (l.node4L x (node size✝ l✝ x✝ r✝) y r).dual = r.dual.node4R y (node size✝ l✝ x✝ r✝).dual x l.dual
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node4R x m y r).dual = r.dual.node4L y m.dual x l.dual

Tactic:
cases m

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
⊢ (l.node4R x nil y r).dual = r.dual.node4L y nil.dual x l.dual

case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (l.node4R x (node size✝ l✝ x✝ r✝) y r).dual = r.dual.node4L y (node size✝ l✝ x✝ r✝).dual x l.dual
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
⊢ supp ⟨a, f⟩ i = f i '' univ

Tactic:
by
  ext x; simp only [supp, image_univ, mem_range, mem_ofPred_eq]
  constructor <;> intro h
  · apply @h fun i x => ∃ y : P.B a i, f i y = x
    rw [liftP_iff']
    intros
    exact ⟨_, rfl⟩
  · simp only [liftP_iff']
    cases h
    subst x
    tauto

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

Goal state before:
pp: n : PosNum
d : ZNum
⊢ subNatNat (↑d).natAbs (↑n.pred' % (↑d).natAbs + 1) = -↑n % ↑d

Tactic:
n.to_int_eq_succ_pred

Goal state after:
n : PosNum
d : ZNum
⊢ subNatNat (↑d).natAbs (↑n.pred' % (↑d).natAbs + 1) = -(↑↑n.pred' + 1) % ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ
F : PFunctor.{uA, uB}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
⊢ sCorec f x₀ (n + 1) = Approx.sMk (F.map (M.corec f) (f x₀)) (n + 1)

Tactic:
· dsimp only [sCorec, Approx.sMk]
    cases f x₀
    dsimp only [PFunctor.map]
    congr

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hl : l.Sized
hm : m.Sized
hr : r.Sized
⊢ (l.node4L x m y r).Sized

Tactic:
cases m

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
hm : nil.Sized
⊢ (l.node4L x nil y r).Sized

case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.node4L x (node size✝ l✝ x✝ r✝) y r).Sized
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hm : m.Sized
⊢ (l.node4L x m y r).size = l.size + m.size + r.size + 2

Tactic:
cases m

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hm : nil.Sized
⊢ (l.node4L x nil y r).size = l.size + nil.size + r.size + 2

case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.node4L x (node size✝ l✝ x✝ r✝) y r).size = l.size + (node size✝ l✝ x✝ r✝).size + r.size + 2
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case neg
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
h✝ : ¬l✝.size < ratio * r✝.size
⊢ (l.node4L x l✝ x✝ r✝).Sized

Tactic:
exact hl.node4L hr.2.1 hr.2.2

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

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

Tactic:
cases m

Goal state after:
case nil
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
⊢ All P (l.node4L x nil y r) ↔ All P l ∧ P x ∧ All P nil ∧ P y ∧ All P r

case node
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (l.node4L x (node size✝ l✝ x✝ r✝) y r) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝) ∧ P y ∧ All P r
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
cases m

Goal state after:
case nil
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
⊢ All P (l.node4R x nil y r) ↔ All P l ∧ P x ∧ All P nil ∧ P y ∧ All P r

case node
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (l.node4R x (node size✝ l✝ x✝ r✝) y r) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝) ∧ P y ∧ All P r
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inr.inr
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * l.size + 3

Tactic:
exact le_trans (Nat.dist_tri_right' _ _) (add_le_add h₂ (le_trans hr (by decide)))

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

Goal state before:
pp: case neg
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : ¬IsPath ps s₁ ∧ ¬IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
obtain ⟨h₀, h₁⟩ := h

Goal state after:
case neg
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h₀ : ¬IsPath ps s₁
h₁ : ¬IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{?u.9} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
⊢ P.WPath (WType.mk a f) ⟹ α

Tactic:
intro i x
  match x with
  | WPath.root _ _ i c => exact g' i c
  | WPath.child _ _ i j c => exact g j i c

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
⊢ P.map f (g x) = ⟨a, f ∘ f'⟩

Tactic:
gxeq,

Goal state after:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
⊢ P.map f ⟨a, f'⟩ = ⟨a, f ∘ f'⟩
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
⊢ P.map (M.corec g) (g x) = ⟨a, M.corec g ∘ f'⟩

Tactic:
gxeq,

Goal state after:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
⊢ P.map (M.corec g) ⟨a, f'⟩ = ⟨a, M.corec g ∘ f'⟩
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α γ : TypeVec.{u} n
g : α ⟹ γ
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ ⟨a, splitFun g (P.wMap g) ⊚ splitFun f' f⟩ = ⟨a, splitFun (g ⊚ f') fun x ↦ P.wMap g (f x)⟩

Tactic:
← splitFun_comp

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α γ : TypeVec.{u} n
g : α ⟹ γ
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ ⟨a, splitFun (g ⊚ f') (P.wMap g ∘ f)⟩ = ⟨a, splitFun (g ⊚ f') fun x ↦ P.wMap g (f x)⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : 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
h✝ : ls > rs
⊢ Valid' o₁
      (((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr))
      o₂ ∧
    (((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).1.balanceR
          ((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr)).size =
      ls + rs

Tactic:
obtain ⟨v, e⟩ := Valid'.eraseMax_aux hl
      suffices H : _ by
        refine ⟨Valid'.balanceR v (hr.of_gt ?_ ?_) H, ?_⟩
        · refine findMax'_all (P := fun a : α => Bounded nil (a : WithTop α) o₂)
            lx lr hl.1.2.to_nil (sep.2.2.imp ?_)
          exact fun x h => hr.1.2.to_nil.mono_left (le_of_lt h.2.1)
        · exact @findMax'_all _ (fun a => All (· > a) (.node rs rl rx rr)) lx lr sep.2.1 sep.2.2
        · rw [size_balanceR v.3 hr.3 v.2 hr.2 H, add_right_comm, ← e, hl.2.1]; rfl
      refine Or.inl ⟨_, Or.inr e, ?_⟩
      rwa [hl.2.eq_node'] at bal

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

Goal state before:
pp: a b : ℕ+
this✝ : 0 < ↑a
this : 0 < ↑b
⊢ (1 * (↑a - 1 + 1) + 0 * (↑b - 1 + 1), 0 * (↑a - 1 + 1) + 1 * (↑b - 1 + 1)) = (↑a, ↑b)

Tactic:
lia +mbtc

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

Goal state before:
pp: u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = ((u.wp + 1) * u.qp + u.x) * u.y

Tactic:
rw [add_mul _ _ u.y, add_comm _ (u.x * u.y), ← hs]

Goal state after:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = u.wp + u.zp + u.wp * u.zp + (u.wp + 1) * u.qp * u.y
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ico a b) = ∏ i, #(Icc (a i) (b i)) - 1

Tactic:
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]

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

Goal state before:
pp: a b : ℕ+
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:
w

Goal state after:
a b : ℕ+
d : ℕ+ := a.gcdD b
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
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.nil
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : nil.Sized
H1 : nil.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * nil.size
this : rl.size = 0 ∧ rr.size = 0
⊢ nil.balanceL x (node rs rl rx rr) = nil.balance x (node rs rl rx rr)

Tactic:
cases sr.2.1.size_eq_zero.1 this.1

Goal state after:
case node.nil.refl
α : Type u_1
x : α
rs : ℕ
rx : α
rr : Ordnode α
sl : nil.Sized
sr : (node rs nil rx rr).Sized
H1 : nil.size = 0 → (node rs nil rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs nil rx rr).size → (node rs nil rx rr).size ≤ delta * nil.size
this : nil.size = 0 ∧ rr.size = 0
⊢ nil.balanceL x (node rs nil rx rr) = nil.balance x (node rs nil rx rr)
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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ splitFun (TypeVec.id ⊚ f') (fixToW ∘ fun x ↦ ⟦f x⟧) = splitFun TypeVec.id wrepr ⊚ splitFun f' f

Tactic:
← splitFun_comp

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ splitFun (TypeVec.id ⊚ f') (fixToW ∘ fun x ↦ ⟦f x⟧) = splitFun (TypeVec.id ⊚ f') (wrepr ∘ 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
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ splitFun (TypeVec.id ⊚ f') (g₁ ∘ fun x ↦ ⟦f x⟧) = splitFun TypeVec.id g₂ ⊚ splitFun f' fun x ↦ ⟦f x⟧

Tactic:
← splitFun_comp

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ splitFun (TypeVec.id ⊚ f') (g₁ ∘ fun x ↦ ⟦f x⟧) = splitFun (TypeVec.id ⊚ f') (g₂ ∘ fun x ↦ ⟦f x⟧)
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
constructor
  · intro h
    have : Liftp (· ∈ supp x) x := by rw [h]; intro u; exact id
    rw [liftp_iff] at this
    rcases this with ⟨a, f, xeq, h'⟩
    refine ⟨a, f, xeq.symm, ?_⟩
    intro a' f' h''
    rintro u ⟨i, _, hfi⟩
    have : u ∈ supp x := by rw [← hfi]; apply h'
    exact (mem_supp x u).mp this _ _ h''
  rintro ⟨a, f, xeq, h⟩ p; rw [liftp_iff]; constructor
  · rintro ⟨a', f', xeq', h'⟩ u usuppx
    rcases (mem_supp x u).mp usuppx a' f' xeq'.symm with ⟨i, _, f'ieq⟩
    rw [← f'ieq]
    apply h'
  intro h'
  refine ⟨a, f, xeq.symm, ?_⟩; intro i
  apply h'; rw [mem_supp]
  intro a' f' xeq'
  apply h a' f' xeq'
  apply mem_image_of_mem _ (mem_univ _)

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

Goal state before:
pp: case refine_1
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ s.destruct.Terminates ↔ t.destruct.Terminates

pp: case refine_2
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ ∀ {a b : Option (α × WSeq α)},
    a ∈ s.destruct → b ∈ t.destruct → LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b

Tactic:
· rw [← head_terminates_iff, ← head_terminates_iff]
      exact terminates_congr (h 0)

Goal state after:
case refine_2
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
⊢ ∀ {a b : Option (α × WSeq α)},
    a ∈ s.destruct → b ∈ t.destruct → LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim
α : Type u
β : Type v
f : α → β
s✝ : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    c1.destruct c2.destruct

Tactic:
rw [h.left, h.right]

Goal state after:
case bisim
α : Type u
β : Type v
f : α → β
s✝ : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f s).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s.destruct).destruct