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

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

Tactic:
simpa using

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

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

Tactic:
apply Subset.antisymm

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

case h₂
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s ⊆ f '' (s₁ ∩ s)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case negSucc.succ
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i n : ℕ
ih : motive (-↑n)
⊢ motive (-↑(n + 1))

Tactic:
simpa using

Goal state after:
case negSucc.succ
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i n : ℕ
ih : motive (-↑n)
⊢ motive (-↑n + -1)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
y : α
hy : y ∈ s
⊢ f y ∈ g ⁻¹' s

Tactic:
simpa using

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
y : α
hy : y ∈ s
⊢ y ∈ s
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case pos
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : z = b
⊢ cast ⋯
      (match z - 1 - b with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match z - b with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))

Tactic:
rw! [show z - 1 - b = -[(b - z).toNat+1] by lia, show z - b = 0 by lia]

Goal state after:
case pos
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : z = b
⊢ cast ⋯
      (match -[(b - z).toNat+1] with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match 0 with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))
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✝¹ : Group G
H : Type u_8
inst✝ : Group H
f : G → H
hf : ∀ (x y : G), f (x / y) = f x / f y
⊢ ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹

Tactic:
simpa using

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✝¹ : Group G
H : Type u_8
inst✝ : Group H
f : G → H
hf : ∀ (x y : G), f (x / y) = f x / f y
⊢ ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ ∃ s', s ⊆ s' ∧ BijOn f s' t'

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ ∃ s', s ⊆ s' ∧ BijOn f s' t'
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
h : range f = {b}
a : α
⊢ f a = b

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
h : range f = {b}
a : α
⊢ f a = b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case mp
M : Type u_4
inst✝ : MulOneClass M
b : M
h : 1 * b = 1
⊢ b = 1

Tactic:
simpa using

Goal state after:
case mp
M : Type u_4
inst✝ : MulOneClass M
b : M
h : 1 * b = 1
⊢ b = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case mpr
M : Type u_4
inst✝ : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1

Tactic:
simpa using

Goal state after:
case mpr
M : Type u_4
inst✝ : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a⁻¹ * b = 1
⊢ a = b
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a * b⁻¹ = 1
⊢ a = b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
inst✝ : DivisionMonoid α
a b c d : α
⊢ 1⁻¹ = 1

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
inst✝ : DivisionMonoid α
a b c d : α
⊢ 1⁻¹ = 1
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : IsLeftCancelMul M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
H : (fun x_1 ↦ x * x_1) y = (fun x_1 ↦ x * x_1) z
⊢ ?m.31 x y z H * f y = ?m.31 x y z H * f z

Tactic:
simpa using

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : IsLeftCancelMul M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
H : (fun x_1 ↦ x * x_1) y = (fun x_1 ↦ x * x_1) z
⊢ ?m.31 x y z H * f y = ?m.31 x y z H * f z
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : IsRightCancelMul M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
H : (fun x_1 ↦ x_1 * x) y = (fun x_1 ↦ x_1 * x) z
⊢ f y * ?m.31 x y z H = f z * ?m.31 x y z H

Tactic:
simpa using

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : IsRightCancelMul M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
H : (fun x_1 ↦ x_1 * x) y = (fun x_1 ↦ x_1 * x) z
⊢ f y * ?m.31 x y z H = f z * ?m.31 x y z H
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : MulOne α
⊢ (∀ (a a_1 : α), opEquiv a * opEquiv a_1 = 1 → opEquiv a_1 * opEquiv a = 1) ↔ ∀ {a b : α}, a * b = 1 → b * a = 1

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : MulOne α
⊢ (∀ (a a_1 : α), a_1 * a = 1 → a * a_1 = 1) ↔ ∀ {a b : α}, a * b = 1 → b * a = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℕ
⊢ a ^ (↑m - ↑n) = a ^ m / a ^ n

Tactic:
simpa using

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (↑n - 1) = a ^ n / a

Tactic:
simpa using

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (1 - ↑n) = a / a ^ n

Tactic:
simpa using

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (1 - ↑n) = a * (a ^ n)⁻¹
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: case e_inv
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ i₁ = i₂

Tactic:
simpa using

Goal state after:
case e_inv
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
i₂ : α
vi₂ : v * i₂ = 1
iv₂ : i₂ * v = 1
⊢ i₁ = i₂
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
simpa using

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

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

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : Monoid α
a : αˣ
b c : α
h : b * ↑a = c * ↑a
⊢ b = c
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: F : Type u_1
G : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : FunLike F M N
inst✝³ : FunLike G N M
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass G N M
f : F
x : M
g : G
hfg : LeftInverse ⇑g ⇑f
h : IsUnit (f x)
⊢ IsUnit x

Tactic:
simpa using

Goal state after:
F : Type u_1
G : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : FunLike F M N
inst✝³ : FunLike G N M
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass G N M
f : F
x : M
g : G
hfg : LeftInverse ⇑g ⇑f
h : IsUnit (f x)
⊢ IsUnit x
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : Bijective fun x ↦ a * x
⊢ (fun x ↦ a * x) (⋯.choose * a) = (fun x ↦ a * x) 1

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
h : Bijective fun x ↦ a * x
⊢ a * (⋯.choose * a) = a
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : Bijective fun x ↦ x * a
⊢ (fun x ↦ x * a) (a * ⋯.choose) = (fun x ↦ x * a) 1

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
h : Bijective fun x ↦ x * a
⊢ a * (⋯.choose * a) = a
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
⊢ a * d = c * b

Tactic:
← mul_one a,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
b d : α
hb : IsUnit b
hd : IsUnit d
a c : α
h : a / b = c / d
⊢ a * 1 * d = c * b
Module: Mathlib.Algebra.Group.Units.Equiv

Goal state before:
pp: F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
x : M
hx : IsUnit (f x)
⊢ IsUnit x

Tactic:
simpa using

Goal state after:
F : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
x : M
hx : IsUnit (f x)
⊢ IsUnit x
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
f : M →ₙ* N × P
x : M
⊢ (((fst N P).comp f).prod ((snd N P).comp f)) x = f x

Tactic:
by simp only [prod_apply, coe_fst, coe_snd, comp_apply]

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:
simpa using

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
⊢ False
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:
simpa using

Goal state after:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
inst✝ : IsRightCancelMulZero M₀
x : M₀
hx : x ^ 2 = x
x✝ : ¬x = 0
⊢ x * x = x
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case left
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : α
⊢ fst✝¹ i = fst✝ i

Tactic:
simpa using

Goal state after:
case left
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : α
⊢ fst✝¹ i = fst✝ i
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case right
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ snd✝¹ i = snd✝ i

Tactic:
simpa using

Goal state after:
case right
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ snd✝¹ i = snd✝ i
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_7
β : α → Type u_8
x y : (a : α) → Perm (β a)
h : (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) y
a : α
b : β a
⊢ (x a) b = (y a) b

Tactic:
simpa using

Goal state after:
α : Type u_7
β : α → Type u_8
x y : (a : α) → Perm (β a)
h : (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) y
a : α
b : β a
⊢ (x a) b = (y a) b
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case left
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
i : { a // p a }
⊢ ↑(fst✝¹ i) = ↑(fst✝ i)

Tactic:
simpa using

Goal state after:
case left
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
i : { a // p a }
⊢ ↑(fst✝¹ i) = ↑(fst✝ i)
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case right
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
i : { a // ¬p a }
⊢ ↑(snd✝¹ i) = ↑(snd✝ i)

Tactic:
simpa using

Goal state after:
case right
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
i : { a // ¬p a }
⊢ ↑(snd✝¹ i) = ↑(snd✝ i)
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:
simpa using

Goal state after:
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 ↑x
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
← mul_one a,

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroOneClass M₀
h : 0 = 1
a : M₀
⊢ a * 1 = 0
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:
simpa using

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
x : α
h : p x
⊢ p ↑(f ⟨x, h⟩)
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:
simpa using

Goal state after:
R : Type u_5
inst✝¹ : Zero R
inst✝ : Pow R ℕ
h : ¬IsReduced R
⊢ ∃ x, IsNilpotent x ∧ ¬x = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
simpa using

Goal state after:
case zero
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
ha : a ^ 0 = 0
⊢ a = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
x : G₀
h : x ≠ 0
y y' : G₀
w : (fun y ↦ x * y) y = (fun y ↦ x * y) y'
⊢ y = y'

Tactic:
simpa using

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
x : G₀
h : x ≠ 0
y y' : G₀
w : (fun y ↦ x * y) y = (fun y ↦ x * y) y'
⊢ y = y'
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
x : G₀
h : x ≠ 0
y y' : G₀
w : (fun y ↦ y * x) y = (fun y ↦ y * x) y'
⊢ y = y'

Tactic:
simpa using

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
x : G₀
h : x ≠ 0
y y' : G₀
w : (fun y ↦ y * x) y = (fun y ↦ y * x) y'
⊢ y = y'
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ 1 / a ≠ 0

Tactic:
simpa using

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a⁻¹ ≠ 0
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✝⁵ : Zero M₀
inst✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom A A'
hf : Surjective ⇑f
smul : ∀ (a : M₀) (b : A), f (a • b) = a • f b
x : A
⊢ 0 • f x = 0

Tactic:
simp [← smul]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / (a / a) = a

Tactic:
div_div_eq_mul_div

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a / a = a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0

Tactic:
simpa using

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ ¬n = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
ι : Type u_12
inst✝ : DecidableEq ι
x : A
i j : ι
⊢ (if j = i then x else 0) = single i x j

Tactic:
single_apply

Goal state after:
M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
ι : Type u_12
inst✝ : DecidableEq ι
x : A
i j : ι
⊢ (if j = i then x else 0) = if j = i then x else 0
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m n : ℕ
h : ↑m = ↑n
⊢ m = n

Tactic:
induction m generalizing n with

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ 2 • x = x + x

Tactic:
rw [← one_add_one_eq_two, add_smul, one_smul]

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

Goal state before:
pp: α : Type u
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ a * (b - c) = a * b - a * c

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ a * (b + -c) = a * b + a * -c
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ (a - b) * c = a * c - b * c

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ (a + -b) * c = a * c + -b * c
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * (b - 1) = a * b - a

Tactic:
by rw [mul_sub, mul_one]

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

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * (1 - b) = a - a * b

Tactic:
by rw [mul_sub, mul_one]

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

Goal state before:
pp: n : ℕ
⊢ n.sqrt ^ 2 ≤ n

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ n.sqrt * n.sqrt ≤ n
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
⊢ n < n.sqrt.succ ^ 2

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ n < (n.sqrt + 1) * (n.sqrt + 1)
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m n : ℕ
⊢ m ≤ n.sqrt ↔ m ^ 2 ≤ n

Tactic:
simpa using

Goal state after:
m n : ℕ
⊢ m ≤ n.sqrt ↔ m * m ≤ n
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n a : ℕ
⊢ a = n.sqrt ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2

Tactic:
simpa using

Goal state after:
n a : ℕ
⊢ a = n.sqrt ↔ a * a ≤ n ∧ n < (a + 1) * (a + 1)
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: a n : ℕ
h : a ≤ n + n
⊢ (n ^ 2 + a).sqrt = n

Tactic:
simpa using

Goal state after:
a n : ℕ
h : a ≤ n + n
⊢ (n * n + a).sqrt = n
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: x : ℕ
⊢ (∃ n, n ^ 2 = x) ↔ x.sqrt ^ 2 = x

Tactic:
simpa using

Goal state after:
x : ℕ
⊢ (∃ n, n * n = x) ↔ x.sqrt * x.sqrt = x
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m n : ℕ
⊢ m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ t, t ^ 2 = n

Tactic:
simpa using

Goal state after:
m n : ℕ
⊢ m * m < n → n < (m + 1) * (m + 1) → ¬∃ t, t * t = n
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare a

Tactic:
simpa using

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare a
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
a : α
h : IsSquare a
⊢ IsSquare a⁻¹

Tactic:
simpa using

Goal state after:
case mpr
α : Type u_2
inst✝ : DivisionMonoid α
a : α
h : IsSquare a
⊢ IsSquare a⁻¹
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: case zero
⊢ IsSquare (sign 0) ↔ 0 ≤ 0

Tactic:
simpa using

Goal state after:
case zero
⊢ IsSquare 0
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
a b : α
x✝ : MulOpposite.op a ∣ MulOpposite.op b
c : αᵐᵒᵖ
hc : MulOpposite.op b = MulOpposite.op a * c
⊢ b = MulOpposite.unop c * a

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Semigroup α
a b : α
x✝ : MulOpposite.op a ∣ MulOpposite.op b
c : αᵐᵒᵖ
hc : MulOpposite.op b = MulOpposite.op a * c
⊢ b = MulOpposite.unop c * a
Module: Mathlib.Algebra.Group.Hom.Instances

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommGroup N
f : M →* N
n : ℤ
x y : M
⊢ (⇑f ^ n) (x * y) = (⇑f ^ n) x * (⇑f ^ n) y

Tactic:
simp [mul_zpow]

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

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

Tactic:
← inv_eq_one_div,

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
⊢ r⁻¹ʳ ^ 0 = (r ^ 0)⁻¹ʳ

Tactic:
rw [pow_zero, pow_zero, Ring.inverse_one]

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : a * ↑u = 0
⊢ a = 0

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : a * ↑u = 0
⊢ a = 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : ↑u * a = 0
⊢ a = 0

Tactic:
simpa using

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : ↑u * a = 0
⊢ a = 0
Module: Mathlib.Algebra.Ring.Semiconj

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a x y x' y' : R
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x - x') (y - y')

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a x y x' y' : R
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x + -x') (y + -y')