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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ f a ∈ lowerBounds (f '' s) ↔ a ∈ lowerBounds s

Tactic:
simp [lowerBounds, hf.le_iff_le]

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
⊢ InjOn (Sum.elim f g) (sumEquiv.symm s)

Tactic:
rintro (a₁ | b₁) h₁ (a₂ | b₂) h₂ heq <;> aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ upperBounds s

Tactic:
h.upperBounds_eq

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ Ici a
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioo x y)
a : α
ha : a ∈ Ioo x y
⊢ ∃ b, b < ⟨a, ha⟩

Tactic:
by
    rcases exists_between ha.1 with ⟨b, hb₁, hb₂⟩
    exact ⟨⟨b, mem_Ioo.mpr ⟨hb₁, hb₂.trans ha.2⟩⟩, hb₂⟩

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
by rw [le_div_iff₀ hb, one_mul]

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α β γ : Type v
g' : α → β
h : β → γ
x : F (G α)
⊢ Comp.map (h ∘ g') (mk x) = Comp.map h (Comp.map g' (mk x))

Tactic:
by simp [Comp.map, Comp.mk, functor_norm, Function.comp_def]

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

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
ne : s.Nonempty
⊢ IsLUB {0} 0

Tactic:
exact isLUB_singleton

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
s : Set α
ha : 0 ≤ a
hs : IsLUB s b
⊢ IsLUB ((fun b ↦ a * b) '' s) (a * b)

Tactic:
by
  obtain ha | rfl := ha.lt_or_eq
  · exact (OrderIso.mulLeft₀ _ ha).isLUB_image'.2 hs
  · simp_rw [zero_mul]
    obtain rfl | ne := s.eq_empty_or_nonempty
    · simp only [Set.image_empty, isLUB_empty_iff] at hs ⊢
      have hb := hs (b + b)
      rw [le_add_iff_nonneg_right] at hb
      exact hs.mono hb
    rw [ne.image_const]
    exact isLUB_singleton

Goal state after:
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 - b * c) / (c * d) < 0 ↔ a / c < b / d

Tactic:
mul_comm b c,

Goal state after:
α : 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
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 - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d

Tactic:
mul_comm b c,

Goal state after:
α : 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
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → α
x✝ : List β
⊢ Forall₂ R (map f []) x✝ ↔ Forall₂ (fun c b ↦ R (f c) b) [] x✝

Tactic:
by simp only [map, forall₂_nil_left_iff]

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

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

pp: case inr.inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a / 0 ≤ 1 ↔ 0 < 0 ∧ a ≤ 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 ≤ a

pp: case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Tactic:
· simp [hb, hb.not_gt, hb.ne, div_le_one_of_neg]

Goal state after:
case inr.inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a / 0 ≤ 1 ↔ 0 < 0 ∧ a ≤ 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 ≤ a

case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₁ : (a :: l₁).length = (b :: l₂).length
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
⊢ Forall₂ R (a :: l₁) (b :: l₂)

Tactic:
· simp only [length_cons, succ.injEq] at h₁
        exact Forall₂.cons (h₂ <| by simp [zip])
          (IH h₁ fun h => h₂ <| by
            simp only [zip, zipWith, mem_cons, Prod.mk.injEq]; right
            simpa [zip] using h)

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
a : M
⊢ ((x :: xs).set 0 a).prod =
    ((take 0 (x :: xs)).prod * if 0 < (x :: xs).length then a else 1) * (drop (0 + 1) (x :: xs)).prod

Tactic:
by simp [set]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
x✝¹ : ℕ
x✝ : M
⊢ ([].set x✝¹ x✝).prod = ((take x✝¹ []).prod * if x✝¹ < [].length then x✝ else 1) * (drop (x✝¹ + 1) []).prod

Tactic:
by simp [set]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
⊢ D * e = D * f

Tactic:
h₄

Goal state after:
M : Type u_1
inst✝ : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
⊢ D * f = D * f
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
a b c D e f : M
h₁ : a = b
h₂ : b = c
h₃ : c = D * e
h₄ : e = f
⊢ a = D * f

Tactic:
by
  rw [h₁, h₂, h₃, h₄]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
he : e ≠ 0
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ ((n, e) ::ᵣ L).eval * ((-n, e) ::ᵣ l).eval = l'.eval

Tactic:
by
  rw [mul_eq_eval₂ n (-n) e h]
  simp [zpow'_zero_of_ne_zero he]

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

Goal state before:
pp: α : Type u
β : Type v
f g : α → β → β
b : β
l : List α
H : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
⊢ foldr f b l = foldr g b l

Tactic:
induction l with | nil => rfl | cons hd tl ih => ?_
  simp only [mem_cons, or_imp, forall_and, forall_eq] at H
  simp only [foldr, ih H.2, H.1]

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

Goal state before:
pp: a : ℤ
b : ℕ
⊢ (mkRat a b)⁻¹ = ↑b /. a

Tactic:
rw [mkRat_eq_divInt, inv_divInt]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
⊢ IsPrimal (m * n)

Tactic:
obtain rfl | h0 := eq_or_ne m 0; · rwa [zero_mul]
  intro b c h
  obtain ⟨a₁, a₂, ⟨b, rfl⟩, ⟨c, rfl⟩, rfl⟩ := hm (dvd_of_mul_right_dvd h)
  rw [mul_mul_mul_comm, mul_dvd_mul_iff_left h0] at h
  obtain ⟨a₁', a₂', h₁, h₂, rfl⟩ := hn h
  exact ⟨a₁ * a₁', a₂ * a₂', mul_dvd_mul_left _ h₁, mul_dvd_mul_left _ h₂, mul_mul_mul_comm _ _ _ _⟩

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

Goal state before:
pp: case succ
m k : ℕ+
n : ℕ
⊢ ↑(k.modDivAux (n + 1) (↑m / ↑k)).fst = if n + 1 = 0 then ↑k else n + 1

Tactic:
if_neg n.succ_ne_zero

Goal state after:
case succ
m k : ℕ+
n : ℕ
⊢ ↑(k.modDivAux (n + 1) (↑m / ↑k)).fst = n + 1
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: case succ
m k : ℕ+
n : ℕ
⊢ (k.modDivAux (n + 1) (↑m / ↑k)).snd = if n + 1 = 0 then ↑m / ↑k - 1 else ↑m / ↑k

Tactic:
if_neg n.succ_ne_zero

Goal state after:
case succ
m k : ℕ+
n : ℕ
⊢ (k.modDivAux (n + 1) (↑m / ↑k)).snd = ↑m / ↑k
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c }.den ∣ b

Tactic:
rw [mk_eq_divInt,
    divInt_eq_divInt_iff b0 (ne_of_gt (Int.natCast_pos.2 (Nat.pos_of_ne_zero h)))] at e

Goal state after:
case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c }.den ∣ b
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
⊢ Injective NNRat.cast

Tactic:
by
  rintro p q hpq
  rw [NNRat.cast_def, NNRat.cast_def, Commute.div_eq_div_iff] at hpq
  on_goal 1 => rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]
  · norm_cast at hpq ⊢
  any_goals norm_cast
  any_goals apply den_ne_zero
  exact Nat.cast_commute ..

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₂ b₂ c : R
ea eb e : ℕ
x : R
x✝¹ : ea + eb = e
x✝ : a₂ * b₂ = c
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c

Tactic:
subst_vars; simp [pow_add, mul_mul_mul_comm]

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

Goal state before:
pp: case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMinOrder ι
f : ι → α
j : ι
⊢ f j ≤ ⨆ i, ⨆ j, ⨆ (_ : j > i), f j

Tactic:
obtain ⟨i, jlt⟩ := exists_lt j

Goal state after:
case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMinOrder ι
f : ι → α
j i : ι
jlt : i < j
⊢ f j ≤ ⨆ i, ⨆ j, ⨆ (_ : j > i), f j
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ ⋂₀ s = ⋂ i, ↑i

Tactic:
by
  simp only [← sInter_range, Subtype.range_coe]

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

Goal state before:
pp: case mp
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ y, range fun s ↦ ↑(f s y)) → x ∈ ⋃₀ C

pp: case mpr
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ x ∈ ⋃₀ C → x ∈ ⋃ y, range fun s ↦ ↑(f s y)

Tactic:
· rintro ⟨s, ⟨y, rfl⟩, ⟨s, hs⟩, rfl⟩
    refine ⟨_, hs, ?_⟩
    exact (f ⟨s, hs⟩ y).2

Goal state after:
case mpr
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ x ∈ ⋃₀ C → x ∈ ⋃ y, range fun s ↦ ↑(f s y)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : InfSet α
s : Set (WithTop α)
hs : ¬s ⊆ {⊤}
h's : BddBelow s
⊢ ¬(s ⊆ {⊤} ∨ ¬BddBelow s)

Tactic:
by simp [hs, h's]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
c : α
bc : b < c
ca : c < a
⊢ False

Tactic:
exact lt_irrefl _ (ca.trans_le (h bc))

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

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a b : α
h : b ≤ a
⊢ Icc (a ⊓ b) (a ⊔ b) = Icc b a

Tactic:
inf_eq_right.2 h,

Goal state after:
α : Type u_1
inst✝ : Lattice α
a b : α
h : b ≤ a
⊢ Icc b (a ⊔ b) = Icc b a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) → ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

Tactic:
rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩

Goal state after:
case mpr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfab : f a < f b
hfcb : f c < f b
⊢ ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

case mpr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ Ioo (min a b) (max a b) = Ioo b a

Tactic:
inf_eq_right.2 h,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ Ioo b (max a b) = Ioo b a
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
⊢ IsChain r (f ⁻¹' c)

Tactic:
intro _ ha _ hb hne

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x✝ : α
ha : x✝ ∈ f ⁻¹' c
y✝ : α
hb : y✝ ∈ f ⁻¹' c
hne : x✝ ≠ y✝
⊢ r x✝ y✝ ∨ r y✝ x✝
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ (s ∩ Icc x y).OrdConnected ↔ Ioo x y ⊆ s

Tactic:
by
  refine ⟨fun h ↦ Ioo_subset_Icc_self.trans fun z hz ↦ ?_, ordConnected_inter_Icc_of_subset⟩
  have hxy : x ≤ y := hz.1.trans hz.2
  exact h.out ⟨hx, left_mem_Icc.2 hxy⟩ ⟨hy, right_mem_Icc.2 hxy⟩ hz |>.1

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
⊢ a = b

Tactic:
← oneLePart_div_leOnePart a,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ = b
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a ≤ b

Tactic:
← oneLePart_div_leOnePart a,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ ≤ b
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ 0 < k * k !

Tactic:
exact Nat.mul_pos hk k.factorial_pos

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

Goal state before:
pp: n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + 1).ascFactorial (k + 2) < (n + (k + 2)) ^ (k + 2)

Tactic:
rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, succ_add_eq_add_succ n (k + 1)]

Goal state after:
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + (k + 1).succ) * (n + 1).ascFactorial (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)
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
⊢ a + b - (↑⌊a⌋ + ↑⌊b⌋) ≤ a + b - ↑⌊a + b⌋ + 1

Tactic:
sub_add,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a + b - (↑⌊a⌋ + ↑⌊b⌋) ≤ a + b - (↑⌊a + b⌋ - 1)
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n : ℤ
d : ℕ
| ⌈↑n / ↑d⌉

Tactic:
← neg_neg ⌈_⌉,

Goal state after:
n : ℤ
d : ℕ
| - -⌈↑n / ↑d⌉
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ ⌊-↑x⌋ = ⌊-x⌋

Tactic:
← Rat.cast_neg,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ ⌊↑(-x)⌋ = ⌊-x⌋
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ (g * g⁻¹) • (↑m * ↑m⁻¹) = 1

Tactic:
Units.mul_inv,

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ (g * g⁻¹) • 1 = 1
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✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
⊢ R (f (l + 1 • a)) (f (l + n • a))

Tactic:
refine Int.rel_of_forall_rel_succ_of_lt R (f := (f <| l + · • a)) (fun k ↦ ?_) hn
        simp_rw [add_comm k 1, add_zsmul, ← add_assoc, one_zsmul, map_add_zsmul]
        refine hR (k • b) (hf _ ?_ _ ?_ ?_) <;> simpa

Goal state after:
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
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ x < ↑(z + 1) / ↑n ∧ ↑(z + 1) / ↑n < y

Tactic:
div_lt_iff₀ n0'

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ x < ↑(z + 1) / ↑n ∧ ↑(z + 1) < y * ↑n
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case coe.coe
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
y : M
hxy : 0 < ↑y
x : M
⊢ ∃ n, ↑x ≤ n • ↑y

Tactic:
| coe x =>

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

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
x y : WithBot M
hxy : 0 < y
⊢ ∃ n, x ≤ n • y

Tactic:
cases y with
  | bot => exact absurd hxy bot_le.not_gt
  | coe y =>
    cases x with
    | bot => refine ⟨0, bot_le⟩
    | coe x => simpa [← WithBot.coe_nsmul] using (Archimedean.arch x (by simpa using hxy))

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

Goal state before:
pp: case coe.coe
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
y : M
hxy : 1 < ↑y
x : M
⊢ ∃ n, ↑x ≤ ↑y ^ n

Tactic:
| coe x =>

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ p₄ : P
⊢ p₁ /ₛ (p₃ /ₛ p₄) • p₂ = (p₁ /ₛ p₃) / (p₂ /ₛ p₄)

Tactic:
sdiv_smul_comm,

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ p₄ : P
⊢ p₁ /ₛ (p₂ /ₛ p₄) • p₃ = (p₁ /ₛ p₃) / (p₂ /ₛ p₄)
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: case empty
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
t : Multiset α
h : Rel r 0 t
⊢ countP (r x) 0 = countP (r x) t

Tactic:
rel_zero_left.mp h

Goal state after:
case empty
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
t : Multiset α
h : Rel r 0 t
⊢ countP (r x) 0 = countP (r x) 0
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
inst✝ : Inhabited α
l : List α
⊢ range l.getI = insert default {x | x ∈ l}

Tactic:
by
  unfold List.getI
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
p : l₁ ~ l₂
a : α
h : a ∈ l₁
⊢ List.count a l₁.dedup = List.count a l₂.dedup

Tactic:
simp [h, nodup_dedup, p.subset h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t = 0 ↔ _root_.Disjoint s t

Tactic:
rw [← subset_zero]; simp [subset_iff, disjoint_left]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.drop n l₁ <+: List.drop n l₂

Tactic:
prefix_iff_eq_take.mp h,

Goal state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.drop n (List.take l₁.length l₂) <+: List.drop n l₂
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.ndinter t = 0 ↔ _root_.Disjoint s t

Tactic:
rw [← subset_zero]; simp [subset_iff, disjoint_left]

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

Goal state before:
pp: case mk.mk
α : Type u_5
a : α
val✝¹ : Multiset α
s : List α
nodup✝¹ : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
val✝ : Multiset α
t : List α
nodup✝ : Nodup (Quot.mk (⇑(List.isSetoid α)) t)
h :
  Disjoint { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ }
    { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ }
⊢ a ∈
      { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ }.disjUnion
        { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ } h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ } ∨
      a ∈ { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ }

Tactic:
apply List.mem_append

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ univ \ {a} = univ.erase a

Tactic:
sdiff_singleton_eq_erase

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ univ.erase a = univ.erase a
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
⊢ (∃ a ∈ s, f a = a✝) ↔ ∃ a ∈ s, g a = a✝

Tactic:
← bex_def

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
⊢ (∃ x, ∃ (_ : x ∈ s), f x = a✝) ↔ ∃ x, ∃ (_ : x ∈ s), g x = a✝
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ finsetEquivSet.symm s = s.toFinset

Tactic:
by simp [finsetEquivSet]

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

Goal state before:
pp: m n k : Int
hn : 0 ≤ n
hk : 0 ≤ k
⊢ (m.fdiv n).fdiv k = m.fdiv (n * k)

Tactic:
Int.fdiv_eq_ediv_of_nonneg _ hn,

Goal state after:
m n k : Int
hn : 0 ≤ n
hk : 0 ≤ k
⊢ (m / n).fdiv k = m.fdiv (n * k)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.val.card = #s

Tactic:
card_def

Goal state after:
α : Type u_1
s : Finset α
⊢ s.val.card = s.val.card
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
i : ℕ
hi : i ∈ range n
⊢ f i ⋯ ∈ s

Tactic:
apply hf'

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

Goal state before:

Tactic:
#s = #((range n).attach.image fun i => f i.1 (mem_range.1 i.2)) := by rw [this]
    _ = #(range n).attach := ?_
    _ = #(range n) := card_attach
    _ = n := card_range n

Goal state after:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun i ↦ f ↑i ⋯) (range n).attach
⊢ #(image (fun i ↦ f ↑i ⋯) (range n).attach) = #(range n).attach