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

Goal state before:
pp: case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a * a).re = (↑(star a * a).re).re

pp: case imI
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a * a).imI = (↑(star a * a).re).imI

pp: case imJ
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a * a).imJ = (↑(star a * a).re).imJ

pp: case imK
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a * a).imK = (↑(star a * a).re).imK

Tactic:
<;>

Goal state after:
case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a * a).re = (↑(star a * a).re).re

case imI
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a * a).imI = (↑(star a * a).re).imI

case imJ
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a * a).imJ = (↑(star a * a).re).imJ

case imK
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (star a * a).imK = (↑(star a * a).re).imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imI + -(a.imI * a.re) + -(c₂ * a.imI * a.imI) + c₃ * a.imJ * a.imK + -(c₃ * a.imK * a.imJ) = 0

pp: case imJ
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) + -(c₂ * a.imJ * a.imI) + c₁ * a.imK * a.imI = 0

pp: case imK
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) = 0

Tactic:
<;>

Goal state after:
case imI
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imI + -(a.imI * a.re) + -(c₂ * a.imI * a.imI) + c₃ * a.imJ * a.imK + -(c₃ * a.imK * a.imJ) = 0

case imJ
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) + -(c₂ * a.imJ * a.imI) + c₁ * a.imK * a.imI = 0

case imK
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) = 0
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case a
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ (star a.im).re = (-a.im).re

pp: case a
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ (star a.im).imI = (-a.im).imI

pp: case a
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ (star a.im).imJ = (-a.im).imJ

pp: case a
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ (star a.im).imK = (-a.im).imK

Tactic:
<;>

Goal state after:
case a
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ (star a.im).re = (-a.im).re

case a
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ (star a.im).imI = (-a.im).imI

case a
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ (star a.im).imJ = (-a.im).imJ

case a
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ (star a.im).imK = (-a.im).imK
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: case inl
M : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : SMul M α
inst✝ : SMul M β
a : M
val✝ : α
⊢ (a • inl val✝).swap = a • (inl val✝).swap

pp: case inr
M : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : SMul M α
inst✝ : SMul M β
a : M
val✝ : β
⊢ (a • inr val✝).swap = a • (inr val✝).swap

Tactic:
<;>

Goal state after:
case inl
M : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : SMul M α
inst✝ : SMul M β
a : M
val✝ : α
⊢ (a • inl val✝).swap = a • (inl val✝).swap

case inr
M : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : SMul M α
inst✝ : SMul M β
a : M
val✝ : β
⊢ (a • inr val✝).swap = a • (inr val✝).swap
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq a + normSq b + (a * star b + b * star a).re = normSq a + normSq b + 2 * (a * star b).re

Tactic:
← star_mul_star a b,

Goal state after:
R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq a + normSq b + (a * star b + star (a * star b)).re = normSq a + normSq b + 2 * (a * star b).re
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case hfP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ ¬(Ideal.Quotient.mk P) f.leadingCoeff = 0

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem]

Goal state after:
case hfP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ f.leadingCoeff ∉ P
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a.re = QuaternionAlgebra.re 0

pp: case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a.imI = QuaternionAlgebra.imI 0

pp: case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a.imJ = QuaternionAlgebra.imJ 0

pp: case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a.imK = QuaternionAlgebra.imK 0

Tactic:
<;>

Goal state after:
case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a.re = QuaternionAlgebra.re 0

case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a.imI = QuaternionAlgebra.imI 0

case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a.imJ = QuaternionAlgebra.imJ 0

case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a.imK = QuaternionAlgebra.imK 0
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).re = (↑x✝¹ • x✝).re

pp: case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imI = (↑x✝¹ • x✝).imI

pp: case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imJ = (↑x✝¹ • x✝).imJ

pp: case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imK = (↑x✝¹ • x✝).imK

Tactic:
<;>

Goal state after:
case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).re = (↑x✝¹ • x✝).re

case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imI = (↑x✝¹ • x✝).imI

case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imJ = (↑x✝¹ • x✝).imJ

case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imK = (↑x✝¹ • x✝).imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).re = (↑x✝¹ • x✝).re

pp: case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imI = (↑x✝¹ • x✝).imI

pp: case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imJ = (↑x✝¹ • x✝).imJ

pp: case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imK = (↑x✝¹ • x✝).imK

Tactic:
<;>

Goal state after:
case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).re = (↑x✝¹ • x✝).re

case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imI = (↑x✝¹ • x✝).imI

case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imJ = (↑x✝¹ • x✝).imJ

case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imK = (↑x✝¹ • x✝).imK
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝² x✝¹ : ℕ+
x✝ : M × N
⊢ (x✝ ^ (x✝² + x✝¹)).1 = (x✝ ^ x✝² * x✝ ^ x✝¹).1

pp: case snd
M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝² x✝¹ : ℕ+
x✝ : M × N
⊢ (x✝ ^ (x✝² + x✝¹)).2 = (x✝ ^ x✝² * x✝ ^ x✝¹).2

Tactic:
<;>

Goal state after:
case fst
M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝² x✝¹ : ℕ+
x✝ : M × N
⊢ (x✝ ^ (x✝² + x✝¹)).1 = (x✝ ^ x✝² * x✝ ^ x✝¹).1

case snd
M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝² x✝¹ : ℕ+
x✝ : M × N
⊢ (x✝ ^ (x✝² + x✝¹)).2 = (x✝ ^ x✝² * x✝ ^ x✝¹).2
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 1).1 = x✝.1

pp: case snd
M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 1).2 = x✝.2

Tactic:
<;>

Goal state after:
case fst
M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 1).1 = x✝.1

case snd
M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 1).2 = x✝.2
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝² x✝¹ : ℕ
x✝ : M × N
⊢ (x✝ ^ (x✝² + x✝¹)).1 = (x✝ ^ x✝² * x✝ ^ x✝¹).1

pp: case snd
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝² x✝¹ : ℕ
x✝ : M × N
⊢ (x✝ ^ (x✝² + x✝¹)).2 = (x✝ ^ x✝² * x✝ ^ x✝¹).2

Tactic:
<;>

Goal state after:
case fst
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝² x✝¹ : ℕ
x✝ : M × N
⊢ (x✝ ^ (x✝² + x✝¹)).1 = (x✝ ^ x✝² * x✝ ^ x✝¹).1

case snd
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝² x✝¹ : ℕ
x✝ : M × N
⊢ (x✝ ^ (x✝² + x✝¹)).2 = (x✝ ^ x✝² * x✝ ^ x✝¹).2
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 0).1 = 1.1

pp: case snd
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 0).2 = 1.2

Tactic:
<;>

Goal state after:
case fst
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 0).1 = 1.1

case snd
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 0).2 = 1.2
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 1).1 = x✝.1

pp: case snd
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 1).2 = x✝.2

Tactic:
<;>

Goal state after:
case fst
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 1).1 = x✝.1

case snd
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 1).2 = x✝.2
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case inl
S : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : LinearOrder G
x✝ : SetLike S G
inst✝ : InvMemClass S G
H : S
x : G
h✝ : |x|ₘ = x
⊢ |x|ₘ ∈ H ↔ x ∈ H

pp: case inr
S : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : LinearOrder G
x✝ : SetLike S G
inst✝ : InvMemClass S G
H : S
x : G
h✝ : |x|ₘ = x⁻¹
⊢ |x|ₘ ∈ H ↔ x ∈ H

Tactic:
<;>

Goal state after:
case inl
S : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : LinearOrder G
x✝ : SetLike S G
inst✝ : InvMemClass S G
H : S
x : G
h✝ : |x|ₘ = x
⊢ |x|ₘ ∈ H ↔ x ∈ H

case inr
S : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : LinearOrder G
x✝ : SetLike S G
inst✝ : InvMemClass S G
H : S
x : G
h✝ : |x|ₘ = x⁻¹
⊢ |x|ₘ ∈ H ↔ x ∈ H
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
inst✝ : IsLeftCancelMulZero α
⊢ #∅ ≤ #(∅ * ∅)

pp: case inl.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
inst✝ : IsLeftCancelMulZero α
⊢ #{0} ≤ #({0} * {0})

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
inst✝ : IsLeftCancelMulZero α
⊢ #∅ ≤ #(∅ * ∅)

case inl.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
inst✝ : IsLeftCancelMulZero α
⊢ #{0} ≤ #({0} * {0})
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: case inl
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ (fst G₀ H₀) ((inl G₀ H₀) 0) = 0

pp: case inr
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : G₀ˣ
⊢ (fst G₀ H₀) ((inl G₀ H₀) ↑w✝) = ↑w✝

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ (fst G₀ H₀) ((inl G₀ H₀) 0) = 0

case inr
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : G₀ˣ
⊢ (fst G₀ H₀) ((inl G₀ H₀) ↑w✝) = ↑w✝
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: case inl
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ ((snd G₀ H₀).comp (inl G₀ H₀)) 0 = 1 0

pp: case inr
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : G₀ˣ
⊢ ((snd G₀ H₀).comp (inl G₀ H₀)) ↑w✝ = 1 ↑w✝

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ ((snd G₀ H₀).comp (inl G₀ H₀)) 0 = 1 0

case inr
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : G₀ˣ
⊢ ((snd G₀ H₀).comp (inl G₀ H₀)) ↑w✝ = 1 ↑w✝
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: case inl
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ ((fst G₀ H₀).comp (inr G₀ H₀)) 0 = 1 0

pp: case inr
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : H₀ˣ
⊢ ((fst G₀ H₀).comp (inr G₀ H₀)) ↑w✝ = 1 ↑w✝

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ ((fst G₀ H₀).comp (inr G₀ H₀)) 0 = 1 0

case inr
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : H₀ˣ
⊢ ((fst G₀ H₀).comp (inr G₀ H₀)) ↑w✝ = 1 ↑w✝
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
⊢ (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹

pp: case inl.inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
⊢ (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹

case inl.inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
⊢ (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹

pp: case inl.inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
⊢ (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹

case inl.inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: case inl
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ (snd G₀ H₀) ((inr G₀ H₀) 0) = 0

pp: case inr
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : H₀ˣ
⊢ (snd G₀ H₀) ((inr G₀ H₀) ↑w✝) = ↑w✝

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ (snd G₀ H₀) ((inr G₀ H₀) 0) = 0

case inr
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : H₀ˣ
⊢ (snd G₀ H₀) ((inr G₀ H₀) ↑w✝) = ↑w✝
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: case inl
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
n : H₀
⊢ Commute ((inl G₀ H₀) 0) ((inr G₀ H₀) n)

pp: case inr
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
n : H₀
w✝ : G₀ˣ
⊢ Commute ((inl G₀ H₀) ↑w✝) ((inr G₀ H₀) n)

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
n : H₀
⊢ Commute ((inl G₀ H₀) 0) ((inr G₀ H₀) n)

case inr
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
n : H₀
w✝ : G₀ˣ
⊢ Commute ((inl G₀ H₀) ↑w✝) ((inr G₀ H₀) n)
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: case inl.inl
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
⊢ Commute ((inl G₀ H₀) 0) ((inr G₀ H₀) 0)

pp: case inl.inr
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : H₀ˣ
⊢ Commute ((inl G₀ H₀) 0) ((inr G₀ H₀) ↑w✝)

pp: case inr.inl
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : G₀ˣ
⊢ Commute ((inl G₀ H₀) ↑w✝) ((inr G₀ H₀) 0)

pp: case inr.inr
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
w✝¹ : G₀ˣ
w✝ : H₀ˣ
⊢ Commute ((inl G₀ H₀) ↑w✝¹) ((inr G₀ H₀) ↑w✝)

Tactic:
<;>

Goal state after:
case inl.inl
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
⊢ Commute ((inl G₀ H₀) 0) ((inr G₀ H₀) 0)

case inl.inr
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : H₀ˣ
⊢ Commute ((inl G₀ H₀) 0) ((inr G₀ H₀) ↑w✝)

case inr.inl
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
w✝ : G₀ˣ
⊢ Commute ((inl G₀ H₀) ↑w✝) ((inr G₀ H₀) 0)

case inr.inr
G₀ : Type u_1
H₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero H₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
w✝¹ : G₀ˣ
w✝ : H₀ˣ
⊢ Commute ((inl G₀ H₀) ↑w✝¹) ((inr G₀ H₀) ↑w✝)
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := ⋯
zero : Zero α := ⋯
⊢ e 0 = 0

pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := ⋯
zero : Zero α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

Tactic:
<;>

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := ⋯
zero : Zero α := ⋯
⊢ e 0 = 0

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := ⋯
zero : Zero α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := ⋯
zero : Zero α := ⋯
⊢ e 0 = 0

pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
<;>

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := ⋯
zero : Zero α := ⋯
⊢ e 0 = 0

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

pp: case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := ⋯
mul : Mul α := ⋯
⊢ ∀ (a b : α), e (a * b) = e a * e b

Tactic:
<;>

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := ⋯
mul : Mul α := ⋯
⊢ e 0 = 0

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MulZeroClass β
zero : Zero α := ⋯
mul : Mul α := ⋯
⊢ ∀ (a b : α), e (a * b) = e a * e b