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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (↑(2 * a.re + c₂ * a.imI) - a) * a = a * (↑(2 * a.re + c₂ * a.imI) - a)

Tactic:
ext

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).re = (a * (↑(2 * a.re + c₂ * a.imI) - a)).re

case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).imI = (a * (↑(2 * a.re + c₂ * a.imI) - a)).imI

case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).imJ = (a * (↑(2 * a.re + c₂ * a.imI) - a)).imJ

case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).imK = (a * (↑(2 * a.re + c₂ * a.imI) - a)).imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ star ↑x = ↑x

Tactic:
ext

Goal state after:
case re
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ (star ↑x).re = (↑x).re

case imI
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ (star ↑x).imI = (↑x).imI

case imJ
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ (star ↑x).imJ = (↑x).imJ

case imK
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ (star ↑x).imK = (↑x).imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a.im = -a.im + ↑c₂ * ↑a.imI

Tactic:
ext

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

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

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

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

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

Tactic:
ext

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: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a.im = -a.im

Tactic:
ext

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.Quaternion

Goal state before:
pp: 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✝ = ↑x✝¹ • x✝

Tactic:
ext

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.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (a • s)⁻¹ = op a⁻¹ • s⁻¹

Tactic:
ext

Goal state after:
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ (a • s)⁻¹ ↔ a✝ ∈ op a⁻¹ • s⁻¹
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (op a • s)⁻¹ = a⁻¹ • s⁻¹

Tactic:
ext

Goal state after:
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ (op a • s)⁻¹ ↔ a✝ ∈ a⁻¹ • s⁻¹
Module: Mathlib.Algebra.Quaternion

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

Tactic:
ext

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.Ideal

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
s : Set M
x : M
⊢ x ∈ s ∪ univ * s ↔ x ∈ s ∨ ∃ y, ∃ z ∈ s, y * z = x

Tactic:
simp [mem_mul]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
⊢ x ∈ univ * s ↔ ∃ y, ∃ z ∈ s, y * z = x

Tactic:
simp [mem_mul]

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
n : ℕ
⊢ ⇑(fwdDiffₗ M G h ^ n) = Δ_[h]^[n]

Tactic:
ext

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
n : ℕ
x✝¹ : M → G
x✝ : M
⊢ (fwdDiffₗ M G h ^ n) x✝¹ x✝ = Δ_[h]^[n] x✝¹ x✝
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Mul (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ+
inst✝ : ∀ (i : ι), PNatPowAssoc (α i)
x✝² x✝¹ : ℕ+
x✝ : (i : ι) → α i
⊢ x✝ ^ (x✝² + x✝¹) = x✝ ^ x✝² * x✝ ^ x✝¹

Tactic:
ext

Goal state after:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Mul (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ+
inst✝ : ∀ (i : ι), PNatPowAssoc (α i)
x✝³ x✝² : ℕ+
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ (x✝³ + x✝²)) x✝ = (x✝¹ ^ x✝³ * x✝¹ ^ x✝²) x✝
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Mul (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ+
inst✝ : ∀ (i : ι), PNatPowAssoc (α i)
x✝ : (i : ι) → α i
⊢ x✝ ^ 1 = x✝

Tactic:
ext

Goal state after:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Mul (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ+
inst✝ : ∀ (i : ι), PNatPowAssoc (α i)
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ 1) x✝ = x✝¹ x✝
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: 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✝¹) = x✝ ^ x✝² * x✝ ^ x✝¹

Tactic:
ext

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: 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 = x✝

Tactic:
ext

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: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝² x✝¹ : ℕ
x✝ : (i : ι) → α i
⊢ x✝ ^ (x✝² + x✝¹) = x✝ ^ x✝² * x✝ ^ x✝¹

Tactic:
ext

Goal state after:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝³ x✝² : ℕ
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ (x✝³ + x✝²)) x✝ = (x✝¹ ^ x✝³ * x✝¹ ^ x✝²) x✝
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝ : (i : ι) → α i
⊢ x✝ ^ 0 = 1

Tactic:
ext

Goal state after:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ 0) x✝ = 1 x✝
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝ : (i : ι) → α i
⊢ x✝ ^ 1 = x✝

Tactic:
ext

Goal state after:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ 1) x✝ = x✝¹ x✝
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: 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✝¹) = x✝ ^ x✝² * x✝ ^ x✝¹

Tactic:
ext

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

Tactic:
ext

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: 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 = x✝

Tactic:
ext

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.ZPowers.Lemmas

Goal state before:
pp: A : Type u_4
inst✝ : AddGroupWithOne A
a : A
⊢ (∃ x, ↑x = a) ↔ ∃ k, k • 1 = a

Tactic:
zsmul_one

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: a b : ℤ
⊢ zmultiples a ⊓ zmultiples b = zmultiples ↑(a.lcm b)

Tactic:
ext

Goal state after:
a b x✝ : ℤ
⊢ x✝ ∈ zmultiples a ⊓ zmultiples b ↔ x✝ ∈ zmultiples ↑(a.lcm b)
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
f : G → α
⊢ τ 0 f = f

Tactic:
ext

Goal state after:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
f : G → α
x✝ : G
⊢ τ 0 f x✝ = f x✝
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ a (τ b f) = τ (a + b) f

Tactic:
ext

Goal state after:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
x✝ : G
⊢ τ a (τ b f) x✝ = τ (a + b) f x✝
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ (a + b) f = τ a (τ b f)

Tactic:
ext

Goal state after:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
x✝ : G
⊢ τ (a + b) f x✝ = τ a (τ b f) x✝
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a : G
f : G → α
⊢ τ a f = DomAddAct.mk (-a) +ᵥ f

Tactic:
ext

