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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a ^ n * a = a * a ^ n

Tactic:
← pow_succ,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a ^ (n + 1) = a * a ^ n
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m + (n + 1)) = a ^ (m + n) * a

Tactic:
← pow_succ,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m + (n + 1)) = a ^ (m + n + 1)
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ f^[m + n.succ] = f^[m] ∘ f^[n.succ]

Tactic:
rw [Nat.add_succ, iterate_succ, iterate_succ, iterate_add m n]; rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (∃ fab, p fab) ↔ ∃ fa fb, p fun t ↦ rec fa fb t

Tactic:
rw [← not_forall_not, forall_sum]

Goal state after:
α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), ¬p fun t ↦ rec fa fb t) ↔
    ∃ fa fb, p fun t ↦ rec fa fb t
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ g⁻¹ • g • a = a

Tactic:
smul_smul,

Goal state after:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ (g⁻¹ * g) • a = a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ g • g⁻¹ • a = a

Tactic:
smul_smul,

Goal state after:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ (g * g⁻¹) • a = a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g⁻¹ • a = b
⊢ a = g • g⁻¹ • a

Tactic:
smul_inv_smul

Goal state after:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g⁻¹ • a = b
⊢ a = a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g⁻¹ • b
⊢ g • g⁻¹ • b = b

Tactic:
smul_inv_smul

Goal state after:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g⁻¹ • b
⊢ b = b
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ s • 1 • (r • 1) • x = s • r • 1 • x

Tactic:
one_smul,

Goal state after:
A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ s • (r • 1) • x = s • r • 1 • x
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j = i

Tactic:
by
  simp_rw [le_antisymm_iff, h j, and_true]
  exact ⟨fun a ↦ a (h j), fun a h' ↦ fun _ ↦ le_trans a (h h')⟩

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

Goal state before:
pp: n m : ℕ
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

Tactic:
by
  rcases le_or_gt m n with h | h
  · simp [h]
  · simp [dvd_sub_iff_left (le_of_lt h) (Nat.dvd_refl _), h.not_ge]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
h : Disjoint a b
x : α
h₁ : x ≤ a
h₂ : x ≤ b
⊢ x = ⊥

Tactic:
by simpa using h h₁ h₂

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x y → Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Tactic:
intro h
    refine ⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, ?_⟩ ⟨hy, ?_⟩).1,
      fun b hx hy ↦ (@h (⊥, b) ⟨?_, hx⟩ ⟨?_, hy⟩).2⟩
    all_goals exact bot_le

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

Goal state before:
pp: α : Type u
s : Set α
⊢ ¬Nonempty ↑s ↔ s = ∅

Tactic:
by
  rw [nonempty_subtype, not_exists, eq_empty_iff_forall_notMem]

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

Goal state before:
pp: α : Type u
a : α
s✝ t : Set α
inst✝ : Subsingleton α
s : Set α
⊢ Subsingleton ↑s

Tactic:
s.subsingleton_coe

Goal state after:
α : Type u
a : α
s✝ t : Set α
inst✝ : Subsingleton α
s : Set α
⊢ s.Subsingleton
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : DistribLattice β
lattice : Lattice α := e.lattice
⊢ DistribLattice α

Tactic:
apply e.injective.distribLattice <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⇨ c ↔ d ≤ a ⊓ b ⇨ c

Tactic:
simp_rw [le_himp_iff, inf_assoc]

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ map e.symm (map e x) = x

Tactic:
by
    convert! (congr_fun (EquivFunctor.map_trans' e e.symm) x).symm
    simp

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (b ⊔ a) \ a = b \ a

Tactic:
sup_sdiff_right_self

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b \ a = b \ a
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab // p ab }
a : α
b : β a
h : p ⟨a, b⟩
⊢ γ (↑default).fst (↑default).snd = γ a b

Tactic:
rw [← show ⟨⟨a, b⟩, h⟩ = uniq.default from uniq.uniq _]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
⊢ univ ×ˢ t = Prod.snd ⁻¹' t

Tactic:
simp [prod_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
⊢ s ×ˢ univ = Prod.fst ⁻¹' s

Tactic:
simp [prod_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
hs : (f ⁻¹' s).Subsingleton
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
⊢ f x = f y

Tactic:
exact congr_arg f (hs hx hy)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
f : α → β
g : β → γ
h : InjOn (g ∘ f) s
x✝¹ : α
hx : x✝¹ ∈ s
x✝ : α
hy : x✝ ∈ s
heq : f x✝¹ = f x✝
⊢ (g ∘ f) x✝¹ = (g ∘ f) x✝

Tactic:
by simp [heq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
⊢ ∀ (g₁ g₂ : α),
    ((⇑(Equiv.prodComm β γ) ∘ f) g₁).1 = ((⇑(Equiv.prodComm β γ) ∘ f) g₂).1 →
      ((⇑(Equiv.prodComm β γ) ∘ f) g₁).2 = ((⇑(Equiv.prodComm β γ) ∘ f) g₂).2

Tactic:
by simp [hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
⊢ SurjOn f (f ⁻¹' t) t

Tactic:
intro u

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
u : β
⊢ u ∈ t → u ∈ f '' f ⁻¹' t
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
⊢ BijOn f s t

Tactic:
by
    have := congrArg (· \ {f a}) (image_insert_eq ▸ h.image_eq)
    simp only [mem_singleton_iff, insert_sdiff_of_mem] at this
    rw [sdiff_singleton_eq_self hfa, sdiff_singleton_eq_self] at this
    · exact ⟨by simp [← this, mapsTo_iff_image_subset], h.injOn.mono (subset_insert ..),
        by simp [← this, surjOn_image]⟩
    simp only [mem_image, not_exists, not_and]
    intro x hx
    rw [h.injOn.eq_iff (by simp [hx]) (by simp)]
    exact ha ∘ (· ▸ hx)

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a ^ (n - 1) * a = a ^ n

Tactic:
← pow_succ,

Goal state after:
M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a ^ (n - 1 + 1) = a ^ n
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (Int.negSucc m * ↑n) = (a ^ (m + 1))⁻¹ ^ n

Tactic:
← inv_pow,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (Int.negSucc m * ↑n) = (a⁻¹ ^ (m + 1)) ^ n
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ ((a * b) ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * (b ^ (n + 1))⁻¹

Tactic:
← inv_pow,

Goal state after:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a * b)⁻¹ ^ (n + 1) = a⁻¹ ^ (n + 1) * b⁻¹ ^ (n + 1)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (↑n - 1) = a ^ n / a

Tactic:
simpa [div_eq_mul_inv] using zpow_sub a n 1

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a * b / a = b

Tactic:
mul_div_cancel_left

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ b = b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ (a * b / a)⁻¹ = b⁻¹

Tactic:
mul_div_cancel_left

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ b⁻¹ = b⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a * b / a * c = b * c

Tactic:
mul_div_cancel_left

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ b * c = b * c
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
simp only [noZeroDivisors_iff, or_iff_not_imp_right]
  exact ⟨fun h b hb a eq ↦ h eq hb, fun h a b eq hb ↦ h b hb a eq⟩

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 0 ^ (n + 1) = 0

Tactic:
rw [pow_succ, mul_zero]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a : M₀
n : ℕ
hn : n ≠ 0
ha : a ^ n ≠ 0
⊢ a ≠ 0

Tactic:
by rintro rfl; exact ha <| zero_pow hn

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
n : ℕ
inst✝ : Nontrivial M₀
⊢ 0 ^ n = 0 → n ≠ 0

Tactic:
by rintro h rfl; simp at h

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ ↑((k + 1) / 2 + (k + 1) / 2) = ↑(1 * ((k + 1) / 2) + (k + 1) / 2)

Tactic:
Nat.one_mul

Goal state after:
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ ↑((k + 1) / 2 + (k + 1) / 2) = ↑((k + 1) / 2 + (k + 1) / 2)
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
h1 : k.succ % 2 = 1
⊢ ↑((k + 1) / 2 + (k + 1) / 2) + 1 = ↑(1 * ((k + 1) / 2) + (k + 1) / 2 + 1)

Tactic:
Nat.one_mul

Goal state after:
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
h1 : k.succ % 2 = 1
⊢ ↑((k + 1) / 2 + (k + 1) / 2) + 1 = ↑((k + 1) / 2 + (k + 1) / 2 + 1)
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 = 2

Tactic:
by
  rw [← Nat.cast_one, ← Nat.cast_add]
  apply congrArg
  decide

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a⁻¹ * a = a

Tactic:
by_cases h : a = 0
  · rw [h, inv_zero, mul_zero]
  · rw [mul_inv_cancel₀ h, one_mul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
ι : Type u_12
inst✝ : DecidableEq ι
x : A
i j : ι
⊢ (if j = i then 1 • x else 0 • x) = single i x j

Tactic:
one_smul,

Goal state after:
M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
ι : Type u_12
inst✝ : DecidableEq ι
x : A
i j : ι
⊢ (if j = i then x else 0 • x) = single i x j
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
subst a
    simp only [false_or, not_true, Ne, hm, hn, false_and, or_false] at h
    rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x y : β
⊢ g • (x / y) = g • x / g • y

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, smul_mul', smul_inv₀']

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
⊢ f n = f (ofAdd 1) ^ toAdd n

Tactic:
rw [← powersHom_symm_apply, ← powersHom_apply, Equiv.apply_symm_apply]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
a b : α
x✝ : a ∣ᵣ b
c : α
hc : b = c * a
⊢ MulOpposite.op b = MulOpposite.op a * MulOpposite.op c

Tactic:
simp [hc]

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
h : IsUnit x
⊢ x⁻¹ʳ * x = 1

Tactic:
rcases h with ⟨u, rfl⟩
  rw [inverse_unit, Units.inv_mul]

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

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

Tactic:
by
  rw [div_mul_eq_mul_div, one_mul, div_mul_cancel_left₀ h, one_div]

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

Goal state before:
pp: case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ ↑n • b + 1 • b = n • b + 1 • b

Tactic:
one_smul,

Goal state after:
case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ ↑n • b + b = n • b + 1 • b
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
⊢ ↑n = 0 ∨ ↑n = 1

Tactic:
by
  obtain hn | hn := Nat.even_or_odd n
  · exact Or.inl <| natCast_eq_zero_of_even_of_two_eq_zero hn h
  · exact Or.inr <| natCast_eq_one_of_odd_of_two_eq_zero hn h

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a⁻¹ < a ↔ 1 < a

Tactic:
by simp [inv_lt_iff_one_lt_mul]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : c + b * c ≤ a + b
⊢ 1 - a ≤ (1 + b) * (1 - c)

Tactic:
rw [mul_one_sub, one_add_mul, sub_le_sub_iff, add_assoc, add_comm b]

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : c + b * c ≤ a + b
⊢ 1 + (c + b * c) ≤ 1 + (a + b)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ c⁻¹ * b ↔ c * a ≤ b

Tactic:
← mul_le_mul_iff_of_pos_left hc,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c * a ≤ c * (c⁻¹ * b) ↔ c * a ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b ≤ a ↔ b ≤ c * a

Tactic:
← mul_le_mul_iff_of_pos_left hc,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c * (c⁻¹ * b) ≤ c * a ↔ b ≤ c * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a c : G₀
hc : 0 ≤ c
hb : 0 ≤ 0
h : a ≤ 0 * c
⊢ 0⁻¹ * a ≤ c

Tactic:
simp [hc]

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

Goal state before:
pp: case inr.inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ 0 * b
ab : 0 ≤ 0 → b < 0
nab : 0 ≤ 0 → 0 < b
⊢ 0 * b < 0

pp: case inr.inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a * b < 0

Tactic:
· exact ((ab le_rfl).asymm (nab le_rfl)).elim

Goal state after:
case inr.inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a * b < 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a c : G₀
hc : 0 ≤ c
hb : 0 ≤ 0
h : a ≤ c * 0
⊢ a * 0⁻¹ ≤ c

Tactic:
simp [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✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 1 < a * b⁻¹ ↔ b < a

Tactic:
lt_mul_inv_iff₀ hb,

Goal state after:
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
⊢ 1 * b < a ↔ b < a
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
a : α
⊢ Acc s (f a) → Acc r a

Tactic:
generalize h : f a = b

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : f a = b
⊢ Acc s b → Acc r 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✝¹ : AddLeftReflectLT R
inst✝ : AddLeftStrictMono R
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
by
  rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff (R := R), neg_pos, neg_lt_zero]

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
a : α
⊢ Acc s (f a) → Acc r a

Tactic:
generalize h : f a = b

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
b : β
h : f a = b
⊢ Acc s b → Acc r a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b * c⁻¹ ↔ c * a < b

Tactic:
lt_mul_inv_iff₀ hc,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a * c < b ↔ c * a < b
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ |(a ^ n)⁻¹|ₘ = a⁻¹ ^ n

Tactic:
← inv_pow,

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ |a⁻¹ ^ n|ₘ = a⁻¹ ^ n
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 / c|ₘ = |a / b * (b / c)|ₘ

Tactic:
by rw [div_mul_div_cancel]

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case negSucc
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (2 * Int.negSucc k + 1) = -a ^ (2 * Int.negSucc k + 1)

Tactic:
| negSucc k =>

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

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

Tactic:
by
  rw [← sub_self_eq_zero_of_ne_top ha, sub_left_inj_of_ne_top ha]

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 : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b + (b - c) = a - c

Tactic:
convert! tsub_add_cancel_of_le (tsub_le_tsub_right hab c) using 2
  rw [tsub_tsub, add_tsub_cancel_of_le hcb]

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 : α
ha : AddLECancellable a
hc : AddLECancellable c
h₁ : a ≤ b
h₂ : c ≤ b
⊢ a ≤ b - c ↔ a + c ≤ b

Tactic:
hc.le_tsub_iff_right h₂

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h₁ : a ≤ b
h₂ : c ≤ b
⊢ a + c ≤ b ↔ a + c ≤ b
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
x✝ y : WithBot α
inst✝ : OrderTop α
x : WithBot α
⊢ x ≤ ⊤

Tactic:
cases x <;> simp [le_def]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
x : WithBot α
⊢ x ≤ x

Tactic:
cases x <;> simp [le_def]

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

Goal state before:
pp: case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
rw [findGreatest_of_not h]
      exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)

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
a b : R
h : a ≤ b
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
· rw [floor_of_nonpos ha]
    exact Nat.zero_le _

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
· exact le_floor ((floor_le ha).trans h)

Goal state after: