mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: case head.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
q : Prop
hq : Mem q l
⊢ a ↔ q

pp: case tail.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
⊢ p ↔ a

pp: case tail.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q

Tactic:
· exact ab.trans (H _ h _ hq)

Goal state after:
case tail.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
⊢ p ↔ a

case tail.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
⊢ IsRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0

Tactic:
rw [isRegular_iff, isLeftRegular_iff_right_eq_zero_of_mul, isRightRegular_iff_left_eq_zero_of_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ (-1)⁻¹ = -1

Tactic:
by rw [← neg_inv, inv_one]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
b c : G₀
⊢ a / b * (c / a) = c / b

Tactic:
by
  rw [mul_comm, div_mul_div_cancel₀ ha]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * a - b * a + (b * a - b * b)

Tactic:
sub_add_sub_cancel

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * a - b * b
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = -1
⊢ (-1) ^ (n + 1) = 1

Tactic:
by rw [pow_succ, h, neg_one_mul, neg_neg]

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ 0 • a = 0

Tactic:
HSMul.hSMul,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ SMul.smul 0 a = 0
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
z : ℕ
a : M
⊢ ↑z.succ • a = ↑z • a + a

Tactic:
HSMul.hSMul,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
z : ℕ
a : M
⊢ SMul.smul (↑z.succ) a = SMul.smul (↑z) a + a
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
⊢ Odd n → ∀ (a : α), (-a) ^ n = -a ^ n

Tactic:
rintro ⟨c, rfl⟩ a; simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ a * b⁻¹ ≤ c ↔ a ≤ b * c

Tactic:
rw [← inv_mul_le_iff_le_mul, mul_comm]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a / c ≤ b ↔ a ≤ b * c

Tactic:
by
  rw [← mul_le_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this✝ : MulLeftMono α
this : MulRightMono α
⊢ a * b = c * d ↔ a = c ∧ b = d

Tactic:
le_antisymm_iff,

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this✝ : MulLeftMono α
this : MulRightMono α
⊢ a * b ≤ c * d ∧ c * d ≤ a * b ↔ a = c ∧ b = d
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this✝ : MulLeftMono α
this : MulRightMono α
⊢ c * d ≤ a * b ↔ a = c ∧ b = d

Tactic:
mul_le_mul_iff_of_ge hac hbd

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this✝ : MulLeftMono α
this : MulRightMono α
⊢ a = c ∧ b = d ↔ a = c ∧ b = d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a < 1
⊢ StrictAnti fun n ↦ a ^ n

Tactic:
refine strictAnti_int_of_succ_lt fun n ↦ ?_

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
⊢ a ^ (n + 1) < a ^ n
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddLeftMono R
inst✝ : NoZeroDivisors R
r : R
⊢ r ^ 2 ≤ 0 ↔ r ^ 2 = 0

Tactic:
le_antisymm_iff,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddLeftMono R
inst✝ : NoZeroDivisors R
r : R
⊢ r ^ 2 ≤ 0 ↔ r ^ 2 ≤ 0 ∧ 0 ≤ r ^ 2
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case ha
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ 0 ≤ c⁻¹

Tactic:
exact Right.inv_nonneg.2 hc

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
h : a < b
hc : 0 < c
⊢ a / c < b / c

Tactic:
rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
  exact mul_lt_mul_of_pos_right h (Right.inv_pos.2 hc)

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a : G₀
inst✝ : PosMulMono G₀
⊢ a⁻¹ ≤ 0 ↔ a ≤ 0

Tactic:
have := PosMulMono.toPosMulReflectLT (α := G₀); simp only [← not_lt, inv_pos]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
e : f a = f b
⊢ a = b

Tactic:
apply Std.Trichotomous.trichotomous (r := r) a b
    · exact fun h => irrefl (r := s) (f a) (by simpa [e] using H _ _ h)
    · exact fun h => irrefl (r := s) (f b) (by simpa [e] using H _ _ h)

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ (c ⊓ (a ⊓ c)))) =
    (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))

Tactic:
inf_comm c (a ⊓ c),

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ (a ⊓ c ⊓ c))) =
    (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.zero
n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
⊢ ∃ a b, a * (p + 1) + b * 0 = n

pp: case succ.succ
n p q : ℕ
dvd : (p + 1).gcd (q + 1) ∣ n
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n

Tactic:
· have ⟨a, eq⟩ := p.gcd_zero_right ▸ dvd
    exact ⟨a, 0, by simpa [mul_comm, eq_comm] using eq⟩

Goal state after:
case succ.succ
n p q : ℕ
dvd : (p + 1).gcd (q + 1) ∣ n
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ a ≠ a * c → 1 < c

Tactic:
rw [one_lt_iff_ne_one]
    apply mt
    rintro rfl
    rw [mul_one]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
rcases le_total a b with hb | hb
  · simp [hb, le_mul_right]
  · rcases le_total a c with hc | hc
    · simp [hc, le_mul_left]
    · simp [hb, hc]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝ : m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : n = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : b = 0
⊢ a = 0 ^ n ∧ b = 0 ^ m

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : a = 0
this : b ^ n = a ^ m
⊢ a = 0 ^ n ∧ b = 0 ^ m

Tactic:
simp_all

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

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

Tactic:
by
  simp [add_comm, add_neg_cancel_of_ne_top ha]

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

Goal state before:
pp: case isTrue
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
h✝ : x✝ = 0
⊢ recZeroCoe 0 Units.val 0 = x✝

Tactic:
simp_all

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

Goal state before:
pp: case isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
h✝ : ¬x✝ = 0
⊢ recZeroCoe 0 Units.val ↑(Units.mk0 x✝ h✝) = x✝

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h1 : c ≤ a
h2 : c ≤ b
⊢ a - c = b - c ↔ a = b

Tactic:
le_antisymm_iff,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h1 : c ≤ a
h2 : c ≤ b
⊢ a - c ≤ b - c ∧ b - c ≤ a - c ↔ a ≤ b ∧ b ≤ a
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a = b - c → a + c = b

Tactic:
rintro rfl
    exact tsub_add_cancel_of_le h

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
⊢ c < b

Tactic:
conv_lhs at h => rw [← tsub_add_cancel_of_le hca]
  exact lt_of_add_lt_add_left (hb.lt_add_of_tsub_lt_right h)

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
⊢ a - b = a - c ↔ b = c

Tactic:
le_antisymm_iff,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
⊢ a - b ≤ a - c ∧ a - c ≤ a - b ↔ b ≤ c ∧ c ≤ b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
⊢ a - b ≤ a - c ∧ b ≤ c ↔ b ≤ c ∧ c ≤ b

Tactic:
ha.tsub_le_tsub_iff_left hc hca,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
⊢ c ≤ b ∧ b ≤ c ↔ b ≤ c ∧ c ≤ b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
w x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
yw : y < w
⊢ x + y < z + w

Tactic:
apply (WithTop.add_lt_add_left xz.ne_top yw).trans_le
  cases w
  · simp
  · exact (WithTop.add_lt_add_right coe_ne_top xz).le

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddMonoid α
a : WithTop α
⊢ 0 • a = 0

Tactic:
HSMul.hSMul,

Goal state after:
α : Type u
β : Type v
inst✝ : AddMonoid α
a : WithTop α
⊢ SMul.smul 0 a = 0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddMonoid α
n : ℕ
a : WithTop α
⊢ (n + 1) • a = n • a + a

Tactic:
HSMul.hSMul,

Goal state after:
α : Type u
β : Type v
inst✝ : AddMonoid α
n : ℕ
a : WithTop α
⊢ SMul.smul (n + 1) a = SMul.smul n a + a
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hn : 0 < n
⊢ 0 ≤ x + ↑n

Tactic:
have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
    rwa [neg_add_cancel] at this

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
a : α
inst✝ : LE α
x : α
h : ↑x ≤ ⊥
⊢ unbotD a ↑x ≤ unbotD a ⊥

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
a : α
inst✝ : LE α
x a✝ : α
h : ↑x ≤ ↑a✝
⊢ unbotD a ↑x ≤ unbotD a ↑a✝

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LE α
y : WithBot α
x : α
h : ↑x ≤ y
⊢ unbotD a ↑x ≤ unbotD a y

Tactic:
cases y <;> simp_all

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
⊢ Nontrivial αˣ

pp: case refine_2
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
⊢ DenselyOrdered αˣ

pp: case refine_3
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
⊢ DenselyOrdered α

Tactic:
· obtain ⟨x, hx, hx'⟩ := exists_between (zero_lt_one' α)
    exact ⟨Units.mk0 x hx.ne', 1, by simpa [Units.ext_iff] using hx'.ne⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
⊢ DenselyOrdered αˣ

case refine_3
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
⊢ DenselyOrdered α
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case refine_2
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₙ ≤ Nat.find hₘ + n

Tactic:
← Nat.sub_le_iff_le_add

Goal state after:
case refine_2
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₙ - n ≤ Nat.find hₘ
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst✝ : DenselyOrdered α
⊢ Nontrivial αˣ

Tactic:
by
  have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
  tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst✝ : DenselyOrdered α
⊢ DenselyOrdered αˣ

Tactic:
by
  have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
  tauto

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : Nontrivial αˣ
⊢ DenselyOrdered αˣ ↔ DenselyOrdered α

Tactic:
by
  have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
  tauto

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : Nonempty α
inst✝ : NoTopOrder α
x : WithBot (WithTop α)
⊢ x = ⊤ → ∀ (a : α), ↑↑a ≤ x

Tactic:
simp_all

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : LE α
a x : α
h : ↑x ≤ 0
⊢ unzeroD a ↑x ≤ unzeroD a 0

Tactic:
simp_all

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

Goal state before:
pp: case coe
α : Type u_1
inst✝ : LE α
a x a✝ : α
h : ↑x ≤ ↑a✝
⊢ unzeroD a ↑x ≤ unzeroD a ↑a✝

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
y : WithZero α
a x : α
h : ↑x ≤ y
⊢ unzeroD a ↑x ≤ unzeroD a y

Tactic:
cases y <;> simp_all

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n

Tactic:
le_antisymm_iff,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ n ∧ n ≤ ⌊a⌋₊ ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n

Tactic:
le_antisymm_iff,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ ≤ n ∧ n ≤ ⌊a⌋₊ ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ ≤ n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n

Tactic:
le_antisymm_iff,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ ≤ n ∧ n ≤ ⌈a⌉₊ ↔ n ≤ ⌈a⌉₊ ∧ ⌈a⌉₊ ≤ n
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝ : LE α
⊢ WithBot.ofDual ⊥ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ ⊥

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ⊥ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ ⊥

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ WithBot.ofDual ⊥ ↔ ⊥ ≤ ↑a✝

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝¹ ≤ WithBot.ofDual ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹

Tactic:
simp_all

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
a : α
b : β
⊢ f a ∣ b ↔ a ∣ (↑f).symm b

Tactic:
obtain ⟨c, rfl⟩ : ∃ c, f c = b := EquivLike.surjective f b
  simp [map_dvd_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
hs : s ⊆ s'
ht : t ⊆ t'
a : α
ha : a ∈ s
b : β
hb : b ∈ t
⊢ f a b ∈ image2 f s' t'

Tactic:
exact mem_image2_of_mem (hs ha) (ht hb)

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : ℤˣ
h✝ : a = 1
⊢ |↑↑a| = 1

Tactic:
simp_all

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : ℤˣ
h✝ : a = -1
⊢ |↑↑a| = 1

Tactic:
simp_all

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

Goal state before:
pp: 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 ^ (n + 1 + 1) - a * b ^ (n + 1) + (a * b ^ (n + 1) - b ^ (n + 1 + 1))

Tactic:
sub_add_sub_cancel

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 ^ (n + 1 + 1) - b ^ (n + 1 + 1)
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: case refine_2
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ upperBounds s

Tactic:
exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (Icc a b).Subsingleton ↔ b ≤ a

Tactic:
refine ⟨fun h ↦ ?_, subsingleton_Icc_of_ge⟩

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a b : α
h : (Icc a b).Subsingleton
⊢ b ≤ a
Module: Mathlib.Tactic.Abel

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

Tactic:
simp [h₁.symm, h₂.symm, term, add_nsmul, add_assoc, add_left_comm]

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

Goal state before:
pp: case eq
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * db + nb * da = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑db * ⅟↑da = ↑nc * ⅟↑dc

Tactic:
h₂,

Goal state after:
case eq
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * db + nb * da = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑db * ⅟↑da = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc