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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ WellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m

Tactic:
by
  refine ⟨fun h => h.has_min, fun h => ⟨fun x => ?_⟩⟩
  by_contra hx
  obtain ⟨m, hm, hm'⟩ := h {x | ¬Acc r x} ⟨x, hx⟩
  refine hm ⟨_, fun y hy => ?_⟩
  by_contra hy'
  exact hm' y hy' hy

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
by_cases ha : a ∈ s <;> by_cases hb : b ∈ s

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: ⊢ Iic False = {False}

Tactic:
by aesop

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

Goal state before:
pp: ⊢ Iic True = univ

Tactic:
by aesop

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

Goal state before:
pp: ⊢ Ici False = univ

Tactic:
by aesop

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

Goal state before:
pp: ⊢ Ici True = {True}

Tactic:
by aesop

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

Goal state before:
pp: ⊢ Iio False = ∅

Tactic:
by aesop

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

Goal state before:
pp: ⊢ Ioi True = ∅

Tactic:
by aesop

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
k : α
n : ℕ
x a a' : α
h : k + a = a'
⊢ k + term n x a = term n x a'

Tactic:
by
  simp [h.symm, term, add_comm, add_assoc]

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ (a + a + a) / 3 = a

Tactic:
← two_mul,

Goal state after:
α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ (2 * a + a) / 3 = a
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: n✝¹ n✝ : ℕ
⊢ ↑n✝¹ % ↑n✝ = ↑(n✝¹.mod n✝)

Tactic:
by aesop

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

Goal state before:
pp: n✝¹ n✝ : ℕ
⊢ ↑n✝¹ / ↑n✝ = ↑(n✝¹.div n✝)

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
← inv_le_inv_of_neg hb (inv_lt_zero'.2 ha),

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ b⁻¹ ≤ a⁻¹⁻¹ ↔ b⁻¹ ≤ a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 = 2⁻¹ + 2⁻¹

Tactic:
← two_mul,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 = 2 * 2⁻¹
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ (a * d - c * b) / (c * d) < 0 ↔ a / c < b / d

Tactic:
← div_sub_div _ _ hc hd,

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ a / c - b / d < 0 ↔ a / c < b / d
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ (a * d - c * b) / (c * d) ≤ 0 ↔ a / c ≤ b / d

Tactic:
← div_sub_div _ _ hc hd,

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ a / c - b / d ≤ 0 ↔ a / c ≤ b / d
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
a b : α
l : List α
⊢ b :: l = replicate (b :: l).length a ↔ ∀ (b_1 : α), b_1 ∈ b :: l → b_1 = a

Tactic:
by simp [eq_replicate_length, replicate_succ]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
L : List M
h : L.prod ≠ 1
⊢ 0 < L.length

Tactic:
cases L

Goal state after:
case nil
M : Type u_4
inst✝ : Monoid M
h : [].prod ≠ 1
⊢ 0 < [].length

case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
h : (head✝ :: tail✝).prod ≠ 1
⊢ 0 < (head✝ :: tail✝).length
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case none
α : Type u
l : List α
h : ∀ (x : α), x ∈ l
⊢ ∃ a, (fun n ↦ l[n]?) a = none

Tactic:
exact ⟨l.length, getElem?_eq_none <| Nat.le_refl _⟩

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

Goal state before:
pp: case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (foldl comp f (lh :: lt))

Tactic:
apply l_ih fun _ h => hl _ (List.mem_cons_of_mem _ h)

Goal state after:
case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (f ∘ lh)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: L : List ℕ
⊢ L.headI + L.tail.sum = L.sum

Tactic:
cases L

Goal state after:
case nil
⊢ [].headI + [].tail.sum = [].sum

case cons
head✝ : ℕ
tail✝ : List ℕ
⊢ (head✝ :: tail✝).headI + (head✝ :: tail✝).tail.sum = (head✝ :: tail✝).sum
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → Option β
l : List α
⊢ filterMap f l = flatMap (fun a ↦ (f a).toList) l

Tactic:
induction l with | nil => ?_ | cons a l ih => ?_

Goal state after:
case nil
α : Type u
β : Type v
f : α → Option β
⊢ filterMap f [] = flatMap (fun a ↦ (f a).toList) []

case cons
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
⊢ filterMap f (a :: l) = flatMap (fun a ↦ (f a).toList) (a :: l)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : BEq ι
inst✝ : LawfulBEq ι
l : List ι
i : ℕ
hi : 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 grind

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

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
⊢ a ∈ t

Tactic:
rwa [hf a a' (hs a ha) (ht a' ha') ha''.symm]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
⊢ n ≤ m

Tactic:
← not_lt

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
⊢ ¬m < n
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c : ℕ
h1 : a.pow b = c
⊢ a.pow (2 * b + 1) = c.mul (c.mul a)

Tactic:
by simp [two_mul, pow_add, mul_assoc, ← h1]

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

Goal state before:
pp: a : ℕ
ha0 : 0 < a
⊢ (↑a)⁻¹.den = a

Tactic:
rw [← Int.ofNat_inj, ← Int.cast_natCast a, inv_intCast_den_of_pos]
  rwa [Int.natCast_pos]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : Semifield R
a b c d : R
x✝¹ : b⁻¹ = c
x✝ : a * c = d
⊢ a / b = d

Tactic:
subst_vars; simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : ⋃ i ∈ t, s i = ⊤
⊢ t.Nonempty

Tactic:
obtain ⟨x, m, -⟩ := exists_set_mem_of_union_eq_top t s w H.some

Goal state after:
α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : ⋃ i ∈ t, s i = ⊤
x : ι
m : x ∈ t
⊢ t.Nonempty
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s t : Set β
⊢ ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

Tactic:
simp_rw [mem_union, iSup_or, iSup_sup_eq]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
⊢ ⨅ a, ⨆ b, g a b = ⨆ g_1, ⨅ a, g a (g_1 a)

Tactic:
let lhs := ⨅ a, ⨆ b, g a b
    let rhs := ⨆ h : ∀ a, β a, ⨅ a, g a (h a)
    suffices lhs ≤ rhs from le_antisymm this le_iInf_iSup
    if h : ∃ x, rhs < x ∧ x < lhs then
      rcases h with ⟨x, hr, hl⟩
      suffices rhs ≥ x from nomatch not_lt.2 this hr
      have : ∀ a, ∃ b, x < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_not_ge fun h =>
            lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) h))
      choose f hf using this
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => le_of_lt (hf a)
    else
      refine le_of_not_gt fun hrl : rhs < lhs => not_le_of_gt hrl ?_
      replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by
        simpa only [not_exists, not_and_or, not_or, not_lt] using h
      have : ∀ a, ∃ b, rhs < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_lt_of_le hrl (iInf_le _ a)
      choose f hf using this
      have : ∀ a, lhs ≤ g a (f a) := fun a =>
        (h (g a (f a))).resolve_left (by simpa using hf a)
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => this _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : MonotoneOn f (Ici a)
x✝¹ : α
x✝ : x✝¹ ∈ Ici a
⊢ f x✝¹ ∈ Ici (f a)

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
b : α
h : MonotoneOn f (Iic b)
x✝¹ : α
x✝ : x✝¹ ∈ Iic b
⊢ f x✝¹ ∈ Iic (f b)

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : AntitoneOn f (Ici a)
x✝¹ : α
x✝ : x✝¹ ∈ Ici a
⊢ f x✝¹ ∈ Iic (f a)

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
b : α
h : AntitoneOn f (Iic b)
x✝¹ : α
x✝ : x✝¹ ∈ Iic b
⊢ f x✝¹ ∈ Ici (f b)

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
⊢ IsGLB s (sInf s)

Tactic:
by_cases hs : BddBelow s
  · exact isGLB_sInf' hs
  · exact isGLB_sInf' (OrderBot.bddBelow _)

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)
  · simp
  · exact hne.pairwise_iff_exists_forall

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
⊢ (s.PairwiseDisjoint fun a ↦ f a '' t) ↔ InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)

Tactic:
refine ⟨fun hs x hx y hy (h : f _ _ = _) => ?_, fun hs x hx y hy h => ?_⟩
  · suffices x.1 = y.1 by exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])
    refine hs.elim hx.1 hy.1 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.2, ?_⟩)
    rw [h]
    exact mem_image_of_mem _ hy.2
  · refine disjoint_iff_inf_le.mpr ?_
    rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩
    exact h (congr_arg Prod.fst <| hs (mk_mem_prod hx ha) (mk_mem_prod hy hb) hab)

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : φ a ≠ φ a'
h₂ : r' (φ a) (φ a')
haa' : a = a'
⊢ φ a = φ a'

Tactic:
by rw [haa']

Goal state after:
Module: Mathlib.Algebra.Order.Nonneg.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
⊢ sSup ∅ = ⊥

Tactic:
by
      rw [@subset_sSup_def α (Set.Ici a) _ _ ⟨⟨a, le_rfl⟩⟩]; simp [bot_eq]

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

Goal state before:
pp: m n : ℕ
hn : 1 < n
⊢ n ! = m ! ↔ n = m

Tactic:
refine ⟨fun h => ?_, congr_arg _⟩
  obtain hnm | rfl | hnm := lt_trichotomy n m
  · rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
    cases lt_irrefl _ hnm
  · rfl
  rw [← one_lt_factorial, h, one_lt_factorial] at hn
  rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
  cases lt_irrefl _ hnm

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2

Tactic:
have H : ⌊2 * fract x⌋ = 1 := by simpa [floor_eq_iff, ← two_mul, fract_lt_one] using h
    suffices 0 < fract x by simp [this, H, ceil_eq_iff, (fract_lt_one _).le]
    contrapose! h
    grw [h]
    simp

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inl.inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m : ℤ
hx : 2 * fract ↑m ≠ 1
hm : ↑(m + m) = 2 * ↑m
⊢ m = (m + m) / 2

Tactic:
← two_mul,

Goal state after:
case inl.inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m : ℤ
hx : 2 * fract ↑m ≠ 1
hm : ↑(m + m) = 2 * ↑m
⊢ m = 2 * m / 2
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ a ≠ 0

Tactic:
intro hzero

Goal state after:
n : ℕ+
a : ℕ
h : a ∣ ↑n
hzero : a = 0
⊢ False
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✝ : R
z a : ℤ
⊢ a ≤ ⌊a✝ + ↑z⌋ ↔ a ≤ ⌊a✝⌋ + z

Tactic:
by
    rw [le_floor, ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, Int.cast_sub]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a < (1 + ↑⌊a / b⌋) * b

Tactic:
← div_lt_iff₀ hb,

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a / b < 1 + ↑⌊a / b⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inr.calc_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (-↑m₀ / ↑n) = fract (↑m₁ / ↑n)

Tactic:
rw [← fract_intCast_add q, ← mul_div_cancel_right₀ (q : k) hn.ne', ← add_div, ← sub_eq_add_neg]
    simp [m₁]

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

Goal state before:
pp: n : ℤ
d : ℕ
⊢ ⌈↑n / ↑d⌉ = -(-n / ↑d)

Tactic:
conv_lhs => rw [← neg_neg ⌈_⌉, ← floor_neg]

Goal state after:
n : ℤ
d : ℕ
⊢ -⌊-(↑n / ↑d)⌋ = -(-n / ↑d)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k : ℕ
hk : g⁻¹ ≤ a ^ k
⊢ -↑k ∈ s

Tactic:
by simpa [s] using inv_le_inv' hk

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

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddCommMonoid G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℕ
x : G
⊢ f (n • a + x) = f x + n • b

Tactic:
by
  rw [add_comm, map_add_nsmul]

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
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
hn : Nat.find this ≠ 0
⊢ False

Tactic:
(Nat.succ_pred_eq_of_ne_zero hn).symm,

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ (Nat.find this).pred.succ < b * c
hn : Nat.find this ≠ 0
⊢ False
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a : α
⊢ ¬0 = {a}

Tactic:
exact (singleton_ne_zero _).symm

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

Goal state before:
pp: α : Type u_1
s : Multiset α
n : ℕ
⊢ (∃ a t, a ::ₘ t = s ∧ t.card = n) → s.card = n + 1

Tactic:
by aesop

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p s t

Tactic:
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.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    (∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ s → r a b) → m1.card = s.card → Rel r m1 s) →
      ∀ {m1 : Multiset α},
        (∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ s → r a_2 b) → m1.card = (a ::ₘ s).card → Rel r m1 (a ::ₘ s)

Tactic:
intro a t ih m h hc

Goal state after:
case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : m.card = (a ::ₘ t).card
⊢ Rel r m (a ::ₘ t)
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case e_tail
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
x : α
hx : x ∈ l
⊢ elem x (take n l) = elem x (b :: List.filter (fun a ↦ elem a (take n l)) l)

Tactic:
have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)

Goal state after:
case e_tail
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
x : α
hx : x ∈ l
this : x ≠ b
⊢ elem x (take n l) = elem x (b :: List.filter (fun a ↦ elem a (take n l)) l)
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ (if a ∈ l.dedup then 1 else 0) = if a ∈ l then 1 else 0

Tactic:
mem_dedup

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

Goal state before:
pp: α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (filter P s).card ≤ n ↔ ∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ a, a ∈ s' ∧ ¬P a

Tactic:
fconstructor
  · intro H s' hs' s'_card
    by_contra! rid
    have card := card_le_card (monotone_filter_left P hs') |>.trans H
    exact s'_card.not_ge (filter_eq_self.mpr rid ▸ card)
  · contrapose!
    exact fun H ↦ ⟨s.filter P, filter_le _ _, H, fun a ha ↦ (mem_filter.mp ha).2⟩

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits = take (n + 1) l.inits

Tactic:
by
  apply ext_getElem <;> (simp [take_take] <;> grind)

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
hs : s.Nontrivial
⊢ s ≠ {a}

Tactic:
by
  rintro rfl; exact not_nontrivial_singleton hs

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ s = {a} ∨ s.Nontrivial

Tactic:
rw [← coe_eq_singleton]; exact Set.eq_singleton_or_nontrivial ha

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t

Tactic:
by
  simp only [disjoint_left, mem_insert, or_imp, forall_and, forall_eq]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ¬a ∈ s ∪ t ↔ ¬a ∈ s ∧ ¬a ∈ t

Tactic:
rw [mem_union, not_or]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi : P a s
⊢ P (insert x s) a

Tactic:
rw [Finset.insert_eq]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi : P a s
⊢ P ({x} ∪ s) a
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a✝ b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi✝ : P a✝ s
a : α
t : Finset α
_ta : a ∉ t
hi : P {x} t
⊢ P (insert a t) {x}

Tactic:
rw [Finset.insert_eq]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a✝ b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi✝ : P a✝ s
a : α
t : Finset α
_ta : a ∉ t
hi : P {x} t
⊢ P ({a} ∪ t) {x}
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ i.pred hi ≤ j ↔ i ≤ j.succ

Tactic:
rw [← succ_le_succ_iff, succ_pred]

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j ≤ i.pred hi ↔ j.succ ≤ i

Tactic:
rw [← succ_le_succ_iff, succ_pred]

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a.castSucc.pred ha < a

Tactic:
rw [pred_castSucc_lt_iff, le_def]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ a + 1 ≤ b

Tactic:
cases n <;> fin_omega

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ s ⊆ t ∧ t ⊆ t ∧ #t = #t

Tactic:
by simp [hst]

Goal state after: