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

Goal state before:
pp: α : Type
ds₁ ds₂ : List ℕ
eq : ds₁ = ds₂
a : Holor α ds₁
⊢ cast ⋯ a = fun t ↦ a (cast ⋯ t)

Tactic:
subst eq; rfl

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

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(x || !y)) m n = Nat.bitwise (fun a b ↦ a && !b) n m

pp: case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || y)) m n = Nat.bitwise (fun a b ↦ a && !b) m n

pp: case negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || !y)) m n = m &&& n

Tactic:
· rw [Nat.bitwise_swap, Function.swap]
    congr
    funext x y
    cases x <;> cases y <;> rfl

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || y)) m n = Nat.bitwise (fun a b ↦ a && !b) m n

case negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || !y)) m n = m &&& n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x && y) m n) = -[m+1].land (ofNat n)

pp: case negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise (fun x y ↦ !(!x && !y)) m n+1] = -[m+1].land -[n+1]

Tactic:
· rw [Nat.bitwise_swap, Function.swap]
    congr
    funext x y
    cases x <;> cases y <;> rfl

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise (fun x y ↦ !(!x && !y)) m n+1] = -[m+1].land -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x && !!y) m n) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)

Tactic:
· rw [Nat.bitwise_swap, Function.swap]
    congr
    funext x y
    cases x <;> cases y <;> rfl

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

Goal state before:
pp: case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) m n+1] else ↑(Nat.bitwise f m n))

Tactic:
by_cases h : f false false <;> simp +decide [h]

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → α
r : α → α → Prop
⊢ IsChain r (ofFn f) ↔ ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)

Tactic:
isChain_iff_getElem,

Goal state after:
α : Type u_1
n : ℕ
f : Fin n → α
r : α → α → Prop
⊢ (∀ (i : ℕ) (_hi : i + 1 < (ofFn f).length), r (ofFn f)[i] (ofFn f)[i + 1]) ↔
    ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(b / r) + ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑(b / r) + ↑(if v % r < b % r then 1 else 0)

Tactic:
rw [add_right_inj]

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑(if v % r < b % r then 1 else 0)
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons.true
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx : x = hd ∨ x ∈ takeWhile p tl
hp : p hd = true
⊢ p x = true

Tactic:
rcases hx with (rfl | hx)

Goal state after:
case cons.true.inl
α : Type u_1
p : α → Bool
l : List α
x : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hp : p x = true
⊢ p x = true

case cons.true.inr
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hp : p hd = true
hx : x ∈ takeWhile p tl
⊢ p x = true
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬p ((dropWhile p l.reverse).reverse.getLast ⋯) = true

Tactic:
rw [getLast_reverse, head_dropWhile_not p]

Goal state after:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬false = true
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l <+: l

Tactic:
← reverse_suffix,

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ (rdropWhile p l).reverse <:+ l.reverse
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
h : n ≤ m
⊢ Ico n (m + 1) = Ico n m ++ [m]

Tactic:
← succ_singleton,

Goal state after:
n m : ℕ
h : n ≤ m
⊢ Ico n (m + 1) = Ico n m ++ Ico m (m + 1)
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
⊢ Acc (Shortlex r) (xa :: xb)

Tactic:
refine Acc.intro (xa :: xb) fun p lt => ?_

Goal state after:
case intro.intro
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
⊢ Acc (Shortlex r) p
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
⊢ (match r a b with
    | true => splitBy.loop r l b (a :: g) gs
    | false => splitBy.loop r l b [] ((a :: g).reverse :: gs)) =
    gs.reverse ++
      match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
split <;> rw [IH]

Goal state after:
case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = false
⊢ ((a :: g).reverse :: gs).reverse ++ splitBy.loop r l b [] [] = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mp
α : Type u_1
p : ℕ
w : List α
⊢ w.HasPeriod p → ∀ i < w.length - p, w[i]? = w[i + p]?

pp: case mpr
α : Type u_1
p : ℕ
w : List α
⊢ (∀ i < w.length - p, w[i]? = w[i + p]?) → w.HasPeriod p

Tactic:
· rw [HasPeriod]
    intro pref j len
    have i1 : j < w.length := by lia
    have i2 : j + p < w.length := by lia
    have min : p < w.length := by lia
    have : j + p - (List.take p w).length = j := by
      simp_all [min_eq_left_of_lt]
    simp_all [getElem_append_right, IsPrefix.getElem pref, min_eq_left_of_lt]

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
⊢ (∀ i < w.length - p, w[i]? = w[i + p]?) → w.HasPeriod p
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
⊢ (u ++ (v ++ w))[j + u.length + p]? = v[j + p]?

Tactic:
have eq : j + u.length + p - u.length = j + p := by lia

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ (u ++ (v ++ w))[j + u.length + p]? = v[j + p]?
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : 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
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : ¬z ∈ Y₂
⊢ 0 < count z Z₁

Tactic:
count_pos

Goal state after:
α : 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
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : ¬z ∈ Y₂
⊢ z ∈ Z₁
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ TransGen OneStep = IsDershowitzMannaLT

Tactic:
by
  ext M N
  exact ⟨isDershowitzMannaLT_of_transGen_oneStep, transGen_oneStep_of_isDershowitzMannaLT⟩

Goal state after:
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: case inr
q : ℚ
hq : 0 ≤ q
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
nth_rw 1 [← Rat.coe_toNNRat q hq]

Goal state after:
case inr
q : ℚ
hq : 0 ≤ q
⊢ (↑q.toNNRat)⁻¹.toNNRat = q.toNNRat⁻¹
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
K : Type u_2
inst✝² : Semifield K
inst✝¹ : CharZero K
inst✝ : Algebra K A
n : ℕ
⊢ IsUnit ↑n !

Tactic:
simp [isUnit_iff_ne_zero, n.factorial_ne_zero]

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

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

Tactic:
rcases h with ⟨n, hx⟩

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ nth p 0 = Nat.find h

Tactic:
rw [nth_zero]

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ sInf (Set.ofPred p) = Nat.find h
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case neg
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ ↑(n.minFacAux fuel k.succ) = (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
rw [ih] <;> [congr; convert! Nat.lt_succ_of_lt h using 1]

Goal state after:
case neg.e_a
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ ↑k.succ.bit1 = ↑k.bit1 + 2

n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ fuel + ↑k.succ.bit1 = (fuel + 1 + ↑k.bit1).succ
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: fuel : ℕ
n k : PosNum
h : (↑n).sqrt < fuel + ↑k.bit1
⊢ ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1

Tactic:
by
  induction fuel generalizing k <;> rw [minFacAux, Nat.minFacAux]
  case zero =>
    rw [Nat.zero_add, Nat.sqrt_lt] at h
    simp only [h, ite_true]
  case succ fuel ih =>
    simp_rw [← mul_to_nat]
    simp only [cast_lt, dvd_to_nat]
    split_ifs <;> try rfl
    rw [ih] <;> [congr; convert! Nat.lt_succ_of_lt h using 1] <;>
      simp only [cast_bit1, cast_succ, Nat.succ_eq_add_one, add_assoc,
        add_left_comm, ← one_add_one_eq_two]

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

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

Tactic:
rcases rl with _ | ⟨_, _, rlx⟩
        · exact node 2 nil x r
        · exact node 3 (ι x) rlx ι rx

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑(Num.casesOn p.pred' 1 bit1) = -↑p + -↑p + 1

Tactic:
rcases e : pred' p with - | a

Goal state after:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑p + -↑p + 1

case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1
Module: Mathlib.Data.Num.ZNum

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

Tactic:
rw [sub', ZNum.cast_bitm1, cast_sub' a b]

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a - ↑b + (↑a - ↑b) - 1 = ↑a.bit0 - ↑b.bit1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : 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 + r.size
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
mm : ml.size + mr.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
have r1 : r.size = 1 := by lia

Goal state after:
case pos
α : 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 + r.size
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
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Module: Mathlib.Data.Num.ZNum

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

Tactic:
neg_eq_iff_eq_neg,

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

Goal state before:
pp: ⊢ (Num.ofNat' 0).toZNum = -(Num.ofNat' 0).toZNum

Tactic:
Num.ofNat'_zero

Goal state after:
⊢ Num.toZNum 0 = -Num.toZNum 0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ (Num.ofNat' 0).toZNum = 0

Tactic:
Num.ofNat'_zero

Goal state after:
α : Type u_1
⊢ Num.toZNum 0 = 0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case neg
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
h : ¬a✝ ≤ b✝
⊢ ↑(gcdAux (b✝.natSize + a✝.natSize) b✝ a✝) = (↑a✝).gcd ↑b✝

Tactic:
Nat.gcd_comm

Goal state after:
case neg
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
h : ¬a✝ ≤ b✝
⊢ ↑(gcdAux (b✝.natSize + a✝.natSize) b✝ a✝) = (↑b✝).gcd ↑a✝
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree (x.approx n) (y.approx (n + 1)) ↔ Agree' n x y

Tactic:
constructor <;> intro h
  · induction n generalizing x y with
    | zero => constructor
    | succ _ n_ih =>
      induction x using PFunctor.M.casesOn'
      induction y using PFunctor.M.casesOn'
      simp only [approx_mk] at h
      obtain - | ⟨_, _, hagree⟩ := h
      constructor <;> try rfl
      intro i
      apply n_ih
      apply hagree
  · induction n generalizing x y with
    | zero => constructor
    | succ _ n_ih =>
      obtain - | @⟨_, a, x', y'⟩ := h
      induction x using PFunctor.M.casesOn' with | _ x_a x_f
      induction y using PFunctor.M.casesOn' with | _ y_a y_f
      simp only [approx_mk]
      have h_a_1 := mk_inj ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩›
      cases h_a_1
      replace h_a_2 := mk_inj ‹M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩›
      cases h_a_2
      constructor
      intro i
      apply n_ih
      simp [*]

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

Goal state before:
pp: F : PFunctor.{uA, uB}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
x : F.M
h : M.mk ⟨a, f⟩ = x
⊢ IsPath (⟨a', i⟩ :: xs) x → a = a'

Tactic:
rintro (_ | ⟨_, _, _, _, rfl, _⟩)

Goal state after:
case cons
F : PFunctor.{uA, uB}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
f✝ : F.B a' → F.M
a✝ : IsPath xs (f✝ i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a', f✝⟩
⊢ a = a'
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
| (TypeVec.id ::: corec P g) ⊚ f

Tactic:
rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
| splitFun (TypeVec.id ⊚ dropFun f) (corec P g ∘ lastFun f)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : 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_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 : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
rr0 : rr.size > 0
⊢ rr.size + rl.size ≤ 2

Tactic:
by rwa [add_comm]

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

Goal state before:
pp: α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.dual.dual.Sized

Tactic:
exact h.dual

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

Goal state before:
pp: case f.f.cons
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
⊢ (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)

Tactic:
have h₁ := bisim.tail h₀ i

Goal state after:
case f.f.cons
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
h₁ : R (f i) (f' i)
⊢ (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
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₁
h₁ : ¬IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
simp only [iselect_eq_default, *, not_false_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t : Ordnode α
h : t.Valid
⊢ t.eraseMax.dual.Valid

Tactic:
dual_eraseMax

Goal state after:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
h : t.Valid
⊢ t.dual.eraseMin.Valid
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_3
α : 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
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ l',
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ r',
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ (((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr)).size =
    ls + rs

Tactic:
· rw [size_balanceR v.3 hr.3 v.2 hr.2 H, add_right_comm, ← e, hl.2.1]; rfl

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ a₁ < ?left.left.b

pp: case left.left.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ ?left.left.b < a₃

pp: case left.left.b
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ ι

Tactic:
repeat' assumption

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₁ ≤ ?right.right.b

pp: case right.right.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ ?right.right.b ≤ b₂✝

pp: case right.right.b
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ α a₁

Tactic:
repeat' assumption

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

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

Tactic:
by cases o₁ <;> cases o₂ <;> trivial

Goal state after: