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

Goal state before:
pp: case succ.succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : n + 1 ≠ 0 → npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec (m + (n + 1 + 1)) a = npowRec m a * npowRec (n + 1 + 1) a

Tactic:
rw [← Nat.add_assoc, npowRec, ih n.succ_ne_zero]; simp only [npowRec, mul_assoc]

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

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

Tactic:
Nat.mul_comm,

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

Goal state before:
pp: case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ f x = g y

Tactic:
· rw [h, Subsingleton.elim x y]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
a i✝ : α
⊢ TransGen r a i✝ ≤ (TransGen p on f) a i✝

Tactic:
hab

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
a i✝ : α
hab : TransGen r a i✝
⊢ (TransGen p on f) a i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (TransGen p on f)
i✝¹ i✝ : α
⊢ TransGen r i✝¹ i✝ ≤ (TransGen p on f) i✝¹ i✝

Tactic:
hab

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (TransGen p on f)
i✝¹ i✝ : α
hab : TransGen r i✝¹ i✝
⊢ (TransGen p on f) i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (ReflTransGen p on f)
i✝¹ i✝ : α
⊢ ReflTransGen r i✝¹ i✝ ≤ (ReflTransGen p on f) i✝¹ i✝

Tactic:
hab

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (ReflTransGen p on f)
i✝¹ i✝ : α
hab : ReflTransGen r i✝¹ i✝
⊢ (ReflTransGen p on f) i✝¹ i✝
Module: Mathlib.Logic.Function.Iterate

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

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

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ FaithfulSMul G α ↔ ∀ (g : G), (∀ (a : α), g • a = a) → g = 1

Tactic:
refine ⟨fun h a ha ↦ h.eq_of_smul_eq_smul ?_, fun h ↦ ⟨fun {a₁ a₂} h' ↦ ?_⟩⟩

Goal state after:
case refine_1
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : FaithfulSMul G α
a : G
ha : ∀ (a_1 : α), a • a_1 = a_1
⊢ ∀ (a_1 : α), a • a_1 = 1 • a_1

case refine_2
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ a₁ = a₂
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul M α
inst✝⁶ : SMul Mᵐᵒᵖ α
inst✝⁵ : IsCentralScalar M α
inst✝⁴ : SMul M N
inst✝³ : SMul Mᵐᵒᵖ N
inst✝² : IsCentralScalar M N
inst✝¹ : SMul N α
inst✝ : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ (m • n) • a = m • n • a

Tactic:
rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m n, smul_assoc]

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Semigroup (f i)
⊢ ∀ (a b c : (i : I) → f i), a * b * c = a * (b * c)

Tactic:
by intros; ext; exact mul_assoc _ _ _

Goal state after:
Module: Mathlib.Order.Defs.PartialOrder

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
hab : a = b
⊢ a ≤ b

Tactic:
hab

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a = b
⊢ b ≤ b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compareOfLessAndEq a b = Ordering.gt ↔ b < a

Tactic:
compareOfLessAndEq_eq_gt le_antisymm le_total not_le

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b < a ↔ b < a
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LT α
inst✝ : DenselyOrdered α
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a < a₂ ∧ a₁ < a

Tactic:
simp_rw [and_comm]

Goal state after:
α : Type u_2
inst✝¹ : LT α
inst✝ : DenselyOrdered α
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ 0 ≤ a * b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
by
  grind [Int.mul_comm, Int.mul_nonneg_iff_of_pos_right]

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

Goal state before:
pp: a b c : ℕ
⊢ a / (b * c) = a / c / b

Tactic:
Nat.mul_comm,

Goal state after:
a b c : ℕ
⊢ a / (c * b) = a / c / b
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case a.inl
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a : ℕ
h : a + 1 < a + 1 + 1
⊢ P (a + 1) (a + 1)

pp: case a.inr
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h✝ : a + 1 < b + 1
h : a + 1 < b
⊢ P (a + 1) b

Tactic:
· exact ha _

Goal state after:
case a.inr
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h✝ : a + 1 < b + 1
h : a + 1 < b
⊢ P (a + 1) b
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictAntiOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ StrictAntiOn f s

Tactic:
strictAntiOn_toDual_comp_iff,

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMonoOn (f ∘ ⇑ofDual) s ↔ StrictAntiOn f s
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
x y : α
h₁ : x ⊓ y ≤ ⊥
h₂ : ⊤ ≤ x ⊔ y
⊢ Codisjoint x y

Tactic:
grind [codisjoint_iff_le_sup]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hab : a ⊔ b = b
hbc : b ⊔ c = c
⊢ a ⊔ b ⊔ c = b ⊔ c

Tactic:
hab

Goal state after:
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hab : a ⊔ b = b
hbc : b ⊔ c = c
⊢ b ⊔ c = b ⊔ c
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
c b a : α
hbc : b ⊓ c = c
hab : a ⊓ b = b
⊢ a ⊓ b ⊓ c = b ⊓ c

Tactic:
hab

Goal state after:
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
c b a : α
hbc : b ⊓ c = c
hab : a ⊓ b = b
⊢ b ⊓ c = b ⊓ c
Module: Mathlib.Data.Set.Disjoint

Goal state before:
pp: α : Type u
β : Sort u_1
γ : Sort u_2
x : β → α
y : γ → α
⊢ Disjoint (range x) (range y) ↔ ∀ (i : β) (j : γ), x i ≠ y j

Tactic:
simp [Set.disjoint_iff_forall_ne]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊔ y) = f x ⊔ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ f x ⊔ f y = f y

Tactic:
by rw [← h _ hx _ hy, sup_eq_right.2 hxy]

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

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

Tactic:
sdiff_sup_self,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ b ⊔ (a ⊔ c)
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ∆ b = a ⊓ bᶜ ⊔ b ⊓ aᶜ

Tactic:
simp only [(· ∆ ·), sdiff_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ ⟨x, hx⟩ ∈ range (Subtype.map f h) ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' f '' {x | p x}

Tactic:
mem_preimage,

Goal state after:
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ ⟨x, hx⟩ ∈ range (Subtype.map f h) ↔ x ∈ f '' {x | p x}
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝¹ : Subsingleton β
inst✝ : Nonempty β
⊢ SurjOn f s univ ↔ s.Nonempty

Tactic:
by
  cases nonempty_unique β; simp [univ_unique, Subsingleton.elim (f _) default, Set.Nonempty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
⊢ f x ∈ f' ⁻¹' s₁

Tactic:
mem_preimage,

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
⊢ f' (f x) ∈ s₁
Module: Mathlib.Data.Int.Init

Goal state before:
pp: motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ zero ≍
    match 0 with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n

Tactic:
← cast_eq_iff_heq

Goal state after:
motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ cast ?m.44 zero =
    match 0 with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n

motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ motive b = (fun x ↦ motive x) (b + 0)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
y : α
hy : y ∈ s
⊢ f y ∈ g ⁻¹' s

Tactic:
mem_preimage,

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
y : α
hy : y ∈ s
⊢ g (f y) ∈ s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
⊢ f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s

Tactic:
mem_preimage,

Goal state after:
case inl
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
⊢ invFun f (f a) ∈ s ↔ f a ∈ f '' s
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ ∃ b, a * b = 1

Tactic:
rcases h with ⟨⟨a, b, hab, _⟩, rfl⟩
  exact ⟨b, hab⟩

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
⊢ IsUnit a → a⁻¹ * a = 1

Tactic:
by
  rintro ⟨u, rfl⟩
  rw [← Units.val_inv_eq_inv_val, Units.inv_mul]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ b / (a * b) = a⁻¹

Tactic:
rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a = b / c ↔ a * c = b

Tactic:
rw [div_eq_mul_inv, h.eq_mul_inv_iff_mul_eq]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b : α
h : IsUnit b
⊢ b / (a * b) = 1 / a

Tactic:
rw [h.div_mul_cancel_right, one_div]

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
⊢ ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y

Tactic:
by
  induction n with
  | zero => intro y; rw [pow_zero, pow_zero, one_mul, one_mul]
  | succ n hn => intro y; rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]

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

Goal state before:
pp: M₀✝ : Type u_1
G₀ : Type u_2
a b c : M₀✝
inst✝² : MulZeroOneClass M₀✝
M₀ : Type u_3
inst✝¹ : MonoidWithZero M₀
inst✝ : IsRightCancelMulZero M₀
a✝ b✝ : M₀
h : a✝ * b✝ = 1
⊢ b✝ * a✝ = 1

Tactic:
by
    cases subsingleton_or_nontrivial M₀
    · exact Subsingleton.elim _ _
    exact (IsRightCancelMulZero.mul_right_cancel_of_ne_zero
      (right_ne_zero_of_mul_eq_one h)).mul_eq_one_symm h

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

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

Tactic:
simp [← one_add_one_eq_two, ← Nat.cast_one, ← three_add_one_eq_four,
    ← two_add_one_eq_three, add_assoc]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
zero_eq_one : 0 = 1
⊢ 1 • x = 0

Tactic:
← zero_eq_one,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
zero_eq_one : 0 = 1
⊢ 0 • x = 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
⊢ SMul.smul (↑z.succ) a = SMul.smul (↑z) a + a

Tactic:
SMul.smul

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
⊢ ↑↑z.succ • a = ↑↑z • a + a
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f x * -f y = -(f x * f y)

Tactic:
by rw [← neg, ← mul, mul_neg, neg, mul]

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

Goal state before:
pp: α : Type u_4
inst✝ : Semiring α
⊢ (Set.range fun x ↦ 2 * x + 1) = {a | Odd a}

Tactic:
by ext x; simp [Odd, eq_comm]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
m n : ℕ
h : Even m ↔ Even n
⊢ (-1) ^ m = (-1) ^ n

Tactic:
simp [h, neg_one_pow_eq_ite]

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

Goal state after:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - (b + c) = a - c - b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab✝ : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
hab : a < b
⊢ a * c < b * d

Tactic:
exact (mul_le_mul_of_nonneg_left hcd a0.le).trans_lt (mul_lt_mul_of_pos_right hab d0)

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ d ≤ c

Tactic:
hab

Goal state after:
case refine_2
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ b * c
⊢ d ≤ c

case ha
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ 0 ≤ c
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ f ⊤ ≤ f (a ⊔ b)

Tactic:
exact f.monotone ha.top_le

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * a ^ 2 ≤ b ^ n * (b * a)

Tactic:
hab

Goal state after:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * (b * a) ≤ b ^ n * (b * a)
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inr.inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : 1 < a * b
⊢ b ≤ 1

Tactic:
rw [mabs_of_one_lt ab, mul_left_inj] at h

Goal state after:
case inr.inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a = a⁻¹
ab : 1 < a * b
⊢ b ≤ 1
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rla : IsLeftRegular a
⊢ IsLeftRegular (a ^ n)

Tactic:
simp only [IsLeftRegular, ← mul_left_iterate, rla.iterate n]

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

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

Tactic:
SMul.smul

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

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

Tactic:
SMul.smul

Goal state after:
α : Type u
β : Type v
inst✝ : AddMonoid α
n : ℕ
a : WithTop α
⊢ (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
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
y : WithBot α
a b : α
hy : ↑b ≤ y
⊢ b ≤ unbotD a y

Tactic:
by
  rwa [le_unbotD_iff]
  exact ne_bot_of_le_ne_bot (by simp) hy

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ x.log < a ↔ x < exp a

Tactic:
by
  rw [← toAdd_unzero_eq_log hx, ← lt_ofAdd_iff hx, exp]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b

Tactic:
hab

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
hab : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ c * (⅟c * a) = c * b ↔ a = c * b

Tactic:
mul_invOf_cancel_left

Goal state after:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a = c * b ↔ a = c * b
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
⊢ a < b → ∃ a_2, a < a_2 ∧ a_2 < b

Tactic:
hab

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
hab : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
Module: Mathlib.Order.WithBot

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

Tactic:
simp_rw [and_comm]

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
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
⊢ a < b → (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b

Tactic:
hab

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a ≤ b → f₂ a ≤ f₂ b

Tactic:
hab

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
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
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a < b → f₂ a < f₂ b

Tactic:
hab

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
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 → x ≤ a
b : α
hb : b ∈ s
⊢ a < b → f a < f b

Tactic:
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 : α
hb : b ∈ s
⊢ b < a → f b < f a

Tactic:
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 : α
hb : b ∈ s
⊢ a < b → f b < f a

Tactic:
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 : α
hb : b ∈ s
⊢ b < a → f a < f b

Tactic:
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