awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e e₁ : A₁ ≃ₐ[R] A₂
e₂ : A₂ ≃ₐ[R] A₃
r : R
⊢ e₂.toFun (e₁.toFun ((algebraMap R A₁ : (a : R) → A₁) r)) = (algebraMap R A₃ : (a : R) → A₃) r
have rw : e₂.toFun ((algebraMap R A₂ : (a : R) → A₂) r) = (algebraMap R A₃ : (a : R) → A₃) r
Tactic: rw [e₁.commutes', e₂.commutes']
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e e₁ : A₁ ≃ₐ[R] A₂
e₂ : A₂ ≃ₐ[R] A₃
r : R
rw : e₂.toFun ((algebraMap R A₂ : (a : R) → A₂) r) = (algebraMap R A₃ : (a : R) → A₃) r
⊢ e₂.toFun (e₁.toFun ((algebraMap R A₁ : (a : R) → A₁) r)) = (algebraMap R A₃ : (a : R) → A₃) r
have rw₁ : Eq.{uA₃ + 1} (α := A₃) ((algebraMap R A₃ : (a : R) → A₃) r : A₃) ((algebraMap R A₃ : (a : R) → A₃) r : A₃)
Tactic: rw [e₁.commutes', e₂.commutes']
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ e.trans e.symm = refl
have h : ∀ (a : A₁), Eq (α := A₁) ((e.trans e.symm : (a : A₁) → A₁) a : A₁) ((refl : (a : A₁) → A₁) a : A₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ e.symm.trans e = refl
have h : ∀ (a : A₂), Eq (α := A₂) ((e.symm.trans e : (a : A₂) → A₂) a : A₂) ((refl : (a : A₂) → A₂) a : A₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
ι : Type u_1
A : ι → Type u_2
inst_13 : (i : ι) → Semiring (A i)
inst_14 : (i : ι) → Algebra.{uR, u_2} R (A i)
i j : ι
h : i = j
x : R
⊢ Eq.{u_2 + 1} (α := A j)
    (Equiv.toFun (RingEquiv.toEquiv (RingEquiv.cast (R := A) h : A i ≃+* A j)) ((algebraMap R (A i) : (a : R) → A i) x))
    ((algebraMap R (A j) : (a : R) → A j) x)
have refl : Eq.{u_2 + 1} (α := A i)
  (Equiv.toFun (RingEquiv.toEquiv (RingEquiv.cast (R := A) sorry : A i ≃+* A i)) ((algebraMap R (A i) : (a : R) → A i) x))
  ((algebraMap R (A i) : (a : R) → A i) x)
Tactic: cases h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁ →ₐ[R] A₂
⊢ (fun (f : A₁' →ₐ[R] A₂') ↦ ((↑e₂.symm : A₂' →ₐ[R] A₂).comp f).comp (↑e₁ : A₁ →ₐ[R] A₁'))
      ((fun (f : A₁ →ₐ[R] A₂) ↦ ((↑e₂ : A₂ →ₐ[R] A₂').comp f).comp (↑e₁.symm : A₁' →ₐ[R] A₁)) f) =
    f
have simp : (↑e₂.symm : A₂' →ₐ[R] A₂).comp ((↑e₂ : A₂ →ₐ[R] A₂').comp (f.comp (AlgHom.id R A₁))) = f
Tactic: simp only [AlgHom.comp_assoc, symm_comp]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁' →ₐ[R] A₂'
⊢ (fun (f : A₁ →ₐ[R] A₂) ↦ ((↑e₂ : A₂ →ₐ[R] A₂').comp f).comp (↑e₁.symm : A₁' →ₐ[R] A₁))
      ((fun (f : A₁' →ₐ[R] A₂') ↦ ((↑e₂.symm : A₂' →ₐ[R] A₂).comp f).comp (↑e₁ : A₁ →ₐ[R] A₁')) f) =
    f
have simp : (↑e₂ : A₂ →ₐ[R] A₂').comp ((↑e₂.symm : A₂' →ₐ[R] A₂).comp (f.comp (AlgHom.id R A₁'))) = f
Tactic: simp only [AlgHom.comp_assoc, comp_symm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
⊢ Eq (α := A₁' →ₐ[R] A₃') ((e₁.arrowCongr e₃ : (a : A₁ →ₐ[R] A₃) → A₁' →ₐ[R] A₃') (g.comp f) : A₁' →ₐ[R] A₃')
    (AlgHom.comp.{uR, uA₁', uA₂', uA₃'} (B := A₂') ((e₂.arrowCongr e₃ : (a : A₂ →ₐ[R] A₃) → A₂' →ₐ[R] A₃') g)
        ((e₁.arrowCongr e₂ : (a : A₁ →ₐ[R] A₂) → A₁' →ₐ[R] A₂') f) :
      A₁' →ₐ[R] A₃')
have H : ∀ (x : A₁'),
  Eq.{uA₃' + 1} (α := A₃')
    ((((e₁.arrowCongr e₃ : (a : A₁ →ₐ[R] A₃) → A₁' →ₐ[R] A₃') (g.comp f) : A₁' →ₐ[R] A₃') : (a : A₁') → A₃') x : A₃')
    ((AlgHom.comp.{uR, uA₁', uA₂', uA₃'} (B := A₂') ((e₂.arrowCongr e₃ : (a : A₂ →ₐ[R] A₃) → A₂' →ₐ[R] A₃') g)
            ((e₁.arrowCongr e₂ : (a : A₁ →ₐ[R] A₂) → A₁' →ₐ[R] A₂') f) :
          (a : A₁') → A₃')
        x :
      A₃')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e_1 e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₁ ≃ₐ[R] A₁'
⊢ (fun (ψ : A₂ ≃ₐ[R] A₂') ↦ e.trans (ψ.trans e'.symm)) ((fun (ψ : A₁ ≃ₐ[R] A₁') ↦ e.symm.trans (ψ.trans e')) ψ) = ψ
have h : ∀ (a : A₁),
  Eq.{uA₁' + 1} (α := A₁')
    (((fun (ψ : A₂ ≃ₐ[R] A₂') ↦ e.trans (ψ.trans e'.symm)) ((fun (ψ : A₁ ≃ₐ[R] A₁') ↦ e.symm.trans (ψ.trans e')) ψ) :
          (a : A₁) → A₁')
        a :
      A₁')
    ((ψ : (a : A₁) → A₁') a : A₁')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e_1 e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₁ ≃ₐ[R] A₁'
a : A₁
h h₁ :
  Eq.{uA₁' + 1} (α := A₁') ((e.trans ((e.symm.trans (ψ.trans e')).trans e'.symm) : (a : A₁) → A₁') a : A₁')
    ((ψ : (a : A₁) → A₁') a : A₁')
⊢ Eq.{uA₁' + 1} (α := A₁')
    (((fun (ψ : A₂ ≃ₐ[R] A₂') ↦ e.trans (ψ.trans e'.symm)) ((fun (ψ : A₁ ≃ₐ[R] A₁') ↦ e.symm.trans (ψ.trans e')) ψ) :
          (a : A₁) → A₁')
        a :
      A₁')
    ((ψ : (a : A₁) → A₁') a : A₁')
have h₂ : Eq.{uA₁' + 1} (α := A₁')
  ((e'.symm : (a : A₂') → A₁')
      ((e' : (a : A₁') → A₂')
          ((ψ : (a : A₁) → A₁') ((e.symm : (a : A₂) → A₁) ((e : (a : A₁) → A₂) a : A₂) : A₁) : A₁') :
        A₂') :
    A₁')
  ((ψ : (a : A₁) → A₁') a : A₁')
Tactic: simp_rw [trans_apply, symm_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e_1 e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₂ ≃ₐ[R] A₂'
⊢ (fun (ψ : A₁ ≃ₐ[R] A₁') ↦ e.symm.trans (ψ.trans e')) ((fun (ψ : A₂ ≃ₐ[R] A₂') ↦ e.trans (ψ.trans e'.symm)) ψ) = ψ
have h : ∀ (a : A₂),
  Eq.{uA₂' + 1} (α := A₂')
    (((fun (ψ : A₁ ≃ₐ[R] A₁') ↦ e.symm.trans (ψ.trans e')) ((fun (ψ : A₂ ≃ₐ[R] A₂') ↦ e.trans (ψ.trans e'.symm)) ψ) :
          (a : A₂) → A₂')
        a :
      A₂')
    ((ψ : (a : A₂) → A₂') a : A₂')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e_1 e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₂ ≃ₐ[R] A₂'
a : A₂
h h₁ :
  Eq.{uA₂' + 1} (α := A₂') ((e.symm.trans ((e.trans (ψ.trans e'.symm)).trans e') : (a : A₂) → A₂') a : A₂')
    ((ψ : (a : A₂) → A₂') a : A₂')
⊢ Eq.{uA₂' + 1} (α := A₂')
    (((fun (ψ : A₁ ≃ₐ[R] A₁') ↦ e.symm.trans (ψ.trans e')) ((fun (ψ : A₂ ≃ₐ[R] A₂') ↦ e.trans (ψ.trans e'.symm)) ψ) :
          (a : A₂) → A₂')
        a :
      A₂')
    ((ψ : (a : A₂) → A₂') a : A₂')
have h₂ : Eq.{uA₂' + 1} (α := A₂')
  ((e' : (a : A₁') → A₂')
      ((e'.symm : (a : A₂') → A₁')
          ((ψ : (a : A₂) → A₂') ((e : (a : A₁) → A₂) ((e.symm : (a : A₂) → A₁) a : A₁) : A₂) : A₂') :
        A₁') :
    A₂')
  ((ψ : (a : A₂) → A₂') a : A₂')
Tactic: simp_rw [trans_apply, apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
x : A₁
⊢ Eq.{uA₂ + 1} (α := Module.End R A₂)
    (((↑f : A₁ ≃ₗ[R] A₂).conj : (a : Module.End R A₁) → Module.End R A₂) (LinearMap.mulLeft R x) : Module.End R A₂)
    (LinearMap.mulLeft R ((f : (a : A₁) → A₂) x) : A₂ →ₗ[R] A₂)
have h : ∀ (x_1 : A₂),
  Eq (α := A₂)
    (((((↑f : A₁ ≃ₗ[R] A₂).conj : (a : Module.End R A₁) → Module.End R A₂) (LinearMap.mulLeft R x) : Module.End R A₂) :
          (a : A₂) → A₂)
        x_1 :
      A₂)
    (((LinearMap.mulLeft R ((f : (a : A₁) → A₂) x) : A₂ →ₗ[R] A₂) : (a : A₂) → A₂) x_1 : A₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
x : A₁
⊢ Eq.{uA₂ + 1} (α := Module.End R A₂)
    (((↑f : A₁ ≃ₗ[R] A₂).conj : (a : Module.End R A₁) → Module.End R A₂) (LinearMap.mulRight R x) : Module.End R A₂)
    (LinearMap.mulRight R ((f : (a : A₁) → A₂) x) : A₂ →ₗ[R] A₂)
have h : ∀ (x_1 : A₂),
  Eq (α := A₂)
    (((((↑f : A₁ ≃ₗ[R] A₂).conj : (a : Module.End R A₁) → Module.End R A₂) (LinearMap.mulRight R x) : Module.End R A₂) :
          (a : A₂) → A₂)
        x_1 :
      A₂)
    (((LinearMap.mulRight R ((f : (a : A₁) → A₂) x) : A₂ →ₗ[R] A₂) : (a : A₂) → A₂) x_1 : A₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
x : A₁ × A₁
⊢ Eq.{uA₂ + 1} (α := Module.End R A₂)
    (((↑f : A₁ ≃ₗ[R] A₂).conj : (a : Module.End R A₁) → Module.End R A₂) (LinearMap.mulLeftRight R x) : Module.End R A₂)
    (LinearMap.mulLeftRight R (Prod.map (⇑f : (a : A₁) → A₂) (⇑f : (a : A₁) → A₂) x) : A₂ →ₗ[R] A₂)
have mk : ∀ (fst snd : A₁),
  Eq.{uA₂ + 1} (α := Module.End R A₂)
    (((↑f : A₁ ≃ₗ[R] A₂).conj : (a : Module.End R A₁) → Module.End R A₂) (LinearMap.mulLeftRight R (fst, snd)) :
      Module.End R A₂)
    (LinearMap.mulLeftRight R (Prod.map (⇑f : (a : A₁) → A₂) (⇑f : (a : A₁) → A₂) (fst, snd)) : A₂ →ₗ[R] A₂)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
f : A₁ ≃ₐ[R] A₂
fst snd : A₁
⊢ Eq.{uA₂ + 1} (α := Module.End R A₂)
    (((↑f : A₁ ≃ₗ[R] A₂).conj : (a : Module.End R A₁) → Module.End R A₂) (LinearMap.mulLeftRight R (fst, snd)) :
      Module.End R A₂)
    (LinearMap.mulLeftRight R (Prod.map (⇑f : (a : A₁) → A₂) (⇑f : (a : A₁) → A₂) (fst, snd)) : A₂ →ₗ[R] A₂)
have mk : ∀ (x : A₂),
  Eq (α := A₂)
    (((((↑f : A₁ ≃ₗ[R] A₂).conj : (a : Module.End R A₁) → Module.End R A₂) (LinearMap.mulLeftRight R (fst, snd)) :
            Module.End R A₂) :
          (a : A₂) → A₂)
        x :
      A₂)
    ((LinearMap.mulLeftRight R (Prod.map (⇑f : (a : A₁) → A₂) (⇑f : (a : A₁) → A₂) (fst, snd)) : (a : A₂) → A₂) x : A₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
e : A₁ ≃ₐ[R] A₁
n : ℕ
⊢ Eq (α := (a : A₁) → A₁) (⇑(e ^ Nat.zero) : (a : A₁) → A₁) (⇑e : (a : A₁) → A₁)^[Nat.zero]
have h : ∀ (x : A₁), (e ^ Nat.zero : (a : A₁) → A₁) x = (⇑e : (a : A₁) → A₁)^[Nat.zero] x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
e : A₁ ≃ₐ[R] A₁
n x : ℕ
ih : Eq (α := (a : A₁) → A₁) (⇑(e ^ x) : (a : A₁) → A₁) (⇑e : (a : A₁) → A₁)^[x]
⊢ Eq (α := (a : A₁) → A₁) (⇑(e ^ x.succ) : (a : A₁) → A₁) (⇑e : (a : A₁) → A₁)^[x.succ]
have h : ∀ (x_1 : A₁), (e ^ x.succ : (a : A₁) → A₁) x_1 = (⇑e : (a : A₁) → A₁)^[x.succ] x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e ϕ : A₁ ≃ₐ[R] A₂
ψ χ : A₁ ≃ₐ[R] A₁
⊢ ϕ.symm.trans ((ψ * χ).trans ϕ) = ϕ.symm.trans (ψ.trans ϕ) * ϕ.symm.trans (χ.trans ϕ)
have h : ∀ (a : A₂),
  Eq (α := A₂) ((ϕ.symm.trans ((ψ * χ).trans ϕ) : (a : A₂) → A₂) a : A₂)
    ((ϕ.symm.trans (ψ.trans ϕ) * ϕ.symm.trans (χ.trans ϕ) : (a : A₂) → A₂) a : A₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x y : A₁ ≃ₐ[R] A₁
z : A₁ˣ
⊢ (x * y) • z = x • y • z
have huv : (↑((x * y) • z) : A₁) = (↑(x • y • z) : A₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ˣ
⊢ HSMul.hSMul (α := A₁ ≃ₐ[R] A₁) 1 x = x
have huv : (↑(HSMul.hSMul (α := A₁ ≃ₐ[R] A₁) 1 x) : A₁) = (↑x : A₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
⊢ HSMul.hSMul (β := A₁ˣ) x 1 = 1
have huv : (↑(HSMul.hSMul (β := A₁ˣ) x 1) : A₁) = (↑1 : A₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R A₁
inst_8 : Algebra R A₂
inst_9 : Algebra R A₃
inst_10 : Algebra R A₁'
inst_11 : Algebra R A₂'
inst_12 : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
y z : A₁ˣ
⊢ x • (y * z) = x • y * x • z
have huv : (↑(x • (y * z)) : A₁) = (↑(x • y * x • z) : A₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R_1 : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R_1
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R_1 A₁
inst_8 : Algebra R_1 A₂
inst_9 : Algebra R_1 A₃
inst_10 : Algebra R_1 A₁'
inst_11 : Algebra R_1 A₂'
inst_12 : Algebra R_1 A₃'
e : A₁ ≃ₐ[R_1] A₂
R : Type u_1
S : Type u_2
inst_13 : CommSemiring R
inst_14 : Semiring S
inst_15 : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
⊢ ((↑(f⁻¹ * f) : S →ₐ[R] S) : (a : S) → S) x = x
have rw : ((↑1 : S →ₐ[R] S) : (a : S) → S) x = x
Tactic: rw [inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R_1 : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst : CommSemiring R_1
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Semiring A₃
inst_4 : Semiring A₁'
inst_5 : Semiring A₂'
inst_6 : Semiring A₃'
inst_7 : Algebra R_1 A₁
inst_8 : Algebra R_1 A₂
inst_9 : Algebra R_1 A₃
inst_10 : Algebra R_1 A₁'
inst_11 : Algebra R_1 A₂'
inst_12 : Algebra R_1 A₃'
e : A₁ ≃ₐ[R_1] A₂
R : Type u_1
S : Type u_2
inst_13 : CommSemiring R
inst_14 : Semiring S
inst_15 : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
⊢ ((↑(f * f⁻¹) : S →ₐ[R] S) : (a : S) → S) x = x
have rw : ((↑1 : S →ₐ[R] S) : (a : S) → S) x = x
Tactic: rw [mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : R
⊢ Eq.{u_1 + 1} (α := R)
    ((e.symm : (a : A) → R)
        (HMul.hMul (α := A) (β := A) ((e : (a : R) → A) 1 : A) ((algebraMap R A : (a : R) → A) x : A)) :
      R)
    ((e.symm : (a : A) → R) (HSMul.hSMul (β := A) x ((e : (a : R) → A) 1 : A)) : R)
have rw : Eq.{u_1 + 1} (α := R)
  ((e.symm : (a : A) → R)
      (HMul.hMul (α := A) (β := A) ((e : (a : R) → A) 1 : A) ((algebraMap R A : (a : R) → A) x : A)) :
    R)
  ((e.symm : (a : A) → R)
      (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) ((e : (a : R) → A) 1 : A)) :
    R)
Tactic: rw [Algebra.smul_def, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : R
rw :
  Eq.{u_1 + 1} (α := R)
    ((e.symm : (a : A) → R)
        (HMul.hMul (α := A) (β := A) ((e : (a : R) → A) 1 : A) ((algebraMap R A : (a : R) → A) x : A)) :
      R)
    ((e.symm : (a : A) → R)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) ((e : (a : R) → A) 1 : A)) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((e.symm : (a : A) → R)
        (HMul.hMul (α := A) (β := A) ((e : (a : R) → A) 1 : A) ((algebraMap R A : (a : R) → A) x : A)) :
      R)
    ((e.symm : (a : A) → R) (HSMul.hSMul (β := A) x ((e : (a : R) → A) 1 : A)) : R)
have rw₁ : Eq.{u_1 + 1} (α := R)
  ((e.symm : (a : A) → R)
      (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) ((e : (a : R) → A) 1 : A)) :
    R)
  ((e.symm : (a : A) → R)
      (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) x : A) ((e : (a : R) → A) 1 : A)) :
    R)
Tactic: rw [Algebra.smul_def, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : R
⊢ (e.symm : (a : A) → R) (HSMul.hSMul (β := A) x ((e : (a : R) → A) 1 : A)) = x
have rw : HSMul.hSMul (β := R) x ((e.symm : (a : A) → R) ((e : (a : R) → A) 1 : A) : R) = x
Tactic: rw [map_smul, e.symm_apply_apply, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : R
rw : HSMul.hSMul (β := R) x ((e.symm : (a : A) → R) ((e : (a : R) → A) 1 : A) : R) = x
⊢ (e.symm : (a : A) → R) (HSMul.hSMul (β := A) x ((e : (a : R) → A) 1 : A)) = x
have rw₁ : HSMul.hSMul (β := R) x 1 = x
Tactic: rw [map_smul, e.symm_apply_apply, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : R
rw : HSMul.hSMul (β := R) x ((e.symm : (a : A) → R) ((e : (a : R) → A) 1 : A) : R) = x
rw₁ : HSMul.hSMul (β := R) x 1 = x
⊢ (e.symm : (a : A) → R) (HSMul.hSMul (β := A) x ((e : (a : R) → A) 1 : A)) = x
have rw₂ : x * 1 = x
Tactic: rw [map_smul, e.symm_apply_apply, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : R
rw : HSMul.hSMul (β := R) x ((e.symm : (a : A) → R) ((e : (a : R) → A) 1 : A) : R) = x
rw₁ : HSMul.hSMul (β := R) x 1 = x
rw₂ : x * 1 = x
⊢ (e.symm : (a : A) → R) (HSMul.hSMul (β := A) x ((e : (a : R) → A) 1 : A)) = x
have rw₃ : x = x
Tactic: rw [map_smul, e.symm_apply_apply, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    HMul.hMul (α := A) (β := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      ((e : (a : R) → A) (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) 1) : A)
have rw : (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
  HMul.hMul (α := A) (β := A)
    ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
    ((e : (a : R) → A) (HMul.hMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) (1 : R)) : A)
Tactic: rw [smul_eq_mul, mul_one, e.apply_symm_apply, mul_one]