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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x : G
⊢ a * x = a * x * 1

Tactic:
mul_one

Goal state after:
G : Type u_3
inst✝ : Group G
a x : G
⊢ a * x = a * x
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a x : G
⊢ a * x = a * x * a⁻¹ * a

Tactic:
rw [mul_assoc, inv_mul_cancel, mul_one]

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

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

Tactic:
mul_one

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m : ℕ
⊢ a ^ m = a ^ m
Module: Mathlib.Algebra.Group.Defs

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

Tactic:
by
  rw [← inv_eq_of_mul_eq_one_right h, inv_inv]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a * 1 = a

Tactic:
mul_one

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
⊢ a = a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ a * b⁻¹ * b = a

Tactic:
rw [mul_assoc, inv_mul_cancel, mul_one]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
a b c : α
hbc : r a c
⊢ TransGen r a c

Tactic:
exact single hbc

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

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : SMulCommClass M N N
x : M
y : N
⊢ x • (y * 1) = x • y

Tactic:
mul_one

Goal state after:
M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : SMulCommClass M N N
x : M
y : N
⊢ x • y = x • y
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
a b : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
inhabited_h : Inhabited ι
⊢ a < b

Tactic:
exact Pi.lt_def.2 ⟨le_of_strongLT h, default, h _⟩

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a ≤ const β b ↔ a ≤ b

Tactic:
by simp [Pi.le_def]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
⊢ compare (f a) (f b) = compareOfLessAndEq a b

Tactic:
have h := LinearOrder.compare_eq_compareOfLessAndEq (f a) (f b)
  simp only [h, compareOfLessAndEq]
  split_ifs <;> try (first | rfl | contradiction)
  · have : ¬ f a = f b := by rename_i h; exact inj.ne h
    contradiction
  · grind

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: o o' : Ordering
⊢ o.swap = o' ↔ o = o'.swap

Tactic:
by
  rw [← swap_inj, swap_swap]

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 x y = cmp x' y'
⊢ cmp y x = cmp y' x'

Tactic:
rwa [cmp_eq_cmp_symm]

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

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

Tactic:
intro M

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
M : α
⊢ ¬P M
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x ⊓ (y ⊓ y') ⊔ x' ⊓ (y ⊓ y') = ⊥

Tactic:
← inf_assoc,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x ⊓ y ⊓ y' ⊔ x' ⊓ (y ⊓ y') = ⊥
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 : α
⊢ b ⊔ (a ⊔ b) = a ⊔ b

Tactic:
by rw [sup_comm, sup_assoc, sup_idem]

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

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
⊢ a ⊓ 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
a b : α
⊢ a ⊓ (a ⊓ b) = a ⊓ b

Tactic:
← inf_assoc,

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
a b : α
⊢ a ⊓ a ⊓ b = a ⊓ b
Module: Mathlib.Order.Lattice

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

Tactic:
sup_sup_sup_comm,

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = a ⊔ a ⊔ (b ⊔ c)
Module: Mathlib.Order.Lattice

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

Tactic:
sup_sup_sup_comm,

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ b ⊔ (c ⊔ c)
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
x y z : α
⊢ x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ x ⊓ z

Tactic:
inf_sup_left

Goal state after:
α : Type u
inst✝ : DistribLattice α
x y z : α
⊢ x ⊓ y ⊔ x ⊓ z ≤ x ⊓ y ⊔ x ⊓ z
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
← inf_assoc,

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

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

Tactic:
exact sdiff_le_sdiff_left hinf

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

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

Tactic:
inf_sup_left

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y
Module: Mathlib.Logic.Equiv.Option

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

Tactic:
removeNoneAux_none _ h1

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

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

Tactic:
inf_of_le_right sdiff_le'

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ⊓ y \ x = x \ y ⊓ y \ x
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
← inf_assoc,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (y \ z) = z ⊓ x ⊓ y ⊔ x \ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
inf_sup_left

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : p a
⊢ (ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)

Tactic:
simp [Perm.subtypeCongr, h]

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

Goal state before:
pp: case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : ¬p a
⊢ (ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)

Tactic:
simp [Perm.subtypeCongr, h]

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

Goal state before:
pp: case fst
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x \ y).fst = (x ⊓ yᶜ).fst

Tactic:
simp [sdiff_eq]

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

Goal state before:
pp: case snd
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x \ y).snd = (x ⊓ yᶜ).snd

Tactic:
simp [sdiff_eq]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
sup_sup_sup_comm,

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

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

Tactic:
← inf_assoc,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ t.restrictPreimage f ⁻¹' u = (fun a ↦ f ↑a) ⁻¹' Subtype.val '' u

Tactic:
by
  rw [← preimage_preimage (g := f) (f := Subtype.val), ← image_val_preimage_restrictPreimage,
    preimage_image_eq _ Subtype.val_injective]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
ht : t.Nonempty
⊢ EqOn f f' s

Tactic:
obtain ⟨x, hxt⟩ := ht

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x : β
hxt : x ∈ t
⊢ EqOn f f' s
Module: Mathlib.Data.Set.Image

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

Tactic:
by rw [← image_nonempty, hf.image_preimage]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Tactic:
apply Set.preimage_subset_preimage_iff

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ range f
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
ht : (s.pi t).Nonempty
i : ι
⊢ t i ⊆ eval i '' s.pi t

Tactic:
obtain ⟨f, hf⟩ := ht
  refine fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩
  obtain rfl | hji := eq_or_ne j i <;> simp [*, hf _ hj]

Goal state after:
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✝¹ : One M
inst✝ : One N
f g : OneHom M N
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by cases f; cases g; congr

Goal state after:
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✝¹ : Mul M
inst✝ : Mul N
f g : M →ₙ* N
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by cases f; cases g; congr

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
⊢ s.Nonempty ∨ t = ∅

Tactic:
by
  by_contra!
  exact (h.comap_nonempty this.2).ne_empty this.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ (a : α), a ∈ s → p (f a)
b : β
hb : b ∈ t
⊢ p b

Tactic:
by obtain ⟨a, ha, rfl⟩ := hf.surjOn hb; exact h _ ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
⊢ (∃ a, a ∈ s ∧ p (f a)) → ∃ b, b ∈ t ∧ p b

Tactic:
rintro ⟨a, ha, h⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
h : p (f a)
⊢ ∃ b, b ∈ t ∧ p b
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) ⊆ f' ⁻¹' s₁ ∩ f '' s

Tactic:
rintro _ ⟨x, ⟨h₁, h⟩, rfl⟩

Goal state after:
case h₁
α : 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₁ ∩ f '' s
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
⊢ y ∈ s

Tactic:
exact hy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (range fa)
⊢ InjOn fb (range f)

Tactic:
rw [← image_univ] at *
  exact h.injOn_image ha.injOn hf

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : IsLeftCancelMul M
a b : M
⊢ a * b = a ↔ a * b = a * 1

Tactic:
mul_one

Goal state after:
M : Type u_4
inst✝¹ : Monoid M
inst✝ : IsLeftCancelMul M
a b : M
⊢ a * b = a ↔ a * b = a
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : One M₁
inst✝ : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f x * 1 = f x

Tactic:
mul_one

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : One M₁
inst✝ : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f x = f x
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
inv_pow,

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

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

Tactic:
inv_pow,

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ a⁻¹ ^ m * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n

Tactic:
inv_pow,

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ (a ^ m)⁻¹ * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ (a ^ m)⁻¹ * (a⁻¹ ^ n)⁻¹ = (a ^ m)⁻¹ * a ^ n

Tactic:
inv_pow,

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
h : n ≤ m
⊢ (a ^ m)⁻¹ * (a ^ n)⁻¹⁻¹ = (a ^ m)⁻¹ * a ^ n
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₂
inst✝¹ : One M₂
inst✝ : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f (x * 1) = f x

Tactic:
mul_one

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₂
inst✝¹ : One M₂
inst✝ : MulOneClass M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
⊢ f x = f x
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rca : r c a
⊢ f a b * (f b c * 1) = f a b * f b c

Tactic:
mul_one

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rca : r c a
⊢ f a b * f b c = f a b * f b c
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
u : αˣ
⊢ a * 1 = a

Tactic:
mul_one

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
u : αˣ
⊢ a = a
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rcb : r c b
⊢ f a c = f a c * 1

Tactic:
mul_one

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b c : α
pab : p a b
pbc : p b c
pac : p a c
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rcb : r c b
⊢ f a c = f a c
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 * 1)
⊢ IsUnit a

Tactic:
mul_one

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
⊢ IsUnit a
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a = a * 1

Tactic:
mul_one

Goal state after:
α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a = a
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a = a * 1

Tactic:
mul_one

Goal state after:
α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ a = a
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
b : αˣ
⊢ a * 1 = a

Tactic:
mul_one

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
b : αˣ
⊢ a = a
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
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
⊢ ↑(g 1) = ↑1

Tactic:
rw [h 1]

Goal state after:
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
⊢ f 1 = ↑1
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
mul_one

Goal state after:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u * a = 1
⊢ ↑u⁻¹ = ↑u⁻¹
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
mul_one

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

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

Tactic:
mul_one

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

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

Tactic:
mul_one

Goal state after:
M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit a
⊢ a * b = a ↔ a * b = a
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝¹ : MulOneClass M
inst✝ : Mul N
b₁ b₂ : N
⊢ (1 * 1, b₁ * b₂) = (1, b₁ * b₂)

Tactic:
mul_one

Goal state after:
M : Type u_3
N : Type u_4
inst✝¹ : MulOneClass M
inst✝ : Mul N
b₁ b₂ : N
⊢ (1, b₁ * b₂) = (1, b₁ * b₂)
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝¹ : Mul M
inst✝ : MulOneClass N
a₁ a₂ : M
⊢ (a₁ * a₂, 1 * 1) = (a₁ * a₂, 1)

Tactic:
mul_one

Goal state after:
M : Type u_3
N : Type u_4
inst✝¹ : Mul M
inst✝ : MulOneClass N
a₁ a₂ : M
⊢ (a₁ * a₂, 1) = (a₁ * a₂, 1)
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: G₀ : Type u
M₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ a b : G₀
hb : b ≠ 0
⊢ a * 1 = a

Tactic:
mul_one

Goal state after:
G₀ : Type u
M₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ a b : G₀
hb : b ≠ 0
⊢ a = a
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ σ * 1 = σ

Tactic:
mul_one

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ σ = σ
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsLeftCancelMulZero M₀
⊢ a * b = a ↔ a * b = a * 1

Tactic:
mul_one

Goal state after:
M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsLeftCancelMulZero M₀
⊢ a * b = a ↔ a * b = a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsLeftCancelMulZero M₀
ha : a ≠ 0
⊢ a * b = a * 1 ↔ a * b = a

Tactic:
mul_one

Goal state after:
M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsLeftCancelMulZero M₀
ha : a ≠ 0
⊢ a * b = a ↔ a * b = a
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ f (if p then 0 else 1) = if p then 0 else 1

Tactic:
split_ifs with h <;> simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ f (if p then 1 else 0) = if p then 1 else 0

Tactic:
split_ifs with h <;> simp

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

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

Tactic:
mul_one

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b : G₀
h : a * b = 1
⊢ a⁻¹ = a⁻¹
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * 1 = a

Tactic:
mul_one

Goal state after:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a = a