Goal state after:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a : G
f : G → α
x✝ : G
⊢ τ a f x✝ = (DomAddAct.mk (-a) +ᵥ f) x✝
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : AddCommMonoid M
a : G
f : ι → G → M
s : Finset ι
⊢ τ a (∑ i ∈ s, f i) = ∑ i ∈ s, τ a (f i)

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : AddCommMonoid M
a : G
f : ι → G → M
s : Finset ι
x✝ : G
⊢ τ a (∑ i ∈ s, f i) x✝ = (∑ i ∈ s, τ a (f i)) x✝
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: G : Type u_5
H : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
f : G → H
⊢ support (τ a f) = a +ᵥ support f

Tactic:
ext

Goal state after:
G : Type u_5
H : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
f : G → H
x✝ : G
⊢ x✝ ∈ support (τ a f) ↔ x✝ ∈ a +ᵥ support f
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : CommMonoid M
a : G
f : ι → G → M
s : Finset ι
⊢ τ a (∏ i ∈ s, f i) = ∏ i ∈ s, τ a (f i)

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : CommMonoid M
a : G
f : ι → G → M
s : Finset ι
x✝ : G
⊢ τ a (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, τ a (f i)) x✝
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: case e'_3.e'_3
M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
⊢ ⋂ s ∈ f, ↑s = (sInf (toSubmonoid '' f)).1.carrier

Tactic:
ext

Goal state after:
case e'_3.e'_3
M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
x✝ : M
⊢ x✝ ∈ ⋂ s ∈ f, ↑s ↔ x✝ ∈ (sInf (toSubmonoid '' f)).1.carrier
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
⊢ 0⁻¹ = 0

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ ∈ 0⁻¹ ↔ a✝ ∈ 0
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹

Tactic:
ext

Goal state after:
case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
a✝ : α
⊢ a✝ ∈ (a •> s)⁻¹ ↔ a✝ ∈ s⁻¹ <• a⁻¹
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹

Tactic:
ext

Goal state after:
case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
a✝ : α
⊢ a✝ ∈ (s <• a)⁻¹ ↔ a✝ ∈ a⁻¹ •> s⁻¹
Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances

Goal state before:
pp: H : Type u_2
inst✝ : CommGroupWithZero H
⊢ MonoidHom.mker MonoidWithZero.inverse = ⊥

Tactic:
ext

Goal state after:
H : Type u_2
inst✝ : CommGroupWithZero H
x✝ : H
⊢ x✝ ∈ MonoidHom.mker MonoidWithZero.inverse ↔ x✝ ∈ ⊥
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝³ : Monoid M
inst✝² : LinearOrder S
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
⊢ v i ∈ closure (v '' {i | 1 < f (v i)}) ↔ 1 < f (v i)

Tactic:
refine ⟨fun hi ↦ ?_, fun hi ↦ subset_closure <| mem_image_of_mem v hi⟩

Goal state after:
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝³ : Monoid M
inst✝² : LinearOrder S
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
⊢ 1 < f (v i)
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : B
⊢ (∃ x_1, (∃ y, f y = ↑x_1) ∧ ↑x_1 = x) ↔ (∃ y, f y = x) ∧ ¬x = 0

Tactic:
constructor

Goal state after:
case mp
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : B
⊢ (∃ x_1, (∃ y, f y = ↑x_1) ∧ ↑x_1 = x) → (∃ y, f y = x) ∧ ¬x = 0

case mpr
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : B
⊢ (∃ y, f y = x) ∧ ¬x = 0 → ∃ x_1, (∃ y, f y = ↑x_1) ∧ ↑x_1 = x
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X : FintypeCat
f : X.obj → X.obj
⊢ homMk f = 𝟙 X ↔ f = id

Tactic:
constructor

Goal state after:
case mp
X : FintypeCat
f : X.obj → X.obj
⊢ homMk f = 𝟙 X → f = id

case mpr
X : FintypeCat
f : X.obj → X.obj
⊢ f = id → homMk f = 𝟙 X
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h : X.obj → Z.obj
⊢ homMk h = homMk f ≫ homMk g ↔ h = g ∘ f

Tactic:
constructor

Goal state after:
case mp
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h : X.obj → Z.obj
⊢ homMk h = homMk f ≫ homMk g → h = g ∘ f

case mpr
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h : X.obj → Z.obj
⊢ h = g ∘ f → homMk h = homMk f ≫ homMk g
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x ↦ a₂, monotone' := ⋯ }
⊢ g₁ ≫ f = g₂ ≫ f

Tactic:
ext

Goal state after:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x ↦ a₂, monotone' := ⋯ }
x✝ : ↑X.toLinOrd
⊢ (LinOrd.Hom.hom (g₁ ≫ f).hom) x✝ = (LinOrd.Hom.hom (g₂ ≫ f).hom) x✝
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
constructor

Goal state after:
case mp
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)

case mpr
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }

Tactic:
exfalso
          exact h₁ (h.trans h₂)

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete C → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete C
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (s.ι ≫ e) ≫ (Fork.ofι i ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι i ⋯).pt}, m ≫ (Fork.ofι i ⋯).ι = s.ι → m = s.ι ≫ e

Tactic:
constructor

Goal state after:
case left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (s.ι ≫ e) ≫ (Fork.ofι i ⋯).ι = s.ι

case right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ ∀ {m : s.pt ⟶ (Fork.ofι i ⋯).pt}, m ≫ (Fork.ofι i ⋯).ι = s.ι → m = s.ι ≫ e
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯ = 𝟙 (equalizer (𝟙 X) p)

Tactic:
ext

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ (equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯) ≫ equalizer.ι (𝟙 X) p = 𝟙 (equalizer (𝟙 X) p) ≫ equalizer.ι (𝟙 X) p
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g ↔ f.f = g.f

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g → f.f = g.f

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g