mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
c : α
⊢ a * c ∣ b * c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
n : ℕ
⊢ a ^ n ∣ b ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
m n : ℕ
hab : a ∣ b
hmn : m ≤ n
⊢ a ^ m ∣ b ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: p : Prop
⊢ [p].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: a b : Prop
l : List Prop
h : b ∈ l
H : (a :: l).TFAE
⊢ a ∈ a :: l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: a b : Prop
l : List Prop
h : b ∈ l
⊢ (a ↔ b) ∧ l.TFAE → (a :: l).TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: a : Prop
l : List Prop
⊢ (a :: a :: l).TFAE ↔ (a :: l).TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: a b : Prop
l : List Prop
h_chain : IsChain (fun x1 x2 ↦ x1 → x2) (a :: b :: l)
h_last : l.getLastD b → a
⊢ (a :: b :: l).TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
⊢ (map (fun p ↦ ∀ (a : α), p a) l).TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
⊢ (map (fun p ↦ ∃ a, p a) l).TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: l : List Prop
⊢ (map Not l).TFAE ↔ l.TFAE

Tactic:
by

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

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : One M
inst✝ : Monoid N
f : OneHom M N
n : ℕ
⊢ (⇑f ^ n) 1 = 1

Tactic:
by

Goal state after:
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✝ : CommMonoid N
f : M →* N
n : ℕ
⊢ (⇑f ^ n) 1 = 1

Tactic:
by

Goal state after:
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✝ : CommMonoid N
f : M →* N
n : ℕ
x y : M
⊢ (⇑f ^ n) (x * y) = (⇑f ^ n) x * (⇑f ^ n) y

Tactic:
by

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

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : One M
inst✝ : Group N
f : OneHom M N
n : ℤ
⊢ (⇑f ^ n) 1 = 1

Tactic:
by

Goal state after:
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 : ℤ
⊢ (⇑f ^ n) 1 = 1

Tactic:
by

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

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

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
mM : MulOneClass M
mN : MulOneClass N
mP : CommMonoid P
f : M →* N →* P
y : N
⊢ (f 1) y = 1

Tactic:
by

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

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
mM : MulOneClass M
mN : MulOneClass N
mP : CommMonoid P
f : M →* N →* P
y : N
x₁ x₂ : M
⊢ (f (x₁ * x₂)) y = (f x₁) y * (f x₂) y

Tactic:
by

Goal state after:
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✝¹ : CommMonoid N
inst✝ : CommMonoid P
⊢ { toFun := comp 1, map_one' := ⋯, map_mul' := ⋯ } = 1

Tactic:
by

Goal state after:
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✝¹ : CommMonoid N
inst✝ : CommMonoid P
g₁ g₂ : N →* P
⊢ { toFun := (g₁ * g₂).comp, map_one' := ⋯, map_mul' := ⋯ } =
    { toFun := g₁.comp, map_one' := ⋯, map_mul' := ⋯ } * { toFun := g₂.comp, map_one' := ⋯, map_mul' := ⋯ }

Tactic:
by

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
⊢ -(x * x - b * x) = x * (b - x)

Tactic:
by

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
this : c = x * (b - x)
⊢ x + (b - x) = b

Tactic:
by

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
this : c = x * (b - x)
⊢ x * (b - x) = c

Tactic:
by

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

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

Goal state before:
pp: α : Type u_3
inst✝¹ : NonAssocRing α
inst✝ : Nontrivial α
a : α
h : a + 1 = a
⊢ a + 1 = a + 0

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝¹ : NonAssocRing α
inst✝ : Nontrivial α
a : α
h : a - 1 = a
⊢ a + -1 = a + -0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : IsLeftRegular r
r' : R
eq : r * r' = 0
⊢ (fun x ↦ r * x) r' = (fun x ↦ r * x) 0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), r * x = 0 → x = 0
r₁ r₂ : R
eq : (fun x ↦ r * x) r₁ = (fun x ↦ r * x) r₂
⊢ r * (r₁ - r₂) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : IsRightRegular r
r' : R
eq : r' * r = 0
⊢ (fun x ↦ x * r) r' = (fun x ↦ x * r) 0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
r₁ r₂ : R
eq : (fun x ↦ x * r) r₁ = (fun x ↦ x * r) r₂
⊢ (r₁ - r₂) * r = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
⊢ IsRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
m n : ℕ
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
⊢ n • a = a * ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonAssocSemiring α
n : ℕ
inst✝ : n.AtLeastTwo
a : α
⊢ OfNat.ofNat n • a = OfNat.ofNat n * a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
m : ℕ
⊢ ↑(m ^ 0) = ↑m ^ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
m n : ℕ
⊢ ↑(m ^ (n + 1)) = ↑m ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : f 1 = 1
⊢ f 0 = ↑0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R].TFAE

Tactic:
by

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

Goal state before:
pp: A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : f 1 = 1
n : ℕ
⊢ f (n + 1) = ↑(n + 1)

Tactic:
by

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

Goal state before:
pp: B : Type u_4
F : Type u_5
inst✝³ : AddMonoidWithOne B
A : Type u_6
inst✝² : AddMonoidWithOne A
inst✝¹ : FunLike F A B
inst✝ : AddMonoidHomClass F A B
f : F
h : f 1 = 1
⊢ ((↑f).comp (Nat.castAddMonoidHom A)) 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Semiring α
⊢ IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
⊢ IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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 / (-1 * a) = 1 / a * (1 / -1)

Tactic:
by

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) = 1 / a * -1

Tactic:
by

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

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

Goal state before:
pp: A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : ZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
⊢ f = g

Tactic:
by

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

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

Goal state before:
pp: R : Type u_3
F : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : FunLike F ℕ R
inst✝ : RingHomClass F ℕ R
f g : F
⊢ f 1 = g 1

Tactic:
by

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 * (1 / -a) = b * -(1 / a)

Tactic:
by

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

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
F : Type u_8
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
n : ℕ
hn : NeZero ↑n
⊢ NeZero (f ↑n)

Tactic:
by

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 * -(1 / a) = -(b * (1 / a))

Tactic:
by

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 * (1 / a)) = -(b / a)

Tactic:
by

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 / a)

Tactic:
by

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 / a

Tactic:
by

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
⊢ -a / -b = a / b

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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✝¹ : NonUnitalNonAssocSemiring α
inst✝ : NonUnitalNonAssocSemiring β
f g : α →ₙ+* β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
⊢ ∃ x y, x < y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
x : Subtype p
⊢ Nontrivial (Subtype p) ↔ ∃ y x_1, y ≠ x.val

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Inhabited α
h : ¬Nontrivial α
x : α
⊢ x = default

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
⊢ g.comp 0 = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
⊢ Nontrivial (Option α)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
f : α →ₙ+* β
⊢ comp 0 f = 0

Tactic:
by

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

Goal state before:
pp: I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
⊢ Nontrivial ((i : I) → f i)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
by

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
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f g : α →+* β
h : (fun f ↦ (↑f.toMonoidHom).toFun) f = (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ ⇑f.toMonoidWithZeroHom = ⇑f

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ 0 = 1 ↔ f 1 = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
h : f 1 = 0
x : α
⊢ f x = 0

Tactic:
by

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
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f : α →+* β
⊢ g (f 1) = 1

Tactic:
by

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
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
n : ℕ
f : α →+* α
⊢ (⇑f)^[n] = ⇑(npowRec n f)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
by

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 : β
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
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
⊢ ↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) = f

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ a * ↑x⁻¹ = ↑y⁻¹ * (↑y * a) * ↑x⁻¹

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ ↑y⁻¹ * (↑y * a) * ↑x⁻¹ = ↑y⁻¹ * a

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a) x y
⊢ ↑a⁻¹ * y = ↑a⁻¹ * (y * ↑a * ↑a⁻¹)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Mˣ
x y : M
h : SemiconjBy (↑a) x y
⊢ ↑a⁻¹ * (y * ↑a * ↑a⁻¹) = x * ↑a⁻¹

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
n : ℕ
⊢ SemiconjBy a ↑(x ^ ↑n) ↑(y ^ ↑n)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
n : ℕ
⊢ SemiconjBy a ↑(x ^ -[n+1]) ↑(y ^ -[n+1])

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : MulZeroClass G₀
a : G₀
⊢ SemiconjBy a 0 0

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : MulZeroClass G₀
x y : G₀
⊢ SemiconjBy 0 x y

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
ha : a = 0
⊢ SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ ↑n) (y ^ ↑n)

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b c : M₀
ha : IsUnit a
k : ℕ
⊢ a⁻¹ʳ ^ k * b = c ↔ b = a ^ k * c

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a / b) c

Tactic:
by

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

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 : ↑u * a = 0
⊢ a = 0

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x✝ : IsUnit 0
a : M₀
a0 : 0 * a = 1
inv_val✝ : a * 0 = 1
⊢ 0 = 1

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ (↑u)⁻¹ʳ = ↑u⁻¹

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
h : IsUnit x
⊢ x * x⁻¹ʳ = 1

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
h : IsUnit x
⊢ x⁻¹ʳ * x = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * x * x⁻¹ʳ = y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Distrib R
a b x y : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a + b) x y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy a (-x) (-y)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy (-a) x y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : MulOneClass R
inst✝ : HasDistribNeg R
a : R
⊢ SemiconjBy a (-1) (-1)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : MulOneClass R
inst✝ : HasDistribNeg R
x : R
⊢ SemiconjBy (-1) x x

Tactic:
by

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

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * x⁻¹ʳ * x = y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a b x y : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a - b) x y

Tactic:
by

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

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

Tactic:
by

Goal state after: