mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.bot
α : Type u_1
inst✝ : LT α
⊢ ⊤ < WithBot.toDual ⊥ ↔ ⊥ < WithTop.ofDual ⊤

Tactic:
simp [lt_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ⊤ < WithBot.toDual ↑a✝ ↔ ↑a✝ < WithTop.ofDual ⊤

Tactic:
simp [lt_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ ↑a✝ < WithBot.toDual ⊥ ↔ ⊥ < WithTop.ofDual ↑a✝

Tactic:
simp [lt_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ : αᵒᵈ
a✝ : α
⊢ ↑a✝¹ < WithBot.toDual ↑a✝ ↔ ↑a✝ < WithTop.ofDual ↑a✝¹

Tactic:
simp [lt_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.bot
α : Type u_1
inst✝ : LT α
⊢ ⊤ < WithBot.ofDual ⊥ ↔ ⊥ < WithTop.toDual ⊤

Tactic:
simp [lt_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.coe
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ ⊤ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < WithTop.toDual ⊤

Tactic:
simp [lt_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ ↑a✝ < WithBot.ofDual ⊥ ↔ ⊥ < WithTop.toDual ↑a✝

Tactic:
simp [lt_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ : α
a✝ : αᵒᵈ
⊢ ↑a✝¹ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < WithTop.toDual ↑a✝¹

Tactic:
simp [lt_toDual]

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h✝ : f a ∣ f b * f c
a₁ a₂ : β
h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂
⊢ a₁ * a₂ = f (EquivLike.inv f a₁) * f (EquivLike.inv f a₂)

Tactic:
EquivLike.apply_inv_apply

Goal state after:
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
c a b : K
hc : c ≠ 0
⊢ (a + b / c) * c = a * c + b

Tactic:
rw [right_distrib, div_mul_cancel₀ _ hc]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤ
⊢ IsUnit u ↔ u = 1 ∨ u = -1

Tactic:
by
  refine ⟨fun h ↦ isUnit_eq_one_or h, fun h ↦ ?_⟩
  rcases h with (rfl | rfl)
  · exact isUnit_one
  · exact ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inr
v : ℤ
h : -1 * v = -1
⊢ -1 = 1 ∧ v = -1 ∨ -1 = -1 ∧ v = 1

Tactic:
simpa [Int.neg_mul] using h

Goal state after:
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: case h
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
⊢ C ∈ upperBounds (range f)

Tactic:
rintro - ⟨x, rfl⟩

Goal state after:
case h
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
x : α
⊢ f x ≤ C
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded (Function.swap r)
inst✝ : Nonempty α
⊢ ¬Relator.LeftTotal r

Tactic:
by
  intro h
  obtain ⟨a, -, ha⟩ := wf.has_min Set.univ Set.univ_nonempty
  obtain ⟨b, hab⟩ := h a
  specialize ha b (Set.mem_univ b)
  contradiction

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst✝³ : EquivLike E { x // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
⊢ (fun i ↦ if h : p i then update v j x (e ⟨i, h⟩) else w i) =
    update (fun i ↦ if h : p i then v (e ⟨i, h⟩) else w i) (↑(EquivLike.inv e j)) x

Tactic:
by
  ext i
  by_cases h : p i
  · simp only [h, update_apply]
    aesop
  · grind

Goal state after:
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
β : Type u_4
inst✝ : Preorder β
s : Set (α × β)
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ IsCofinalFor ((Prod.fst '' s) ×ˢ (Prod.snd '' s)) s

Tactic:
rintro ⟨_, _⟩ ⟨⟨x, hx, rfl⟩, y, hy, rfl⟩
  obtain ⟨z, hz, hxz, hyz⟩ := hs _ hx _ hy
  exact ⟨z, hz, hxz.1, hyz.2⟩

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ termg n₁ x a₁ + termg n₂ x a₂ = termg n' x a'

Tactic:
by
  simp only [termg, h₁.symm, add_zsmul, h₂.symm]
  exact add_add_add_comm (n₁ • x) a₁ (n₂ • x) a₂

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 ≤ b
⊢ a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε

Tactic:
by
  refine ⟨fun h _ hε ↦ h.trans <| le_mul_of_one_le_right hb hε.le, fun h ↦ ?_⟩
  obtain rfl | hb := hb.eq_or_lt
  · simp_rw [zero_mul] at h
    exact h 2 one_lt_two
  refine le_of_forall_gt_imp_ge_of_dense fun x hbx => ?_
  convert h (x / b) ((one_lt_div hb).mpr hbx)
  rw [mul_div_cancel₀ _ hb.ne']

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

Goal state before:
pp: α : Type u_1
f : α → α
a : α
n : ℕ
l : List α
⊢ iterateTR.loop f a n l = l.reverse ++ iterate f a n

Tactic:
by
  induction n generalizing a l <;> simp [*]

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
⊢ AntitoneOn (fun x ↦ x⁻¹) (Set.Ioi 0)

Tactic:
convert! sub_inv_antitoneOn_Ioi (α := α)

Goal state after:
case e'_5
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
x✝ : α
⊢ x✝ = x✝ - 0
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
v : List β
huv : Forall₂ r [] v
⊢ (Forall₂ r ∘r Perm) [] v

Tactic:
cases huv; exact ⟨[], Forall₂.nil, Perm.nil⟩

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
hb : ¬b = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
simpa [zpow', ha, hb] using mul_zpow a b n

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
t s : List α
h : s ≠ []
⊢ (s ++ t).head! = s.head!

Tactic:
induction s
  · contradiction
  · rfl

Goal state after:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: a b c : ℤ
h : ¬c = 0
⊢ (a + b) * (c * c) = (a * c + b * c) * c

Tactic:
simp [Int.add_mul, Int.mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: a : ℤ
b : ℕ
hb : b ≠ 0
⊢ 0 < mkRat a b ↔ 0 < a

Tactic:
by
  grind [mkRat_nonneg_iff, Rat.mkRat_eq_zero]

Goal state after:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: a : ℚ≥0
⊢ ↑(a ^ 0) = ↑1

Tactic:
apply Field.zpow_zero'

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
x✝ : a ∣ b * ↑u
c : α
eq : b * ↑u = a * c
⊢ b = b * ↑u * ↑u⁻¹

Tactic:
Units.mul_inv_cancel_right

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
x✝ : a ∣ b * ↑u
c : α
eq : b * ↑u = a * c
⊢ b = b
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x : α
n : ℕ
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x

Tactic:
rcases eq_or_ne n 0 with rfl | hn
  · simp [isUnit_iff_dvd_one]
  · simp [hn, dvd_pow_self]

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible (↑ad ^ b)
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)

Tactic:
← Nat.cast_pow

Goal state after:
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible ↑(ad ^ b)
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
an ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible (↑ad ^ b)
⊢ IsNNRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)

Tactic:
← Nat.cast_pow

Goal state after:
α : Type u_1
inst✝ : Semiring α
an ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible ↑(ad ^ b)
⊢ IsNNRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
p : Prop
inst✝ : Decidable p
a : p → α
⊢ ⨆ (h : p), a h = if h : p then a h else ⊥

Tactic:
by by_cases h : p <;> simp [h]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
a : α
f : (i : ι) → κ i → α
⊢ Disjoint a (⨆ i, ⨆ j, f i j) ↔ ∀ (i : ι) (j : κ i), Disjoint a (f i j)

Tactic:
disjoint_iSup_iff

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ sSup ∅ = sSup univ

Tactic:
csSup_of_not_bddAbove (s := univ)

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ sSup ∅ = sSup ∅

α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ ¬BddAbove univ
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
y : α
yt : y ∈ t
⊢ False

Tactic:
by simpa using ht y yt

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi b ⊆ Ioi a ↔ a ≤ b

Tactic:
refine ⟨fun h => ?_, Ioi_subset_Ioi⟩

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Ioi b ⊆ Ioi a
⊢ a ≤ b
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
r : α → α → Prop
c c₁ c₂ s✝ t : Set α
a✝ b✝ x y : α
inst✝¹ : PartialOrder α
inst✝ : DecidableLE α
s : Set α
hs : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ ⟨a, ha⟩ ≤ ⟨b, hb⟩ ∨ ⟨b, hb⟩ ≤ ⟨a, ha⟩

Tactic:
exact hs.total ha hb

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
⊢ IsGLB S (if hS : S = ∅ then ⟨b, ⋯⟩ else ⟨sInf (Subtype.val '' S), ⋯⟩)

Tactic:
split_ifs with hS
    · subst hS; simp only [isGLB_empty_iff, isTop_iff_eq_top]; rfl
    · exact .of_image Subtype.coe_le_coe <| isGLB_csInf ((Set.nonempty_iff_ne_empty.mpr hS).image _)
        ((Subtype.mono_coe _).map_bddBelow (OrderBot.bddBelow S))

Goal state after:
Module: Mathlib.Tactic.NormNum.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ IsNat |a| na

Tactic:
rw [pa.out, Nat.abs_cast]

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ IsNat (↑na) na
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ ↑r / ↑b' + q = q

Tactic:
rw [Int.ediv_eq_zero_of_lt, zero_add] <;> [simp; simpa using h₂]

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

Goal state before:
pp: case inr
k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
· exact cast_div n_dvd (cast_ne_zero.mpr hn)

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

Goal state before:
pp: i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ (n + 1) * (n + 1)!

Tactic:
exact Nat.mul_pos n.succ_pos n.succ.factorial_pos

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

Goal state before:
pp: ⊢ descFactorial 0 0 = 0!

Tactic:
rw [descFactorial_zero, factorial_zero]

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

Goal state before:
pp: case pos
a b : ℕ+
h : b < a
⊢ ↑a - ↑b ≤ ↑a

Tactic:
exact Nat.sub_le a b

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

Goal state before:
pp: m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Tactic:
have := modDivAux_spec k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ)) this

Goal state after:
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this✝ : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
this : ↑(k.modDivAux (↑m % ↑k) (↑m / ↑k)).1 + ↑k * (k.modDivAux (↑m % ↑k) (↑m / ↑k)).2 = ↑m % ↑k + ↑k * (↑m / ↑k)
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
h0 : b ≤ a
⊢ ↑⌊a⌋ + 1 - ↑⌊b⌋ = 1

Tactic:
by rw [h, add_sub_cancel_left]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
ε : K
hε : 0 < ε
⊢ ∃ n, 1 / (↑n + 1) < ε

Tactic:
by
  obtain ⟨n, hn⟩ := exists_nat_gt (1 / ε)
  use n
  rw [div_lt_iff₀, ← div_lt_iff₀' hε]
  · apply hn.trans
    simp [zero_lt_one]
  · exact n.cast_add_one_pos

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

Goal state before:
pp: case right
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : (↑q.den).natAbs.Coprime q.num.natAbs
this : (↑q.den).natAbs = q.den
⊢ ↑(↑q.den / ↑q.num).den = ↑q.num.natAbs

Tactic:
q_num_abs_eq_q_num

Goal state after:
case right
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : (↑q.den).natAbs.Coprime q.num.natAbs
this : (↑q.den).natAbs = q.den
⊢ ↑(↑q.den / ↑q.num).den = q.num
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ |δ| ≤ δ

Tactic:
abs_eq_self.mpr (by positivity)

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ δ ≤ δ
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r p : α → β → Prop
s : Multiset α
t : Multiset β
hst : Rel r s t
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b
⊢ Rel p s t

Tactic:
by
  induction hst with
  | zero => exact Rel.zero
  | @cons a b s t hab _hst ih =>
    apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
    exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ (range fun x ↦ l[x]?) = insert none (some '' {x | x ∈ l})

Tactic:
← range_list_get,

Goal state after:
α : Type u_1
l : List α
⊢ (range fun x ↦ l[x]?) = insert none (some '' range l.get)
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp.cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
b' : β
bs' : Multiset β
h₁ : r a b'
h₂ : Rel r cs bs'
eq : bs = b' ::ₘ bs'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

Tactic:
exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l.Nodup
i : ℕ
h : i < l.length
⊢ l.erase l[i] = l.eraseIdx i

Tactic:
induction l generalizing i with
  | nil => simp
  | cons a l IH =>
    cases i with
    | zero => simp
    | succ i => grind

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
h : a ∉ s
⊢ (a :: s.toList).Nodup

Tactic:
by simp [h, nodup_toList s]

Goal state after:
Module: Mathlib.Data.Finset.Range

Goal state before:
pp: x✝ : ℕ
⊢ range x✝ ⊂ range (x✝ + 1)

Tactic:
by simp [ssubset_def]

Goal state after:
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑s
⊢ s.toFinset = Finset.univ ↔ s = univ

Tactic:
by
  rw [← coe_inj, coe_toFinset, coe_univ]

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

Goal state before:
pp: case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

Tactic:
refine ⟨⟨2, by lia⟩, ?_⟩

Goal state after:
case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ ↑⟨2, ⋯⟩ ≠ i ∧ ↑⟨2, ⋯⟩ ≠ j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ j.succ.castSucc = j.castSucc.succ

pp: case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ j.succ ≤ i

Tactic:
succ_castSucc

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ j.succ.castSucc = j.succ.castSucc

case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ j.succ ≤ i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ j.castSucc.succ = j.succ.castSucc

Tactic:
succ_castSucc

Goal state after:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ j.succ.castSucc = j.succ.castSucc
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i.rev = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i)

Tactic:
rcases rev_surjective i with ⟨i, rfl⟩
  rw [rev_rev]
  induction i using Fin.addCases
  · simp [rev_castAdd]
  · simp [cast_rev, rev_addNat]

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

Goal state before:
pp: n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
i : Fin (n.succ + 1)
⊢ cons a (snoc q b) i = snoc (cons a q) b i

Tactic:
cases i using Fin.cases with

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ False

Tactic:
refine lt_irrefl (Fintype.card α) ?_

Goal state after:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ Fintype.card α < Fintype.card α
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
suffices ∀ b' : α, b' ∈ List.orderedInsert r a l → r b b' by
        simpa [orderedInsert_cons, h', h.of_cons.orderedInsert a l]

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
⊢ ∀ (b' : α), b' ∈ List.orderedInsert r a l → r b b'
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ univ.Infinite

Tactic:
exact infinite_univ

Goal state after:
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : p x
⊢ op (f x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))

pp: case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : ¬p x
⊢ op (g x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))

Tactic:
· have : x ∉ Finset.filter p s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]

Goal state after:
case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : ¬p x
⊢ op (g x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
Module: Mathlib.Data.List.Range

Goal state before:
pp: l : List ℕ
⊢ map length l.ranges = l

Tactic:
induction l with
  | nil => simp only [ranges, map_nil]
  | cons a l hl => -- (a :: l)
    simp only [ranges, map_cons, length_range, map_map, cons.injEq, true_and]
    conv_rhs => rw [← hl]
    apply map_congr_left
    intro s _
    simp only [Function.comp_apply, length_map]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ IsChain R l ↔ Forall₂ R l.dropLast l.tail

Tactic:
induction l using twoStepInduction <;> simp_all

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ s.toList.prod = s.prod

Tactic:
conv_rhs => rw [← coe_toList s]
  rw [prod_coe]

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

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
⊢ ((a :: l).rotate' (n + 1)).length = (a :: l).length

Tactic:
rw [List.rotate', length_rotate' (l ++ [a]) n]

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
⊢ (l ++ [a]).length = (a :: l).length
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l : List ℕ
n : ℕ
⊢ (∃ s, s ∈ l.ranges ∧ n ∈ s) ↔ n ∈ range l.sum

Tactic:
← ranges_flatten,

Goal state after:
l : List ℕ
n : ℕ
⊢ (∃ s, s ∈ l.ranges ∧ n ∈ s) ↔ n ∈ l.ranges.flatten
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
n : ℕ
⊢ Injective fun l ↦ l.rotate n

Tactic:
by
  rintro l l' (h : l.rotate n = l'.rotate n)
  have hle : l.length = l'.length := (l.length_rotate n).symm.trans (h.symm ▸ l'.length_rotate n)
  rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod] at h
  obtain ⟨hd, ht⟩ := append_inj h (by simp_all)
  rw [← take_append_drop _ l, ht, hd, take_append_drop]

Goal state after:
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
b : β
h : (↑s).PairwiseDisjoint t
⊢ b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a

Tactic:
simp only [mem_def, disjiUnion_val, Multiset.mem_bind]

Goal state after: