mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
⊢ l₁ ≤ i ∨ l₂ ≤ j

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0

Tactic:
let (i : Fin 6) : AddCommGroup (Vs i) := match i with
  | 0 => ‹_› | 1 => ‹_› | 2 => ‹_› | 3 => ‹_› | 4 => ‹_› | 5 => ‹_›

Goal state after:
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
this : (i : Fin 6) → AddCommGroup (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁷
    | 1 => inst✝¹⁴
    | 2 => inst✝¹¹
    | 3 => inst✝⁸
    | 4 => inst✝⁵
    | 5 => inst✝²
⊢ ↑(finrank k V₀) - ↑(finrank k V₁) + ↑(finrank k V₂) - ↑(finrank k V₃) + ↑(finrank k V₄) - ↑(finrank k V₅) = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (-f - μ • 1).ker ≠ ⊥ ↔ (f - -μ • 1).ker ≠ ⊥

Tactic:
← LinearMap.ker_neg

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (-(-f - μ • 1)).ker ≠ ⊥ ↔ (f - -μ • 1).ker ≠ ⊥
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
head_eq✝ : (x, b) = a
H : (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3

Tactic:
r,

Goal state after:
case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
head_eq✝ : (x, b) = a
H : (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case inl
α : Type u
inst✝ : Nonempty α
hR : Finite α
x : Fintype α
⊢ Nonempty (CommRing α)

Tactic:
have : NeZero (Fintype.card α) := ⟨by simp⟩

Goal state after:
case inl
α : Type u
inst✝ : Nonempty α
hR : Finite α
x : Fintype α
this : NeZero (Fintype.card α)
⊢ Nonempty (CommRing α)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : AddZeroClass R
⊢ ↑(x + y) = ↑x + ↑y

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ ↑(-x) = -↑x

Tactic:
ext <;> simp

Goal state after:
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
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ 1 * x✝ = x✝

Tactic:
ext <;> simp

Goal state after:
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
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝ * 1 = x✝

Tactic:
ext <;> simp

Goal state after:
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
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ 0 * x✝ = 0

Tactic:
ext <;> simp

Goal state after:
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
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝ * 0 = 0

Tactic:
ext <;> simp

Goal state after:
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
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝

Tactic:
ext <;> simp

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
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝².re * (x✝¹.re + x✝.re) + c₁ * x✝².imI * (x✝¹.imI + x✝.imI) + c₃ * x✝².imJ * (x✝¹.imJ + x✝.imJ) +
        c₂ * c₃ * x✝².imJ * (x✝¹.imK + x✝.imK) -
      c₁ * c₃ * x✝².imK * (x✝¹.imK + x✝.imK) =
    x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
        c₁ * c₃ * x✝².imK * x✝¹.imK +
      (x✝².re * x✝.re + c₁ * x✝².imI * x✝.imI + c₃ * x✝².imJ * x✝.imJ + c₂ * c₃ * x✝².imJ * x✝.imK -
        c₁ * c₃ * x✝².imK * x✝.imK)

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
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝².re * (x✝¹.imI + x✝.imI) + x✝².imI * (x✝¹.re + x✝.re) + c₂ * x✝².imI * (x✝¹.imI + x✝.imI) -
        c₃ * x✝².imJ * (x✝¹.imK + x✝.imK) +
      c₃ * x✝².imK * (x✝¹.imJ + x✝.imJ) =
    x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK + c₃ * x✝².imK * x✝¹.imJ +
      (x✝².re * x✝.imI + x✝².imI * x✝.re + c₂ * x✝².imI * x✝.imI - c₃ * x✝².imJ * x✝.imK + c₃ * x✝².imK * x✝.imJ)

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
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝².re * (x✝¹.imJ + x✝.imJ) + c₁ * x✝².imI * (x✝¹.imK + x✝.imK) + x✝².imJ * (x✝¹.re + x✝.re) +
        c₂ * x✝².imJ * (x✝¹.imI + x✝.imI) -
      c₁ * x✝².imK * (x✝¹.imI + x✝.imI) =
    x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI - c₁ * x✝².imK * x✝¹.imI +
      (x✝².re * x✝.imJ + c₁ * x✝².imI * x✝.imK + x✝².imJ * x✝.re + c₂ * x✝².imJ * x✝.imI - c₁ * x✝².imK * x✝.imI)

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
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝².re * (x✝¹.imK + x✝.imK) + x✝².imI * (x✝¹.imJ + x✝.imJ) + c₂ * x✝².imI * (x✝¹.imK + x✝.imK) -
        x✝².imJ * (x✝¹.imI + x✝.imI) +
      x✝².imK * (x✝¹.re + x✝.re) =
    x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re +
      (x✝².re * x✝.imK + x✝².imI * x✝.imJ + c₂ * x✝².imI * x✝.imK - x✝².imJ * x✝.imI + x✝².imK * x✝.re)
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
inj : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
y : R
⊢ IsIntegral R ((algebraMap R A) y)

Tactic:
apply isIntegral_algebraMap

Goal state after:
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
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
ext <;> simp

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
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re + x✝¹.re) * x✝.re + c₁ * (x✝².imI + x✝¹.imI) * x✝.imI + c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imJ +
        c₂ * c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imK -
      c₁ * c₃ * (x✝².imK + x✝¹.imK) * x✝.imK =
    x✝².re * x✝.re + c₁ * x✝².imI * x✝.imI + c₃ * x✝².imJ * x✝.imJ + c₂ * c₃ * x✝².imJ * x✝.imK -
        c₁ * c₃ * x✝².imK * x✝.imK +
      (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
        c₁ * c₃ * x✝¹.imK * x✝.imK)

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
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re + x✝¹.re) * x✝.imI + (x✝².imI + x✝¹.imI) * x✝.re + c₂ * (x✝².imI + x✝¹.imI) * x✝.imI -
        c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imK +
      c₃ * (x✝².imK + x✝¹.imK) * x✝.imJ =
    x✝².re * x✝.imI + x✝².imI * x✝.re + c₂ * x✝².imI * x✝.imI - c₃ * x✝².imJ * x✝.imK + c₃ * x✝².imK * x✝.imJ +
      (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ)

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
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re + x✝¹.re) * x✝.imJ + c₁ * (x✝².imI + x✝¹.imI) * x✝.imK + (x✝².imJ + x✝¹.imJ) * x✝.re +
        c₂ * (x✝².imJ + x✝¹.imJ) * x✝.imI -
      c₁ * (x✝².imK + x✝¹.imK) * x✝.imI =
    x✝².re * x✝.imJ + c₁ * x✝².imI * x✝.imK + x✝².imJ * x✝.re + c₂ * x✝².imJ * x✝.imI - c₁ * x✝².imK * x✝.imI +
      (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI - c₁ * x✝¹.imK * x✝.imI)

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
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re + x✝¹.re) * x✝.imK + (x✝².imI + x✝¹.imI) * x✝.imJ + c₂ * (x✝².imI + x✝¹.imI) * x✝.imK -
        (x✝².imJ + x✝¹.imJ) * x✝.imI +
      (x✝².imK + x✝¹.imK) * x✝.re =
    x✝².re * x✝.imK + x✝².imI * x✝.imJ + c₂ * x✝².imI * x✝.imK - x✝².imJ * x✝.imI + x✝².imK * x✝.re +
      (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re)
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case mp
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : integralClosure R A ≤ ⊥
y : R
⊢ IsIntegral R ((algebraMap R A) y)

Tactic:
apply isIntegral_algebraMap

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : CommRing R
⊢ ↑(x * y) = ↑x * ↑y

Tactic:
ext <;> simp

Goal state after:
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
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ { re := (x✝¹ * x✝).re, imI := (x✝¹ * x✝).imJ, imJ := (x✝¹ * x✝).imI, imK := -(x✝¹ * x✝).imK } =
    { re := x✝¹.re, imI := x✝¹.imJ, imJ := x✝¹.imI, imK := -x✝¹.imK } *
      { re := x✝.re, imI := x✝.imJ, imJ := x✝.imI, imK := -x✝.imK }

Tactic:
ext <;> simp

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
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ - c₁ * c₃ * x✝¹.imK * x✝.imK =
    x✝¹.re * x✝.re + c₃ * x✝¹.imJ * x✝.imJ + c₁ * x✝¹.imI * x✝.imI - c₃ * c₁ * x✝¹.imK * x✝.imK

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
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re - c₁ * x✝¹.imK * x✝.imI =
    x✝¹.re * x✝.imJ + x✝¹.imJ * x✝.re + c₁ * x✝¹.imI * x✝.imK + -(c₁ * x✝¹.imK * x✝.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
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ x✝¹.re * x✝.imI + x✝¹.imI * x✝.re - c₃ * x✝¹.imJ * x✝.imK =
    x✝¹.re * x✝.imI + -(c₃ * x✝¹.imJ * x✝.imK) + x✝¹.imI * x✝.re

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
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ -(x✝¹.imK * x✝.re) + (x✝¹.imJ * x✝.imI - (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ)) =
    -(x✝¹.re * x✝.imK) + x✝¹.imJ * x✝.imI - x✝¹.imI * x✝.imJ + -(x✝¹.imK * x✝.re)
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
a b : ℍ[R,c₁,c₂,c₃]
⊢ star (a * b) = star b * star a

Tactic:
ext <;> simp

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ a.re * b.re + c₁ * a.imI * b.imI + c₃ * a.imJ * b.imJ + c₂ * c₃ * a.imJ * b.imK - c₁ * c₃ * a.imK * b.imK +
      c₂ * (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI - c₃ * a.imJ * b.imK + c₃ * a.imK * b.imJ) =
    (b.re + c₂ * b.imI) * (a.re + c₂ * a.imI) + c₁ * b.imI * a.imI + c₃ * b.imJ * a.imJ + c₂ * c₃ * b.imJ * a.imK -
      c₁ * c₃ * b.imK * a.imK

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ -(c₃ * a.imK * b.imJ) + (c₃ * a.imJ * b.imK - (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI)) =
    -((b.re + c₂ * b.imI) * a.imI) + -(b.imI * (a.re + c₂ * a.imI)) + c₂ * b.imI * a.imI - c₃ * b.imJ * a.imK +
      c₃ * b.imK * a.imJ

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ c₁ * a.imK * b.imI - (a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re + c₂ * a.imJ * b.imI) =
    -((b.re + c₂ * b.imI) * a.imJ) + c₁ * b.imI * a.imK + -(b.imJ * (a.re + c₂ * a.imI)) + c₂ * b.imJ * a.imI -
      c₁ * b.imK * a.imI

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ -(a.imK * b.re) + (a.imJ * b.imI - (a.re * b.imK + a.imI * b.imJ + c₂ * a.imI * b.imK)) =
    -((b.re + c₂ * b.imI) * a.imK) + b.imI * a.imJ + c₂ * b.imI * a.imK - b.imJ * a.imI + -(b.imK * (a.re + c₂ * a.imI))
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 <;> simp

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.re) * a.re = a.re * (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.re) * a.imI + -(a.imI * a.re) = -(a.re * a.imI) + a.imI * (2 * a.re + c₂ * a.imI - a.re)

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.re) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) =
    -(a.re * a.imJ) + -(c₁ * a.imI * a.imK) + a.imJ * (2 * a.re + c₂ * a.imI - a.re)

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.re) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) =
    -(a.re * a.imK) + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + a.imK * (2 * a.re + c₂ * a.imI - a.re)
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 <;> simp

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

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
b : Option α
⊢ 1 • b = b

Tactic:
by
    cases b
    exacts [rfl, congr_arg some (one_smul _ _)]

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

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.Group.Action.Sigma

Goal state before:
pp: case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
fst✝ : ι
snd✝ : α fst✝
⊢ 1 • ⟨fst✝, snd✝⟩ = ⟨fst✝, snd✝⟩

Tactic:
rw [smul_mk, one_smul]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a.re + 0 * a.imI = a.re

Tactic:
zero_mul,

Goal state after:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a.re + 0 = a.re
Module: Mathlib.Algebra.Quaternion

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

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a.im ^ 2 = -↑(normSq a.im)

Tactic:
by
  simp_rw [sq, ← star_mul_self, star_im, neg_mul, neg_neg]

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

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

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

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this✝ : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range j
this : i < j
⊢ i < n

Tactic:
lia

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this✝ : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range n
this : i < n
⊢ i < n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case inv
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x✝ x : M
hx : x ∈ closure (Set.range f)
hx' : ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∃ a, x⁻¹ = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
obtain ⟨a, rfl⟩ := hx'
    use -a
    rw [Finsupp.prod_neg_index]
    · simp
    · simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
a : C
ha : (∃ y_1 ∈ x, ∃ z ∈ y, y_1 * z = a) ∧ a ∈ z
⊢ a ∈ x ⊔ y ⊓ z

Tactic:
rcases ha with ⟨⟨b, hb, c, hc, rfl⟩, haz⟩

Goal state after:
C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
b : C
hb : b ∈ x
c : C
hc : c ∈ y
haz : b * c ∈ z
⊢ b * c ∈ x ⊔ y ⊓ z
Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances

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

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
j : Fin (n + 1)
⊢ j ≤ j

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
⊢ j < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
⊢ j + l < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ↑i + j < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin 2
⊢ ↑i✝ + j = j + ↑i✝

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin 2
⊢ ↑i✝ + 1 + j = j + ↑i✝ + 1

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i✝ : Fin l
i : Fin 2
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x ↦
                  match x with
                  | 0 => i✝.castSucc
                  | 1 => i✝.succ,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        i) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x ↦
                match x with
                | 0 => ⟨j + ↑i✝, ⋯⟩.castSucc
                | 1 => ⟨j + ↑i✝, ⋯⟩.succ,
              monotone' := ⋯ }))
        i)

Tactic:
match i with | 0 | 1 => simp; lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
⊢ l + j = j + l

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
⊢ (toKaroubi C).essImage P

Tactic:
rcases IsIdempotentComplete.idempotents_split P.X P.p P.idem with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
    use Y
    exact
      Nonempty.intro
        { hom := ⟨i, by simp [← Category.assoc, h₁, ← h₂]⟩
          inv := ⟨e, by simp [Category.assoc, h₁, ← h₂]⟩ }

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : k < j
h✝ : i ≤ k
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : j ≤ k
h✝ : k + 1 < i
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ k = k + 1 + 1

Tactic:
lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 ≤ k
h✝¹ : k < j
h✝ : k < i
⊢ False

Tactic:
lia

Goal state after: