awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂')
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₂')
⊢ 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:
simp_rw [trans_apply, apply_symm_apply]

Premises used: AlgEquiv.apply_symm_apply, AlgEquiv.trans_apply
-- Module: Mathlib.Algebra.Algebra.Equiv
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₁'
⊢ Eq (α := (A₁ ≃ₐ[R] A₁') ≃ A₁ ≃ₐ[R] A₁') (equivCongr refl refl) (Equiv.refl (A₁ ≃ₐ[R] A₁'))

Tactic:
rfl

Premises used: Equiv.trans, AlgEquiv.equivCongr, AlgEquiv.trans, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
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 : Algebra R A₁
inst_6 : Algebra R A₂
inst_7 : Algebra R A₁'
inst_8 : Algebra R A₂'
e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
⊢ (e.equivCongr e').symm = e.symm.equivCongr e'.symm

Tactic:
rfl

Premises used: AlgEquiv.symm, AlgEquiv.equivCongr, AlgEquiv.trans, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₃
e₂₃' : A₂' ≃ₐ[R] A₃'
⊢ (e₁₂.equivCongr e₁₂').trans (e₂₃.equivCongr e₂₃') = (e₁₂.trans e₂₃).equivCongr (e₁₂'.trans e₂₃')

Tactic:
rfl

Premises used: Equiv.trans, AlgEquiv.equivCongr, AlgEquiv.trans, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
g : A₂ →ₐ[R] A₁
h₁ : f.comp g = AlgHom.id R A₂
h₂ : g.comp f = AlgHom.id R A₁
⊢ (↑(ofAlgHom f g h₁ h₂) : A₁ →ₐ[R] A₂) = f

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
g : A₂ →ₐ[R] A₁
h₁ : (↑f : A₁ →ₐ[R] A₂).comp g = AlgHom.id R A₂
h₂ : g.comp (↑f : A₁ →ₐ[R] A₂) = AlgHom.id R A₁
⊢ ofAlgHom (↑f : A₁ →ₐ[R] A₂) g h₁ h₂ = f

Tactic:
ext fun _ => rfl

Premises used: AlgEquiv.ext, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
g : A₂ →ₐ[R] A₁
h₁ : f.comp g = AlgHom.id R A₂
h₂ : g.comp f = AlgHom.id R A₁
⊢ (ofAlgHom f g h₁ h₂).symm = ofAlgHom g f h₂ h₁

Tactic:
rfl

Premises used: AlgEquiv.symm, AlgEquiv.ofAlgHom, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
⊢ Eq (α := A₁ ≃ₗ[R] A₁) (↑refl : A₁ ≃ₗ[R] A₁) (LinearEquiv.refl R A₁)

Tactic:
rfl

Premises used: AlgEquiv.toLinearEquiv, LinearEquiv.refl, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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 : A₂ ≃ₗ[R] A₁) = (↑e : A₁ ≃ₗ[R] A₂).symm

Tactic:
rfl

Premises used: LinearEquiv.symm, AlgEquiv.toLinearEquiv, LinearEquiv.toEquiv, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
⊢ Eq (α := (a : A₁) → A₂) (⇑(↑e : A₁ ≃ₗ[R] A₂) : (a : A₁) → A₂) (⇑e : (a : A₁) → A₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
⊢ Eq (α := (a : A₂) → A₁) (⇑(↑e : A₁ ≃ₗ[R] A₂).symm : (a : A₂) → A₁) (⇑e.symm : (a : A₂) → A₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
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 : Algebra R A₁
inst_5 : Algebra R A₂
inst_6 : Algebra R A₃
e₁ : A₁ ≃ₐ[R] A₂
e₂ : A₂ ≃ₐ[R] A₃
⊢ (↑(e₁.trans e₂) : A₁ ≃ₗ[R] A₃) = (↑e₁ : A₁ ≃ₗ[R] A₂) ≪≫ₗ (↑e₂ : A₂ ≃ₗ[R] A₃)

Tactic:
rfl

Premises used: AlgEquiv.toLinearEquiv, LinearEquiv.toEquiv, LinearEquiv.trans, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
⊢ Function.Injective (α := A₁ ≃ₐ[R] A₂) toLinearEquiv

Tactic:
fun _ _ h => ext <| LinearEquiv.congr_fun h

Premises used: AlgEquiv.ext, LinearEquiv.congr_fun, Function.Injective
-- Module: Mathlib.Algebra.Algebra.Equiv
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 : A₁ →ₐ[R] A₂).toLinearMap = (↑(↑e : A₁ ≃ₗ[R] A₂) : A₁ →ₗ[R] A₂)

Tactic:
rfl

Premises used: AlgHom.toLinearMap, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
g : A₂ →ₐ[R] A₁
h₁ : f.comp g = AlgHom.id R A₂
h₂ : g.comp f = AlgHom.id R A₁
⊢ (ofAlgHom f g h₁ h₂).toLinearMap = f.toLinearMap

Tactic:
LinearMap.ext fun _ => rfl

Premises used: LinearMap.ext, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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 : A₁ ≃ₗ[R] A₂) : A₁ →ₗ[R] A₂) = e.toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
x : A₁
⊢ Eq.{uA₂ + 1} (α := A₂) ((e.toLinearMap : (a : A₁) → A₂) x : A₂) ((e : (a : A₁) → A₂) x : A₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
⊢ Function.Injective (α := A₁ ≃ₐ[R] A₂) toLinearMap

Tactic:
fun _ _ h =>
  ext <| LinearMap.congr_fun h

Premises used: LinearMap.congr_fun, AlgEquiv.ext, Function.Injective
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
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 : Algebra R A₁
inst_5 : Algebra R A₂
inst_6 : Algebra R A₃
f : A₁ ≃ₐ[R] A₂
g : A₂ ≃ₐ[R] A₃
⊢ (f.trans g).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₁
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₂)
⊢ 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₂)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
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₁
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:
simp
-- Module: Mathlib.Algebra.Algebra.Equiv
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₁
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₂)
⊢ 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₂)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
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₁
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:
simp
-- Module: Mathlib.Algebra.Algebra.Equiv
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₁
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₂)
⊢ 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₂)

Tactic:
cases x
-- Module: Mathlib.Algebra.Algebra.Equiv
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₁
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₂)
⊢ 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:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
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₁
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:
simp
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
hf : Function.Bijective.{uA₁ + 1, uA₂ + 1} (α := A₁) (β := A₂) (⇑f : (a : A₁) → A₂)
⊢ Eq (α := (a : A₁) → A₂) (⇑(ofBijective f hf) : (a : A₁) → A₂) (⇑f : (a : A₁) → A₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
hf : Function.Bijective.{uA₁ + 1, uA₂ + 1} (α := A₁) (β := A₂) (⇑f : (a : A₁) → A₂)
a : A₁
⊢ Eq.{uA₂ + 1} (α := A₂) ((ofBijective f hf : (a : A₁) → A₂) a : A₂) ((f : (a : A₁) → A₂) a : A₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
hf : Function.Bijective.{uA₁ + 1, uA₂ + 1} (α := A₁) (β := A₂) (⇑f : (a : A₁) → A₂)
⊢ (ofBijective f hf).toLinearMap =
    (↑f :
      [inst_5 : FunLike (A₁ →ₐ[R] A₂) A₁ A₂] → [SemilinearMapClass (A₁ →ₐ[R] A₂) (RingHom.id R) A₁ A₂] → A₁ →ₗ[R] A₂)

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
hf : Function.Bijective.{uA₁ + 1, uA₂ + 1} (α := A₁) (β := A₂) (⇑f : (a : A₁) → A₂)
⊢ (↑(ofBijective f hf) : A₁ →ₐ[R] A₂) = f

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
hf : Function.Bijective.{uA₁ + 1, uA₂ + 1} (α := A₁) (β := A₂) (⇑f : (a : A₁) → A₂)
x : A₂
⊢ (f : (a : A₁) → A₂) (((ofBijective f hf).symm : (a : A₂) → A₁) x : A₁) = x

Tactic:
(ofBijective f hf).apply_symm_apply x

Premises used: AlgEquiv.ofBijective, AlgEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
hf : Function.Bijective.{uA₁ + 1, uA₂ + 1} (α := A₁) (β := A₂) (⇑f : (a : A₁) → A₂)
x : A₁
⊢ ((ofBijective f hf).symm : (a : A₂) → A₁) ((f : (a : A₁) → A₂) x : A₂) = x

Tactic:
(ofBijective f hf).symm_apply_apply x

Premises used: AlgEquiv.ofBijective, AlgEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
l : A₁ ≃ₗ[R] A₂
map_one : Eq.{uA₂ + 1} (α := A₂) ((l : (a : A₁) → A₂) 1 : A₂) (1 : A₂)
map_mul :
  ∀ (x y : A₁),
    (l : (a : A₁) → A₂) (x * y) =
      HMul.hMul (α := A₂) (β := A₂) ((l : (a : A₁) → A₂) x : A₂) ((l : (a : A₁) → A₂) y : A₂)
⊢ (ofLinearEquiv l map_one map_mul).symm = ofLinearEquiv l.symm ⋯ ⋯

Tactic:
rfl

Premises used: AlgEquiv.symm, AlgEquiv.ofLinearEquiv, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
map_mul : Eq.{uA₂ + 1} (α := A₂) (((↑e : A₁ ≃ₗ[R] A₂) : (a : A₁) → A₂) 1 : A₂) (1 : A₂)
map_one :
  ∀ (x y : A₁),
    ((↑e : A₁ ≃ₗ[R] A₂) : (a : A₁) → A₂) (x * y) =
      HMul.hMul (α := A₂) (β := A₂) (((↑e : A₁ ≃ₗ[R] A₂) : (a : A₁) → A₂) x : A₂)
        (((↑e : A₁ ≃ₗ[R] A₂) : (a : A₁) → A₂) y : A₂)
⊢ ofLinearEquiv (↑e : A₁ ≃ₗ[R] A₂) map_mul map_one = e

Tactic:
rfl

Premises used: AlgEquiv.ofLinearEquiv, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
l : A₁ ≃ₗ[R] A₂
map_one : Eq.{uA₂ + 1} (α := A₂) ((l : (a : A₁) → A₂) 1 : A₂) (1 : A₂)
map_mul :
  ∀ (x y : A₁),
    (l : (a : A₁) → A₂) (x * y) =
      HMul.hMul (α := A₂) (β := A₂) ((l : (a : A₁) → A₂) x : A₂) ((l : (a : A₁) → A₂) y : A₂)
⊢ (↑(ofLinearEquiv l map_one map_mul) : A₁ ≃ₗ[R] A₂) = l

Tactic:
rfl

Premises used: AlgEquiv.toLinearEquiv, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
x : A₁
⊢ (1 : (a : A₁) → A₁) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
e₁ e₂ : A₁ ≃ₐ[R] A₁
x : A₁
⊢ Eq (α := A₁) ((e₁ * e₂ : (a : A₁) → A₁) x : A₁) ((e₁ : (a : A₁) → A₁) ((e₂ : (a : A₁) → A₁) x : A₁) : A₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
ϕ : A₁ ≃ₐ[R] A₁
⊢ ϕ⁻¹ = ϕ.symm

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
ϕ : A₁ ≃ₐ[R] A₁
⊢ Eq (α := (a : A₁) → A₁) (⇑ϕ⁻¹ : (a : A₁) → A₁) (⇑ϕ.symm : (a : A₁) → A₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
e : A₁ ≃ₐ[R] A₁
n : ℕ
h : ∀ (x : A₁), (e ^ Nat.zero : (a : A₁) → A₁) x = (⇑e : (a : A₁) → A₁)^[Nat.zero] x
⊢ Eq (α := (a : A₁) → A₁) (⇑(e ^ Nat.zero) : (a : A₁) → A₁) (⇑e : (a : A₁) → A₁)^[Nat.zero]

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
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 : A₁
⊢ (e ^ Nat.zero : (a : A₁) → A₁) x = (⇑e : (a : A₁) → A₁)^[Nat.zero] x

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Equiv
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]
h : ∀ (x_1 : A₁), (e ^ x.succ : (a : A₁) → A₁) x_1 = (⇑e : (a : A₁) → A₁)^[x.succ] x_1
⊢ Eq (α := (a : A₁) → A₁) (⇑(e ^ x.succ) : (a : A₁) → A₁) (⇑e : (a : A₁) → A₁)^[x.succ]

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
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]
x_1 : A₁
⊢ (e ^ x.succ : (a : A₁) → A₁) x_1 = (⇑e : (a : A₁) → A₁)^[x.succ] x_1

Tactic:
simp [pow_succ, ih]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Algebra.Equiv
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₁
h :
  ∀ (a : A₂),
    Eq (α := A₂) ((ϕ.symm.trans ((ψ * χ).trans ϕ) : (a : A₂) → A₂) a : A₂)
      ((ϕ.symm.trans (ψ.trans ϕ) * ϕ.symm.trans (χ.trans ϕ) : (a : A₂) → A₂) a : A₂)
⊢ ϕ.symm.trans ((ψ * χ).trans ϕ) = ϕ.symm.trans (ψ.trans ϕ) * ϕ.symm.trans (χ.trans ϕ)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Equiv
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₁
a : A₂
⊢ Eq (α := A₂) ((ϕ.symm.trans ((ψ * χ).trans ϕ) : (a : A₂) → A₂) a : A₂)
    ((ϕ.symm.trans (ψ.trans ϕ) * ϕ.symm.trans (χ.trans ϕ) : (a : A₂) → A₂) a : A₂)

Tactic:
simp only [mul_apply, trans_apply, symm_apply_apply]

Premises used: AlgEquiv.symm_apply_apply, AlgEquiv.mul_apply, AlgEquiv.trans_apply
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
⊢ Eq.{uA₁ + 1} (α := (A₁ ≃ₐ[R] A₁) ≃* A₁ ≃ₐ[R] A₁) (autCongr refl) (MulEquiv.refl (A₁ ≃ₐ[R] A₁))

Tactic:
rfl

Premises used: MulEquiv.refl, AlgEquiv.autCongr, Equiv.trans, AlgEquiv.trans, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
ϕ : A₁ ≃ₐ[R] A₂
⊢ ϕ.autCongr.symm = ϕ.symm.autCongr

Tactic:
rfl

Premises used: AlgEquiv.autCongr, AlgEquiv.symm, AlgEquiv.trans, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
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 : Algebra R A₁
inst_5 : Algebra R A₂
inst_6 : Algebra R A₃
ϕ : A₁ ≃ₐ[R] A₂
ψ : A₂ ≃ₐ[R] A₃
⊢ ϕ.autCongr.trans ψ.autCongr = (ϕ.trans ψ).autCongr

Tactic:
rfl

Premises used: AlgEquiv.autCongr, Equiv.trans, MulEquiv.trans, AlgEquiv.trans, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
R : Type uR
A₁ : Type uA₁
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Algebra R A₁
f : A₁ ≃ₐ[R] A₁
a : A₁
⊢ f • a = (f : (a : A₁) → A₁) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
⊢ FaithfulSMul (A₁ ≃ₐ[R] A₁) A₁

Tactic:
⟨AlgEquiv.ext⟩

Premises used: FaithfulSMul.mk, AlgEquiv.ext
-- Module: Mathlib.Algebra.Algebra.Equiv
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₂
S : Type u_1
inst_13 : SMul S R
inst_14 : SMul S A₁
inst_15 : IsScalarTower S R A₁
⊢ SMulCommClass (A₁ ≃ₐ[R] A₁) S A₁

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm