mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_lt_n : a < n
one_le_b : 1 ≤ b
b_lt_n : b < n
⊢ a < n * b ∧ b < n * a

Tactic:
exact ⟨lt_mul_of_lt_of_one_le a_lt_n one_le_b, lt_mul_of_lt_of_one_le b_lt_n one_le_a⟩

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ 1 < |a|ₘ ↔ a ≠ 1

Tactic:
obtain ha | rfl | ha := lt_trichotomy a 1

Goal state after:
case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : a < 1
⊢ 1 < |a|ₘ ↔ a ≠ 1

case inr.inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
⊢ 1 < |1|ₘ ↔ 1 ≠ 1

case inr.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : 1 < a
⊢ 1 < |a|ₘ ↔ a ≠ 1
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑1 < ↑n ↔ 1 < n

Tactic:
cast_lt

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ 1 < n ↔ 1 < n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: k n r : ℕ
hkn : n.Coprime k
hk : k ≠ 0
⊢ ∃ m, m < k ∧ n * m % k = r % k

Tactic:
obtain rfl | hk : k = 1 ∨ 1 < k := by lia

Goal state after:
case inl
n r : ℕ
hkn : n.Coprime 1
hk : 1 ≠ 0
⊢ ∃ m, m < 1 ∧ n * m % 1 = r % 1

case inr
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
⊢ ∃ m, m < k ∧ n * m % k = r % k
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b

Tactic:
refine ⟨?_, ?_⟩
  · rintro ⟨ab, ba⟩
    exact
      ⟨⟨IsLeftRegular.of_mul ba.left, IsRightRegular.of_mul ab.right⟩,
        ⟨IsLeftRegular.of_mul ab.left, IsRightRegular.of_mul ba.right⟩⟩
  · rintro ⟨ha, hb⟩
    exact ⟨ha.mul hb, hb.mul ha⟩

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : α
hm : Even m
hn : Even n
⊢ Even (m - n)

Tactic:
obtain ⟨a, rfl⟩ := hm
  obtain ⟨b, rfl⟩ := hn
  refine ⟨a - b, ?_⟩
  obtain h | h := le_total a b
  · rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]
  · exact (tsub_add_tsub_comm h h).symm

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

Goal state before:
pp: R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
⊢ Monotone Int.cast

Tactic:
intro m n h

Goal state after:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
h : m ≤ n
⊢ ↑m ≤ ↑n
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ ↑0 < ↑n ↔ 0 < n

Tactic:
cast_lt

Goal state after:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ 0 < n ↔ 0 < n
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ ↑n < ↑0 ↔ n < 0

Tactic:
cast_lt

Goal state after:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ n < 0 ↔ n < 0
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z < ⌊a⌋ ↔ ↑z + 1 ≤ a

Tactic:
← add_one_le_iff,

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z + 1 ≤ ⌊a⌋ ↔ ↑z + 1 ≤ a
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌈a⌉ < z ↔ a ≤ ↑z - 1

Tactic:
← le_sub_one_iff,

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌈a⌉ ≤ z - 1 ↔ a ≤ ↑z - 1
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
⊢ Nat.cast ⁻¹' Ioc a b = Ioc ⌊a⌋₊ ⌊b⌋₊

Tactic:
ext
  simp [floor_lt, le_floor_iff, hb, ha]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
ι : Sort u_3
r : α → α → Prop
f : ι → α
⊢ (∀ x ∈ Set.range f, ∀ y ∈ Set.range f, ∃ z ∈ Set.range f, r x z ∧ r y z) ↔
    ∀ (x y : ι), ∃ z, r (f x) (f z) ∧ r (f y) (f z)

Tactic:
Set.forall_mem_range,

Goal state after:
α : Type u_1
ι : Sort u_3
r : α → α → Prop
f : ι → α
⊢ (∀ (i i_1 : ι), ∃ z ∈ Set.range f, r (f i) z ∧ r (f i_1) z) ↔ ∀ (x y : ι), ∃ z, r (f x) (f z) ∧ r (f y) (f z)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp.top
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
hab : a < b
hc : ↑a < ⊤ ∧ ⊤ < ↑b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
| top =>

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : WithBot α
⊢ a < b ↔ ∃ x, ↑x < b ∧ a < ↑x

Tactic:
rw [lt_iff_exists_coe_btwn]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : WithBot α
⊢ (∃ x, a < ↑x ∧ ↑x < b) ↔ ∃ x, ↑x < b ∧ a < ↑x
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ y * ↑x + y * x.neg = 0

Tactic:
by simp [← mul_add]

Goal state after:
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ y * x.neg + y * ↑x = 0

Tactic:
by simp [← mul_add]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
⊢ MonotoneOn f (insert a s) ↔
    (∀ (b : α), b ∈ s → b ≤ a → f b ≤ f a) ∧ (∀ (b : α), b ∈ s → a ≤ b → f a ≤ f b) ∧ MonotoneOn f s

Tactic:
by
  simp [MonotoneOn, forall_and]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : 0 ≤ n
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

pp: case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

Tactic:
· obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le n0
    simp only [mabs_pow, zpow_natCast, Nat.abs_cast]

Goal state after:
case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n : ℕ
inst✝ : IsOrderedRing α
⊢ |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n

Tactic:
induction n with | zero => simp [geomSum] | succ n ih => ?_

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |geomSum a b (n + 1)| ≤ (↑(n + 1) + 1) * max |a| |b| ^ (n + 1)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
a b : α
n : ℕ
⊢ a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n

Tactic:
induction n with | zero => simp [geomSum] | succ n ih => ?_

Goal state after:
case succ
α : Type u_1
inst✝ : CommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
Module: Mathlib.Order.Bounds.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : α
⊢ IsLUB (⇑f '' s) (f x) ↔ IsLUB s x

Tactic:
isLUB_image,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : α
⊢ IsLUB s (f.symm (f x)) ↔ IsLUB s x
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Icc a b ∩ Icc b c = {b}

Tactic:
rw [← Ici_inter_Iic, ← Iic_inter_Ici, inter_inter_inter_comm, Iic_inter_Ici]
  simp [hab, hbc]

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

Goal state before:
pp: case inl
γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_eq_i : j = i
⊢ j = i ∨ Iio i = Iic j

pp: case inr
γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ j = i ∨ Iio i = Iic j

Tactic:
· exact Or.inl hj_eq_i

Goal state after:
case inr
γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ j = i ∨ Iio i = Iic j
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ (a₁ + a₁) / 2 < (a₁ + a₂) / 2

Tactic:
gcongr; exact zero_lt_two

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ (a₁ + a₂) / 2 < (a₂ + a₂) / 2

Tactic:
gcongr; exact zero_lt_two

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
⊢ 2 * a * b ≤ ε * a ^ 2 + ε⁻¹ * b ^ 2

Tactic:
have h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2 := two_mul_le_add_sq (ε * a) b

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * a * b ≤ ε * a ^ 2 + ε⁻¹ * b ^ 2
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
⊢ idxOf x l = idxOf y l ↔ x = y

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩
  rw [← getElem_idxOf (idxOf_lt_length_iff.mpr hx)]
  simp [h]

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

Goal state before:
pp: α : Type u
l : List α
h : l.length = 1
⊢ l = [l.get ⟨0, ⋯⟩]

Tactic:
by
  refine ext_get (by convert! h) (by grind)

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

Goal state before:
pp: α : Type u
p : α → Prop
x : α
l : List α
⊢ Forall p (x :: l) ↔ p x ∧ ∀ (x : α), x ∈ l → p x

Tactic:
forall_cons,

Goal state after:
α : Type u
p : α → Prop
x : α
l : List α
⊢ p x ∧ Forall p l ↔ p x ∧ ∀ (x : α), x ∈ l → p x
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ { num := ↑q.den, den := q.num, den_nz := ⋯, reduced := ?m.26 }.num.natAbs = q.den

pp: q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num

Tactic:
Int.natAbs_natCast

Goal state after:
q : ℚ≥0
hq : q ≠ 0
⊢ q.den = q.den

q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
by
  rw [mul_den]
  exact ((Nat.dvd_iff_div_mul_eq _ _).mp (Nat.gcd_dvd_right _ _)).symm

Goal state after:
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: case hbd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ Commute ↑p.den ↑q.den

Tactic:
exact Nat.cast_commute ..

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

Goal state before:
pp: case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.den * ↑r.den ≠ 0

Tactic:
exact mul_ne_zero hq hr

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

Goal state before:
pp: case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑q.den * ↑r.num ≠ 0

Tactic:
exact mul_ne_zero hq hr

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

Goal state before:
pp: case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.den * ↑r.den ≠ 0

Tactic:
exact mul_ne_zero hq hr

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

Goal state before:
pp: n : ℤ
hn : ¬n = 0
⊢ ↑n ≠ 0

Tactic:
← intCast_inj

Goal state after:
n : ℤ
hn : ¬↑n = ↑0
⊢ ↑n ≠ 0
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_2
n n' : ℤ
r : R
inst✝ : CommRing R
hr : ↑n = r
hn : n' = n
a : R
⊢ n' • a = r * a

Tactic:
subst_vars
  simp only [zsmul_eq_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ : R
h : IsNat (a₁ + b₁) 0
⊢ 0 + (a₂ + b₂) = a₂ + b₂

Tactic:
add_pf_zero_add

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ : R
h : IsNat (a₁ + b₁) 0
⊢ a₂ + b₂ = a₂ + b₂
Module: Mathlib.Order.ConditionallyCompleteLattice.Defs

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
s : Set α
H : ¬BddAbove s
⊢ sSup s = sSup ∅

Tactic:
BddAbove

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
s : Set α
H : ¬(upperBounds s).Nonempty
⊢ sSup s = sSup ∅
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ ⋃ i, ⋃ j, s i j = univ ↔ ∀ (a : α), ∃ i j, a ∈ s i j

Tactic:
by
  simp only [iUnion_eq_univ_iff, mem_iUnion]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨆ x ∈ ⋃ i, ↑i, f x = ⨆ s ∈ S, ⨆ x ∈ s, f x

Tactic:
iSup_iUnion,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨆ i, ⨆ a ∈ ↑i, f a = ⨆ s ∈ S, ⨆ x ∈ s, f x
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
⊢ sInf (f '' s) = sInf (f '' t)

Tactic:
obtain rfl | hs := Set.eq_empty_or_nonempty s

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : ∅ ⊆ t
h : ∀ y ∈ t, ∃ x ∈ ∅, x ≤ y
⊢ sInf (f '' ∅) = sInf (f '' t)

case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) = sInf (f '' t)
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁺ᵐ * a⁻ᵐ = |a|ₘ

Tactic:
rw [oneLePart_def, sup_mul, one_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel, sup_assoc,
    ← sup_assoc a, sup_eq_right.2 le_sup_right]
  exact sup_eq_left.2 <| one_le_mabs a

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

Goal state before:
pp: n k : ℕ
⊢ n ! * (n + 1).ascFactorial k * (n + 1 + k) = (n + k + 1) * (n + k)!

Tactic:
factorial_mul_ascFactorial n k,

Goal state after:
n k : ℕ
⊢ (n + k)! * (n + 1 + k) = (n + k + 1) * (n + k)!
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
β : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
f : F
α : Type u_7
inst✝² : FunLike F α β
inst✝¹ : CommGroup α
inst✝ : GroupSeminormClass F α β
x y : α
⊢ f (x⁻¹ * y) = f (x * y⁻¹)

Tactic:
rw [← map_inv_eq_map, inv_mul', inv_inv, div_eq_mul_inv]

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).ascFactorial n * n ! ≤ (n + n) ^ n * n !

Tactic:
exact Nat.mul_le_mul_right _ (ascFactorial_le_pow_add _ _)

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
⊢ round ↑m = (m + m) / 2

Tactic:
round_intCast,

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 = (m + m) / 2
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
⊢ ⌊a + 1⌋ = ⌊a⌋ + 1

Tactic:
rw [← cast_one, floor_add_intCast]

Goal state after:
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⌋
⊢ |a - b| < 1

Tactic:
wlog h0 : b ≤ a generalizing a b

Goal state after:
case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
this : ∀ {a b : R}, ⌊a⌋ = ⌊b⌋ → b ≤ a → |a - b| < 1
h0 : ¬b ≤ a
⊢ |a - b| < 1

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 - b| < 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
x : R
hx : fract x ≠ 0
⊢ fract (-x) = 1 - fract x

Tactic:
fract_eq_iff

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x ∧ 1 - fract x < 1 ∧ ∃ z, -x - (1 - fract x) = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inr
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₀ : ℕ
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n

Tactic:
let q := ⌈↑m₀ / (n : k)⌉

Goal state after:
case inr.inr
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⌉
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
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 : n < 0
⊢ l + a + n • a = l + (a + n • a)

Tactic:
add_assoc

Goal state after:
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 : n < 0
⊢ l + (a + n • a) = l + (a + n • a)
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ • p₁ = v₂ • p₂ ↔ v₁⁻¹ * v₂ = p₁ /ₛ p₂

Tactic:
rw [eq_smul_iff_sdiv_eq, smul_sdiv_assoc, ← mul_right_inj v₁⁻¹, inv_mul_cancel_left, eq_comm]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p : P
⊢ v₁ * (p /ₛ p) / v₂ = v₁ / v₂

Tactic:
sdiv_self,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p : P
⊢ v₁ * 1 / v₂ = v₁ / v₂
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ (pointReflection x) y = (Equiv.symm (pointReflection x)) y

Tactic:
by rw [pointReflection_symm]

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
h✝ : ∀ (x : K), ∃ n, x < ↑n
x : K
n : ℤ
h : x < ↑n
⊢ ↑n ≤ ↑n.toNat

Tactic:
exact mod_cast Int.self_le_toNat _

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

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
f : ↑(Ico 0 1) → G
x : R
⊢ f ⟨Int.fract (x + 1), ⋯⟩ + ⌊x + 1⌋ • a = f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a + a

Tactic:
simp [add_one_zsmul, add_assoc]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
hs : ¬a ∈ s
w✝ : Multiset α
h₁ : a ∈ a ::ₘ w✝
h₂ : s ≤ a ::ₘ w✝
⊢ a ::ₘ s ≤ a ::ₘ w✝

Tactic:
exact cons_le_cons _ ((le_cons_of_notMem hs).mp h₂)

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.Nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?

Tactic:
by
  grind [List.pairwise_iff_getElem]

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

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

Tactic:
exact ⟨b, bs, ha'b, h, rfl⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l.Nodup
i : Fin l.length
⊢ l.erase (l.get i) = l.eraseIdx ↑i

Tactic:
by
  simp [erase_getElem, hl]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Tactic:
rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih,
        map_cons]

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : x ∈ t₁
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

Tactic:
have h₂ : x ∉ t₂ := h h₁
      simp [*]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
s : Multiset α
inst✝ : DecidableEq β
b : β
⊢ count b (map f s) = (filter (fun a ↦ b = f a) s).card

Tactic:
by
  simp [count, countP_map]

Goal state after: