awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
a : A
m : M
x : A
⊢ ∀ (x_1 y : A), x ⊗ₜ[R] ((x_1 + y) • m) = HAdd.hAdd (α := A ⊗[R] M) (x ⊗ₜ[R] (x_1 • m)) (x ⊗ₜ[R] (y • m))

Tactic:
simp [add_smul, tmul_add]

Premises used: add_smul, TensorProduct.tmul_add
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
a : A
m : M
x : A
⊢ ∀ (m_1 : R) (x_1 : A),
    x ⊗ₜ[R] ((m_1 • x_1) • m) =
      HSMul.hSMul (α := R) (β := A ⊗[R] M) ((RingHom.id R : (a : R) → R) m_1 : R) (x ⊗ₜ[R] (x_1 • m))

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
a : A
m : M
x y : A
h :
  ∀ (x_1 : A),
    Eq (α := A ⊗[R] M)
      (({ toFun := fun (y_1 : A) ↦ (x + y) ⊗ₜ[R] (y_1 • m), map_add' := ⋯, map_smul' := ⋯ } : (a : A) → A ⊗[R] M) x_1 :
        A ⊗[R] M)
      ((HAdd.hAdd (α := A →ₗ[R] A ⊗[R] M)
              { toFun := fun (y : A) ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] A ⊗[R] M }
              { toFun := fun (y_1 : A) ↦ y ⊗ₜ[R] (y_1 • m), map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] A ⊗[R] M } :
            (a : A) → A ⊗[R] M)
          x_1 :
        A ⊗[R] M)
⊢ { toFun := fun (y_1 : A) ↦ (x + y) ⊗ₜ[R] (y_1 • m), map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := A →ₗ[R] A ⊗[R] M)
      { toFun := fun (y : A) ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] A ⊗[R] M }
      { toFun := fun (y_1 : A) ↦ y ⊗ₜ[R] (y_1 • m), map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] A ⊗[R] M }

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
a : A
m : M
x y x_1 : A
⊢ Eq (α := A ⊗[R] M)
    (({ toFun := fun (y_1 : A) ↦ (x + y) ⊗ₜ[R] (y_1 • m), map_add' := ⋯, map_smul' := ⋯ } : (a : A) → A ⊗[R] M) x_1 :
      A ⊗[R] M)
    ((HAdd.hAdd (α := A →ₗ[R] A ⊗[R] M)
            { toFun := fun (y : A) ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] A ⊗[R] M }
            { toFun := fun (y_1 : A) ↦ y ⊗ₜ[R] (y_1 • m), map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] A ⊗[R] M } :
          (a : A) → A ⊗[R] M)
        x_1 :
      A ⊗[R] M)

Tactic:
simp [add_tmul]

Premises used: TensorProduct.add_tmul
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
a : A
m : M
m_1 : R
x : A
h :
  ∀ (x_1 : A),
    Eq (α := A ⊗[R] M)
      (({ toFun := fun (y : A) ↦ (m_1 • x) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } : (a : A) → A ⊗[R] M) x_1 :
        A ⊗[R] M)
      ((HSMul.hSMul (α := R) (β := A →ₗ[R] A ⊗[R] M) ((RingHom.id R : (a : R) → R) m_1 : R)
              { toFun := fun (y : A) ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] A ⊗[R] M } :
            (a : A) → A ⊗[R] M)
          x_1 :
        A ⊗[R] M)
⊢ { toFun := fun (y : A) ↦ (m_1 • x) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := A →ₗ[R] A ⊗[R] M) ((RingHom.id R : (a : R) → R) m_1 : R)
      { toFun := fun (y : A) ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] A ⊗[R] M }

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
a : A
m : M
m_1 : R
x x_1 : A
⊢ Eq (α := A ⊗[R] M)
    (({ toFun := fun (y : A) ↦ (m_1 • x) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } : (a : A) → A ⊗[R] M) x_1 :
      A ⊗[R] M)
    ((HSMul.hSMul (α := R) (β := A →ₗ[R] A ⊗[R] M) ((RingHom.id R : (a : R) → R) m_1 : R)
            { toFun := fun (y : A) ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] A ⊗[R] M } :
          (a : A) → A ⊗[R] M)
        x_1 :
      A ⊗[R] M)

Tactic:
simp [smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
a : A
m : M
f : A ⊗[R] A →ₗ[R] A ⊗[R] M :=
  lift
    { toFun := fun (x : A) ↦ { toFun := fun (y : A) ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }
⊢ Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (a • m)) (a ⊗ₜ[R] m)

Tactic:
simpa [f] using congr_arg f (tmul_comm R 1 a)

Premises used: congr_arg, Algebra.tmul_comm, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
m : M
⊢ ((AlgebraTensorModule.lift (LinearMap.restrictScalarsₗ R A M M A ∘ₗ LinearMap.lsmul A M) : A ⊗[R] M →ₗ[A] M) :
        (a : A ⊗[R] M) → M)
      (1 ⊗ₜ[R] m) =
    m

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
a : A
m : M
⊢ (lid' R A M : (a : A ⊗[R] M) → M) (a ⊗ₜ[R] m) = a • m

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Algebra.Epi
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Algebra.IsEpi R A
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module A M
inst_7 : IsScalarTower R A M
m : M
⊢ Eq.{u_3 + 1} (α := M)
    ((lid' R A M : (a : A ⊗[R] M) → M) ((LinearEquiv.symm (lid' R A M) : (a : M) → A ⊗[R] M) m : A ⊗[R] M) : M)
    ((lid' R A M : (a : A ⊗[R] M) → M) (1 ⊗ₜ[R] m) : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : EquivLike F A B
h : AlgEquivClass F R A B
⊢ AlgHomClass F R A B

Tactic:
{ h with }

Premises used: AlgEquivClass.commutes, AlgHomClass.mk
-- Module: Mathlib.Algebra.Algebra.Equiv
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : EquivLike F A B
h : AlgEquivClass F R A B
⊢ LinearEquivClass F R A B

Tactic:
{ h with map_smulₛₗ := fun f => map_smulₛₗ f }

Premises used: MulActionSemiHomClass.map_smulₛₗ, SemilinearEquivClass.mk
-- 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 f g : A₁ ≃ₐ[R] A₂
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
obtain :
  ∀ (f : A₁ → A₂) (invFun : A₂ → A₁) (left_inv : Function.LeftInverse invFun f)
    (right_inv : Function.RightInverse invFun f)
    (map_mul' :
      ∀ (x y : A₁),
        { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun (x * y) =
          { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun x *
            { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun y)
    (map_add' :
      ∀ (x y : A₁),
        { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun (x + y) =
          { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun x +
            { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun y)
    (commutes' :
      ∀ (r : R),
        { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A₁ ≃ A₂ }.toFun
            ((algebraMap R A₁ : (a : R) → A₁) r) =
          (algebraMap R A₂ : (a : R) → A₂) r)
    (h₁ :
      { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
            map_add' := map_add', commutes' := commutes' : A₁ ≃ₐ[R] A₂ }.toFun =
        g.toFun)
    (h₂ :
      { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
            map_add' := map_add', commutes' := commutes' : A₁ ≃ₐ[R] A₂ }.invFun =
        g.invFun),
    { toFun := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
        map_add' := map_add', commutes' := commutes' : A₁ ≃ₐ[R] A₂ } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨f, _⟩, _⟩ := f
-- 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 g : A₁ ≃ₐ[R] A₂
h : ∀ (a : A₁), Eq.{uA₂ + 1} (α := A₂) ((f : (a : A₁) → A₂) a : A₂) ((g : (a : A₁) → A₂) a : A₂)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.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 x' : A₁
⊢ x = x' → Eq.{uA₂ + 1} (α := A₂) ((f : (a : A₁) → A₂) x : A₂) ((f : (a : A₁) → A₂) x' : A₂)

Tactic:
DFunLike.congr_arg f

Premises used: DFunLike.congr_arg
-- 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 g : A₁ ≃ₐ[R] A₂
h : f = g
x : A₁
⊢ Eq.{uA₂ + 1} (α := A₂) ((f : (a : A₁) → A₂) x : A₂) ((g : (a : A₁) → A₂) x : A₂)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- 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₂
toEquiv : A₁ ≃ A₂
map_mul : ∀ (x y : A₁), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y
map_add : ∀ (x y : A₁), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y
commutes : ∀ (r : R), toEquiv.toFun ((algebraMap R A₁ : (a : R) → A₁) r) = (algebraMap R A₂ : (a : R) → A₂) r
⊢ Eq (α := (a : A₁) → A₂)
    (⇑{ toEquiv := toEquiv, map_mul' := map_mul, map_add' := map_add, commutes' := commutes : A₁ ≃ₐ[R] A₂ } :
      (a : A₁) → A₂)
    (⇑toEquiv : (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₂
e' : A₂ → A₁
h₁ : Function.LeftInverse e' (⇑e : (a : A₁) → A₂)
h₂ : Function.RightInverse e' (⇑e : (a : A₁) → A₂)
h₃ :
  ∀ (x y : A₁),
    { toFun := (⇑e : (a : A₁) → A₂), invFun := e', left_inv := h₁, right_inv := h₂ : A₁ ≃ A₂ }.toFun (x * y) =
      { toFun := (⇑e : (a : A₁) → A₂), invFun := e', left_inv := h₁, right_inv := h₂ : A₁ ≃ A₂ }.toFun x *
        { toFun := (⇑e : (a : A₁) → A₂), invFun := e', left_inv := h₁, right_inv := h₂ : A₁ ≃ A₂ }.toFun y
h₄ :
  ∀ (x y : A₁),
    { toFun := (⇑e : (a : A₁) → A₂), invFun := e', left_inv := h₁, right_inv := h₂ : A₁ ≃ A₂ }.toFun (x + y) =
      { toFun := (⇑e : (a : A₁) → A₂), invFun := e', left_inv := h₁, right_inv := h₂ : A₁ ≃ A₂ }.toFun x +
        { toFun := (⇑e : (a : A₁) → A₂), invFun := e', left_inv := h₁, right_inv := h₂ : A₁ ≃ A₂ }.toFun y
h₅ :
  ∀ (r : R),
    { toFun := (⇑e : (a : A₁) → A₂), invFun := e', left_inv := h₁, right_inv := h₂ : A₁ ≃ A₂ }.toFun
        ((algebraMap R A₁ : (a : R) → A₁) r) =
      (algebraMap R A₂ : (a : R) → A₂) r
⊢ { toFun := (⇑e : (a : A₁) → A₂), invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄,
      commutes' := h₅ : A₁ ≃ₐ[R] A₂ } =
    e

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₂
e : A₁ ≃ₐ[R] A₂
⊢ e.toEquiv = (↑e : A₁ ≃ A₂)

Tactic:
rfl

Premises used: EquivLike.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₂
F : Type u_1
inst_5 : EquivLike F A₁ A₂
inst_6 : AlgEquivClass F R A₁ A₂
f : F
⊢ Eq (α := (a : A₁) → A₂) (⇑(↑f : A₁ ≃ₐ[R] A₂) : (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₂
⊢ Function.Injective (β := A₁ → A₂) fun (e : A₁ ≃ₐ[R] A₂) ↦ (⇑e : (a : A₁) → A₂)

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_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₂
⊢ Eq (α := (a : A₁) → A₂) (⇑(↑e : A₁ ≃ 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₂
⊢ e.toRingEquiv = e.toRingEquiv

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₂) (↑e.toRingEquiv : A₁ →+* A₂) (↑e : A₁ →+* A₂)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, 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.toRingEquiv : (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₂
⊢ Function.Injective (α := A₁ ≃ₐ[R] A₂) toRingEquiv

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

Premises used: RingEquiv.congr_fun, AlgEquiv.ext, 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₂) = (↑e : A₁ →ₐ[R] 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₂
x : A₁
⊢ Eq.{uA₂ + 1} (α := A₂) (((↑e : A₁ →ₐ[R] A₂) : (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₂
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₂
⊢ Function.Injective (α := A₁ ≃ₐ[R] A₂) toAlgHom

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

Premises used: AlgEquiv.ext, AlgHom.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₂
⊢ Eq (α := A₁ →+* A₂) (↑(↑e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) (↑e : A₁ →+* A₂)

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, 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₂) (↑(↑e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) (↑e.toRingEquiv : A₁ →+* A₂)

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, 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₂
⊢ ∀ (r : R),
    Eq.{uA₂ + 1} (α := A₂) ((e : (a : A₁) → A₂) ((algebraMap R A₁ : (a : R) → A₁) r : A₁) : A₂)
      ((algebraMap R A₂ : (a : R) → A₂) r : A₂)

Tactic:
e.commutes'

Premises used: AlgEquiv.commutes'
-- 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₂
⊢ Function.Bijective.{uA₁ + 1, uA₂ + 1} (α := A₁) (β := A₂) (⇑e : (a : A₁) → A₂)

Tactic:
EquivLike.bijective e

Premises used: EquivLike.bijective
-- 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₂
⊢ Function.Injective.{uA₁ + 1, uA₂ + 1} (α := A₁) (β := A₂) (⇑e : (a : A₁) → A₂)

Tactic:
EquivLike.injective e

Premises used: EquivLike.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₂
⊢ Function.Surjective.{uA₁ + 1, uA₂ + 1} (α := A₁) (β := A₂) (⇑e : (a : A₁) → A₂)

Tactic:
EquivLike.surjective e

Premises used: EquivLike.surjective
-- 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₁) (AlgHom.id R A₁)

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, AlgHom.id, 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₁ →+* A₁) (↑refl : A₁ →+* A₁) (RingHom.id A₁)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, 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.{uA₁ + 1} (α := (a : A₁) → A₁) (⇑refl : (a : A₁) → A₁) id

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_1 e : A₁ ≃ₐ[R] A₂
r : R
rw :
  e.toRingEquiv.symm.toFun ((algebraMap R A₂ : (a : R) → A₂) r) =
    (e.toRingEquiv.symm : (a : A₂) → A₁)
      ((e.toRingEquiv : (a : A₁) → A₂) ((algebraMap R A₁ : (a : R) → A₁) r : A₁) : A₂)
⊢ e.toRingEquiv.symm.toFun ((algebraMap R A₂ : (a : R) → A₂) r) = (algebraMap R A₁ : (a : R) → A₁) r

Tactic:
rw [← e.toRingEquiv.symm_apply_apply (algebraMap R A₁ r)]

Premises used: Algebra.algebraMap, RingEquiv.symm_apply_apply, AlgEquiv.toRingEquiv, DFunLike.coe
-- 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₂
r : R
e_a :
  Eq.{uA₂ + 1} (α := A₂) ((algebraMap R A₂ : (a : R) → A₂) r : A₂)
    ((e.toRingEquiv : (a : A₁) → A₂) ((algebraMap R A₁ : (a : R) → A₁) r : A₁) : A₂)
⊢ e.toRingEquiv.symm.toFun ((algebraMap R A₂ : (a : R) → A₂) r) =
    (e.toRingEquiv.symm : (a : A₂) → A₁)
      ((e.toRingEquiv : (a : A₁) → A₂) ((algebraMap R A₁ : (a : R) → A₁) r : A₁) : A₂)

Tactic:
congr
-- 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₂
r : R
⊢ Eq.{uA₂ + 1} (α := A₂) ((algebraMap R A₂ : (a : R) → A₂) r : A₂)
    ((e.toRingEquiv : (a : A₁) → A₂) ((algebraMap R A₁ : (a : R) → A₁) r : A₁) : 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₂
e : A₁ ≃ₐ[R] A₂
⊢ e.invFun = (⇑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₂
inst : CommSemiring R
inst_1 : Semiring A₁
inst_2 : Semiring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
F : Type u_1
inst_5 : EquivLike F A₁ A₂
inst_6 : AlgEquivClass F R A₁ A₂
f : F
x : A₂
⊢ (f : (a : A₁) → A₂) ((symm (↑f : A₁ ≃ₐ[R] A₂) : (a : A₂) → A₁) x : A₁) = x

Tactic:
EquivLike.right_inv f x

Premises used: EquivLike.right_inv
-- 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 : Type u_1
inst_5 : EquivLike F A₁ A₂
inst_6 : AlgEquivClass F R A₁ A₂
f : F
x : A₁
⊢ (symm (↑f : A₁ ≃ₐ[R] A₂) : (a : A₂) → A₁) ((f : (a : A₁) → A₂) x : A₂) = x

Tactic:
EquivLike.left_inv f x

Premises used: EquivLike.left_inv
-- 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₁ ≃ A₂).symm = (↑e.symm : A₂ ≃ A₁)

Tactic:
rfl

Premises used: Equiv.symm, EquivLike.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₂
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: AlgEquiv.symm, Equiv.symm, rfl