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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Total r
a b : α
⊢ Decidable.decide (r a b) = true ∨ Decidable.decide (r b a) = true

Tactic:
by simpa using total a b

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
x : α
⊢ ∃ y, y ≠ x

Tactic:
exact Decidable.exists_ne x

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

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

Tactic:
refine ⟨fun h ↦ funext fun z ↦ ?_, fun h ↦ ?_⟩
  · rwa [Subsingleton.elim x z, Subsingleton.elim y z] at h
  · rw [h, Subsingleton.elim x y]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝ : Nontrivial α
b : β
⊢ ¬Injective fun x ↦ b

Tactic:
rw [not_injective_iff]

Goal state after:
α : Type u_4
β : Type u_5
inst✝ : Nontrivial α
b : β
⊢ ∃ a b_1, b = b ∧ a ≠ b_1
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f (Classical.choose h') = b

Tactic:
apply Classical.choose_spec h'

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

Goal state before:
pp: case refine_2
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b) → ∀ (a : α), ∃! b, r a b

Tactic:
· rintro ⟨f, hf⟩
    simp [hf]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
⊢ Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁)

Tactic:
by
  grind [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : α → β
⊢ Relation.Map (Relation.Map r f f on f) f f = Relation.Map r f f

Tactic:
by
  grind [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
⊢ (Relation.Map (r on f) f f on f) = (r on f)

Tactic:
by
  grind [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
f : α → β
a₁ a₂ : α
⊢ Relation.Map (r on f) f f (f a₁) (f a₂) ↔ r (f a₁) (f a₂)

Tactic:
by
  grind [Relation.Map]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
exact Or.inr (IH.tail bd)

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : { a // p a } ≃ { b // q b }
⊢ (∃! a, p a) ↔ ∃! b, q b

Tactic:
by
  simp [← unique_subtype_iff_existsUnique, unique_iff_subsingleton_and_nonempty,
        nonempty_congr e, subsingleton_congr e]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul M β
inst✝¹ : SMul N β
inst✝ : SMulCommClass M N β
f : α → β
hf : Injective f
h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x
h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x
c₁ : M
c₂ : N
x : α
⊢ f (c₁ • c₂ • x) = f (c₂ • c₁ • x)

Tactic:
simp only [h₁, h₂, smul_comm c₁ c₂ (f x)]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ x • y • z = y • x • z

Tactic:
← H x z,

Goal state after:
M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ x • y • z = y • (z * x • 1)
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
x : Option α
f : α → β
⊢ some b = Option.map f x ↔ ∃ a, x = some a ∧ f a = b

Tactic:
by
  rw [eq_comm, map_eq_some_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {a b : α}, compare a b = Ordering.eq ↔ (a == b) = true

Tactic:
by simp [compare_eq_iff_eq]

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)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ compare (f a) (f b) = compareOfLessAndEq a b

Tactic:
simp only [h, compareOfLessAndEq]

Goal state after:
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
⊢ m + f n ≤ f (m + n)

Tactic:
rw [Nat.add_comm m, Nat.add_comm m]
  induction m with
  | zero => rw [Nat.add_zero, Nat.add_zero]
  | succ m ih =>
    rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le_iff]
    exact ih.trans_lt (hf (n + m).lt_succ_self)

Goal state after:
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' ⊔ x ⊔ y) ⊓ (x' ⊔ x ⊔ y') = ⊤

Tactic:
sup_assoc,

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

Tactic:
sup_assoc,

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

Tactic:
sup_assoc,

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 : α
⊢ a ⊔ (b ⊔ b) = a ⊔ b
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 : α
hac : a ⊔ c = c
hbc : b ⊔ c = c
⊢ a ⊔ b ⊔ c = c

Tactic:
sup_assoc,

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 : α
hac : a ⊔ c = c
hbc : b ⊔ c = c
⊢ a ⊔ (b ⊔ c) = c
Module: Mathlib.Order.Lattice

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

Tactic:
sup_assoc,

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

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

Tactic:
sup_assoc,

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

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

Tactic:
sup_assoc,

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

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

Tactic:
sup_assoc,

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ Disjoint (insert a t) s ↔ ¬a ∈ s ∧ Disjoint s t

Tactic:
disjoint_insert_left,

Goal state after:
α : Type u_1
s t : Set α
a : α
⊢ ¬a ∈ s ∧ Disjoint t s ↔ ¬a ∈ s ∧ Disjoint s t
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: case mp
α : Type u
s : Set α
h : Subsingleton ↑s
a : α
ha : a ∈ s
b : α
⊢ b ∈ s → a = b

Tactic:
hb

Goal state after:
case mp
α : Type u
s : Set α
h : Subsingleton ↑s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
conv_rhs at s => rw [← sup_inf_sdiff x y, sup_comm]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
by simp_rw [← sdiff_le_iff, le_inf_iff, sdiff_le_iff, ← le_inf_iff]; rfl

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

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
y x z : α
h : y ≤ x ⊔ z
⊢ x ⊔ z ⊔ x ≤ z ⊔ x

Tactic:
sup_assoc,

Goal state after:
α : Type u
β : Type u_1
x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
y x z : α
h : y ≤ x ⊔ z
⊢ x ⊔ (z ⊔ x) ≤ z ⊔ x
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
y x z : α
h : y ≤ x ⊔ z
⊢ z ⊔ x ⊔ x ≤ z ⊔ x

Tactic:
sup_assoc,

Goal state after:
α : Type u
β : Type u_1
x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
y x z : α
h : y ≤ x ⊔ z
⊢ z ⊔ (x ⊔ x) ≤ z ⊔ x
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ (z ⊔ x) ⊓ y ⊔ z = y

Tactic:
sup_comm z,

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

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

Tactic:
rw [← sup_inf_right]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a \ a ⊔ a \ ￢a

Tactic:
hnot_sdiff,

Goal state after:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a \ ￢a
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 b : α
⊢ f b ⊔ (f a)ᶜ = f (b ⊔ aᶜ)

Tactic:
rw [map_sup, map_compl]

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:
simp only [Set.ssubset_iff_exists]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ (range f ∩ s ⊆ range f ∩ s' ∧ ∃ x, x ∈ range f ∩ s' ∧ ¬x ∈ range f ∩ s) ↔
    f ⁻¹' s ⊆ f ⁻¹' s' ∧ ∃ x, x ∈ f ⁻¹' s' ∧ ¬x ∈ f ⁻¹' s
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f)ᶜ.domRestrict (extend f g g') = g' ∘ Subtype.val

Tactic:
by
  classical
  exact domRestrict_dite_compl _ _

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

Goal state before:
pp: X : Type u_1
Y : Sort u_2
f : X → Y
⊢ pullbackDiagonal f ∩ Subtype.val ⁻¹' univ ×ˢ univ = pullbackDiagonal f

Tactic:
univ_prod_univ,

Goal state after:
X : Type u_1
Y : Sort u_2
f : X → Y
⊢ pullbackDiagonal f ∩ Subtype.val ⁻¹' univ = pullbackDiagonal f
Module: Mathlib.Data.Set.Function

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

Tactic:
simp [heq]

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

Goal state before:
pp: F : 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
inst✝³ : EquivLike F M N
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulEquivClass F M N
e : F
⊢ e 1 * e (EquivLike.inv e 1) = e (EquivLike.inv e 1)

Tactic:
← map_mul,

Goal state after:
F : 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
inst✝³ : EquivLike F M N
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulEquivClass F M N
e : F
⊢ e (1 * EquivLike.inv e 1) = e (EquivLike.inv e 1)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : MulOne M
inst✝² : MulOne N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ f a * f b = 1

Tactic:
← map_mul,

Goal state after:
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : MulOne M
inst✝² : MulOne N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ f (a * b) = 1
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
b : β
⊢ b ∈ t → g₁ b = g₂ b

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
b : β
hb : b ∈ t
⊢ g₁ b = g₂ b
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: F : Type u_7
G : Type u_8
H : Type u_9
inst✝³ : Group G
inst✝² : MulOneClass H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), f a = 1 → a = 1
x y : G
hxy : f x = f y
⊢ f y * f y⁻¹ = 1

Tactic:
← map_mul,

Goal state after:
F : Type u_7
G : Type u_8
H : Type u_9
inst✝³ : Group G
inst✝² : MulOneClass H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), f a = 1 → a = 1
x y : G
hxy : f x = f y
⊢ f (y * y⁻¹) = 1
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : CommGroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
⊢ ∀ (x₁ x₂ : G), f x₁ * f x₂ = f x₂ * f x₁

Tactic:
← map_mul,

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : CommGroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
⊢ ∀ (x₁ x₂ : G), f (x₁ * x₂) = f (x₂ * x₁)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: m n : ℕ
h : n.succ ≤ m
⊢ ↑m + -(↑n + ↑1) = ↑(m - n.succ)

Tactic:
← Int.natCast_add,

Goal state after:
m n : ℕ
h : n.succ ≤ m
⊢ ↑m + -↑(n + 1) = ↑(m - n.succ)
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:
by rw [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝ : MulOne α
⊢ IsDedekindFiniteMonoid αᵐᵒᵖ ↔ IsDedekindFiniteMonoid α

Tactic:
by
  simp_rw [isDedekindFiniteMonoid_iff, ← opEquiv.forall_congr_right]
  simpa [← op_one, ← op_mul] using forall_comm

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℤ
⊢ (a / b) ^ n = a ^ n / b ^ n

Tactic:
simp only [div_eq_mul_inv, mul_zpow, inv_zpow]

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

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

Tactic:
← mul_assoc b⁻¹,

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a * (b⁻¹ * b * c) = a * c
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
⊢ a /ₚ u = a / ↑u

Tactic:
by
  rw [div_eq_mul_inv, divp, u.val_inv_eq_inv_val]

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

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

Tactic:
by rw [mul_one]

Goal state after:
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:
by rw [mul_one]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroOneClass M₀
h : 0 = 1
a : M₀
⊢ a = 0

Tactic:
rw [← mul_one a, ← h, mul_zero]

Goal state after:
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:
by rw [mul_one]

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocSemiring α
n : α
⊢ n * 1 + n * 1 = n + n

Tactic:
by rw [mul_one]

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

Goal state before:
pp: x : ℕ
x✝ : ∃ n, n * n = x
n : ℕ
hn : n * n = x
⊢ x.sqrt * x.sqrt = x

Tactic:
by rw [← hn, sqrt_eq]

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

Goal state before:
pp: α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
⊢ ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c

Tactic:
have : c = x * (b - x) := (eq_neg_of_add_eq_zero_right h).trans (by simp [mul_sub, mul_comm])
  refine ⟨b - x, ?_, by simp, by rw [this]⟩
  rw [this, sub_add, ← sub_mul, sub_self]

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

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
⊢ NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α

Tactic:
rw [← isCancelMulZero_iff_noZeroDivisors, isCancelMulZero_iff_isDomain_or_subsingleton]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + (f (x * y) - f x * f y - f x * f y) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
sub_sub,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + (f (x * y) - (f x * f y + f x * f y)) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
obtain (⟨ha, hb⟩ | ⟨ha, hb⟩ | ⟨ha, hb⟩) :
      (IsUnit a ∧ ¬ IsUnit b) ∨ (¬ IsUnit a ∧ IsUnit b) ∨ (IsUnit a ∧ IsUnit b) := by grind
  · have : ¬ IsUnit (a * b) := by simpa [ha.mul_left_iff]
    simp [Ring.inverse_non_unit, hb, this]
  · have : ¬ IsUnit (a * b) := by simpa [hb.mul_right_iff]
    simp [Ring.inverse_non_unit, ha, this]
  · simp [Ring.inverse_of_isUnit, ha, hb, ha.mul hb, ← Units.val_mul, ← mul_inv_rev]
    simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
a : R
⊢ (-a) ^ 2 = a ^ 2

Tactic:
simp [sq]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ (n % 2) * ((-1) ^ 2) ^ (n / 2) = (-1) ^ ((n % 2 + 2 * (n / 2)) % 2)

Tactic:
simp [sq]

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

Goal state before:
pp: α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
inst✝ : LeftDistribClass α
b k : α
⊢ Even (b * (k + k))

Tactic:
use b * k

Goal state after:
case h
α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
inst✝ : LeftDistribClass α
b k : α
⊢ b * (k + k) = b * k + b * k
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
⊢ r b c

Tactic:
rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a]
    exact h a⁻¹ bc

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

Goal state before:
pp: case inl
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Even n
⊢ 1 = if Even n then 1 else -1

Tactic:
if_pos h

Goal state after:
case inl
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Even n
⊢ 1 = 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case inl
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Even n
⊢ (-1) ^ n = if Even n then 1 else -1

Tactic:
rw [h.neg_one_pow, if_pos h]

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

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

Tactic:
by rw [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 b : α
⊢ b < a * 1 ↔ b < a

Tactic:
by rw [mul_one]

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

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

Tactic:
rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right, one_mul]

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

Goal state before:
pp: α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a b : α
inst✝¹ : MulLeftMono α
inst✝ : MulLeftReflectLE α
⊢ (∃ c, 1 ≤ c ∧ a * c = b) → a ≤ b

Tactic:
by rintro ⟨c, hc, rfl⟩; exact le_mul_of_one_le_right' hc

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 2

Tactic:
by
  rw [← one_add_one_eq_two]
  exact add_nonneg zero_le_one zero_le_one

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a * c ≤ b * d

Tactic:
exact mul_le_mul' hab hcd

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

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

Tactic:
simpa only [div_eq_mul_inv] using mul_lt_mul_iff_right _

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulLeftReflectLE α
a b : α
⊢ a ≤ a * b ↔ a * 1 ≤ a * b

Tactic:
by rw [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulLeftReflectLE α
a b : α
⊢ a * b ≤ a ↔ a * b ≤ a * 1

Tactic:
by rw [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulLeftReflectLT α
a b : α
⊢ a < a * b ↔ a * 1 < a * b

Tactic:
by rw [mul_one]

Goal state after: