mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondMod R
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : P ⊗ (free R).obj S.toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : ↑((P ⟹ B).obj.obj (Opposite.op S))
⊢ ∃ S' φ,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
      ∃ x,
        (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) x =
          (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op φ))) g

Tactic:
specialize h e S ((ihomPoints _ _ _ _) g)

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : ↑((P ⟹ B).obj.obj (Opposite.op S))
h :
  ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (ihomPoints R P B S) g = g' ≫ e
⊢ ∃ S' φ,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
      ∃ x,
        (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) x =
          (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op φ))) g
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
ih : ofFin a✝.toFin = a✝
⊢ ofFin a✝.fs.toFin = a✝.fs

Tactic:
exact congrArg fs ih

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : ReaderT ρ m α) (next : Label ω (ReaderT ρ m) γ → α → ReaderT ρ m ω),
    (callCC fun f ↦ cmd >>= next f) = do
      let x ← cmd
      callCC fun f ↦ next f x

Tactic:
intros; simp only [callCC, ReaderT.callCC, ReaderT.run_bind,
                                    callCC_bind_right]; ext; rfl

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Equiv.traverse eqv (Comp.mk ∘ map f ∘ g) x = Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)

Tactic:
rw [traverse_def, comp_traverse, Comp.map_mk]
  simp only [map_map, traverse_def, symm_apply_apply]

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: case succ
w : ℕ
x : BitVec w
n : ℕ
ih : (x ^ n).toFin = x.toFin ^ n
⊢ (x ^ (n + 1)).toFin = x.toFin ^ (n + 1)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
F : Ctop α σ
E : σ ≃ τ
f : σ → Set α
T : α → σ
h₁ : ∀ (x : α), x ∈ f (T x)
I : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ
h₂ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (I a b x h)
h₃ : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (I a b x h) ⊆ f a ∩ f b
x : α
⊢ x ∈ f (E.symm (E (T x)))

Tactic:
simpa using h₁ x

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Curry

Goal state before:
pp: case succ
τ : Type u
n : ℕ
ih : ∀ {p : Fin n → Type u} (f : FromTypes p τ), curry f.uncurry = f
p : Fin (n + 1) → Type u
f : FromTypes p τ
⊢ curry f.uncurry = f

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Curry

Goal state before:
pp: case succ
τ : Type u
n : ℕ
ih : ∀ {p : Fin n → Type u} (f : ((i : Fin n) → p i) → τ) (args : (i : Fin n) → p i), (curry f).uncurry args = f args
p : Fin (n + 1) → Type u
f : ((i : Fin (n + 1)) → p i) → τ
args : (i : Fin (n + 1)) → p i
⊢ (curry f).uncurry args = f args

Tactic:
| succ n ih =>

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ (kextract a s.entries).snd.NodupKeys

Tactic:
rw [kextract_eq_dlookup_kerase]; exact s.nodupKeys.kerase _

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ extract a s = (lookup a s, erase a s)

Tactic:
simp [extract]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s ∧ { entries := kerase a s.entries, nodupKeys := ⋯ } = erase a s
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
⊢ insert a b (singleton a b') = singleton a b

Tactic:
simp only [singleton, Finmap.insert_toFinmap, AList.insert_singleton_eq]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s✝ : Finmap β
s : AList β
⊢ extract a ⟦s⟧ = (lookup a ⟦s⟧, erase a ⟦s⟧)

Tactic:
simp [extract]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

Tactic:
· have : x ∉ singleton a b := by rwa [mem_singleton]
      rw [lookup_union_left_of_not_in this, lookup_erase_ne h']

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
⊢ (foldr (fun x ↦ kinsert x.fst x.snd) [] l).NodupKeys

Tactic:
generalize hl : nil = l'

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ (foldr (fun x ↦ kinsert x.fst x.snd) l' l).NodupKeys
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : i = j
⊢ (unitVec d j ⊗ x).slice i hid t = (if i = j then x else 0) t

Tactic:
simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ (unitVec d j ⊗ x).slice i hid t = (if i = j then x else 0) t

Tactic:
simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ 0 = 0 t
Module: Mathlib.Data.Holor

Goal state before:
pp: case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0

Tactic:
intro (hid' : Subtype.mk i _ ∉ Finset.attach (Finset.range d))

Goal state after:
case h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : ⟨i, ⋯⟩ ∉ (Finset.range d).attach
⊢ (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
⊢ (∀ x ∈ ∅, CPRankMax n (f x)) → CPRankMax (∅.card * n) (∑ x ∈ ∅, f x)

Tactic:
by simp [CPRankMax.zero]

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

Goal state before:
pp: a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b

Tactic:
exact natAbs_lt_iff_mul_self_lt

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

Goal state before:
pp: p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
⊢ p ^ (k + l + 1) ∣ m.natAbs * n.natAbs

Tactic:
← Int.natAbs_mul

Goal state after:
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
⊢ p ^ (k + l + 1) ∣ (m * n).natAbs
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bitwise or (bit a m) (bit b n) = bit (a || b) (bitwise or m n)

Tactic:
bitwise_bit

Goal state after:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bit (a || b) (bitwise or m n) = bit (a || b) (bitwise or m n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bitwise and (bit a m) (bit b n) = bit (a && b) (bitwise and m n)

Tactic:
bitwise_bit

Goal state after:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bit (a && b) (bitwise and m n) = bit (a && b) (bitwise and m n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bitwise (fun a b ↦ a && !b) (bit a m) (bit b n) = bit (a && !b) (bitwise (fun a b ↦ a && !b) m n)

Tactic:
bitwise_bit

Goal state after:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bit (a && !b) (bitwise (fun a b ↦ a && !b) m n) = bit (a && !b) (bitwise (fun a b ↦ a && !b) m n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bitwise xor (bit a m) (bit b n) = bit (a ^^ b) (bitwise xor m n)

Tactic:
bitwise_bit

Goal state after:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bit (a ^^ b) (bitwise xor m n) = bit (a ^^ b) (bitwise xor m n)
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true

Tactic:
simp only [h_p_hd, length_cons, Nat.zero_lt_succ, getElem_cons_zero, not_true_eq_false,
        imp_false, iff_false]

Goal state after:
case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
⊢ ¬dropWhile p tl = hd :: tl
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c ↦ f c a) ⊆ Set.range fun b c ↦ g c b
a : α
⊢ Set.range (foldl f a) ⊆ Set.range (foldl g a)

Tactic:
by
  change (Set.range fun l => _) ⊆ Set.range fun l => _
  -- Porting note: have to write `(foldr_reverse)` instead of `foldr_reverse`.
  simp_rw [← (foldr_reverse), Set.range_comp' _ reverse,
    reverse_involutive.bijective.surjective.range_eq, Set.image_univ]
  exact foldr_range_subset_of_range_subset hfg a

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

Goal state before:
pp: case refine_2.cons
α : Type u_1
L✝ : List (List α)
f✝ : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L
fs : f ∈ L.sections
⊢ a :: f ∈ (l :: L).sections

Tactic:
simp only [sections, mem_flatMap, mem_map]
      exact ⟨f, fs, a, al, rfl⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
hn : l ≠ []
⊢ ((splitBy r l).head ⋯).head ⋯ = l.head hn

Tactic:
simp [head_head_eq_head_flatten]

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

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ ↑(q₁ * q₂).num = ↑q₁.num * ↑q₂.num / ↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den))

Tactic:
convert! Rat.mul_num q₁ q₂

Goal state after:
case e'_2
q₁ q₂ : ℚ≥0
⊢ ↑(q₁ * q₂).num = (↑q₁ * ↑q₂).num

case e'_3.e'_5.e'_5
q₁ q₂ : ℚ≥0
⊢ ↑q₁.num = (↑q₁).num

case e'_3.e'_5.e'_6
q₁ q₂ : ℚ≥0
⊢ ↑q₂.num = (↑q₂).num

case e'_3.e'_6.e'_1
q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = ((↑q₁).num * (↑q₂).num).natAbs
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a b : ℕ
s : ι → ℕ
i : ι
l : List ι
ih : List.Pairwise (Coprime on s) l → (a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i])
co : List.Pairwise (Coprime on s) (i :: l)
⊢ (s i).Coprime (List.map s l).prod

Tactic:
simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]

Goal state after:
ι : Type u_1
a b : ℕ
s : ι → ℕ
i : ι
l : List ι
ih : List.Pairwise (Coprime on s) l → (a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i])
co : List.Pairwise (Coprime on s) (i :: l)
⊢ ∀ a ∈ l, (s i).Coprime (s a)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
⊢ (s i).Coprime (List.map s l).prod

Tactic:
simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]

Goal state after:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
⊢ ∀ a ∈ l, (s i).Coprime (s a)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ (s i).Coprime (List.map s l).prod

Tactic:
simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]

Goal state after:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ ∀ a ∈ l, (s i).Coprime (s a)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ (s i).Coprime (List.map s l).prod

Tactic:
simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]

Goal state after:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ ∀ a ∈ l, (s i).Coprime (s a)
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit ↑n ! ↔ n < p
⊢ IsUnit ↑(n + 1)! ↔ n + 1 < p

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
n✝ p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
n : ℕ
ih : n < p → IsUnit ↑n !
h : n + 1 < p
⊢ IsUnit ↑(n + 1)!

Tactic:
| succ n ih =>

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

Goal state before:
pp: n : ℕ
⊢ n.dist n = 0

Tactic:
simp [dist, tsub_self]

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ (if h : (Set.ofPred p).Finite then (h.toFinset.sort fun a b ↦ a ≤ b).getD n 0
    else ↑((Subtype.orderIsoOfNat (Set.ofPred p)) n)) =
    0

Tactic:
dif_pos hf,

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b).getD n 0 = 0
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
this : multiplicity n.minFac ((Icc 1 (n - 1)).gcd n.choose) = 1
⊢ ∏ p, ↑p ^ ((Icc 1 (n - 1)).gcd n.choose).factorization ↑p = n.minFac

Tactic:
primeFactors_gcd_choose_of_isPrimePow h

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
this : multiplicity n.minFac ((Icc 1 (n - 1)).gcd n.choose) = 1
⊢ ∏ p, ↑p ^ ((Icc 1 (n - 1)).gcd n.choose).factorization ↑p = n.minFac
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : nth p a = 0
⊢ nth p b = 0

Tactic:
by
  simp only [nth_eq_zero, h₀, false_and, false_or] at ha ⊢
  exact ha.imp fun hf hle => hle.trans hab

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

Goal state before:
pp: case neg
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hf : (Set.ofPred p).Finite
hn : #⋯.toFinset ≤ n
⊢ (if h : (Set.ofPred p).Finite then (h.toFinset.sort fun a b ↦ a ≤ b).getD n 0
    else ↑((Subtype.orderIsoOfNat (Set.ofPred p)) n)) ≤
    f n

Tactic:
dif_pos hf,

Goal state after:
case neg
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hf : (Set.ofPred p).Finite
hn : #⋯.toFinset ≤ n
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b).getD n 0 ≤ f n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case succ
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ f (n + 1) ≤ nth p (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: case zero
p : ℕ → Prop
inst✝ : DecidablePred p
hn : ∀ (hf : (Set.ofPred p).Finite), 0 < #hf.toFinset
⊢ count p (nth p 0) = 0

Tactic:
exact count_nth_zero _

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ ∀ (hf : (Set.ofPred p).Finite), k < #hf.toFinset

Tactic:
exact fun hf => h.trans_le (count_le_card hf n)

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = Num.zero.succ'
| p = Num.zero.succ'

Tactic:
change p = 1

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = Num.zero.succ'
| p = 1
Module: Mathlib.Data.Num.ZNum

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

Tactic:
conv at ep => change p = 1

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

Goal state before:
pp: p : PosNum
this : (↑p).bit0 = (ZNum.pos p).bit0
⊢ ↑p.bit0 = ZNum.pos p.bit0

Tactic:
rwa [← ZNum.bit0_of_bit0] at this

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a : ZNum
⊢ ↑(0 + a) = ↑0 + ↑a

Tactic:
cases a <;> exact (_root_.zero_add _).symm

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

Goal state before:
pp: m n : ZNum
x✝ : ↑m ∣ ↑n
k : ℤ
e : ↑n = ↑m * k
⊢ n = m * ↑k

Tactic:
← of_to_int n,

Goal state after:
m n : ZNum
x✝ : ↑m ∣ ↑n
k : ℤ
e : ↑n = ↑m * k
⊢ ↑↑n = m * ↑k
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateL x r).dual = r.dual.rotateR x l.dual

Tactic:
cases r

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x : α
⊢ (l.rotateL x nil).dual = nil.dual.rotateR x l.dual

case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).dual = (node size✝ l✝ x✝ r✝).dual.rotateR x l.dual
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) < 2 ^ n

Tactic:
refine lt_of_mul_lt_mul_right (lt_of_le_of_lt ?_ h) (Nat.zero_le 2)

Goal state after:
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) * 2 ≤ ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a)))
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
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂

Tactic:
have hlp : size l > 0 → ¬size rl + size rr ≤ 1 := fun l0 hb =>
    absurd (le_trans (le_trans (Nat.mul_le_mul_left _ l0) H2) hb) (by decide)

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 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_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
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) rr.size

Tactic:
have := hr.3.1

Goal state after:
case pos.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_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
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz rl.size rr.size
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) rr.size
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case neg.inr.inl.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_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
⊢ l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
    0 < l.size ∧
      ratio * rr.size ≤ rl.size ∧
        delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size

Tactic:
have := hr.3.1

Goal state after:
case neg.inr.inl.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_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
this : BalancedSz rl.size rr.size
⊢ l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
    0 < l.size ∧
      ratio * rr.size ≤ rl.size ∧
        delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size