awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Opposite (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : SMulCommClass R S A
inst_9 : IsScalarTower R S A
x : R
⊢ Eq (α := Module.End A A)
    (Equiv.toFun (RingEquiv.toEquiv (RingEquiv.moduleEndSelf A)) ((algebraMap R Aᵐᵒᵖ : (a : R) → Aᵐᵒᵖ) x))
    ((algebraMap R (Module.End A A) : (a : R) → Module.End A A) x)
have h : Eq (α := A)
  ((Equiv.toFun (RingEquiv.toEquiv (RingEquiv.moduleEndSelf A)) ((algebraMap R Aᵐᵒᵖ : (a : R) → Aᵐᵒᵖ) x) : (a : A) → A)
      1 :
    A)
  ((((algebraMap R (Module.End A A) : (a : R) → Module.End A A) x : Module.End A A) : (a : A) → A) 1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Opposite (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : SMulCommClass R S A
inst_9 : IsScalarTower R S A
x : R
⊢ Eq (α := Module.End Aᵐᵒᵖ A)
    (Equiv.toFun (RingEquiv.toEquiv (RingEquiv.moduleEndSelfOp A)) ((algebraMap R A : (a : R) → A) x))
    ((algebraMap R (Module.End Aᵐᵒᵖ A) : (a : R) → Module.End Aᵐᵒᵖ A) x)
have h : Eq (α := A)
  ((Equiv.toFun (RingEquiv.toEquiv (RingEquiv.moduleEndSelfOp A)) ((algebraMap R A : (a : R) → A) x) : (a : A) → A) 1 :
    A)
  ((((algebraMap R (Module.End Aᵐᵒᵖ A) : (a : R) → Module.End Aᵐᵒᵖ A) x : Module.End Aᵐᵒᵖ A) : (a : A) → A) 1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} R (A i)
a : R
f : (i : ι) → A i
⊢ HMul.hMul (α := (i : ι) → A i)
      (((Pi.ringHom (f := A) fun (i : ι) ↦ algebraMap R (A i) : R →+* (i : ι) → A i) : (a : R) → (i : ι) → A i) a :
        (i : ι) → A i)
      f =
    HMul.hMul (β := (i : ι) → A i) f
      (((Pi.ringHom (f := A) fun (i : ι) ↦ algebraMap R (A i) : R →+* (i : ι) → A i) : (a : R) → (i : ι) → A i) a :
        (i : ι) → A i)
have h : ∀ (x : ι),
  HMul.hMul (α := (i : ι) → A i)
      (((Pi.ringHom (f := A) fun (i : ι) ↦ algebraMap R (A i) : R →+* (i : ι) → A i) : (a : R) → (i : ι) → A i) a :
        (i : ι) → A i)
      f x =
    HMul.hMul (β := (i : ι) → A i) f
      (((Pi.ringHom (f := A) fun (i : ι) ↦ algebraMap R (A i) : R →+* (i : ι) → A i) : (a : R) → (i : ι) → A i) a :
        (i : ι) → A i)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} R (A i)
a : R
f : (i : ι) → A i
⊢ a • f =
    HMul.hMul (α := (i : ι) → A i)
      (((Pi.ringHom (f := A) fun (i : ι) ↦ algebraMap R (A i) : R →+* (i : ι) → A i) : (a : R) → (i : ι) → A i) a :
        (i : ι) → A i)
      f
have h : ∀ (x : ι),
  (a • f) x =
    HMul.hMul (α := (i : ι) → A i)
      (((Pi.ringHom (f := A) fun (i : ι) ↦ algebraMap R (A i) : R →+* (i : ι) → A i) : (a : R) → (i : ι) → A i) a :
        (i : ι) → A i)
      f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} R (A i)
B : Type u_4
inst_3 : Semiring B
inst_4 : Algebra R B
g : (i : ι) → AlgHom.{u_2, u_4, u_3} R B (A i)
r : R
⊢ Eq (α := (i : ι) → A i)
    (OneHom.toFun (M := B)
      ((↑(↑(Pi.ringHom (f := A) fun (i : ι) ↦ (g i).toRingHom) : B →* (i : ι) → A i) : OneHom B ((i : ι) → A i)) :
        OneHom B ((i : ι) → A i))
      ((algebraMap R B : (a : R) → B) r : B))
    ((algebraMap R ((i : ι) → A i) : (a : R) → (i : ι) → A i) r)
have h : ∀ (x : ι),
  Eq.{u_3 + 1} (α := A x)
    (OneHom.toFun (M := B)
        ((↑(↑(Pi.ringHom (f := A) fun (i : ι) ↦ (g i).toRingHom) : B →* (i : ι) → A i) : OneHom B ((i : ι) → A i)) :
          OneHom B ((i : ι) → A i))
        ((algebraMap R B : (a : R) → B) r : B) x :
      A x)
    ((algebraMap R ((i : ι) → A i) : (a : R) → (i : ι) → A i) r x : A x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Pi (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
ι : Type u_4
c : R
⊢ Eq (α := ι → B)
    (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := A) (⇑f : (a : A) → B) ((algebraMap R (ι → A) : (a : R) → ι → A) c))
    ((algebraMap R (ι → B) : (a : R) → ι → B) c)
have h : ∀ (x : ι),
  Eq.{u_3 + 1} (α := B)
    (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := A) (⇑f : (a : A) → B) ((algebraMap R (ι → A) : (a : R) → ι → A) c)
        x :
      B)
    ((algebraMap R (ι → B) : (a : R) → ι → B) c x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Pi (goal)
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A₁ i)
inst_2 : (i : ι) → Semiring (A₂ i)
inst_3 : (i : ι) → Semiring (A₃ i)
inst_4 : (i : ι) → Algebra.{u_3, u_5} R (A₁ i)
inst_5 : (i : ι) → Algebra.{u_3, u_6} R (A₂ i)
inst_6 : (i : ι) → Algebra.{u_3, u_7} R (A₃ i)
e : (i : ι) → AlgEquiv.{u_3, u_5, u_6} R (A₁ i) (A₂ i)
r : R
⊢ Eq (α := (i : ι) → A₂ i)
    (fun (j : ι) ↦ ((e j : (a : A₁ j) → A₂ j) ((algebraMap R ((i : ι) → A₁ i) : (a : R) → (i : ι) → A₁ i) r j) : A₂ j))
    ((algebraMap R ((i : ι) → A₂ i) : (a : R) → (i : ι) → A₂ i) r : (i : ι) → A₂ i)
have h : ∀ (i : ι),
  Eq.{u_6 + 1} (α := A₂ i)
    ((e i : (a : A₁ i) → A₂ i) ((algebraMap R ((i : ι) → A₁ i) : (a : R) → (i : ι) → A₁ i) r i) : A₂ i)
    ((algebraMap R ((i : ι) → A₂ i) : (a : R) → (i : ι) → A₂ i) r i : A₂ i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Pi (goal)
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A₁ i)
inst_2 : (i : ι) → Semiring (A₂ i)
inst_3 : (i : ι) → Semiring (A₃ i)
inst_4 : (i : ι) → Algebra.{u_3, u_5} R (A₁ i)
inst_5 : (i : ι) → Algebra.{u_3, u_6} R (A₂ i)
inst_6 : (i : ι) → Algebra.{u_3, u_7} R (A₃ i)
S : Type u_8
inst_7 : Semiring S
inst_8 : Algebra R S
x : R
⊢ Eq (α := (α → S) × (β → S))
    (((RingEquiv.sumArrowEquivProdArrow α β S : (α ⊕ β → S) ≃+* (α → S) × (β → S)) :
          (a : α ⊕ β → S) → (α → S) × (β → S))
        ((algebraMap R (α ⊕ β → S) : (a : R) → α ⊕ β → S) x) :
      (α → S) × (β → S))
    ((algebraMap R ((α → S) × (β → S)) : (a : R) → (α → S) × (β → S)) x : (α → S) × (β → S))
have fst : ∀ (x_1 : α),
  Eq.{u_8 + 1} (α := S)
    ((((RingEquiv.sumArrowEquivProdArrow α β S : (α ⊕ β → S) ≃+* (α → S) × (β → S)) :
            (a : α ⊕ β → S) → (α → S) × (β → S))
          ((algebraMap R (α ⊕ β → S) : (a : R) → α ⊕ β → S) x)).1
      x_1)
    (((algebraMap R ((α → S) × (β → S)) : (a : R) → (α → S) × (β → S)) x).1 x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Pi (goal)
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A₁ i)
inst_2 : (i : ι) → Semiring (A₂ i)
inst_3 : (i : ι) → Semiring (A₃ i)
inst_4 : (i : ι) → Algebra.{u_3, u_5} R (A₁ i)
inst_5 : (i : ι) → Algebra.{u_3, u_6} R (A₂ i)
inst_6 : (i : ι) → Algebra.{u_3, u_7} R (A₃ i)
S : Type u_8
inst_7 : Semiring S
inst_8 : Algebra R S
x : R
fst :
  ∀ (x_1 : α),
    Eq.{u_8 + 1} (α := S)
      ((((RingEquiv.sumArrowEquivProdArrow α β S : (α ⊕ β → S) ≃+* (α → S) × (β → S)) :
              (a : α ⊕ β → S) → (α → S) × (β → S))
            ((algebraMap R (α ⊕ β → S) : (a : R) → α ⊕ β → S) x)).1
        x_1)
      (((algebraMap R ((α → S) × (β → S)) : (a : R) → (α → S) × (β → S)) x).1 x_1)
⊢ Eq (α := (α → S) × (β → S))
    (((RingEquiv.sumArrowEquivProdArrow α β S : (α ⊕ β → S) ≃+* (α → S) × (β → S)) :
          (a : α ⊕ β → S) → (α → S) × (β → S))
        ((algebraMap R (α ⊕ β → S) : (a : R) → α ⊕ β → S) x) :
      (α → S) × (β → S))
    ((algebraMap R ((α → S) × (β → S)) : (a : R) → (α → S) × (β → S)) x : (α → S) × (β → S))
have snd : ∀ (x_1 : β),
  Eq.{u_8 + 1} (α := S)
    ((((RingEquiv.sumArrowEquivProdArrow α β S : (α ⊕ β → S) ≃+* (α → S) × (β → S)) :
            (a : α ⊕ β → S) → (α → S) × (β → S))
          ((algebraMap R (α ⊕ β → S) : (a : R) → α ⊕ β → S) x)).2
      x_1)
    (((algebraMap R ((α → S) × (β → S)) : (a : R) → (α → S) × (β → S)) x).2 x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
t : R
v : ι → R
⊢ (⇑(algebraMap R A) : (a : R) → A) ∘ (t • v) =
    HSMul.hSMul (α := R) (β := ι → A) ((RingHom.id R : (a : R) → R) t : R) ((⇑(algebraMap R A) : (a : R) → A) ∘ v)
have h : ∀ (x : ι),
  ((⇑(algebraMap R A) : (a : R) → A) ∘ (t • v)) x =
    HSMul.hSMul (α := R) (β := ι → A) ((RingHom.id R : (a : R) → R) t : R) ((⇑(algebraMap R A) : (a : R) → A) ∘ v) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Prod (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
r : R
a : A
b : B
⊢ HMul.hMul (α := A × B) ((RingHom.prod (algebraMap R A) (algebraMap R B) : (a : R) → A × B) r : A × B) (a, b) =
    HMul.hMul (β := A × B) (a, b) ((RingHom.prod (algebraMap R A) (algebraMap R B) : (a : R) → A × B) r : A × B)
have dsimp : (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
    HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b) =
  (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
    HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) r : B))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Prod (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
r : R
a : A
b : B
⊢ (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b) =
    (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
      HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) r : B))
have rw : (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
    HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b) =
  (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
    HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) r : B))
Tactic: rw [commutes r a, commutes r b]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Prod (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
r : R
a : A
b : B
rw :
  (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b) =
    (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
      HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) r : B))
⊢ (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b) =
    (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
      HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) r : B))
have rw₁ : (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
    HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) r : B)) =
  (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A),
    HMul.hMul (β := B) b ((algebraMap R B : (a : R) → B) r : B))
Tactic: rw [commutes r a, commutes r b]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Prod (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
r : R
a : A
b : B
⊢ r • (a, b) =
    HMul.hMul (α := A × B) ((RingHom.prod (algebraMap R A) (algebraMap R B) : (a : R) → A × B) r : A × B) (a, b)
have dsimp : (r • a, r • b) =
  (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
    HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Prod (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
r : R
a : A
b : B
⊢ (r • a, r • b) =
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b)
have rw : (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a, r • b) =
  (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
    HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b)
Tactic: rw [Algebra.smul_def r a, Algebra.smul_def r b]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Prod (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
r : R
a : A
b : B
rw :
  (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a, r • b) =
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b)
⊢ (r • a, r • b) =
    (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
      HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b)
have rw₁ : (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
    HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b) =
  (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a,
    HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) r : B) b)
Tactic: rw [Algebra.smul_def r a, Algebra.smul_def r b]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Prod (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
⊢ comp (fst R B C) (f.prod g) = f
have H : ∀ (x : A), Eq.{u_3 + 1} (α := B) ((comp (fst R B C) (f.prod g) : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Prod (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
⊢ comp (snd R B C) (f.prod g) = g
have H : ∀ (x : A), Eq.{u_4 + 1} (α := C) ((comp (snd R B C) (f.prod g) : (a : A) → C) x : C) ((g : (a : A) → C) x : C)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.RestrictScalars (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Semiring S
inst_3 : Algebra R S
inst_4 : Module S M
r : R
s : S
x : M
⊢ (AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M) ((r • s) • x) =
    HSMul.hSMul (β := RestrictScalars R S M) r
      ((AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M) (s • x) : RestrictScalars R S M)
have rw : (AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) (s • x)) =
  HSMul.hSMul (β := RestrictScalars R S M) r
    ((AddEquiv.symm (addEquiv R S M) : (a : M) → RestrictScalars R S M) (s • x) : RestrictScalars R S M)
Tactic: rw [Algebra.smul_def, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a)
⊢ HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * r • (↑h.unit⁻¹ : A) = 1
have rw : r • (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * (↑h.unit⁻¹ : A)) = 1
Tactic: rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_val_inv]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a)
rw : r • (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * (↑h.unit⁻¹ : A)) = 1
⊢ HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * r • (↑h.unit⁻¹ : A) = 1
have rw₁ : r • HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * (↑h.unit⁻¹ : A) = 1
Tactic: rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_val_inv]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a)
rw : r • (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * (↑h.unit⁻¹ : A)) = 1
rw₁ : r • HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * (↑h.unit⁻¹ : A) = 1
⊢ HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * r • (↑h.unit⁻¹ : A) = 1
have rw₂ : (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - r • r⁻¹ • a) * (↑h.unit⁻¹ : A) = 1
Tactic: rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_val_inv]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a)
rw : r • (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * (↑h.unit⁻¹ : A)) = 1
rw₁ : r • HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * (↑h.unit⁻¹ : A) = 1
rw₂ : (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - r • r⁻¹ • a) * (↑h.unit⁻¹ : A) = 1
⊢ HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * r • (↑h.unit⁻¹ : A) = 1
have rw₃ : (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a) * (↑h.unit⁻¹ : A) = 1
Tactic: rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_val_inv]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a)
rw : r • (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * (↑h.unit⁻¹ : A)) = 1
rw₁ : r • HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * (↑h.unit⁻¹ : A) = 1
rw₂ : (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - r • r⁻¹ • a) * (↑h.unit⁻¹ : A) = 1
rw₃ : (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a) * (↑h.unit⁻¹ : A) = 1
⊢ HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * r • (↑h.unit⁻¹ : A) = 1
have rw₄ : Eq.{v + 1} (α := A) 1 1
Tactic: rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_val_inv]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a)
⊢ r • (↑h.unit⁻¹ : A) * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) = 1
have rw : r • ((↑h.unit⁻¹ : A) * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a)) = 1
Tactic: rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.val_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a)
rw : r • ((↑h.unit⁻¹ : A) * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a)) = 1
⊢ r • (↑h.unit⁻¹ : A) * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) = 1
have rw₁ : (↑h.unit⁻¹ : A) * r • HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) = 1
Tactic: rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.val_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a)
rw : r • ((↑h.unit⁻¹ : A) * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a)) = 1
rw₁ : (↑h.unit⁻¹ : A) * r • HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) = 1
⊢ r • (↑h.unit⁻¹ : A) * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) = 1
have rw₂ : (↑h.unit⁻¹ : A) * (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - r • r⁻¹ • a) = 1
Tactic: rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.val_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a)
rw : r • ((↑h.unit⁻¹ : A) * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a)) = 1
rw₁ : (↑h.unit⁻¹ : A) * r • HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) = 1
rw₂ : (↑h.unit⁻¹ : A) * (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - r • r⁻¹ • a) = 1
⊢ r • (↑h.unit⁻¹ : A) * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) = 1
have rw₃ : (↑h.unit⁻¹ : A) * (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a) = 1
Tactic: rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.val_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a)
rw : r • ((↑h.unit⁻¹ : A) * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a)) = 1
rw₁ : (↑h.unit⁻¹ : A) * r • HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) = 1
rw₂ : (↑h.unit⁻¹ : A) * (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - r • r⁻¹ • a) = 1
rw₃ : (↑h.unit⁻¹ : A) * (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a) = 1
⊢ r • (↑h.unit⁻¹ : A) * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) = 1
have rw₄ : Eq.{v + 1} (α := A) 1 1
Tactic: rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.val_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial A
r : R
a : A
⊢ r ∈ σ a ↔ resolvent a r = 0
have refine : ∀ (hr : resolvent a r = 0), r ∈ σ a
Tactic: refine ⟨resolvent_zero_of_mem_spectrum, fun hr ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
⊢ 0 ∈ σ a ↔ ¬IsUnit a
have rw : ¬IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) 0 : A) a) ↔ ¬IsUnit a
Tactic: rw [mem_iff, map_zero, zero_sub, IsUnit.neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
rw : ¬IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) 0 : A) a) ↔ ¬IsUnit a
⊢ 0 ∈ σ a ↔ ¬IsUnit a
have rw₁ : ¬IsUnit (0 - a) ↔ ¬IsUnit a
Tactic: rw [mem_iff, map_zero, zero_sub, IsUnit.neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
rw : ¬IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) 0 : A) a) ↔ ¬IsUnit a
rw₁ : ¬IsUnit (0 - a) ↔ ¬IsUnit a
⊢ 0 ∈ σ a ↔ ¬IsUnit a
have rw₂ : ¬IsUnit (-a) ↔ ¬IsUnit a
Tactic: rw [mem_iff, map_zero, zero_sub, IsUnit.neg_iff]