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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
u : Mˣ × Nˣ
⊢ (↑u.1, ↑u.2) * (↑u.1⁻¹, ↑u.2⁻¹) = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
u : Mˣ × Nˣ
⊢ (↑u.1⁻¹, ↑u.2⁻¹) * (↑u.1, ↑u.2) = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
u : (M × N)ˣ
⊢ (fun u ↦ { val := (↑u.1, ↑u.2), inv := (↑u.1⁻¹, ↑u.2⁻¹), val_inv := ⋯, inv_val := ⋯ })
      (((Units.map (MonoidHom.fst M N)).prod (Units.map (MonoidHom.snd M N))) u) =
    u

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : Mˣ × Nˣ
u₁ : Mˣ
u₂ : Nˣ
⊢ ((Units.map (MonoidHom.fst M N)).prod (Units.map (MonoidHom.snd M N)))
      ((fun u ↦ { val := (↑u.1, ↑u.2), inv := (↑u.1⁻¹, ↑u.2⁻¹), val_inv := ⋯, inv_val := ⋯ }) (u₁, u₂)) =
    (u₁, u₂)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Subsingleton Mˣ
inst✝ : Subsingleton Nˣ
⊢ ∀ (a : M × N), IsUnit a → a = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
α : Type u_6
inst✝ : Monoid α
⊢ (↑1, op ↑1⁻¹) = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
α : Type u_6
inst✝ : Monoid α
x y : αˣ
⊢ (↑(x * y), op ↑(x * y)⁻¹) = (↑x, op ↑x⁻¹) * (↑y, op ↑y⁻¹)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ x <*> f <$> y = (fun x ↦ x ∘ f) <$> x <*> y

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
⊢ f <$> (x <*> y) = (fun x ↦ f ∘ x) <$> x <*> y

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : α → m β
⊢ f >=> pure = f

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
f : α → m β
⊢ pure >=> f = f

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β γ φ : Type u
f : α → m β
g : β → m γ
h : γ → m φ
⊢ (f >=> g) >=> h = f >=> g >=> h

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
f : α → β
a : m (m α)
⊢ joinM (Functor.map f <$> a) = f <$> joinM a

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
a : m (m (m α))
⊢ joinM (joinM <$> a) = joinM (joinM a)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
a : m α
⊢ joinM (pure <$> a) = a

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: F : Type → Type v
inst✝ : Alternative F
h : Decidable True
⊢ guard True = pure ()

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: F : Type → Type v
inst✝ : Alternative F
h : Decidable False
⊢ guard False = failure

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ LawfulFunctor (Sum e)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (x : e ⊕ α) (y : e ⊕ β), x <* y = Function.const β <$> x <*> y

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (x : e ⊕ α) (y : e ⊕ β), x *> y = Function.const α id <$> x <*> y

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (g : α → β) (x : e ⊕ α), pure g <*> x = g <$> x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (f : α → β) (x : e ⊕ α),
    (do
        let a ← x
        pure (f a)) =
      f <$> x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (f : e ⊕ (α → β)) (x : e ⊕ α),
    (do
        let x_1 ← f
        x_1 <$> x) =
      f <*> x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (x : α) (f : α → e ⊕ β), pure x >>= f = f x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β γ : Type u} (x : e ⊕ α) (f : α → e ⊕ β) (g : β → e ⊕ γ), x >>= f >>= g = x >>= fun x ↦ f x >>= g

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ f <$> a <*> b = (fun p ↦ f p.fst p.snd) <$> (Prod.mk <$> a <*> b)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun p ↦ f p.fst p.snd) <$> (Prod.mk <$> a <*> b) = (fun b a ↦ f a b) <$> b <*> a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FunProp.Decl

Goal state before:
pp: ⊢ Name

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.FunProp.Theorems

Goal state before:
pp: ⊢ Name

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.NeZero

Goal state before:
pp: R : Type u_1
inst✝ : Zero R
n : R
⊢ ¬NeZero n ↔ n = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsLeftCancelMulZero M₀
a b c : M₀
⊢ a * b = a * c ↔ b = c ∨ a = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsRightCancelMulZero M₀
a b c : M₀
⊢ a * c = b * c ↔ a = b ∨ c = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ x = 1 * x

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_2
inst✝¹ : Mul M₀
inst✝ : Zero M₀
⊢ IsCancelMulZero M₀ ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 1 * x = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 0 = 1 * y

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 1 * y = y

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
⊢ 1 ≠ 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬f 0 = f 1

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a⁻¹ * a = a⁻¹ * a * a⁻¹ * a⁻¹⁻¹

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a⁻¹ * a * a⁻¹ * a⁻¹⁻¹ = a⁻¹ * a⁻¹⁻¹

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a⁻¹ * a⁻¹⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
inst✝² : Mul N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : Nᵐᵒᵖ
z : N
⊢ x • y • z = y • x • z

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝ : Monoid α
⊢ Monoid.toMulAction αᵐᵒᵖ = instMulAction

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
⊢ ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Div M₀
inst✝ : MulDivCancelClass M₀
b a : M₀
ha : a ≠ 0
⊢ b * a / a = b

Tactic:
mul_div_cancel_right₀ _ ha

Goal state after:
M₀ : Type u_1
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Div M₀
inst✝ : MulDivCancelClass M₀
b a : M₀
ha : a ≠ 0
⊢ b = b
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: M₀ : Type u_1
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Div M₀
inst✝ : MulDivCancelClass M₀
b a : M₀
ha : a ≠ 0
⊢ a * b / a = b

Tactic:
by

Goal state after:
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 * b / b = a

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
inst✝ : IsRightCancelMulZero M₀
x : M₀
hx : x ^ 2 = x
x✝ : ¬x = 0
⊢ (fun a ↦ a * x) x = (fun a ↦ a * x) 1

Tactic:
by

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

Goal state before:
pp: G₀ : Type u
inst✝ : GroupWithZero G₀
b : G₀
h : b ≠ 0
a : G₀
⊢ a * (b * b⁻¹) = a

Tactic:
by

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

Goal state before:
pp: G₀ : Type u
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
b : G₀
⊢ a * a⁻¹ * b = b

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), x * y = 0 → y = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → (∀ (y : M₀), x * y = 0 → y = 0) ∧ ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
⊢ 0 = a * b ↔ a = 0 ∨ b = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a : M₀
⊢ a * a = 0 ↔ a = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a : M₀
⊢ 0 = a * a ↔ a = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
hb : b ≠ 0
⊢ a * b = 0 ↔ a = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
ha : a ≠ 0
⊢ a * b ≠ 0 ↔ b ≠ 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
hb : b ≠ 0
⊢ a * b ≠ 0 ↔ a ≠ 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
mul : ∀ (a b : M₀'), f (a * b) = f a * f b
a : M₀'
⊢ f (0 * a) = f 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
mul : ∀ (a b : M₀'), f (a * b) = f a * f b
a : M₀'
⊢ f (a * 0) = f 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀ → M₀'
hf : Surjective f
zero : f 0 = 0
mul : ∀ (a b : M₀), f (a * b) = f a * f b
x : M₀
⊢ 0 * f x = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀ → M₀'
hf : Surjective f
zero : f 0 = 0
mul : ∀ (a b : M₀), f (a * b) = f a * f b
x : M₀
⊢ f x * 0 = 0

Tactic:
by

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
⊢ f a * f b = 0

Tactic:
by

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

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

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

Goal state before:
pp: α : Type u_7
σ : Perm α
m n : ℤ
x : α
⊢ (σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x)

Tactic:
← Equiv.Perm.mul_apply,

Goal state after:
α : Type u_7
σ : Perm α
m n : ℤ
x : α
⊢ (σ ^ m * σ ^ n) x = (σ ^ n) ((σ ^ m) x)
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_7
σ : Perm α
m n : ℤ
x : α
⊢ (σ ^ m * σ ^ n) x = (σ ^ n) ((σ ^ m) x)

Tactic:
← Equiv.Perm.mul_apply,

Goal state after:
α : Type u_7
σ : Perm α
m n : ℤ
x : α
⊢ (σ ^ m * σ ^ n) x = (σ ^ n * σ ^ m) x
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_7
σ : Perm α
m n : ℤ
x : α
⊢ (σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x)

Tactic:
by

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

Goal state before:
pp: α : Type u_7
β : Type u_8
⊢ Function.Injective ⇑(sumCongrHom α β)

Tactic:
by

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

Goal state before:
pp: α : Type u_7
β : α → Type u_8
⊢ Function.Injective ⇑(sigmaCongrRightHom β)

Tactic:
by

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✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
this : f a✝ * f x✝¹ = f a✝ * f x✝
Hfa : f a✝ = 0
⊢ f a✝ = f 0

Tactic:
by

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✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
⊢ x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective ⇑(subtypeCongrHom p)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
p : α → Prop
f✝ f : Perm α
h : ∀ (x : α), p (f x) ↔ p x
x : { x // p x }
⊢ p (f (f⁻¹ ↑x))

Tactic:
by

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
p : α → Prop
f✝ f : Perm α
h : ∀ (x : α), p (f x) ↔ p x
x✝ : { x // p x }
⊢ (fun x ↦ ⟨f⁻¹ ↑x, ⋯⟩) ((fun x ↦ ⟨f ↑x, ⋯⟩) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
p : α → Prop
f✝ f : Perm α
h : ∀ (x : α), p (f x) ↔ p x
x✝ : { x // p x }
⊢ (fun x ↦ ⟨f ↑x, ⋯⟩) ((fun x ↦ ⟨f⁻¹ ↑x, ⋯⟩) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
⊢ (∀ (x : α), p (f (f⁻¹ x)) ↔ p (f⁻¹ x)) ↔ ∀ (x : α), p (f⁻¹ x) ↔ p x

Tactic:
by

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✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
this : f x✝¹ * f a✝ = f x✝ * f a✝
Hfa : f a✝ = 0
⊢ f a✝ = f 0

Tactic:
by

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✝ : IsRightCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
⊢ x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
n : ℕ
hf : ∀ (x : α), p (f x) ↔ p x
⊢ f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
⊢ ∀ (x : α), p ((f ^ Int.negSucc n) x) ↔ p x

Tactic:
by

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

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
n : ℤ
hf : ∀ (x : α), p (f x) ↔ p x
⊢ f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : a = 0
⊢ a * b = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : ¬a = 0
⊢ a * b = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
⊢ a * b = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

Tactic:
by

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
x : α
h : p x
⊢ p ((ofSubtype f) x) ↔ p x

Tactic:
by

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:
by

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
x : α
h : ¬p x
⊢ p ((ofSubtype f) x) ↔ p x

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
⊢ f 0⁻¹ = f 0

Tactic:
by

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective ⇑ofSubtype

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
⊢ (x ^ n.succ) ^ N = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝ : MonoidWithZero R
x : R
m : ℕ
h✝ : IsNilpotent (x ^ m)
n : ℕ
h : (x ^ m) ^ n = 0
⊢ x ^ (m * n) = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
hn : n ≠ 0
⊢ IsNilpotent (x ^ n)

Tactic:
by

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

Goal state before:
pp: R : Type u_5
inst✝¹ : Zero R
inst✝ : Pow R ℕ
h : ¬IsReduced R
⊢ ∃ x, x ≠ 0 ∧ IsNilpotent x

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 0 ^ (n + 1) = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
⊢ (swap x y * f) z = (f * swap (f⁻¹ x) (f⁻¹ y)) z

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y : α
⊢ f * swap x y = swap (f x) (f y) * f

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
⊢ 0 ^ n = if n = 0 then 1 else 0

Tactic:
by

Goal state after: