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

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
a : M
⊢ a * 1 = 1 * a

Tactic:
mul_one,

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
a : M
⊢ a = 1 * a
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor a b ↔ (¬a ↔ b)

Tactic:
by simp only [← @xor_not_left _ b, not_not]

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ default = y

Tactic:
h y

Goal state after:
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ default = default
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b

Tactic:
unfold extend
  congr

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a b b✝ c✝ : α
a✝ : ReflTransGen r a b✝
hdb : r b✝ c✝
IH : ∀ {c : α}, r b✝ c → TransGen r a c
c : α
hbc : r c✝ c
⊢ TransGen r a c

Tactic:
exact tail (IH hdb) hbc

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

Goal state before:
pp: case inl
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : m ≤ n
⊢ f^[m - n] a = a

pp: case inr
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a

Tactic:
{ simp [Nat.sub_eq_zero_of_le h] }

Goal state after:
case inr
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
⊢ ∀ (a : α),
    ((fun a ↦ q (e a)) a ∧ ∀ (y : α), (fun a ↦ q (e a)) y → y = a) ↔
      (fun b ↦ q b) (e a) ∧ ∀ (y : β), (fun b ↦ q b) y → y = e a

Tactic:
by simpa using fun _ _ ↦ e.forall_congr (by simp)

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

Goal state before:
pp: ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
inst✝² : (i : ι) → One (M i)
inst✝¹ : (i : ι) → One (N i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i
hf' : ∀ (i : ι), f' i 1 = 1
i : ι
x : M i
j : ι
⊢ f' j (mulSingle i x j) = mulSingle i (f' i x) j

Tactic:
by
  simpa only [Pi.one_apply, hf', mulSingle] using! Function.apply_update f' 1 i x j

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

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

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

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

Goal state before:
pp: α : Sort u_1
π : α → Sort u_4
⊢ IsEmpty ((a : α) → π a) ↔ ∃ a, IsEmpty (π a)

Tactic:
by
  simp only [← not_nonempty_iff, Classical.nonempty_pi, not_forall]

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

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

Tactic:
rw [LinearOrder.compare_eq_compareOfLessAndEq,
    compareOfLessAndEq_eq_gt le_antisymm le_total not_le]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ a i < update a i c i

Tactic:
by rwa [update_self]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ update a i c i < b i

Tactic:
by rwa [update_self]

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

Goal state before:
pp: b : Bool
⊢ ofNat b.toNat = b

Tactic:
by grind [cases Bool]

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

Goal state before:
pp: α : Sort u_1
f : Bool → α
H : f false ≠ f true
x y : Bool
⊢ f x = f y → x = y

Tactic:
by grind [cases Bool]

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

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} ↦ next)
x y : C n
H : leRecOn ⋯ (fun {k} ↦ next) x = leRecOn ⋯ (fun {k} ↦ next) y
⊢ x = y

Tactic:
rw [leRecOn_succ hnm, leRecOn_succ hnm] at H

Goal state after:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} ↦ next)
x y : C n
H : next (leRecOn hnm (fun {k} ↦ next) x) = next (leRecOn hnm (fun {k} ↦ next) y)
⊢ x = y
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
⊢ ∃ f, StrictMono f

Tactic:
rcases Nat.exists_strictAnti' (default : α) with ⟨g, hg, hg₀⟩

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

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u
inst✝⁴ : Lattice α
inst✝³ : DecidableEq α
inst✝² : DecidableLE α
inst✝¹ : DecidableLT α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ ∀ (a b : α), a ⊓ b = if a ≤ b then a else b

Tactic:
by exact congr_fun₂ inf_eq_minDefault

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]

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ a ⊔ (b ⊔ c)
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:
by
  conv_rhs at s => rw [← sup_inf_sdiff x y, sup_comm]
  rw [sup_comm] at s
  conv_rhs at i => rw [← inf_inf_sdiff x y, inf_comm]
  rw [inf_comm] at i
  exact (eq_of_inf_eq_sup_eq i s).symm

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

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

Tactic:
by
  simp [removeNoneAux, Option.not_isSome_iff_eq_none.mpr h]

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

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

Tactic:
by
          rw [inf_idem, inf_sup_right, ← inf_comm x y, inf_inf_sdiff, bot_sup_eq]

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

Goal state before:
pp: α : Type u_1
t s s' u : Set α
⊢ (∀ (x : α), x ∈ u → x ∈ t.ite s s') ↔ ∀ (x : α), (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')

Tactic:
refine forall_congr' fun x => ?_

Goal state after:
α : Type u_1
t s s' u : Set α
x : α
⊢ x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ z ⊓ y \ x = ⊥ ↔ z ≤ x

Tactic:
by
  rw [← disjoint_iff]
  exact disjoint_sdiff_iff_le hz hx

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

Goal state before:
pp: case inr
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
ha : ia ≠ ja
⊢ update f ⟨ia, ib⟩ x ⟨ja, jb⟩ =
    update (fun x y ↦ f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y ↦ f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ja jb

Tactic:
Function.update_of_ne (ne_of_apply_ne Sigma.fst _),

Goal state after:
case inr
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
ha : ia ≠ ja
⊢ f ⟨ja, jb⟩ = update (fun x y ↦ f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y ↦ f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ja jb

α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
ha : ia ≠ ja
⊢ ⟨ja, jb⟩.fst ≠ ⟨ia, ib⟩.fst
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
sdiff_sup,

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

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
f : ℕ → Type u
⊢ LeftInverse (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id)) fun x ↦
    Sigma.casesOn x fun n ↦
      Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩

Tactic:
rintro ⟨n | n, x⟩

Goal state after:
case zero
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
f : ℕ → Type u
x : f 0
⊢ Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id)
      ((fun x ↦
          Sigma.casesOn x fun n ↦
            Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩)
        ⟨0, x⟩) =
    ⟨0, x⟩

case succ
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
f : ℕ → Type u
n : ℕ
x : f (n + 1)
⊢ Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id)
      ((fun x ↦
          Sigma.casesOn x fun n ↦
            Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩)
        ⟨n + 1, x⟩) =
    ⟨n + 1, x⟩
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
  rw [symmDiff_symmDiff_left, symmDiff_symmDiff_right]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ b ⇔ c = b ⇔ a ⇔ c

Tactic:
bihimp_comm

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
bihimp_comm

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

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
⊢ RightInverse (fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s) fun p ↦
    Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ InjOn (s.piecewise f g) (s ∪ sᶜ) ↔ InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y

Tactic:
injOn_union (@disjoint_compl_right _ _ s),

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ (InjOn (s.piecewise f g) s ∧
      InjOn (s.piecewise f g) sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ sᶜ → s.piecewise f g x ≠ s.piecewise f g y) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : OneHom N P
f₁ f₂ : OneHom M N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ (g.comp f₂) x = g (f₂ x)

Tactic:
OneHom.comp_apply

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : OneHom N P
f₁ f₂ : OneHom M N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ g (f₂ x) = g (f₂ x)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a, a ∈ s ∧ f a = b
⊢ invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b

Tactic:
invFunOn,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a, a ∈ s ∧ f a = b
⊢ (if h : ∃ a, a ∈ s ∧ f a = b then Classical.choose h else Classical.choice inst✝) ∈ s ∧
    f (if h : ∃ a, a ∈ s ∧ f a = b then Classical.choose h else Classical.choice inst✝) = b
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ¬∃ a, a ∈ s ∧ f a = b
⊢ invFunOn f s b = Classical.choice inst✝

Tactic:
invFunOn,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ¬∃ a, a ∈ s ∧ f a = b
⊢ (if h : ∃ a, a ∈ s ∧ f a = b then Classical.choose h else Classical.choice inst✝) = Classical.choice inst✝
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a * a ^ (n - 1) = a ^ n

Tactic:
rw [← pow_succ', Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]

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

Goal state before:
pp: G : Type u_3
inst✝ : DivInvOneMonoid G
a : G
⊢ a / 1 = a

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x y : α
⊢ op (x / y) = (op y)⁻¹ * op x

Tactic:
simp [div_eq_mul_inv]

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

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

Tactic:
rw [← h, mul_inv_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
⊢ ∀ (u₁ u₂ : αˣ), ↑(u₁ / u₂) = ↑u₁ / ↑u₂

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
a : M
inst✝ : Subsingleton Mˣ
⊢ IsUnit a → a = 1

Tactic:
by rintro ⟨u, rfl⟩; simp [u.eq_one]

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

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

Tactic:
rw [← h, mul_inv_cancel_right]

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

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

Tactic:
rw [← h, mul_inv_cancel_right]

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

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ f x = ↑((liftRight f g h) x) * 1

Tactic:
mul_one,

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

Goal state before:
pp: F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst✝ : Group G
a b : G
⊢ (fun b ↦ b⁻¹ * a) ((fun b ↦ a / b) b) = b

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst✝ : Group G
a b : G
⊢ (fun b ↦ a / b) ((fun b ↦ b⁻¹ * a) b) = b

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst✝ : Group G
a b : G
⊢ (fun b ↦ b * a) ((fun b ↦ b / a) b) = b

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
inst✝ : Group G
a b : G
⊢ (fun b ↦ b / a) ((fun b ↦ b * a) b) = b

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H✝ : a * b = 0
this : f a * f b = 0
H : f a = 0
⊢ f a = f 0

Tactic:
by rwa [zero]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H✝ : a * b = 0
this : f a * f b = 0
H : f b = 0
⊢ f b = f 0

Tactic:
by rwa [zero]

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

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

Tactic:
swap_eq_one_iff

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ i = j ↔ i = j
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
R : Type u_12
S : Type u_13
M : Type u_14
inst✝² : AddZeroClass M
inst✝¹ : DistribSMul R M
inst✝ : SMul S M
f : R → S
hf : Surjective f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
c : R
x y : M
⊢ f c • (x + y) = f c • x + f c • y

Tactic:
simp only [hsmul, smul_add]

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

Goal state before:
pp: m : ℤ
n : ℕ
⊢ m ∣ ↑n ↔ m.natAbs ∣ n

Tactic:
obtain hn | hn := natAbs_eq m <;> rw [hn] <;> simp [← natCast_dvd_natCast, Int.neg_dvd]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ 1 / a * -1 = -(1 / a)

Tactic:
mul_neg,

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ -(1 / a * 1) = -(1 / a)
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x / x') (y / y')

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  exact h.mul_right h'.inv_right₀

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n : ℕ
a✝ b✝ : M
u✝ u₁ u₂ u : Mˣ
a b : M
hu : a * b = ↑u
hc : Commute a b
this : Commute a ↑u
⊢ b * ↑u⁻¹ * a = 1

Tactic:
← this.units_inv_right.right_comm,

Goal state after:
M : Type u_1
inst✝ : Monoid M
n : ℕ
a✝ b✝ : M
u✝ u₁ u₂ u : Mˣ
a b : M
hu : a * b = ↑u
hc : Commute a b
this : Commute a ↑u
⊢ b * a * ↑u⁻¹ = 1
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
⊢ a / b = 0 ↔ a = 0 ∨ b = 0

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * 1 * a = d * b * (d⁻¹ * c) ↔ d * a = b * c

Tactic:
mul_one,

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ d * a = d * b * (d⁻¹ * c) ↔ d * a = b * c
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * 1 * ↑u₁⁻¹ + ↑u₂⁻¹ * 1 * b

Tactic:
mul_one,

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

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

Tactic:
mul_one,

Goal state after:
R : Type x
inst✝ : Semiring R
a : Rˣ
b : R
⊢ ↑a + b = ↑a + ↑a * (↑a⁻¹ * 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 ∨ a + b = 0 ↔ a = b ∨ a = -b

Tactic:
add_eq_zero_iff_eq_neg

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + 2 * a * -b + b ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

Tactic:
mul_neg,

Goal state after:
R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + -(2 * a * b) + b ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + b ^ 2 + 2 * a * -b = a ^ 2 + b ^ 2 - 2 * a * b

Tactic:
mul_neg,

Goal state after:
R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + b ^ 2 + -(2 * a * b) = a ^ 2 + b ^ 2 - 2 * a * b
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
h : n = 0
⊢ ↑n = 0

Tactic:
by rw [h, cast_zero]

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

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

Tactic:
mul_neg,

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

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

Tactic:
mul_neg,

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) * 1 = 2 * (2 * a * b + b + a) + 1

Tactic:
mul_one,

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * a * (2 * b) + 1 * (2 * b) + (2 * a + 1) = 2 * (2 * a * b + b + a) + 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = 2 * -(k + 1) + 1

Tactic:
mul_neg,

Goal state after:
case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = -(2 * (k + 1)) + 1