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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
⊢ r a c

Tactic:
rcases trichotomous_of r b c with (h₃ | rfl | h₃)
  · exact _root_.trans h₁ h₃
  · exact h₁
  · exact absurd h₃ h₂

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

Goal state before:
pp: G : Type u_1
inst✝ : CommMagma G
a : G
⊢ IsLeftRegular a ↔ IsRegular a

Tactic:
by
  simp [isRegular_iff, IsLeftRegular, IsRightRegular, mul_comm]

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

Goal state before:
pp: G : Type u_1
inst✝ : CommMagma G
a : G
⊢ IsRightRegular a ↔ IsRegular a

Tactic:
by
  simp [isRegular_iff, IsLeftRegular, IsRightRegular, mul_comm]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, r = fun x1 x2 ↦ f x1 = x2

Tactic:
by
  simp [forall_existsUnique_iff, funext_iff]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ b = a ∨ TransGen r a b

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · cases h with
    | refl => exact Or.inl rfl
    | tail hac hcb => exact Or.inr (TransGen.tail' hac hcb)
  · rcases h with (rfl | h)
    · rfl
    · exact h.to_reflTransGen

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
⊢ f^[m + n] a = f^[n] a ↔ f^[n] (f^[m] a) = f^[n] a

Tactic:
rw [← iterate_add_apply, Nat.add_comm]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower N P Q
m : M
p : P
q : Q
⊢ (m • p) • q = m • p • q

Tactic:
by rw [← smul_one_smul N m, smul_assoc, smul_one_smul]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty β
⊢ LeftTotal R ↔ IsEmpty α

Tactic:
by
  simp only [LeftTotal, IsEmpty.exists_iff, isEmpty_iff]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ max a b = if a < b then b else a

Tactic:
rw [max_comm, max_def, ← ite_not]; simp only [not_le]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
⊢ ∀ (a b : BoundedOrder α), a = b

Tactic:
rintro ⟨⟩ ⟨⟩; congr <;> exact Subsingleton.elim _ _

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
⊢ cmp x y = cmp x' y'

Tactic:
← cmp_swap y',

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
⊢ cmp x y = (cmp y' x').swap
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hexists : ∃ M, P M
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
⊢ P ⊤

Tactic:
contrapose! hexists
  intro M
  induction M using WellFoundedGT.induction with
  | ind x IH =>
    by_cases hx : x = ⊤
    · exact hx ▸ hexists
    · intro hx'
      obtain ⟨M, hM, hM'⟩ := hind x hx hx'
      exact IH _ hM hM'

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

Goal state before:
pp: case refine_2
α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : MonotoneOn f {x | k ≤ x}
x y : ℕ
hle✝ : x ≤ y
hle : x + ?m.52 ≤ y + ?m.52
⊢ (fun n ↦ f (n + k)) x ≤ (fun n ↦ f (n + k)) y

pp: α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : MonotoneOn f {x | k ≤ x}
x y : ℕ
hle : x ≤ y
⊢ ℕ

Tactic:
exact h (Nat.le_add_left k x) (Nat.le_add_left k y) hle

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c x : α
⊢ a ⊔ b ⊔ c ≤ x ↔ a ⊔ (b ⊔ c) ≤ x

Tactic:
simp only [sup_le_iff]; rw [and_assoc]

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

Goal state before:
pp: case mp
α : Type u_1
a : α
n : ℕ
hn : n > 0
H : n ≤ 1
⊢ List.replicate n a = [a]

Tactic:
simp [show n = 1 by lia]

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ (a ⇨ b) ⊓ a ≤ b

Tactic:
← le_himp_iff

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⇨ b ≤ a ⇨ b
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
← le_himp_iff

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ (a ⇨ b) ⊓ a ≤ (b ⇨ c) ⇨ c
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y : α
⊢ x \ y ⊔ x ⊓ y = x

Tactic:
by rw [sup_comm, sup_inf_sdiff]

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

Goal state before:
pp: α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab // p ab }
a : α
b : β a
c : γ a b
h : p ⟨a, b⟩
⊢ (sigmaSigmaSubtype p h).symm c = ⟨⟨a, ⟨b, c⟩⟩, h⟩

Tactic:
rw [Equiv.symm_apply_eq]; simp

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by rw [symmDiff_eq_sup_sdiff_inf]

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁹ : Max α
inst✝⁸ : Min α
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ⊔ f aᶜ = f ⊤

Tactic:
rw [map_compl, sup_compl_eq_top, map_top]

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

Goal state before:
pp: case mp
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
⊢ a ∈ Set.image (⇑(swap i j)) s → a ∈ insert j s \ {i}

Tactic:
rintro ⟨a, ha, rfl⟩
      obtain rfl | ne := eq_or_ne a i
      · rw [swap_apply_left]; exact ⟨.inl rfl, (ne_of_mem_of_not_mem hi hj).symm⟩
      · rw [swap_apply_of_ne_of_ne ne (ne_of_mem_of_not_mem ha hj)]; exact ⟨.inr ha, ne⟩

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_eq

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
symmDiff_eq

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set β
f : α → β
⊢ (f ⁻¹' s).Nonempty ↔ (s ∩ range f).Nonempty

Tactic:
by
  simp [Set.Nonempty]

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

Goal state before:
pp: case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i

Tactic:
rw [h]
    simp

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

Goal state before:
pp: X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' pullbackDiagonal f ↔ ⟨(p₁, p₂), he⟩ ∈ pullbackDiagonal snd

Tactic:
pullbackDiagonal,

Goal state after:
X : Type u_2
Y : Sort u_3
Z : Type u_1
f : X → Y
g : Z → Y
p₁ p₂ : Pullback f g
he : (p₁, p₂).1.snd = (p₁, p₂).2.snd
⊢ ⟨(p₁, p₂), he⟩ ∈ map_fst ⁻¹' {p | p.fst = p.snd} ↔ ⟨(p₁, p₂), he⟩ ∈ {p | p.fst = p.snd}
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case pos
α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
i : α
ht : i ∈ t
hs : i ∈ s
⊢ s.piecewise f g i ∈ t' i

Tactic:
simp [hf i ht, hg i ht, hs]

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

Goal state before:
pp: case neg
α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
i : α
ht : i ∈ t
hs : ¬i ∈ s
⊢ s.piecewise f g i ∈ t' i

Tactic:
simp [hf i ht, hg i ht, hs]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Surjective (image f) ↔ Surjective f

Tactic:
refine ⟨fun h y => ?_, Surjective.image_surjective⟩

Goal state after:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
⊢ ∃ a, f a = y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : ¬a ∈ s
⊢ InjOn f (insert a s) ↔ InjOn f s ∧ ¬f a ∈ f '' s

Tactic:
by
  rw [← union_singleton, injOn_union (disjoint_singleton_right.2 has)]
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ (g₁.extendDomain f) ((g₂.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a

Tactic:
simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ (g₂.extendDomain f) ((g₁.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a

Tactic:
simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]

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

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

Tactic:
simp only [mul_left_comm, mul_comm]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * (b * c) = b * (c * a)

Tactic:
simp only [mul_left_comm, mul_comm]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ m = a ^ (m % n)

Tactic:
calc
    a ^ m = a ^ (m % n + n * (m / n)) := by rw [Nat.mod_add_div]
    _ = a ^ (m % n) := by simp [pow_add, pow_mul, ha]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a / b = 1
⊢ a * b⁻¹ = 1

Tactic:
rwa [← div_eq_mul_inv]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
u : αˣ
⊢ a * (↑u * ↑u⁻¹) = a

Tactic:
Units.mul_inv,

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
u : αˣ
⊢ a * 1 = a
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
this : IsUnit (a * (↑u * ↑u⁻¹))
⊢ IsUnit a

Tactic:
Units.mul_inv,

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
u : Mˣ
x✝ : IsUnit (a * ↑u)
v : Mˣ
hv : ↑v = a * ↑u
this : IsUnit (a * 1)
⊢ IsUnit a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case inr
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
⊢ ∃ b, a * b = 1

Tactic:
refine ⟨b, ?_⟩

Goal state after:
case inr
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
⊢ a * b = 1
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ⇑f
smul : ∀ (c : R) (x : M), f (c • x) = c • f x
x : M₂
⊢ 0 • x = 0

Tactic:
rcases hf x with ⟨x, rfl⟩
      rw [← f.map_zero, ← smul, zero_smul]

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

Goal state before:
pp: n : ℕ
⊢ ↑(↑n).toNat.sqrt = ↑n.sqrt

Tactic:
toNat_natCast

Goal state after:
n : ℕ
⊢ ↑n.sqrt = ↑n.sqrt
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ (b - x) * (b - x) - b * (b - x) + x * (b - x) = 0

Tactic:
sub_add,

Goal state after:
α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ (b - x) * (b - x) - (b * (b - x) - x * (b - x)) = 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit a⁻¹ʳ

Tactic:
rw [Ring.inverse_non_unit _ h]

Goal state after:
case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
| a / b = c / d

Tactic:
rw [← mul_left_inj' hb, div_mul_cancel₀ _ hb]

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
| a = c / d * b
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ b = b * (↑u * ↑u⁻¹)

Tactic:
Units.mul_inv,

Goal state after:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ b = b * 1
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: R : Type x
inst✝ : Semiring R
a : Rˣ
b : R
⊢ ↑a + b = ↑a + ↑a * ↑a⁻¹ * b

Tactic:
Units.mul_inv,

Goal state after:
R : Type x
inst✝ : Semiring R
a : Rˣ
b : R
⊢ ↑a + b = ↑a + 1 * b
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NoZeroDivisors R
a b : R
h : Commute a b
⊢ a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b

Tactic:
or_comm,

Goal state after:
R : Type u
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NoZeroDivisors R
a b : R
h : Commute a b
⊢ a - b = 0 ∨ a + b = 0 ↔ a = b ∨ a = -b
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ f b * f a ≤ f c * f a

Tactic:
exact mul_le_mul_of_nonneg_right (le.2 hbc) (by rwa [← zero, le])

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 / c ↔ a ≤ b

Tactic:
by
  simpa only [div_eq_mul_inv] using mul_le_mul_iff_right _

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

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
b c a : α
⊢ a * b⁻¹ < a * c⁻¹ ↔ c < b

Tactic:
← mul_lt_mul_iff_left a⁻¹,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
b c a : α
⊢ a⁻¹ * (a * b⁻¹) < a⁻¹ * (a * c⁻¹) ↔ c < b
Module: Mathlib.Algebra.Ring.GrindInstances

Goal state before:
pp: α : Type u_1
s : Semiring α
⊢ ∀ (a : α), a * 1 = a

Tactic:
simp [mul_one]

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₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
hn : 0 < n
⊢ a ^ n < 1

Tactic:
by
  simpa using zpow_right_strictAnti₀ ha₀ ha₁ hn

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₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
hn : n < 0
⊢ 1 < a ^ n

Tactic:
by
  simpa using zpow_right_strictAnti₀ ha₀ ha₁ hn

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 : G₀
⊢ 0 < a⁻¹ ↔ 0 < a

Tactic:
suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
  intro a ha
  apply lt_of_mul_lt_mul_right _ ha.le
  apply lt_of_mul_lt_mul_right _ ha.le
  simpa [ha.ne']

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 : G₀
hb : 0 < b
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
by rw [le_div_iff₀ hb, one_mul]

Goal state after:
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 ≤ c⁻¹ * b ↔ a * c ≤ b

Tactic:
by
  rw [le_inv_mul_iff₀ hc, mul_comm]

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 * a = b ^ n * a ^ 2

Tactic:
by rw [mul_assoc, sq]

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

Goal state before:
pp: case inr.inl.inl
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 : a * b ≤ 1
⊢ b⁻¹ = b

Tactic:
rwa [mabs_of_le_one ab, mul_inv_rev, mul_comm, mul_right_inj] at h

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 : G
⊢ a ≤ b ∨ a ≤ b⁻¹ ↔ b ≤ a⁻¹ ∨ a ≤ b

Tactic:
or_comm,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ a ≤ b⁻¹ ∨ a ≤ b ↔ b ≤ a⁻¹ ∨ a ≤ b
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 n : G
one_le_a : 1 ≤ a
a_le_n : a ≤ n
one_le_b : 1 ≤ b
b_le_n : b ≤ n
⊢ |a / b|ₘ ≤ n

Tactic:
rw [mabs_div_le_iff, div_le_iff_le_mul, div_le_iff_le_mul]

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_le_n : a ≤ n
one_le_b : 1 ≤ b
b_le_n : b ≤ n
⊢ a ≤ n * b ∧ b ≤ n * a
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ |a|ₘ ≤ |b|ₘ

Tactic:
by
  rw [mabs_of_le_one ha, mabs_of_le_one (hab.trans ha)]; exact inv_le_inv_iff.mpr hab

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

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' : ℤ
⊢ ∀ {t' : ℤ}, x.P y (a, s, t) → x.P y (b, s', t') → x.P y (a.xgcdAux s t b s' t')

Tactic:
t'

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' t' : ℤ
⊢ x.P y (a, s, t) → x.P y (b, s', t') → x.P y (a.xgcdAux s t b s' t')
Module: Mathlib.Algebra.Regular.Basic

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

Tactic:
rw [h]; exact isRegular_one.right

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ a, f a = b
b : β
⊢ ∃ a, (map' f) a = ↑b

Tactic:
· obtain ⟨a, ha⟩ := h b
    use a
    simp [ha]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
x y z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) x y) (swap (fun x1 x2 ↦ x1 + x2) x z)

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using fun _ ↦ by gcongr

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 c : α
inst✝ : AddLeftReflectLE α
d : α
h : c ≤ c + d
⊢ a - (c + d - c) = a + c - (c + d)

Tactic:
rw [add_tsub_cancel_left c, add_comm a c, add_tsub_add_eq_tsub_left]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithTop α
⊢ x < y ↔ (∃ a, x = ↑a) ∧ y = ⊤ ∨ ∃ a b, a < b ∧ x = ↑a ∧ y = ↑b

Tactic:
grind [WithTop.lt_def']

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
x y z : WithBot α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) x y) (swap (fun x1 x2 ↦ x1 + x2) x z)

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using fun _ ↦ by gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b : α
n : ℕ
a : (Additive α)ᵒᵈ
⊢ ⊤ + a = ⊤

Tactic:
ext; simp; simp [bot_eq_zero (α := α)]

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ 0 ≤ ⌈a⌉

Tactic:
rw [← FloorRing.intCast_strictMono.le_iff_le (β := α), Int.cast_zero]
  exact ha.trans (le_ceil a)

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithZero α
a b : α
hx : x = 0 → a ≤ b
⊢ unzeroD a x ≤ b ↔ x ≤ ↑b

Tactic:
by
  cases x <;> simp [hx]

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

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithZero α
a b : α
hx : x = 0 → a < b
⊢ unzeroD a x < b ↔ x < ↑b

Tactic:
by
  cases x <;> simp [hx]

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

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

Tactic:
apply one_ne_zero (α := M₀')

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

Goal state before:
pp: case inr
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
a : G₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f a = g a
ha : a ≠ 0
⊢ f a⁻¹ = g a⁻¹

Tactic:
exact (IsUnit.mk0 a ha).eq_on_inv f g h

Goal state after: