mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
m n : ℤ
⊢ m - n = 0 ↔ m = n

Tactic:
sub_eq_zero

Goal state after:
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
m n : ℤ
⊢ m = n ↔ m = n
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case inl
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b : N
bc : b ≤ b
⊢ μ a b ≤ μ a b

pp: case inr
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b c : N
bc✝ : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c

Tactic:
· exact le_rfl

Goal state after:
case inr
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b c : N
bc✝ : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ 0 = 0 * b

Tactic:
zero_mul

Goal state after:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 =
    a ^ (2 * k + 1 + 2) + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * k + 3)

Tactic:
add_right_comm

Goal state after:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * (k + 1) + 1) =
    a ^ (2 * k + 1 + 2) + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * k + 3)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - b - c = a - c - b

Tactic:
by
  rw [← tsub_add_eq_tsub_tsub, tsub_add_eq_tsub_tsub_swap]

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

Goal state before:
pp: α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
a : α
inst✝ : Nontrivial α
⊢ ∀ (a : α), ∃ b, a < b

Tactic:
obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'

Goal state after:
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
a : α
inst✝ : Nontrivial α
y : α
hy : 1 < y
⊢ ∀ (a : α), ∃ b, a < b
Module: Mathlib.Algebra.Order.Group.Defs

Goal state before:
pp: α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
a : α
inst✝ : Nontrivial α
⊢ ∀ (a : α), ∃ b, b < a

Tactic:
obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'

Goal state after:
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
a : α
inst✝ : Nontrivial α
y : α
hy : 1 < y
⊢ ∀ (a : α), ∃ b, b < a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝² : MulZeroClass α
a✝ b✝ c✝ d : α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLE α
a : α>0
b c : α
h : ↑a * b < ↑a * c
⊢ b ≠ c

Tactic:
by
        rintro rfl
        simp at h

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝² : MulZeroClass α
a✝ b✝ c✝ d : α
inst✝¹ : PartialOrder α
inst✝ : MulPosReflectLE α
a : α>0
b c : α
h : b * ↑a < c * ↑a
⊢ b ≠ c

Tactic:
by
        rintro rfl
        simp at h

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝³ : MulZeroClass α
b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < 0 * b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

Tactic:
zero_mul

Goal state after:
case inr.inl
α : Type u_1
inst✝³ : MulZeroClass α
b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < 0
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
by
  rw [← inv_le_inv₀ hb (inv_pos.2 ha), inv_inv]

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ a ^ 2 + b ^ 2 + 2 * a * b = a ^ 2 + 2 * a * b + b ^ 2

Tactic:
add_right_comm

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ a ^ 2 + 2 * a * b + b ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ -a * -b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
mul_nonneg_iff_pos_imp_nonneg (R := R)

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ a * -b ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
mul_nonneg_iff_pos_imp_nonneg (R := R)

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ -a * b ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
mul_nonneg_iff_pos_imp_nonneg (R := R)

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝⁶ : LE α✝
inst✝⁵ : LE β✝
inst✝⁴ : LE γ✝
inst✝³ : LE δ
α : Type u_6
β : Type u_7
γ : Type u_8
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
x✝¹ x✝ : (α × β) × γ
fst✝¹ : α
snd✝³ : β
snd✝² : γ
fst✝ : α
snd✝¹ : β
snd✝ : γ
⊢ (Equiv.prodAssoc α β γ) ((fst✝¹, snd✝³), snd✝²) ≤ (Equiv.prodAssoc α β γ) ((fst✝, snd✝¹), snd✝) ↔
    ((fst✝¹, snd✝³), snd✝²) ≤ ((fst✝, snd✝¹), snd✝)

Tactic:
by simp [Equiv.prodAssoc, and_assoc]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : EquivLike F α β
inst✝² : MulZeroClass α
inst✝¹ : MulZeroClass β
inst✝ : MulEquivClass F α β
f : F
⊢ f 0 = f (0 * EquivLike.inv f 0)

Tactic:
zero_mul

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : EquivLike F α β
inst✝² : MulZeroClass α
inst✝¹ : MulZeroClass β
inst✝ : MulEquivClass F α β
f : F
⊢ f 0 = f 0
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular 1

Tactic:
exact isRegular_one.left

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
h : ∀ (x y : R), x * y = 1 → IsLeftRegular x
a✝ b✝ : R
eq : a✝ * b✝ = 1
⊢ (fun x ↦ a✝ * x) (b✝ * a✝) = (fun x ↦ a✝ * x) 1

Tactic:
by simp [← mul_assoc, eq]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
hb : b ≠ ⊤
a : α
⊢ a + -b + b = a

Tactic:
by
  simp [add_assoc, neg_add_cancel_of_ne_top hb]

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

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ 0 * f ↑x⁻¹ = 0

Tactic:
zero_mul

Goal state after:
G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : ↑a ≠ 0
H : f ↑a = 0
⊢ 0 * f ↑a⁻¹ = 0

Tactic:
zero_mul

Goal state after:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀ˣ
hx : ↑a ≠ 0
H : f ↑a = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedRing R
inst✝ : ExistsAddOfLE R
a : R
k : ℕ
⊢ 0 ≤ a ^ k * a ^ k

Tactic:
exact mul_self_nonneg _

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₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
obtain ⟨a₁, a₂, h⟩ := DecompositionMonoid.primal _ h

Goal state after:
α : 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₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ ∀ (b : α), b ∈ s → a < b → f a < f b

Tactic:
intro b hb hab

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
b : α
hb : b ∈ s
hab : a < b
⊢ f a < f b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ ∀ (b : α), b ∈ s → b < a → f b < f a

Tactic:
intro b hb hab

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
b : α
hb : b ∈ s
hab : b < a
⊢ f b < f a
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ ∀ (b : α), b ∈ s → a < b → f b < f a

Tactic:
intro b hb hab

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
b : α
hb : b ∈ s
hab : a < b
⊢ f b < f a
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ ∀ (b : α), b ∈ s → b < a → f a < f b

Tactic:
intro b hb hab

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
b : α
hb : b ∈ s
hab : b < a
⊢ f a < f b
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ WellFoundedLT (Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2) ↔ WellFoundedLT α

Tactic:
isWellFounded_iff,

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ (WellFounded fun x1 x2 ↦ x1 < x2) ↔ WellFounded fun x1 x2 ↦ x1 < x2
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hb : b ≠ 0
he : Even n
this : a ^ n > -b ^ n
⊢ a ^ n = -b ^ n ↔ a = -b ∧ Odd n

Tactic:
simpa [he, not_odd_iff_even.2 he] using this.ne'

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

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

Tactic:
by
  simp [upperBounds, lowerBounds, hf.le_iff_ge]

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

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

Tactic:
by
  simp [upperBounds, lowerBounds, hf.le_iff_ge]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s

Tactic:
intro x hx y hy

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ s, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
⊢ Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)

Tactic:
ext ⟨x, y⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
x : α
y : β
⊢ (x, y) ∈ Icc a₁ a₂ ×ˢ Icc b₁ b₂ ↔ (x, y) ∈ Icc (a₁, b₁) (a₂, b₂)
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
s : Set α
⊢ upperBounds (insert a s) = Ici a ∩ upperBounds s

Tactic:
by
  rw [insert_eq, upperBounds_union, upperBounds_singleton]

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

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

Tactic:
zero_mul

Goal state after:
case inl
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : 0 ≤ 0
h : ∀ (ε : α), 1 < ε → a ≤ 0
⊢ a ≤ 0
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
zero_mul

Goal state after:
case inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun a ↦ 0) '' s) 0
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
zero_mul

Goal state after:
case inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
⊢ IsLUB ((fun a ↦ 0) '' s) 0
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
⊢ 1 / a < 1 / b ↔ b < a

Tactic:
simpa [one_div] using inv_lt_inv_of_neg ha hb

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 : α
a2 : 2 ≤ a
⊢ (1 - 1 / a)⁻¹ ≤ 2

Tactic:
refine (inv_anti₀ (inv_pos.2 <| zero_lt_two' α) ?_).trans_eq (inv_inv (2 : α))

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 2⁻¹ ≤ 1 - 1 / a
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case e_tail
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ (b :: l).dropLast ++ [(b :: l).getLast ⋯] = b :: l

Tactic:
exact dropLast_append_getLast (cons_ne_nil b l)

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

Goal state before:
pp: α : Type u
s t : List α
x : α
h : x ∈ s.head?
⊢ x ∈ (s ++ t).head?

Tactic:
by
  grind [Option.mem_def]

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
l : List M
a : M
inst✝ : DecidableEq M
ha : a ∈ l
comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x
⊢ a * (l.erase a).prod = l.prod

Tactic:
induction l with
  | nil => simp only [not_mem_nil] at ha
  | cons b l ih =>
    obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem ha
    · simp only [erase_cons_head, prod_cons]
    rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : f x = f y
hxys : map f xs = map f ys
⊢ x :: xs = y :: ys

Tactic:
h hxy,

Goal state after:
α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : f x = f y
hxys : map f xs = map f ys
⊢ y :: xs = y :: ys
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a /. b = 0 ↔ a = 0

Tactic:
rw [← zero_divInt b, divInt_eq_divInt_iff b0 b0, Int.zero_mul, Int.mul_eq_zero, or_iff_left b0]

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

Goal state before:
pp: case nil
n : ℤ
⊢ [].sum % n = (map (fun x ↦ x % n) []).sum % n

Tactic:
simp [Int.add_emod, *]

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

Goal state before:
pp: case cons
n head✝ : ℤ
tail✝ : List ℤ
tail_ih✝ : tail✝.sum % n = (map (fun x ↦ x % n) tail✝).sum % n
⊢ (head✝ :: tail✝).sum % n = (map (fun x ↦ x % n) (head✝ :: tail✝)).sum % n

Tactic:
simp [Int.add_emod, *]

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

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

Tactic:
zero_mul

Goal state after:
case inl
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
hm : IsPrimal 0
⊢ IsPrimal 0
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
n : ℤ
⊢ (q + ↑n).den = q.den

Tactic:
apply Nat.dvd_antisymm

Goal state after:
case a
q : ℚ
n : ℤ
⊢ (q + ↑n).den ∣ q.den

case a
q : ℚ
n : ℤ
⊢ q.den ∣ (q + ↑n).den
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
q : ℚ≥0
⊢ ↑q = 0 ↔ q = 0

Tactic:
by rw [← cast_zero, cast_inj]

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
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 }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
this : ↑b = 0 * ↑k
⊢ False

Tactic:
zero_mul

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
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 }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
this : ↑b = 0
⊢ False
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ n2 * t1 * e2 = t1 * t2

Tactic:
mul_comm n2,

Goal state after:
α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ t1 * n2 * e2 = t1 * t2
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ i, ⨆ (_ : i ≥ n), u i = ⨆ i, u (i + n)

Tactic:
by
  apply le_antisymm <;> simp only [iSup_le_iff]
  · refine fun i hi => le_sSup ⟨i - n, ?_⟩
    dsimp only
    rw [Nat.sub_add_cancel hi]
  · exact fun i => le_sSup ⟨i + n, iSup_pos (Nat.le_add_left _ _)⟩

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
s : ι → Set α
h_Union : (⋃ i, s i).Nonempty
⊢ Nonempty ι

Tactic:
by
  obtain ⟨x, hx⟩ := h_Union
  exact ⟨Classical.choose <| mem_iUnion.mp hx⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
⊢ (⨆ i, ⨆ (_ : ∃ i_1, e i_1 = i), extend e f ⊥ i) ⊔ ⨆ i, ⨆ (_ : ¬∃ i_1, e i_1 = i), extend e f ⊥ i = ⨆ i, f i

Tactic:
simp +contextual [he.extend_apply, extend_apply', @iSup_comm _ β ι]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β → γ → α
s : Set β
t : Set γ
⊢ sSup (image2 f s t) = ⨆ a ∈ s, ⨆ b ∈ t, f a b

Tactic:
by rw [← image_prod, sSup_image, biSup_prod]

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

Goal state before:
pp: α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
⊢ i.pi s \ i.pi t ⊆ ⋃ a ∈ i, eval a ⁻¹' (s a \ t a)

Tactic:
refine sdiff_subset_comm.2 fun x hx a ha => ?_
  simp only [mem_sdiff, mem_pi, mem_iUnion, not_exists, mem_preimage, not_and, not_not] at hx
  exact hx.2 _ ha (hx.1 _ ha)

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
⊢ DirectedOn r (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]

Goal state after:
α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
⊢ DirectedOn r (⋃ i, ↑i)
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
simp_rw [iSup_disjoint_iff]

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:
by
  simp_rw [disjoint_iSup_iff]

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

Goal state before:
pp: case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
ha : none ∈ upperBounds s
⊢ ⊤ ≤ none

pp: case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a

Tactic:
· exact le_rfl

Goal state after:
case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a