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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

Tactic:
by_cases h₁ : a = ah <;> by_cases h₂ : a' = ah

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : a = ah
h₂ : a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case trans
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
l₁✝ l₂✝ l₃✝ : List (Sigma β)
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁₂ : ∀ (l : List (Sigma β)), l₁✝.kunion l ~ l₂✝.kunion l
ih₂₃ : ∀ (l : List (Sigma β)), l₂✝.kunion l ~ l₃✝.kunion l
l : List (Sigma β)
⊢ l₁✝.kunion l ~ l₃✝.kunion l

Tactic:
exact Perm.trans (ih₁₂ l) (ih₂₃ l)

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : ¬a ∈ l₁.keys
⊢ dlookup a (l₁.kunion l₂) = dlookup a l₂

Tactic:
by
  induction l₁ generalizing l₂ with
  | nil => simp
  | cons _ _ ih => simp_all [not_or]

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

Goal state before:
pp: case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M))) a = ↑l
hd : List.Pairwise (Disjoint on Finsupp.support) l
⊢ List.Pairwise (Disjoint on Finsupp.support) a

Tactic:
simp only [Multiset.quot_mk_to_coe'', Multiset.coe_eq_coe] at hl

Goal state after:
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a l : List (ι →₀ M)
hd : List.Pairwise (Disjoint on Finsupp.support) l
hl : a.Perm l
⊢ List.Pairwise (Disjoint on Finsupp.support) a
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
⊢ ↑(#({x ∈ Ico a b | r ∣ x})) = max (⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉) 0

Tactic:
Ico_filter_dvd_eq _ _ hr,

Goal state after:
a b r : ℤ
hr : 0 < r
⊢ ↑(#(map { toFun := fun x ↦ x * r, inj' := ⋯ } (Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉))) = max (⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉) 0
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p (dropWhile p l) = dropWhile p l

Tactic:
simp only [dropWhile_eq_self_iff]
  exact fun h => dropWhile_get_zero_not p l h

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

Goal state before:
pp: case nil
α : Type u_1
m : List α
r : α → α → Bool
g : List α
a : α
h : IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
ha : ∀ (x : α), x ∈ m.head? → r ([a].getLast ⋯) x = false
⊢ splitBy.loop r m a g [] = (g.reverse ++ [a]) :: splitBy r m

Tactic:
cases m with
    | nil => simp [splitBy.loop]
    | cons c m => simp_all [splitBy.loop, splitByLoop_eq_append [_], splitBy]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
⊢ A.toCols₁.fromCols A.toCols₂ = A

Tactic:
ext i (j | j)

Goal state after:
case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₁
⊢ A.toCols₁.fromCols A.toCols₂ i (Sum.inl j) = A i (Sum.inl j)

case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₂
⊢ A.toCols₁.fromCols A.toCols₂ i (Sum.inr j) = A i (Sum.inr j)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ (A₁.fromRows A₂)ᵀ = A₁ᵀ.fromCols A₂ᵀ

Tactic:
ext i (j | j)

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
j : m₁
⊢ (A₁.fromRows A₂)ᵀ i (Sum.inl j) = A₁ᵀ.fromCols A₂ᵀ i (Sum.inl j)

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
j : m₂
⊢ (A₁.fromRows A₂)ᵀ i (Sum.inr j) = A₁ᵀ.fromCols A₂ᵀ i (Sum.inr j)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix n m₁ R
A₂ : Matrix n m₂ R
⊢ -A₁.fromCols A₂ = (-A₁).fromCols (-A₂)

Tactic:
ext i (j | j)

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix n m₁ R
A₂ : Matrix n m₂ R
i : n
j : m₁
⊢ (-A₁.fromCols A₂) i (Sum.inl j) = (-A₁).fromCols (-A₂) i (Sum.inl j)

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix n m₁ R
A₂ : Matrix n m₂ R
i : n
j : m₂
⊢ (-A₁.fromCols A₂) i (Sum.inr j) = (-A₁).fromCols (-A₂) i (Sum.inr j)
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ M = M - {b} + {b}

Tactic:
· rw [tsub_add_cancel_of_le]
    have : b ∈ a ::ₘ M := by simp [h0]
    simpa [hab.symm] using this

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N : Multiset α
hMN : TransGen OneStep M N
⊢ ∀ {a b : Multiset α}, a.OneStep b → a.IsDershowitzMannaLT b

Tactic:
by rintro _ _ ⟨X, Y, a, rfl, rfl, hYa⟩; exact ⟨X, Y, {a}, by simpa⟩

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

Goal state before:
pp: case left
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌈x⌉₊ < ↑x + 1

pp: case right
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑x ≤ ↑↑⌈x⌉₊

Tactic:
· exact_mod_cast NNRat.cast_strictMono <| Nat.ceil_lt_add_one zero_le

Goal state after:
case right
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑x ≤ ↑↑⌈x⌉₊
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
⊢ n = 0 → n.greatestFib = 0

Tactic:
by rintro rfl; rfl

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
⊢ (map fib n.zeckendorf).sum = n

Tactic:
by
  induction n using zeckendorf.induct <;> simp_all [fib_greatestFib_le]

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
⊢ StrictMonoOn (nth p) (Set.Iio #hf.toFinset)

Tactic:
by
  rintro m (hm : m < _) n (hn : n < _) h
  simp only [nth_eq_orderEmbOfFin, *]
  exact OrderEmbedding.strictMono _ h

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

Goal state before:
pp: p : ℕ → Prop
h : p 0
⊢ nth p 0 = 0

Tactic:
simp [nth_zero, h]

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

Goal state before:
pp: 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
⊢ ↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) =
    if ↑n < ↑k.bit1 * ↑k.bit1 then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
← mul_to_nat

Goal state after:
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
⊢ ↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) =
    if ↑n < ↑(k.bit1 * k.bit1) then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit1
n : PosNum
⊢ ↑(n.bit1.minFacAux (↑n) 1) = (↑n.bit1).minFacAux 3

Tactic:
rw [minFacAux_to_nat]

Goal state after:
case bit1
n : PosNum
⊢ (↑n.bit1).minFacAux ↑(bit1 1) = (↑n.bit1).minFacAux 3

case bit1
n : PosNum
⊢ (↑n.bit1).sqrt < ↑n + ↑(bit1 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
| ↑n.bitm1

Tactic:
← zneg_zneg n

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
| ↑(- -n).bitm1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : ZNum), a ≤ b → b ≤ c → a ≤ c

Tactic:
intro a b c
    transfer_rw
    apply le_trans

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

Goal state before:
pp: case inr
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
h : ¬l + r₂ ≤ 1
H : l ≤ delta * r₁ ∧ r₁ ≤ delta * l
⊢ l ≤ delta * r₂

Tactic:
exact le_trans H.1 (Nat.mul_le_mul_left _ h₁)

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

Goal state before:
pp: case neg.inl
α : 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₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * 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
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size = 0
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
rw [ml0, mul_zero, Nat.le_zero] at mm₂

Goal state after:
case neg.inl
α : 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₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * 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
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size = 0
ml0 : ml.size = 0
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : 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 + 1
H3 : 2 * (Ordnode.node rs rl rx rr).size ≤ 9 * l.size + 5 ∨ (Ordnode.node rs rl rx rr).size ≤ 3
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂

Tactic:
Nat.lt_succ_iff

Goal state after:
case node
α : 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 * (Ordnode.node rs rl rx rr).size ≤ 9 * l.size + 5 ∨ (Ordnode.node rs rl rx rr).size ≤ 3
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.hx
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x x

Tactic:
rw [← agree_iff_agree']
      apply x.consistent

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

Goal state before:
pp: u : PrimeMultiset
n : ℕ+
h : u.prod ∣ n.factorMultiset.prod ↔ u ≤ n.factorMultiset := prod_dvd_iff
⊢ u.prod ∣ n ↔ u ≤ n.factorMultiset

Tactic:
n.prod_factorMultiset

Goal state after:
u : PrimeMultiset
n : ℕ+
h : u.prod ∣ n ↔ u ≤ n.factorMultiset
⊢ u.prod ∣ n ↔ u ≤ n.factorMultiset
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : delta * ls < rs
this : delta * Nat.succ 0 < rl.size + rr.size + 1
⊢ delta ≤ rl.size + rr.size

Tactic:
Nat.lt_succ_iff

Goal state after:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : delta * ls < rs
this : delta * Nat.succ 0 ≤ rl.size + rr.size
⊢ delta ≤ rl.size + rr.size
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : u.r + (u.bp + 1) * u.q = u.ap + 1 := rq_eq u
⊢ u.q = u.qp + 1

Tactic:
rw [hr, hq, mul_zero, add_zero] at h

Goal state after:
case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : 0 = u.ap + 1
⊢ u.q = u.qp + 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
this : delta * Nat.succ 0 < ll.size + lr.size + 1
⊢ delta ≤ ll.size + lr.size

Tactic:
Nat.lt_succ_iff

Goal state after:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
this : delta * Nat.succ 0 ≤ ll.size + lr.size
⊢ delta ≤ ll.size + lr.size
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : (node ls (node lls lll llx llr) lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
ld : delta ≤ (node lls lll llx llr).size + nil.size
⊢ (node ls (node lls lll llx llr) lx nil).rotateR x (node rs rl rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then
              node (ls + rs + 1) (node lls lll llx llr) lx (node (size_1 + rs + 1) nil x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          nil)
      (node lls lll llx llr)

Tactic:
exact absurd (le_trans ld (balancedSz_zero.1 hl.1)) (by decide)

Goal state after:
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 : ι) → LocallyFiniteOrderBot (α i)
b : (i : ι) → α i
⊢ #(Iio b) = ∏ i, #(Iic (b i)) - 1

Tactic:
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]

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
α : TypeVec.{u} n
x : F α
⊢ (∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u) →
    ∃ a f,
      abs ⟨a, f⟩ = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ

pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ (∃ a f,
      abs ⟨a, f⟩ = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ) →
    ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u

Tactic:
· intro h
    have : LiftP (fun i u => u ∈ supp x i) x := by rw [h]; introv; exact id
    rw [liftP_iff] at this
    rcases this with ⟨a, f, xeq, h'⟩
    refine ⟨a, f, xeq.symm, ?_⟩
    intro a' f' h''
    rintro hu u ⟨j, _h₂, hfi⟩
    have hh : u ∈ supp x a' := by rw [← hfi]; apply h'
    exact (mem_supp x _ u).mp hh _ _ hu

Goal state after:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ (∃ a f,
      abs ⟨a, f⟩ = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ) →
    ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
Module: Mathlib.Data.QPF.Multivariate.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 α
⊢ WEquiv x y → WEquiv y x

Tactic:
by
  intro h; induction h with
  | ind a f' f₀ f₁ _h ih => exact WEquiv.ind _ _ _ _ ih
  | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => exact WEquiv.abs _ _ _ _ _ _ h.symm
  | trans x y z _e₁ _e₂ ih₁ ih₂ => exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁

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

Goal state before:
pp: case mp
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
⊢ Liftp p x → ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

pp: case mpr
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) → Liftp p x

Tactic:
· rintro ⟨y, hy⟩
    rcases h : repr y with ⟨a, f⟩
    use a, fun i => (f i).val
    constructor
    · rw [← hy, ← abs_repr y, h, ← abs_map]
      rfl
    intro i
    apply (f i).property

Goal state after:
case mpr
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) → Liftp p x
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
⊢ abs (Wrepr (WType.mk a f)).dest = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest

Tactic:
have : Wrepr ⟨a, f⟩ = PFunctor.W.mk (repr (abs (q.P.map Wrepr ⟨a, f⟩))) := rfl

Goal state after:
case mk.a
F : Type u → Type v
q : QPF F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs ((P F).map Wrepr ⟨a, f⟩)))
⊢ abs (Wrepr (WType.mk a f)).dest = abs (PFunctor.W.mk ((P F).map Wrepr ⟨a, f⟩)).dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
x✝ : F₂ (F₁ α)
a : (P F₂).A
f : (P F₂).B a → F₁ α
x : (P F₂).B a
⊢ abs ⟨(repr (f x)).fst, fun y ↦ (repr (f x)).snd y⟩ = f x

Tactic:
rcases h' : repr (f x) with ⟨b, g⟩

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
x✝ : F₂ (F₁ α)
a : (P F₂).A
f : (P F₂).B a → F₁ α
x : (P F₂).B a
b : (P F₁).A
g : (P F₁).B b → α
h' : repr (f x) = ⟨b, g⟩
⊢ abs ⟨⟨b, g⟩.fst, fun y ↦ ⟨b, g⟩.snd y⟩ = f x
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
⊢ s.tail.destruct = s.destruct >>= tail.aux

Tactic:
by
  simp only [tail, destruct_flatten]; rw [← bind_pure_comp, LawfulMonad.bind_assoc]
  apply congr_arg; ext1 (_ | ⟨a, s⟩) <;> apply (@pure_bind Computation _ _ _ _ _ _).trans _ <;> simp

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

Goal state before:
pp: case refine_2.some.some
α : 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 : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').1 = (b, t').1
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s')) (some (b, t'))

Tactic:
refine ⟨ab, fun n => ?_⟩

Goal state after:
case refine_2.some.some
α : 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 : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').1 = (b, t').1
n : ℕ
⊢ s'.get? n ~ t'.get? n
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
r : R a b
h : LiftRel R s t
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some (a, s))) (destruct_append.aux t2 (some (b, t)))

Tactic:
simpa using ⟨r, Or.inr ⟨s, rfl, t, rfl, h⟩⟩

Goal state after:
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case3
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ (if { s := ofList s₁.s.toList, i := s₁.i }.hasNext = true then
      if
          { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr =
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr then
        ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next
          { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next
      else
        decide
          ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr)
    else true) =
    true

Tactic:
if_neg (by simpa using h₂)

Goal state after:
case case3
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ true = true
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
β : Type v
s : WSeq α
f : α → WSeq β
b : β
h : b ∈ s.bind f
t : WSeq β
tm : t ∈ map f s
bt : b ∈ t
a : α
as : a ∈ s
e : f a = t
⊢ b ∈ f a

Tactic:
rwa [e]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s

Tactic:
have : (n + 1) * m = l - k := by
    apply Nat.mul_div_cancel'
    exact (Nat.modEq_iff_dvd' hkl.le).1 hn

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
⊢ (dynEntourage T (U ○ U) n).IsCover F ↑s

Tactic:
isCover_iff_subset_iUnion_ball

Goal state after:
case inr
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
⊢ F ⊆ ⋃ y ∈ ↑s, ball y (dynEntourage T (U ○ U) n)