mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: 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
⊢ μ a b ≤ μ a c

Tactic:
rcases bc.eq_or_lt with (rfl | bc)

Goal state after:
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

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.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b - (a + c) ≤ b - c

Tactic:
by
  grw [tsub_le_iff_left, add_assoc, ← le_add_tsub]

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:
by rw [div_le_iff_le_mul, mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝³ : LE α
inst✝² : MulOneClass α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a * b ≤ a ↔ b ≤ 1

Tactic:
ha.mul_le_iff_le_one_right

Goal state after:
α : Type u_1
inst✝³ : LE α
inst✝² : MulOneClass α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ b ≤ 1 ↔ b ≤ 1
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
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

Tactic:
exact hab.false.elim

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a b : M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosMono M₀
hab : a < b
ha : 0 ≤ a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ (n + 2) < b ^ (n + 2)

Tactic:
simpa only [pow_succ] using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
      (pow_le_pow_left₀ ha hab.le _) hab ha (pow_succ_pos (ha.trans_lt hab) _)

Goal state after:
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : α ↪ γ
⊢ (fun f ↦ Embedding.congr h.symm h'.symm f) ((fun f ↦ Embedding.congr h h' f) x) = x

Tactic:
ext
    simp

Goal state after:
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : β ↪ δ
⊢ (fun f ↦ Embedding.congr h h' f) ((fun f ↦ Embedding.congr h.symm h'.symm f) x) = x

Tactic:
ext
    simp

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₀
hc : 0 < c
⊢ b / c ≤ a ↔ b ≤ a * c

Tactic:
rw [div_eq_mul_inv, mul_inv_le_iff₀ 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 b : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hb : b ≤ 0
⊢ a / b ≤ 0

Tactic:
by
  rw [div_eq_mul_inv]; exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
⊢ r = ⇑f ⁻¹'o s

Tactic:
ext a b
  exact f.map_rel_iff.symm

Goal state after:
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✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 ↦ x1 < x2) ↪r fun x1 x2 ↦ x1 < x2
⊢ ∀ {a b : α}, f.toEmbedding a ≤ f.toEmbedding b ↔ a ≤ b

Tactic:
simp [le_iff_lt_or_eq, f.map_rel_iff, f.injective.eq_iff]

Goal state after:
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 c : G
⊢ |a / b|ₘ ≤ c ↔ a / b ≤ c ∧ b / a ≤ c

Tactic:
mabs_le,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ c⁻¹ ≤ a / b ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
Module: Mathlib.Data.Nat.Cast.NeZero

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 1 ≤ n

Tactic:
by have := NeZero.ne n; lia

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

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

Tactic:
cases n

Goal state after:
case zero
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ 0 < ↑0 ↔ 0 < 0

case succ
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n✝ : ℕ
⊢ 0 < ↑(n✝ + 1) ↔ 0 < n✝ + 1
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑n < ↑n

Tactic:
q.pred_succ

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑n < ↑n
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
⊢ (∃ c, a = c ^ n ∧ b = c ^ m) → a ^ m = b ^ n

Tactic:
rintro ⟨c, rfl, rfl⟩

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
m n : ℕ
hmn : m.Coprime n
c : α
hab : Commute (c ^ n) (c ^ m)
⊢ (c ^ n) ^ m = (c ^ m) ^ n
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝ : Group α
γ : (WithZero α)ˣ
⊢ ↑(unitsWithZeroEquiv γ) = ↑γ

Tactic:
by
  simp only [WithZero.unitsWithZeroEquiv, MulEquiv.coe_mk, Equiv.coe_fn_mk, WithZero.coe_unzero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ (if n + 1 = 0 then 0 else ↑↑(n + 1)) = (if n = 0 then 0 else ↑↑n) + 1

Tactic:
cases n

Goal state after:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddMonoidWithOne α
⊢ (if 0 + 1 = 0 then 0 else ↑↑(0 + 1)) = (if 0 = 0 then 0 else ↑↑0) + 1

case succ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddMonoidWithOne α
n✝ : ℕ
⊢ (if n✝ + 1 + 1 = 0 then 0 else ↑↑(n✝ + 1 + 1)) = (if n✝ + 1 = 0 then 0 else ↑↑(n✝ + 1)) + 1
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G : Type u_5
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
n : ℤ
⊢ (x ^ n).log = n • x.log

Tactic:
cases n

Goal state after:
case ofNat
G : Type u_5
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
a✝ : ℕ
⊢ (x ^ Int.ofNat a✝).log = Int.ofNat a✝ • x.log

case negSucc
G : Type u_5
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
a✝ : ℕ
⊢ (x ^ Int.negSucc a✝).log = Int.negSucc a✝ • x.log
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
β : Type v
inst✝ : AddMonoid α
n : ℕ
⊢ (match ⊤, n + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ⊤, n with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ⊤

Tactic:
cases n

Goal state after:
case top.zero
α : Type u
β : Type v
inst✝ : AddMonoid α
⊢ (match ⊤, 0 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ⊤, 0 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ⊤

case top.succ
α : Type u
β : Type v
inst✝ : AddMonoid α
n✝ : ℕ
⊢ (match ⊤, n✝ + 1 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ⊤, n✝ + 1 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe
α : Type u
β : Type v
inst✝ : AddMonoid α
n : ℕ
a✝ : α
⊢ (match ↑a✝, n + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ↑a✝, n with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ↑a✝

Tactic:
cases n

Goal state after:
case coe.zero
α : Type u
β : Type v
inst✝ : AddMonoid α
a✝ : α
⊢ (match ↑a✝, 0 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ↑a✝, 0 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ↑a✝

case coe.succ
α : Type u
β : Type v
inst✝ : AddMonoid α
a✝ : α
n✝ : ℕ
⊢ (match ↑a✝, n✝ + 1 + 1 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match ↑a✝, n✝ + 1 with
      | Option.some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      ↑a✝
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
n : ℕ
hn : n < Nat.find h₂ + 1
⊢ ¬p n

Tactic:
cases n

Goal state after:
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
hn : 0 < Nat.find h₂ + 1
⊢ ¬p 0

case succ
p : ℕ → Prop
inst✝ : DecidablePred p
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
n✝ : ℕ
hn : n✝ + 1 < Nat.find h₂ + 1
⊢ ¬p (n✝ + 1)
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case step
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
⊢ findGreatest P m ≤ findGreatest P m✝.succ

Tactic:
| step hmk ih =>

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
ι : Sort u_3
κ : Sort u_4
r : α → α → Prop
f : ι → κ
hf : Surjective f
g : κ → α
⊢ Directed r (g ∘ f) ↔ Directed r g

Tactic:
by simp [Directed, hf.forall, hf.exists]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
han : a ≤ ↑n
⊢ ⌈a⌉₊ ≤ n

Tactic:
Nat.ceil_le

Goal state after:
case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
han : a ≤ ↑n
⊢ a ≤ ↑n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
⊢ Subsingleton (FloorSemiring R)

Tactic:
by
  refine ⟨fun H₁ H₂ => ?_⟩
  have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil.l_unique H₂.gc_ceil) fun n => rfl
  have : H₁.floor = H₂.floor := by
    ext a
    rcases lt_or_ge a 0 with h | h
    · rw [H₁.floor_of_neg, H₂.floor_of_neg] <;> exact h
    · refine eq_of_forall_le_iff fun n => ?_
      rw [H₁.gc_floor, H₂.gc_floor] <;> exact h
  cases H₁
  cases H₂
  congr

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual x

Tactic:
cases x <;> cases y <;> simp [le_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual x

Tactic:
cases x <;> cases y <;> simp [le_toDual]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = ⅟a * a + ⅟b * a + (⅟a * b + ⅟b * b) ↔ 1 = 1 + ⅟b * a + (1 + ⅟a * b)

Tactic:
rw [invOf_mul_self, invOf_mul_self, add_comm _ 1]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
inverse_invertible,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ ⅟a + ⅟b = ⅟a * (a + b) * ⅟b
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
· have hb := h.not.mp ha
    simp [inverse_non_unit, ha, hb]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
inverse_invertible,

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ ⅟a - ⅟b = ⅟a * (b - a) * ⅟b
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
· have hb := h.not.mp ha
    simp [inverse_non_unit, ha, hb]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ 2 ^ (n + (n - 1)) * (a ^ (2 * n) + b ^ (2 * n)) = 2 ^ (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))

Tactic:
cases n

Goal state after:
case zero
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ 2 ^ (0 + (0 - 1)) * (a ^ (2 * 0) + b ^ (2 * 0)) = 2 ^ (2 * 0 - 1) * (a ^ (2 * 0) + b ^ (2 * 0))

case succ
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n✝ : ℕ
⊢ 2 ^ (n✝ + 1 + (n✝ + 1 - 1)) * (a ^ (2 * (n✝ + 1)) + b ^ (2 * (n✝ + 1))) =
    2 ^ (2 * (n✝ + 1) - 1) * (a ^ (2 * (n✝ + 1)) + b ^ (2 * (n✝ + 1)))
Module: Mathlib.Algebra.Order.Ring.Abs

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

Tactic:
obtain ⟨m, h⟩ := Int.eq_ofNat_of_zero_le (neg_nonneg.2 n0)
    rw [← mabs_inv, ← zpow_neg, ← abs_neg, h, zpow_natCast, Nat.abs_cast, zpow_natCast]
    exact mabs_pow m _

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| = |b| ↔ a * a = b * b

Tactic:
by
  rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
  exact (mul_self_inj (abs_nonneg a) (abs_nonneg b)).symm

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

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

Tactic:
classical
    refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩
    · suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
      exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
    · exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
    · exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
c : ℕ
⊢ smul c 0 = 0

Tactic:
by
  simp [smul, nsmul_zero]

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

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

Tactic:
by
  rwa [lt_div_iff₀' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)]

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

Goal state before:
pp: x y : ℕ
⊢ x.ble y = false ↔ y < x

Tactic:
← Nat.not_le,

Goal state after:
x y : ℕ
⊢ x.ble y = false ↔ ¬x ≤ y
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:
by
  simpa [one_div] using inv_le_inv_of_neg ha hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (take l₁.length l) (take l₁.length (l₁ ++ l₂))
⊢ Forall₂ R (take l₁.length l) l₁

Tactic:
take_left

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (take l₁.length l) l₁
⊢ Forall₂ R (take l₁.length l) l₁
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ SublistForall₂ R l₁ (map f l₂) ↔ SublistForall₂ (fun a c ↦ R a (f c)) l₁ l₂

Tactic:
simp only [sublistForall₂_iff]
  constructor
  · rintro ⟨l1, h1, h2⟩
    obtain ⟨l', hl1, rfl⟩ := sublist_map_iff.mp h2
    use l'
    simpa [hl1] using h1
  · rintro ⟨l1, h1, h2⟩
    use l1.map f
    simp [h1, h2.map]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
by_cases hab : a = b
  · exact Or.inl hab
  · exact ((List.mem_cons.1 h).elim Or.inl (fun h => Or.inr ⟨hab, h⟩))

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

Goal state before:
pp: α : Type u
m : ℕ
a : α
⊢ (replicate (m + 1) a).getLast ⋯ = a

Tactic:
simp only [replicate_succ']

Goal state after:
α : Type u
m : ℕ
a : α
⊢ (replicate m a ++ [a]).getLast ⋯ = a
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Semiring M
x₁ x₂ X₁ X₂ Y y a : M
h₁ : x₁ = a * X₁
h₂ : x₂ = a * X₂
H_atom : X₁ + X₂ = Y
hy : a * Y = y
⊢ x₁ + x₂ = y

Tactic:
subst h₁ h₂ H_atom hy

Goal state after:
M : Type u_1
inst✝ : Semiring M
X₁ X₂ a : M
⊢ a * X₁ + a * X₂ = a * (X₁ + X₂)
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Ring M
x₁ x₂ X₁ X₂ Y y a : M
h₁ : x₁ = a * X₁
h₂ : x₂ = a * X₂
H_atom : X₁ - X₂ = Y
hy : a * Y = y
⊢ x₁ - x₂ = y

Tactic:
subst h₁ h₂ H_atom hy

Goal state after:
M : Type u_1
inst✝ : Ring M
X₁ X₂ a : M
⊢ a * X₁ - a * X₂ = a * (X₁ - X₂)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: n₁ d₁ n₂ d₂ : ℤ
⊢ n₁ /. d₁ * (n₂ /. d₂)⁻¹ = n₁ * d₂ /. (d₁ * n₂)

Tactic:
inv_divInt,

Goal state after:
n₁ d₁ n₂ d₂ : ℤ
⊢ n₁ /. d₁ * (d₂ /. n₂) = n₁ * d₂ /. (d₁ * n₂)
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x * (d /. x)⁻¹ = n /. d

Tactic:
inv_divInt,

Goal state after:
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x * (x /. d) = n /. d
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ x /. n * (x /. d)⁻¹ = d /. n

Tactic:
inv_divInt,

Goal state after:
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ x /. n * (d /. x) = d /. n
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
H1 : IsRelPrime x z
H2 : x ∣ y * z
h : IsPrimal x
⊢ x ∣ y

Tactic:
obtain ⟨a, b, ha, hb, rfl⟩ := h H2
  exact (H1.of_mul_left_right.isUnit_of_dvd hb).mul_right_dvd.mpr ha

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
⊢ ↑b = ↑d * ↑k

Tactic:
rw [ke, Int.cast_mul, Int.cast_natCast]

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

Goal state before:
pp: b c : ℤ
⊢ ↑c * (↑b / ↑b) = ↑c * ↑b / ↑b

Tactic:
mul_div_assoc

Goal state after:
b c : ℤ
⊢ ↑c * (↑b / ↑b) = ↑c * (↑b / ↑b)
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c : ℕ
h1 : a.pow b = c
⊢ (Int.ofNat a).pow b = Int.ofNat c

Tactic:
by simp [← h1]

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

Goal state before:
pp: n : ℕ
⊢ n ∈ {0} ∪ range succ ↔ n ∈ univ

Tactic:
cases n

Goal state after:
case zero
⊢ 0 ∈ {0} ∪ range succ ↔ 0 ∈ univ

case succ
n✝ : ℕ
⊢ n✝ + 1 ∈ {0} ∪ range succ ↔ n✝ + 1 ∈ univ
Module: Mathlib.Order.CompleteLattice.Lemmas

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

Tactic:
· 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
s : Set α
⊢ ⋃ x ∈ s, s = s

Tactic:
biUnion_self

Goal state after:
α : Type u_1
s : Set α
⊢ s = s
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ (⋂ i, f i).Nonempty ↔ ∃ x, ∀ (i : ι), x ∈ f i

Tactic:
simp [nonempty_iff_ne_empty, iInter_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
⊢ (⋃ y, range fun x ↦ ↑(f x y)) = ⋃ x, C x

Tactic:
ext x; rw [mem_iUnion, mem_iUnion]; constructor
  · rintro ⟨y, i, rfl⟩
    exact ⟨i, (f i y).2⟩
  · rintro ⟨i, hx⟩
    obtain ⟨y, hy⟩ := hf i ⟨x, hx⟩
    exact ⟨y, i, congr_arg Subtype.val hy⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
hb' : b' ≤ f a
x : α
hx : x ∈ Icc a b
⊢ b' ≤ f x

Tactic:
exact hb'.trans <| h' (left_mem_Icc.mpr hab) hx hx.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]

Tactic:
rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf] <;>
    apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]

Tactic:
rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf] <;>
    apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ (⇑e '' s).OrdConnected

Tactic:
by
  erw [(e : α ≃o β).image_eq_preimage_symm]
  apply ordConnected_preimage (e : α ≃o β).symm

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = 1 ↔ 1 ≤ a

Tactic:
by simp [leOnePart_eq_one']

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i j : ι
a b : M
ha : a ≠ 1
hb : b ≠ 1
⊢ Disjoint (mulSupport (mulSingle i a)) (mulSupport (mulSingle j b)) ↔ i ≠ j

Tactic:
rw [mulSupport_mulSingle_of_ne ha, mulSupport_mulSingle_of_ne hb, disjoint_singleton]

Goal state after: