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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowBinRecAuto (n + 1) m = npowBinRec n m * m

Tactic:
← npowRec_eq_npowBinRec

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowBinRec n m * m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowBinRecAuto n m * m

Tactic:
← npowRec_eq_npowBinRec

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowRecAuto n m * m
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, z * x = 1
x y : M
h : x * y = 1
⊢ y * x = 1

Tactic:
have ⟨z, hz⟩ := ex x y h
    rwa [show y = z by simpa [mul_assoc, h] using congr_arg (· * y) hz.symm]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
⊢ c = c'

Tactic:
have := inj (a₁ := fun _ ↦ c) (a₂ := (if · = b₀ then c' else c)) ?_

Goal state after:
case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
this : (fun x ↦ c) = fun x ↦ if x = b₀ then c' else c
⊢ c = c'

case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
⊢ ((fun g ↦ g ∘ f) fun x ↦ c) = (fun g ↦ g ∘ f) fun x ↦ if x = b₀ then c' else c
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝ : LE α
⊢ NoBotOrder α ↔ ∀ (x : α), ¬IsBot x

Tactic:
by
  simp_rw [noBotOrder_iff', IsBot, not_forall]

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
ha' : IsMax a
b : α
hb : b ≠ a
⊢ False

Tactic:
exact hb <| ha'.eq_of_ge (ha.lt_of_ne hb.symm).le

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ ¬IsMax a ↔ a < ⊤

Tactic:
rw [not_isMax_iff]
  exact ⟨fun ⟨b, hb⟩ ↦ hb.trans_le le_top, fun h ↦ ⟨⊤, h⟩⟩

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: P Q : Prop
⊢ IsCompl P Q ↔ ¬(P ↔ Q)

Tactic:
rw [_root_.isCompl_iff, Prop.disjoint_iff, Prop.codisjoint_iff, not_iff]

Goal state after:
P Q : Prop
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
⊢ ∃ f, StrictMono f

Tactic:
rcases Nat.exists_strictMono' (default : α) with ⟨f, hf, hf₀⟩

Goal state after:
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
⊢ ∃ f, StrictMono f
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
⊢ Monotone f

Tactic:
intro x y hxy

Goal state after:
α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
x y : α
hxy : x ≤ y
⊢ f x ≤ f y
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
s : Set α
⊢ (s = ∅ ∨ ∃ x, s = {x}) → s.Subsingleton

Tactic:
by rintro (_ | ⟨_, rfl⟩) <;> simp_all

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 \ b

Tactic:
rw [sdiff_le_iff, sdiff_le_iff, sup_left_comm, sup_sdiff_self, sup_left_comm, sdiff_sup_self,
    sup_left_comm]
  exact le_sup_left

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
⊢ ⊥ᶜ = ⊤

Tactic:
rw [← himp_bot, himp_self]

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

Goal state before:
pp: case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
removeNoneAux_none _ h2

Goal state after:
case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (e none) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x
Module: Mathlib.Logic.Equiv.Basic

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

Tactic:
rintro ⟨rfl | has, hai⟩
      · exact ⟨i, hi, swap_apply_left ..⟩
      · exact ⟨a, has, swap_apply_of_ne_of_ne hai (ne_of_mem_of_not_mem has hj)⟩

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:
bihimp,

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
hf' : ¬∃ b, f ⁻¹' {b} = univ
this : ∀ (x : α) (b : β), f x ≠ b
⊢ ∃ b, f = const α b

Tactic:
exact ⟨Classical.arbitrary β, funext fun x ↦ absurd rfl (this x _)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
⊢ ∅ ×ˢ t = ∅

Tactic:
ext
  exact iff_of_eq (false_and _)

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

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

Tactic:
by
  simp only [Set.ssubset_iff_exists]
  apply and_congr ?_ (by aesop)
  constructor
  all_goals
    intro r x hx
    simp_all only [subset_inter_iff, inter_subset_left, true_and, mem_preimage,
      mem_inter_iff, mem_range, true_and]
    aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range g ∪ g' '' (range f)ᶜ ⊆ range (extend f g g')

Tactic:
rintro z (⟨x, rfl⟩ | ⟨y, hy, rfl⟩)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
x : α
⊢ g x ∈ range (extend f g g')

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
y : β
hy : y ∈ (range f)ᶜ
⊢ g' y ∈ range (extend f g g')
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.offDiag.Nonempty ↔ s.Nontrivial

Tactic:
simp [offDiag, Set.Nonempty, Set.Nontrivial]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
⊢ f '' ∅ = ∅

Tactic:
image_empty

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
⊢ ∅ = ∅
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
⊢ InjOn f (s₁ ∪ s₂) ↔ InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y

Tactic:
refine ⟨fun H => ⟨H.mono subset_union_left, H.mono subset_union_right, ?_⟩, ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
⊢ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y

case refine_2
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
⊢ (InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y) → InjOn f (s₁ ∪ s₂)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' ∅ = ∅

Tactic:
image_empty

Goal state after:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ ∅ = ∅
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
N✝ : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝⁵ : MulOne M✝
inst✝⁴ : MulOne N✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : RightCancelMonoid N
f : M →ₙ* N
h : 1 * f 1 = f 1 * f 1
⊢ f 1 = 1

Tactic:
exact (mul_right_cancel h).symm

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:
by rw [div_eq_inv_mul, inv_mul_cancel_left]

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
⊢ f x ^ 0 = 1

Tactic:
← zpow,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
⊢ f (x ^ 0) = 1
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f x ^ ↑n.succ = f x ^ ↑n * f x

Tactic:
← zpow,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ ↑n.succ) = f x ^ ↑n * f x
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ ↑n.succ) = f x ^ ↑n * f x

Tactic:
← zpow,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ ↑n.succ) = f (x ^ ↑n) * f x
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑u₁ * ↑u₂ * (u₂.inv * u₁.inv) = 1

Tactic:
by rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv]

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f x ^ Int.negSucc n = (f x ^ ↑n.succ)⁻¹

Tactic:
← zpow,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ Int.negSucc n) = (f x ^ ↑n.succ)⁻¹
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ Int.negSucc n) = (f x ^ ↑n.succ)⁻¹

Tactic:
← zpow,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ Int.negSucc n) = (f (x ^ ↑n.succ))⁻¹
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
hu : ↑u = a
⊢ IsUnit a⁻¹

Tactic:
rw [← hu, ← Units.val_inv_eq_inv_val]

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
hu : ↑u = a
⊢ IsUnit ↑u⁻¹
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
val inv : M
val_inv : val * inv = 1
inv_val : inv * val = 1
⊢ f val * f inv = 1

Tactic:
by simp [← map_mul, val_inv]

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

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b = 1

Tactic:
RightCancelMonoid.eq_one_of_mul_right h,

Goal state after:
α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : 1 * b = 1
⊢ b = 1
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ha : a ^ n = 0
⊢ a = 0

Tactic:
induction n with
    | zero => simpa using congr_arg (a * ·) ha
    | succ n ih => rw [pow_succ, mul_eq_zero] at ha; exact ha.elim ih id

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

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝³ : AddZeroClass A
inst✝² : DistribSMul M A
inst✝¹ : AddZeroClass B
inst✝ : SMul M B
f : B →+ A
hf : Injective ⇑f
smul : ∀ (c : M) (x : B), f (c • x) = c • f x
c : M
x y : B
⊢ f (c • (x + y)) = f (c • x + c • y)

Tactic:
by simp only [smul, map_add, smul_add]

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

Goal state before:
pp: M : Type u_3
inst✝² : AddCommMonoid M
R : Type u_5
inst✝¹ : Ring R
inst✝ : Module R M
r : R
m : M
⊢ (r + (1 - r)) • m = m

Tactic:
add_sub_cancel,

Goal state after:
M : Type u_3
inst✝² : AddCommMonoid M
R : Type u_5
inst✝¹ : Ring R
inst✝ : Module R M
r : R
m : M
⊢ 1 • m = m
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
a : α
n : ℕ
ha : IsSquare a
⊢ IsSquare (a ^ n)

Tactic:
by
  aesop (add simp Commute.mul_pow)

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

Goal state before:
pp: case neg
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)

Goal state after:
case neg.inl
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

case neg.inr
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : αˣ
⊢ ↑a = -1 ↔ a = -1

Tactic:
rw [← Units.coe_neg_one, val_inj]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)

Tactic:
simp only [divp, add_mul, mul_inv_rev, val_mul]

Goal state after:
α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + b * ↑u₂⁻¹ = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₁ * b * (↑u₂⁻¹ * ↑u₁⁻¹)
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)

Tactic:
by
  simp only [divp, add_mul, mul_inv_rev, val_mul]
  rw [mul_comm (↑u₁ * b), mul_comm b]
  rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Odd (a + 1 + a)

Tactic:
by simp [add_comm _ a]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a : α
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
by
  rw [← mul_le_mul_iff_left a]
  simp

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a : α
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
by
  rw [← mul_le_mul_iff_left a]
  simp

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

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

Tactic:
by
  rw [← mul_le_mul_iff_left a]
  simp

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a : α
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
by
  rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a : α
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
by
  rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 3 + 1

Tactic:
exact lt_add_of_lt_of_nonneg zero_lt_three zero_le_one

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

Goal state before:
pp: case inr
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
hb' : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
exact mul_lt_mul_of_le_of_lt ha hb'

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₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ 1 ≤ b * a

Tactic:
rw [← mul_inv_le_iff₀ ha, one_mul]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 2 * 2 * (r * r) ≤ (a + b) * (a + b)

Tactic:
← pow_two r,

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 2 * 2 * r ^ 2 ≤ (a + b) * (a + b)
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
⊢ Injective f

Tactic:
intro x y hxy

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
⊢ x = y
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a

Tactic:
by
  constructor
  · exact RelHomClass.acc (Quotient.mkRelHom H) a
  · intro ac
    induction ac with | intro _ _ IH => ?_
    refine ⟨_, fun q h => ?_⟩
    obtain ⟨a', rfl⟩ := q.exists_rep
    exact IH a' h

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ 1 ≤ a

Tactic:
by
  suffices this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 by
    rwa [← inf_eq_right, ← mul_eq_left]
  rw [mul_inf, inf_mul, ← pow_two, mul_one, one_mul, inf_assoc, inf_left_idem, inf_comm,
    inf_assoc, inf_of_le_left ha]

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

Goal state before:
pp: case left
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ x * y

Tactic:
← inf_mul_sup x y

Goal state after:
case left
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ y) * (x ⊔ y)
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

Tactic:
cases le_or_gt 1 a <;> simp [*, le_of_lt]

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

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ a * a⁻¹ ≤ a * |a|ₘ

Tactic:
inv_le_mabs a

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ a * |a|ₘ ≤ a * |a|ₘ
Module: Mathlib.Order.Interval.Set.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ {x | b < x ∧ x < a} = {x | x < a ∧ b < x}

Tactic:
simp only [and_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ {x | b < x ∧ x ≤ a} = {x | x ≤ a ∧ b < x}

Tactic:
simp only [and_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ {x | b ≤ x ∧ x < a} = {x | x < a ∧ b ≤ x}

Tactic:
simp only [and_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ {x | b ≤ x ∧ x ≤ a} = {x | x ≤ a ∧ b ≤ x}

Tactic:
simp only [and_comm]

Goal state after: