awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := A ≃+* Aᵐᵒᵖᵐᵒᵖ) (toRingEquiv (opOp R A)) (RingEquiv.opOp A)

Tactic:
rfl

Premises used: Equiv.trans, RingEquiv.opOp, rfl
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
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
f : A →ₐ[R] B
hf : ∀ (x y : A), Commute.{u_4} (S := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
⊢ (f.fromOpposite hf).toLinearMap = f.toLinearMap ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
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
f : A →ₐ[R] B
hf : ∀ (x y : A), Commute.{u_4} (S := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
⊢ (↑(f.fromOpposite hf) : Aᵐᵒᵖ →+* B) = RingHom.fromOpposite (↑f : A →+* B) hf

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, RingHom.fromOpposite, rfl
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
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
f : A →ₐ[R] B
hf : ∀ (x y : A), Commute.{u_4} (S := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
⊢ (f.toOpposite hf).toLinearMap = (↑(opLinearEquiv R) : B →ₗ[R] Bᵐᵒᵖ) ∘ₗ f.toLinearMap

Tactic:
rfl

Premises used: rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
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
f : A →ₐ[R] B
hf : ∀ (x y : A), Commute.{u_4} (S := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
⊢ (↑(f.toOpposite hf) : A →+* Bᵐᵒᵖ) = RingHom.toOpposite (↑f : A →+* B) hf

Tactic:
rfl

Premises used: RingHom.toOpposite, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
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
f : A →ₐ[R] B
⊢ Eq (α := RingHom.{u_3, u_4} Aᵐᵒᵖ Bᵐᵒᵖ)
    (toRingHom.{u_1, u_3, u_4} (R := R) ((AlgHom.op : (a : A →ₐ[R] B) → Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) f))
    ((RingHom.op : (a : A →+* B) → Aᵐᵒᵖ →+* Bᵐᵒᵖ) f.toRingHom)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
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
f : AlgHom.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ
⊢ Eq (α := A →+* B) (toRingHom.{u_1, u_3, u_4} (R := R) ((unop : (a : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) → A →ₐ[R] B) f))
    ((RingHom.unop : (a : Aᵐᵒᵖ →+* Bᵐᵒᵖ) → A →+* B) f.toRingHom)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
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
f : A ≃ₐ[R] B
⊢ Eq (α := AlgHom.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) (↑((op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) f) : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ)
    ((AlgHom.op : (a : A →ₐ[R] B) → Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) (↑f : A →ₐ[R] B))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
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
f : A ≃ₐ[R] B
⊢ Eq (α := RingEquiv.{u_3, u_4} Aᵐᵒᵖ Bᵐᵒᵖ)
    (toRingEquiv.{u_1, u_3, u_4} (R := R) ((op : (a : A ≃ₐ[R] B) → Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) f))
    ((RingEquiv.op : (a : A ≃+* B) → Aᵐᵒᵖ ≃+* Bᵐᵒᵖ) f.toRingEquiv)

Tactic:
rfl

Premises used: Equiv.trans, rfl
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
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
f : AlgEquiv.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ
⊢ Eq (α := A →ₐ[R] B) (↑((unop : (a : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) → A ≃ₐ[R] B) f) : A →ₐ[R] B)
    ((AlgHom.unop : (a : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) → A →ₐ[R] B) (↑f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
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
f : AlgEquiv.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ
⊢ Eq (α := A ≃+* B) (toRingEquiv.{u_1, u_3, u_4} (R := R) ((unop : (a : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) → A ≃ₐ[R] B) f))
    ((RingEquiv.unop : (a : Aᵐᵒᵖ ≃+* Bᵐᵒᵖ) → A ≃+* B) f.toRingEquiv)

Tactic:
rfl

Premises used: Equiv.trans, rfl
-- Module: Mathlib.Algebra.Algebra.Opposite
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Opposite
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 (α := 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:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Opposite
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Opposite
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 (α := 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:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
⊢ Eq (α := A ≃+* Aᵐᵒᵖ) (toRingEquiv (toOpposite R A)) (RingEquiv.toOpposite A)

Tactic:
rfl

Premises used: MulOpposite.opEquiv, RingEquiv.toOpposite, rfl
-- Module: Mathlib.Algebra.Algebra.Opposite
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
⊢ Eq (α := A ≃ₗ[R] Aᵐᵒᵖ) (↑(toOpposite R A) : A ≃ₗ[R] Aᵐᵒᵖ) (opLinearEquiv R)

Tactic:
rfl

Premises used: MulOpposite.opLinearEquiv, AlgEquiv.toLinearEquiv, rfl
-- Module: Mathlib.Algebra.Algebra.Pi
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
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
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Pi
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
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:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Pi
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
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
⊢ 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

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Pi
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
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:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Pi
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
⊢ Eq (α := (i : ι) → A i) ((algebraMap R ((i : ι) → A i) : (a : R) → (i : ι) → A i) a : (i : ι) → A i) fun (i : ι) ↦
    ((algebraMap R (A i) : (a : R) → A i) a : A i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Pi
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
i : ι
⊢ Eq.{u_3 + 1} (α := A i) ((algebraMap R ((i : ι) → A i) : (a : R) → (i : ι) → A i) a i : A i)
    ((algebraMap R (A i) : (a : R) → A i) a : A i)

Tactic:
rfl

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

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Pi
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
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:
simp
-- Module: Mathlib.Algebra.Algebra.Pi
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)
⊢ Eq (α := ((i : ι) → A i) →ₐ[R] (i : ι) → A i) (algHom R A (evalAlgHom R A)) (AlgHom.id R ((i : ι) → A i))

Tactic:
rfl

Premises used: Pi.algHom, AlgHom.id, Pi.ringHom, rfl
-- Module: Mathlib.Algebra.Algebra.Pi
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
C : Type u_5
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
g : (i : ι) → AlgHom.{u_2, u_5, u_3} R C (A i)
h : B →ₐ[R] C
⊢ (algHom R A g).comp h = algHom R A fun (i : ι) ↦ (g i).comp h

Tactic:
rfl

Premises used: Pi.algHom, Pi.ringHom, AlgHom.comp, rfl
-- Module: Mathlib.Algebra.Algebra.Pi
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)
S : ι → Type u_4
inst_3 : (i : ι) → CommSemiring (S i)
⊢ Eq (α := Algebra ((i : ι) → S i) ((i : ι) → S i)) (instAlgebraForall S S) (Algebra.id ((i : ι) → S i))

Tactic:
rfl

Premises used: Pi.ringHom, rfl
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_5
⊢ Eq (α := R →+* A → R) (constRingHom A R) (algebraMap R (A → R))

Tactic:
rfl

Premises used: Pi.ringHom, Pi.constRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_5
⊢ Eq (α := R →ₐ[R] A → R) (constAlgHom R A R) (Algebra.ofId R (A → R))

Tactic:
rfl

Premises used: Pi.constAlgHom, Pi.ringHom, Algebra.ofId, rfl
-- Module: Mathlib.Algebra.Algebra.Pi
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Pi
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
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:
f.commutes' c

Premises used: AlgHom.commutes'
-- Module: Mathlib.Algebra.Algebra.Pi
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
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:
exact f.commutes' c

Premises used: AlgHom.commutes'
-- Module: Mathlib.Algebra.Algebra.Pi
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
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)
⊢ 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)

Tactic:
ext i
-- Module: Mathlib.Algebra.Algebra.Pi
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
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:
simp
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A₁ i)
inst_2 : (i : ι) → Algebra.{u_3, u_5} R (A₁ i)
⊢ Eq (α := ((i : ι) → A₁ i) ≃ₐ[R] (i : ι) → A₁ i) (piCongrRight (A₁ := A₁) (A₂ := A₁) fun (i : ι) ↦ refl) refl

Tactic:
rfl

Premises used: AlgEquiv.piCongrRight, AlgEquiv.refl, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A₁ i)
inst_2 : (i : ι) → Semiring (A₂ i)
inst_3 : (i : ι) → Algebra.{u_3, u_5} R (A₁ i)
inst_4 : (i : ι) → Algebra.{u_3, u_6} R (A₂ i)
e : (i : ι) → AlgEquiv.{u_3, u_5, u_6} R (A₁ i) (A₂ i)
⊢ (piCongrRight (A₁ := A₁) (A₂ := A₂) e).symm = piCongrRight (A₁ := A₂) (A₂ := A₁) fun (i : ι) ↦ (e i).symm

Tactic:
rfl

Premises used: AlgEquiv.symm, AlgEquiv.piCongrRight, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
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)
e₂ : (i : ι) → AlgEquiv.{u_3, u_6, u_7} R (A₂ i) (A₃ i)
⊢ (piCongrRight (A₁ := A₁) (A₂ := A₂) e₁).trans (piCongrRight (A₁ := A₂) (A₂ := A₃) e₂) =
    piCongrRight (A₁ := A₁) (A₂ := A₃) fun (i : ι) ↦ (e₁ i).trans (e₂ i)

Tactic:
rfl

Premises used: Equiv.trans, AlgEquiv.piCongrRight, AlgEquiv.trans, rfl
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A₁ i)
inst_2 : (i : ι) → Algebra.{u_3, u_5} R (A₁ i)
ι' : Type u_8
e : ι ≃ ι'
x : (i : ι) → A₁ i
⊢ Eq (α := (i : ι') → A₁ ((e.symm : (a : ι') → ι) i))
    ((piCongrLeft' R A₁ e : (a : (i : ι) → A₁ i) → (i : ι') → A₁ ((e.symm : (a : ι') → ι) i)) x :
      (i : ι') → A₁ ((e.symm : (a : ι') → ι) i))
    ((Equiv.piCongrLeft' A₁ e : (a : (a : ι) → A₁ a) → (b : ι') → A₁ ((e.symm : (a : ι') → ι) b)) x :
      (b : ι') → A₁ ((e.symm : (a : ι') → ι) b))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A₁ i)
inst_2 : (i : ι) → Algebra.{u_3, u_5} R (A₁ i)
ι' : Type u_8
e : ι ≃ ι'
x : (i : ι') → A₁ ((e.symm : (a : ι') → ι) i)
⊢ Eq (α := (i : ι) → A₁ i)
    ((symm (piCongrLeft' R A₁ e) : (a : (i : ι') → A₁ ((e.symm : (a : ι') → ι) i)) → (i : ι) → A₁ i) x : (i : ι) → A₁ i)
    (((Equiv.piCongrLeft' A₁ e).symm : (a : (b : ι') → A₁ ((e.symm : (a : ι') → ι) b)) → (a : ι) → A₁ a) x :
      (a : ι) → A₁ a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A₁ i)
inst_2 : (i : ι) → Algebra.{u_3, u_5} R (A₁ i)
ι' : Type u_8
e : ι' ≃ ι
x : (i : ι') → A₁ ((e : (a : ι') → ι) i)
⊢ Eq (α := (i : ι) → A₁ i)
    ((piCongrLeft R A₁ e : (a : (i : ι') → A₁ ((e : (a : ι') → ι) i)) → (i : ι) → A₁ i) x : (i : ι) → A₁ i)
    ((Equiv.piCongrLeft A₁ e : (a : (a : ι') → A₁ ((e : (a : ι') → ι) a)) → (b : ι) → A₁ b) x : (b : ι) → A₁ b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A₁ i)
inst_2 : (i : ι) → Algebra.{u_3, u_5} R (A₁ i)
ι' : Type u_8
e : ι' ≃ ι
x : (i : ι) → A₁ i
⊢ Eq (α := (i : ι') → A₁ ((e : (a : ι') → ι) i))
    ((symm (piCongrLeft R A₁ e) : (a : (i : ι) → A₁ i) → (i : ι') → A₁ ((e : (a : ι') → ι) i)) x :
      (i : ι') → A₁ ((e : (a : ι') → ι) i))
    (((Equiv.piCongrLeft A₁ e).symm : (a : (b : ι) → A₁ b) → (a : ι') → A₁ ((e : (a : ι') → ι) a)) x :
      (a : ι') → A₁ ((e : (a : ι') → ι) a))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Pi
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
inst_9 : Unique ι
⊢ ∀ (x : R),
    Eq.{u_8 + 1} (α := S)
      (((RingEquiv.piUnique fun (i : ι) ↦ S : ((i : ι) → S) ≃+* S) : (a : ι → S) → S)
          ((algebraMap R (ι → S) : (a : R) → ι → S) x : ι → S) :
        S)
      ((algebraMap R S : (a : R) → S) x : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
R : Type u_3
ι : Type u_4
inst : CommSemiring R
S : Type u_8
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Unique ι
x : ι → S
⊢ Eq.{u_8 + 1} (α := S) ((funUnique R ι S : (a : ι → S) → S) x : S) ((Equiv.funUnique ι S : (a : ι → S) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Pi
Goal:
R : Type u_3
ι : Type u_4
inst : CommSemiring R
S : Type u_8
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Unique ι
x : S
⊢ Eq (α := ι → S) ((symm (funUnique R ι S) : (a : S) → ι → S) x : ι → S)
    (((Equiv.funUnique ι S).symm : (a : S) → ι → S) x : ι → S)

Tactic:
rfl

Premises used: Eq.mpr, uniqueElim, rfl