awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BrauerGroup.Defs
Goal:
K : Type u
inst : Field K
A : CSA.{u, u_1} K
B : CSA.{u, u_2} K
C : CSA.{u, u_3} K
hAB : IsBrauerEquivalent A B
hBC : IsBrauerEquivalent B C
obtain :
  ∀ (n m : ℕ) (hn : n ≠ 0) (hm : m ≠ 0)
    (iso1 :
      AlgEquiv.{u, u_1, u_2} K (Matrix (Fin n) (Fin n) (↑A.toAlgCat : Type u_1))
        (Matrix (Fin m) (Fin m) (↑B.toAlgCat : Type u_2))),
    IsBrauerEquivalent A C
⊢ IsBrauerEquivalent A C

Tactic:
obtain ⟨n, m, hn, hm, ⟨iso1⟩⟩ := hAB
-- Module: Mathlib.Algebra.BrauerGroup.Defs
Goal:
K : Type u
inst : Field K
A : CSA.{u, u_1} K
B : CSA.{u, u_2} K
C : CSA.{u, u_3} K
hBC : IsBrauerEquivalent B C
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 :
  AlgEquiv.{u, u_1, u_2} K (Matrix (Fin n) (Fin n) (↑A.toAlgCat : Type u_1))
    (Matrix (Fin m) (Fin m) (↑B.toAlgCat : Type u_2))
obtain :
  ∀ (p q : ℕ) (hp : p ≠ 0) (hq : q ≠ 0)
    (iso2 :
      AlgEquiv.{u, u_2, u_3} K (Matrix (Fin p) (Fin p) (↑B.toAlgCat : Type u_2))
        (Matrix (Fin q) (Fin q) (↑C.toAlgCat : Type u_3))),
    IsBrauerEquivalent A C
⊢ IsBrauerEquivalent A C

Tactic:
obtain ⟨p, q, hp, hq, ⟨iso2⟩⟩ := hBC
-- Module: Mathlib.Algebra.BrauerGroup.Defs
Goal:
K : Type u
inst : Field K
A : CSA.{u, u_1} K
B : CSA.{u, u_2} K
C : CSA.{u, u_3} K
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 :
  AlgEquiv.{u, u_1, u_2} K (Matrix (Fin n) (Fin n) (↑A.toAlgCat : Type u_1))
    (Matrix (Fin m) (Fin m) (↑B.toAlgCat : Type u_2))
p q : ℕ
hp : p ≠ 0
hq : q ≠ 0
iso2 :
  AlgEquiv.{u, u_2, u_3} K (Matrix (Fin p) (Fin p) (↑B.toAlgCat : Type u_2))
    (Matrix (Fin q) (Fin q) (↑C.toAlgCat : Type u_3))
⊢ p * n ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.BrauerGroup.Defs
Goal:
K : Type u
inst : Field K
A : CSA.{u, u_1} K
B : CSA.{u, u_2} K
C : CSA.{u, u_3} K
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 :
  AlgEquiv.{u, u_1, u_2} K (Matrix (Fin n) (Fin n) (↑A.toAlgCat : Type u_1))
    (Matrix (Fin m) (Fin m) (↑B.toAlgCat : Type u_2))
p q : ℕ
hp : p ≠ 0
hq : q ≠ 0
iso2 :
  AlgEquiv.{u, u_2, u_3} K (Matrix (Fin p) (Fin p) (↑B.toAlgCat : Type u_2))
    (Matrix (Fin q) (Fin q) (↑C.toAlgCat : Type u_3))
⊢ m * q ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.BrauerGroup.Defs
Goal:
K : Type u
inst : Field K
A : CSA.{u, u_1} K
B : CSA.{u, u_2} K
C : CSA.{u, u_3} K
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 :
  AlgEquiv.{u, u_1, u_2} K (Matrix (Fin n) (Fin n) (↑A.toAlgCat : Type u_1))
    (Matrix (Fin m) (Fin m) (↑B.toAlgCat : Type u_2))
p q : ℕ
hp : p ≠ 0
hq : q ≠ 0
iso2 :
  AlgEquiv.{u, u_2, u_3} K (Matrix (Fin p) (Fin p) (↑B.toAlgCat : Type u_2))
    (Matrix (Fin q) (Fin q) (↑C.toAlgCat : Type u_3))
⊢ IsBrauerEquivalent A C

Tactic:
exact ⟨p * n, m * q, by simp_all, by simp_all,
    ⟨reindexAlgEquiv _ _ finProdFinEquiv |>.symm.trans <| compAlgEquiv _ _ _ _|>.symm.trans <|
    iso1.mapMatrix (m := Fin p)|>.trans <| compAlgEquiv _ _ _ _|>.trans <|
    reindexAlgEquiv K B (.prodComm (Fin p) (Fin m))|>.trans <| compAlgEquiv _ _ _ _|>.symm.trans <|
    iso2.mapMatrix.trans <| compAlgEquiv _ _ _ _|>.trans <| reindexAlgEquiv _ _ finProdFinEquiv⟩⟩
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : Ring X
inst_2 : Algebra R X
⊢ (↑(of R X) : Type v) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A : AlgCat.{v, u} R
⊢ Hom.hom (𝟙 A) = AlgHom.id R (↑A : Type v)

Tactic:
rfl

Premises used: AlgHom.id, rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A : AlgCat.{v, u} R
a : (↑A : Type v)
⊢ (@ConcreteCategory.hom _ (instCategory R) (fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v))
          carrier
          (fun (X Y : AlgCat.{v, u} R) ↦
            (AlgHom.funLike : FunLike ((↑X : Type v) →ₐ[R] (↑Y : Type v)) (↑X : Type v) (↑Y : Type v)))
          _ _ _ (𝟙 A : A ⟶ A) :
        (a : (↑A : Type v)) → (↑A : Type v))
      a =
    a

Tactic:
simp
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B C : AlgCat.{v, u} R
f : A ⟶ B
g : B ⟶ C
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: AlgHom.comp, rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B C : AlgCat.{v, u} R
f : A ⟶ B
g : B ⟶ C
a : (↑A : Type v)
⊢ Eq (α := (↑C : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier)
            (f ≫ g) :
          (a : (↑A : Type v)) → (↑C : Type v))
        a :
      (↑C : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier)
            g :
          (a : (↑B : Type v)) → (↑C : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
                carrier) f :
              (a : (↑A : Type v)) → (↑B : Type v))
            a :
          (↑B : Type v)) :
      (↑C : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B : AlgCat.{v, u} R
f g : A ⟶ B
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: AlgCat.Hom.ext
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : Type v
inst_1 : Ring X
inst_2 : Algebra R X
inst_3 : Ring Y
inst_4 : Algebra R Y
f : X →ₐ[R] Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B : AlgCat.{v, u} R
f : A ⟶ B
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : Ring X
inst_2 : Algebra R X
⊢ Eq (α := Quiver.Hom (V := AlgCat.{v, u} R) (of R X) (of R X)) (ofHom (AlgHom.id R X)) (𝟙 (of R X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : Type v
inst_1 : Ring X
inst_2 : Ring Y
inst_3 : Ring Z
inst_4 : Algebra R X
inst_5 : Algebra R Y
inst_6 : Algebra R Z
f : X →ₐ[R] Y
g : Y →ₐ[R] Z
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : Type v
inst_1 : Ring X
inst_2 : Algebra R X
inst_3 : Ring Y
inst_4 : Algebra R Y
f : X →ₐ[R] Y
x : X
⊢ Eq (α := (↑(of R Y) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier)
            (ofHom f) :
          (a : (↑(of R X) : Type v)) → (↑(of R Y) : Type v))
        x :
      (↑(of R Y) : Type v))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B : AlgCat.{v, u} R
e : A ≅ B
x : (↑A : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier)
          e.inv :
        (a : (↑B : Type v)) → (↑A : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier)
              e.hom :
            (a : (↑A : Type v)) → (↑B : Type v))
          x :
        (↑B : Type v)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B : AlgCat.{v, u} R
e : A ≅ B
x : (↑B : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier)
          e.hom :
        (a : (↑A : Type v)) → (↑B : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier)
              e.inv :
            (a : (↑B : Type v)) → (↑A : Type v))
          x :
        (↑A : Type v)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A : AlgCat.{v, u} R
⊢ Functor.obj
      (forget (AlgCat.{v, u} R) (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
        carrier))
      A =
    (↑A : Type v)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B : AlgCat.{v, u} R
f : A ⟶ B
⊢ Eq (α :=
    (a :
        (fun (X : Type v) ↦ X)
          (Functor.obj
            (forget (AlgCat.{v, u} R) (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
              carrier))
            A)) →
      (fun (X : Type v) ↦ X)
        (Functor.obj
          (forget (AlgCat.{v, u} R) (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
            carrier))
          B))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget (AlgCat.{v, u} R) (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
              carrier))
            f)) :
      (a : (fun (X : Type v) ↦ X) ((forget (AlgCat R)).obj A)) → (fun (X : Type v) ↦ X) ((forget (AlgCat R)).obj B))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier)
          f) :
      (a : (↑A : Type v)) → (↑B : Type v))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : AlgCat.{v, u} R
⊢ Functor.obj
      (forget₂ (AlgCat.{v, u} R) (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
        carrier) (ModuleCat.{v, u} R) (FD := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CD := ModuleCat.carrier))
      X =
    ModuleCat.of R (↑X : Type v)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : AlgCat.{v, u} R
f : X ⟶ Y
⊢ CategoryTheory.Functor.map
      (forget₂ (AlgCat.{v, u} R) (FC := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
        carrier) (ModuleCat.{v, u} R) (FD := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CD := ModuleCat.carrier))
      f =
    ModuleCat.ofHom (Hom.hom f).toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
x : Type u
x_1 : AlgCat R
f : Functor.obj (free R) x ⟶ x_1
⊢ (fun
          (f :
            x ⟶
              Functor.obj
                (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
                x_1) ↦
        (ofHom
            ((FreeAlgebra.lift R : (a : x → (↑x_1 : Type u)) → FreeAlgebra R x →ₐ[R] (↑x_1 : Type u))
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                (a : (fun (X : Type u) ↦ X) x) → (fun (X : Type u) ↦ X) ((forget (AlgCat R)).obj x_1))) :
          Quiver.Hom (V := AlgCat R) (of R (FreeAlgebra R x)) (of R (↑x_1 : Type u))))
      ((fun (f : Functor.obj (free R) x ⟶ x_1) ↦
          (↾(Equiv.symm (FreeAlgebra.lift R) :
                  (a : FreeAlgebra R x →ₐ[R] (forget (AlgCat R)).obj x_1) → x → (forget (AlgCat R)).obj x_1)
                (Hom.hom f) :
            x ⟶
              Functor.obj
                (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
                x_1))
        f) =
    f

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
x : Type u
x_1 : AlgCat R
f :
  x ⟶
    Functor.obj (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
      x_1
⊢ (fun (f : Functor.obj (free R) x ⟶ x_1) ↦
        (↾(Equiv.symm (FreeAlgebra.lift R) :
                (a : FreeAlgebra R x →ₐ[R] (forget (AlgCat R)).obj x_1) → x → (forget (AlgCat R)).obj x_1)
              (Hom.hom f) :
          x ⟶
            Functor.obj
              (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
              x_1))
      ((fun
            (f :
              x ⟶
                Functor.obj
                  (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC :=
                    carrier))
                  x_1) ↦
          (ofHom
              ((FreeAlgebra.lift R : (a : x → (↑x_1 : Type u)) → FreeAlgebra R x →ₐ[R] (↑x_1 : Type u))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                  (a : (fun (X : Type u) ↦ X) x) → (fun (X : Type u) ↦ X) ((forget (AlgCat R)).obj x_1))) :
            Quiver.Hom (V := AlgCat R) (of R (FreeAlgebra R x)) (of R (↑x_1 : Type u))))
        f) =
    f

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
⊢ Functor.IsRightAdjoint
    (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))

Tactic:
(adj R).isRightAdjoint

Premises used: CategoryTheory.Adjunction.isRightAdjoint, AlgCat.adj
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X₁ X₂ : Type u
X Y : AlgCat.{u_1, u} R
i : X ≅ Y
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{u_1, u} R) ↦ (↑x1 : Type u_1) →ₐ[R] (↑x2 : Type u_1)) (CC :=
          AlgCat.carrier) i.inv :
        (a : (↑Y : Type u_1)) → (↑X : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{u_1, u} R) ↦ (↑x1 : Type u_1) →ₐ[R] (↑x2 : Type u_1)) (CC :=
              AlgCat.carrier) i.hom :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X₁ X₂ : Type u
X Y : AlgCat.{u_1, u} R
i : X ≅ Y
x : (↑Y : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{u_1, u} R) ↦ (↑x1 : Type u_1) →ₐ[R] (↑x2 : Type u_1)) (CC :=
          AlgCat.carrier) i.hom :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{u_1, u} R) ↦ (↑x1 : Type u_1) →ₐ[R] (↑x2 : Type u_1)) (CC :=
              AlgCat.carrier) i.inv :
            (a : (↑Y : Type u_1)) → (↑X : Type u_1))
          x :
        (↑X : Type u_1)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X₁ X₂ : Type u
X Y : AlgCat R
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
    X ≅
  Functor.obj (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃ₐ[R] (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑(↑__src.toRingHom : (↑X : Type u) →* (↑Y : Type u)) : OneHom (↑X : Type u) (↑Y : Type u)).toFun,
    invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ IsIso f

Tactic:
e.toAlgebraIso.isIso_hom

Premises used: AlgEquiv.toAlgHom, CategoryTheory.Iso.isIso_hom, AlgEquiv.toAlgebraIso
-- Module: Mathlib.Algebra.Category.AlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X₁ X₂ : Type u
X Y : AlgCat R
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier)) f)
i : Functor.obj (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
    X ≅
  Functor.obj (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (AlgCat R) (FC := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier)) f)
e : (↑X : Type u) ≃ₐ[R] (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑(↑__src.toRingHom : (↑X : Type u) →* (↑Y : Type u)) : OneHom (↑X : Type u) (↑Y : Type u)).toFun,
    invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toAlgebraIso.isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, AlgEquiv.toAlgebraIso
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
⊢ Small.{w, max v w} ↥(sectionsSubalgebra F)

Tactic:
inferInstanceAs <| Small.{w} (F ⋙ forget _).sections

Premises used: _private.0.AlgCat.instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra._proof_1
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
j : J
this : Small.{w, max v w}
  (↑((F ⋙
            forget₂ (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
                carrier) RingCat (FD := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CD :=
                RingCat.carrier) ⋙
              forget₂ RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier)
                SemiRingCat (FD := fun (R S : SemiRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CD :=
                SemiRingCat.carrier)) ⋙
          forget SemiRingCat (FC := fun (R S : SemiRingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
            SemiRingCat.carrier)).sections :
    Type (max v w)) :=
  ⋯
x : R
⊢ Eq.{w + 1} (α :=
    ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier) (F.obj j))
    ((↑((algebraMap R
                  (↑(F ⋙
                          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                            (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                    Type (max w v)) :
                (a : R) → (↑(F ⋙ forget (AlgCat R)).sections : Type (max w v)))
              x) :
          (j : J) → ToType (F.obj j))
        j :
      ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier) (F.obj j))
    ((algebraMap R
            (ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)
              (F.obj j)) :
          (a : R) → ToType (F.obj j))
        x :
      ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier) (F.obj j))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
x x_1 : J
f : x ⟶ x_1
hf :
  ∀
    (x_2 :
      (↑(Functor.obj
            (Functor.obj (Functor.const J)
              (of R
                (Types.Small.limitCone
                    (F ⋙
                      forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                        (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier))).pt))
            x) :
        Type w)),
    Eq (α := (↑(F.obj x_1) : Type w))
      ((Hom.hom
              (CategoryTheory.Functor.map
                  (Functor.obj (Functor.const J)
                    (of R
                      (Types.Small.limitCone
                          (F ⋙
                            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                              (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier))).pt))
                  f ≫
                ofHom (limitπAlgHom F x_1)) :
            (a :
                (↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt)).obj x) : Type w)) →
              (↑(F.obj x_1) : Type w))
          x_2 :
        (↑(F.obj x_1) : Type w))
      ((Hom.hom (ofHom (limitπAlgHom F x) ≫ F.map f) :
            (a :
                (↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt)).obj x) : Type w)) →
              (↑(F.obj x_1) : Type w))
          x_2 :
        (↑(F.obj x_1) : Type w))
⊢ Eq.{w + 1} (α :=
    Functor.obj
        (Functor.obj (Functor.const J)
          (of R
            (Types.Small.limitCone
                (F ⋙
                  forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier))).pt))
        x ⟶
      F.obj x_1)
    (CategoryTheory.Functor.map
        (Functor.obj (Functor.const J)
          (of R
            (Types.Small.limitCone
                (F ⋙
                  forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier))).pt))
        f ≫
      ofHom (limitπAlgHom F x_1))
    (ofHom (limitπAlgHom F x) ≫ F.map f)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
x x_1 : J
f : x ⟶ x_1
x_2 :
  (↑(Functor.obj
        (Functor.obj (Functor.const J)
          (of R
            (Types.Small.limitCone
                (F ⋙
                  forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier))).pt))
        x) :
    Type w)
⊢ Eq (α := (↑(F.obj x_1) : Type w))
    ((Hom.hom
            (CategoryTheory.Functor.map
                (Functor.obj (Functor.const J)
                  (of R
                    (Types.Small.limitCone
                        (F ⋙
                          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                            (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier))).pt))
                f ≫
              ofHom (limitπAlgHom F x_1)) :
          (a : (↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt)).obj x) : Type w)) →
            (↑(F.obj x_1) : Type w))
        x_2 :
      (↑(F.obj x_1) : Type w))
    ((Hom.hom (ofHom (limitπAlgHom F x) ≫ F.map f) :
          (a : (↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt)).obj x) : Type w)) →
            (↑(F.obj x_1) : Type w))
        x_2 :
      (↑(F.obj x_1) : Type w))

Tactic:
simpa using (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality_apply, CategoryTheory.Limits.Types.Small.limitCone, CategoryTheory.Functor.comp, CategoryTheory.forget