awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : IsTopologicalRing.{u} (↑R : Type u)
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial (↑B : Type u) (↑A : Type u))
PC : CommRingCat := of (MvPolynomial (↑C : Type u) (↑A : Type u))
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB :
  Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC :
  Function.Surjective (α := (↑PC : Type u)) (β := (↑C : Type u)) (⇑(Hom.hom fC) : (a : (↑PC : Type u)) → (↑C : Type u))
this :
  IsEmbedding.{u, u} (X := (B ⟶ R) × (C ⟶ R)) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial ((↑B : Type u) ⊕ (↑C : Type u)) (↑A : Type u))
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim (⇑(Hom.hom (pushout.inl φ ψ)) : (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u))
        (⇑(Hom.hom (pushout.inr φ ψ)) : (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u))))
hfBC :
  Function.Surjective (α := (↑PBC : Type u)) (β := (↑(pushout φ ψ) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) fBC) :
      (a : (↑PBC : Type u)) → (↑(pushout φ ψ) : Type u))
F : (A ⟶ R) × ((↑B : Type u) ⊕ (↑C : Type u) → (↑R : Type u)) →
  ((A ⟶ R) × ((↑B : Type u) → (↑R : Type u))) × (A ⟶ R) × ((↑C : Type u) → (↑R : Type u)) :=
  fun (x : (A ⟶ R) × ((↑B : Type u) ⊕ (↑C : Type u) → (↑R : Type u))) ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
H :
  IsEmbedding (X := ((A ⟶ R) × ((↑B : Type u) → (↑R : Type u))) × (A ⟶ R) × ((↑C : Type u) → (↑R : Type u))) (Y :=
    (of (MvPolynomial (↑B : Type u) (↑A : Type u)) ⟶ R) × (of (MvPolynomial (↑C : Type u) (↑A : Type u)) ⟶ R))
    (Prod.map
      (⇑(Homeomorph.symm (mvPolynomialHomeomorph (↑B : Type u) R A)) :
        (a : (A ⟶ R) × ((↑B : Type u) → (↑R : Type u))) → of (MvPolynomial (↑B : Type u) (↑A : Type u)) ⟶ R)
      (⇑(Homeomorph.symm (mvPolynomialHomeomorph (↑C : Type u) R A)) :
        (a : (A ⟶ R) × ((↑C : Type u) → (↑R : Type u))) → of (MvPolynomial (↑C : Type u) (↑A : Type u)) ⟶ R))
⊢ ∀ (s : (↑A : Type u)),
    Eq (α := (↑(pushout φ ψ) : Type u))
      ((Hom.hom (pushout.inr φ ψ) : (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u))
          ((Hom.hom ψ : (a : (↑A : Type u)) → (↑C : Type u)) s : (↑C : Type u)) :
        (↑(pushout φ ψ) : Type u))
      ((Hom.hom (pushout.inl φ ψ) : (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u))
          ((Hom.hom φ : (a : (↑A : Type u)) → (↑B : Type u)) s : (↑B : Type u)) :
        (↑(pushout φ ψ) : Type u))

Tactic:
have (s : _) : (pushout.inr φ ψ).hom (ψ.hom s) = (pushout.inl φ ψ).hom (φ.hom s) :=
    congr($(pushout.condition (f := φ)).hom s).symm
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
A B : Under R
f : A ⟶ B
a : (↑R : Type u)
⊢ Eq (α := (↑B.right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (A.hom ≫ Under.Hom.right f) :
          (a : (↑R : Type u)) → (↑B.right : Type u))
        a :
      (↑B.right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) B.hom :
          (a : (↑R : Type u)) → (↑B.right : Type u))
        a :
      (↑B.right : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
A B : Under R
f : A ⟶ B
a : (↑R : Type u)
⊢ Eq (α := (↑B.right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (A.hom ≫ Under.Hom.right f) :
          (a : (↑R : Type u)) → (↑B.right : Type u))
        a :
      (↑B.right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) B.hom :
          (a : (↑R : Type u)) → (↑B.right : Type u))
        a :
      (↑B.right : Type u))

Tactic:
have : (A.hom ≫ f.right) a = B.hom a := by simp
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
A B : Under R
f : A ⟶ B
a : (↑R : Type u)
this :
  Eq (α := (↑B.right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (A.hom ≫ Under.Hom.right f) :
          (a : (↑R : Type u)) → (↑B.right : Type u))
        a :
      (↑B.right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) B.hom :
          (a : (↑R : Type u)) → (↑B.right : Type u))
        a :
      (↑B.right : Type u))
⊢ (↑(↑(Hom.hom (Under.Hom.right f)) : (↑A.right : Type u) →* (↑B.right : Type u)) :
          OneHom (↑A.right : Type u) (↑B.right : Type u)).toFun
      ((algebraMap (↑R : Type u) (↑A.right : Type u) : (a : (↑R : Type u)) → (↑A.right : Type u)) a) =
    (algebraMap (↑R : Type u) (↑B.right : Type u) : (a : (↑R : Type u)) → (↑B.right : Type u)) a

Tactic:
simpa only [Functor.const_obj_obj, Functor.id_obj, CommRingCat.comp_apply] using this

Premises used: CommRingCat.comp_apply, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R : CommRingCat
A : Under R
⊢ toAlgHom (𝟙 A) = AlgHom.id (↑R : Type u) (↑A.right : Type u)

Tactic:
rfl

Premises used: AlgHom.id, CommRingCat.toAlgHom, rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R : CommRingCat
A B C : Under R
f : A ⟶ B
g : B ⟶ C
⊢ toAlgHom (f ≫ g) = (toAlgHom g).comp (toAlgHom f)

Tactic:
rfl

Premises used: CommRingCat.toAlgHom, AlgHom.comp, rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R : CommRingCat
A B : Under R
f : A ⟶ B
a : (↑A.right : Type u)
⊢ Eq (α := (↑B.right : Type u)) ((toAlgHom f : (a : (↑A.right : Type u)) → (↑B.right : Type u)) a : (↑B.right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (Under.Hom.right f) :
          (a : (↑A.right : Type u)) → (↑B.right : Type u))
        a :
      (↑B.right : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R : CommRingCat
A : Type u
inst : CommRing A
inst_1 : Algebra (↑R : Type u) A
B : Under R
f g : R.mkUnder A ⟶ B
h :
  ∀ (a : A),
    Eq (α := (↑B.right : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (Under.Hom.right f) :
            (a : (↑(R.mkUnder A).right : Type u)) → (↑B.right : Type u))
          a :
        (↑B.right : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (Under.Hom.right g) :
            (a : (↑(R.mkUnder A).right : Type u)) → (↑B.right : Type u))
          a :
        (↑B.right : Type u))
h₁ :
  ∀ (x : (↑(R.mkUnder A).right : Type u)),
    Eq (α := (↑B.right : Type u))
      ((Hom.hom (Under.Hom.right f) : (a : (↑(R.mkUnder A).right : Type u)) → (↑B.right : Type u)) x :
        (↑B.right : Type u))
      ((Hom.hom (Under.Hom.right g) : (a : (↑(R.mkUnder A).right : Type u)) → (↑B.right : Type u)) x :
        (↑B.right : Type u))
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R : CommRingCat
A : Type u
inst : CommRing A
inst_1 : Algebra (↑R : Type u) A
B : Under R
f g : R.mkUnder A ⟶ B
h :
  ∀ (a : A),
    Eq (α := (↑B.right : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (Under.Hom.right f) :
            (a : (↑(R.mkUnder A).right : Type u)) → (↑B.right : Type u))
          a :
        (↑B.right : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (Under.Hom.right g) :
            (a : (↑(R.mkUnder A).right : Type u)) → (↑B.right : Type u))
          a :
        (↑B.right : Type u))
x : (↑(R.mkUnder A).right : Type u)
⊢ Eq (α := (↑B.right : Type u))
    ((Hom.hom (Under.Hom.right f) : (a : (↑(R.mkUnder A).right : Type u)) → (↑B.right : Type u)) x :
      (↑B.right : Type u))
    ((Hom.hom (Under.Hom.right g) : (a : (↑(R.mkUnder A).right : Type u)) → (↑B.right : Type u)) x :
      (↑B.right : Type u))

Tactic:
h x
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R : CommRingCat
A : Type u
inst : CommRing A
inst_1 : Algebra (↑R : Type u) A
B : Under R
f g : R.mkUnder A ⟶ B
h :
  ∀ (a : A),
    Eq (α := (↑B.right : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (Under.Hom.right f) :
            (a : (↑(R.mkUnder A).right : Type u)) → (↑B.right : Type u))
          a :
        (↑B.right : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (Under.Hom.right g) :
            (a : (↑(R.mkUnder A).right : Type u)) → (↑B.right : Type u))
          a :
        (↑B.right : Type u))
x : (↑(R.mkUnder A).right : Type u)
⊢ Eq (α := (↑B.right : Type u))
    ((Hom.hom (Under.Hom.right f) : (a : (↑(R.mkUnder A).right : Type u)) → (↑B.right : Type u)) x :
      (↑B.right : Type u))
    ((Hom.hom (Under.Hom.right g) : (a : (↑(R.mkUnder A).right : Type u)) → (↑B.right : Type u)) x :
      (↑B.right : Type u))

Tactic:
exact h x
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
A B : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra (↑R : Type u) A
inst_3 : Algebra (↑R : Type u) B
f : A →ₐ[(↑R : Type u)] B
hf :
  ∀ (a : (↑R : Type u)),
    Eq (α := (↑(R.mkUnder B).right : Type u))
      ((CommRingCat.Hom.hom ((R.mkUnder A).hom ≫ CommRingCat.ofHom f.toRingHom) :
            (a : (↑R : Type u)) → (↑(R.mkUnder B).right : Type u))
          a :
        (↑(R.mkUnder B).right : Type u))
      ((CommRingCat.Hom.hom (R.mkUnder B).hom : (a : (↑R : Type u)) → (↑(R.mkUnder B).right : Type u)) a :
        (↑(R.mkUnder B).right : Type u))
⊢ (R.mkUnder A).hom ≫ CommRingCat.ofHom f.toRingHom = (R.mkUnder B).hom

Tactic:
ext a
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
A B : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra (↑R : Type u) A
inst_3 : Algebra (↑R : Type u) B
f : A →ₐ[(↑R : Type u)] B
a : (↑R : Type u)
⊢ Eq (α := (↑(R.mkUnder B).right : Type u))
    ((CommRingCat.Hom.hom ((R.mkUnder A).hom ≫ CommRingCat.ofHom f.toRingHom) :
          (a : (↑R : Type u)) → (↑(R.mkUnder B).right : Type u))
        a :
      (↑(R.mkUnder B).right : Type u))
    ((CommRingCat.Hom.hom (R.mkUnder B).hom : (a : (↑R : Type u)) → (↑(R.mkUnder B).right : Type u)) a :
      (↑(R.mkUnder B).right : Type u))

Tactic:
f.commutes' a

Premises used: AlgHom.commutes'
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
A B : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra (↑R : Type u) A
inst_3 : Algebra (↑R : Type u) B
f : A →ₐ[(↑R : Type u)] B
a : (↑R : Type u)
⊢ Eq (α := (↑(R.mkUnder B).right : Type u))
    ((CommRingCat.Hom.hom ((R.mkUnder A).hom ≫ CommRingCat.ofHom f.toRingHom) :
          (a : (↑R : Type u)) → (↑(R.mkUnder B).right : Type u))
        a :
      (↑(R.mkUnder B).right : Type u))
    ((CommRingCat.Hom.hom (R.mkUnder B).hom : (a : (↑R : Type u)) → (↑(R.mkUnder B).right : Type u)) a :
      (↑(R.mkUnder B).right : Type u))

Tactic:
exact f.commutes' a

Premises used: AlgHom.commutes'
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R : CommRingCat
A B : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra (↑R : Type u) A
inst_3 : Algebra (↑R : Type u) B
f : A →ₐ[(↑R : Type u)] B
a : A
⊢ Eq (α := (↑(R.mkUnder B).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Under.Hom.right f.toUnder) :
          (a : (↑(R.mkUnder A).right : Type u)) → (↑(R.mkUnder B).right : Type u))
        a :
      (↑(R.mkUnder B).right : Type u))
    ((f : (a : A) → B) a : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R : CommRingCat
A B C : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra (↑R : Type u) A
inst_4 : Algebra (↑R : Type u) B
inst_5 : Algebra (↑R : Type u) C
f : A →ₐ[(↑R : Type u)] B
g : B →ₐ[(↑R : Type u)] C
⊢ (g.comp f).toUnder = f.toUnder ≫ g.toUnder

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.Under.homMk, AlgHom.toUnder, rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
A B : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra (↑R : Type u) A
inst_3 : Algebra (↑R : Type u) B
f : A ≃ₐ[(↑R : Type u)] B
h :
  ∀ (a : (↑(R.mkUnder A).right : Type u)),
    Eq (α := (↑(R.mkUnder A).right : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier)
              (Under.Hom.right ((↑f : A →ₐ[(↑R : Type u)] B).toUnder ≫ (↑f.symm : B →ₐ[(↑R : Type u)] A).toUnder)) :
            (a : (↑(R.mkUnder A).right : Type u)) → (↑(R.mkUnder A).right : Type u))
          a :
        (↑(R.mkUnder A).right : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Under.Hom.right (𝟙 (R.mkUnder A))) :
            (a : (↑(R.mkUnder A).right : Type u)) → (↑(R.mkUnder A).right : Type u))
          a :
        (↑(R.mkUnder A).right : Type u))
⊢ (↑f : A →ₐ[(↑R : Type u)] B).toUnder ≫ (↑f.symm : B →ₐ[(↑R : Type u)] A).toUnder = 𝟙 (R.mkUnder A)

Tactic:
ext (a : (CommRingCat.mkUnder R A).right)

Premises used: CommRingCat.mkUnder, CategoryTheory.Under.right
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
A B : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra (↑R : Type u) A
inst_3 : Algebra (↑R : Type u) B
f : A ≃ₐ[(↑R : Type u)] B
a : (↑(R.mkUnder A).right : Type u)
⊢ Eq (α := (↑(R.mkUnder A).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier)
            (Under.Hom.right ((↑f : A →ₐ[(↑R : Type u)] B).toUnder ≫ (↑f.symm : B →ₐ[(↑R : Type u)] A).toUnder)) :
          (a : (↑(R.mkUnder A).right : Type u)) → (↑(R.mkUnder A).right : Type u))
        a :
      (↑(R.mkUnder A).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Under.Hom.right (𝟙 (R.mkUnder A))) :
          (a : (↑(R.mkUnder A).right : Type u)) → (↑(R.mkUnder A).right : Type u))
        a :
      (↑(R.mkUnder A).right : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
A B : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra (↑R : Type u) A
inst_3 : Algebra (↑R : Type u) B
f : A ≃ₐ[(↑R : Type u)] B
h :
  ∀ (a : B),
    Eq (α := (↑(R.mkUnder B).right : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier)
              (Under.Hom.right ((↑f.symm : B →ₐ[(↑R : Type u)] A).toUnder ≫ (↑f : A →ₐ[(↑R : Type u)] B).toUnder)) :
            (a : (↑(R.mkUnder B).right : Type u)) → (↑(R.mkUnder B).right : Type u))
          a :
        (↑(R.mkUnder B).right : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Under.Hom.right (𝟙 (R.mkUnder B))) :
            (a : (↑(R.mkUnder B).right : Type u)) → (↑(R.mkUnder B).right : Type u))
          a :
        (↑(R.mkUnder B).right : Type u))
⊢ (↑f.symm : B →ₐ[(↑R : Type u)] A).toUnder ≫ (↑f : A →ₐ[(↑R : Type u)] B).toUnder = 𝟙 (R.mkUnder B)

Tactic:
ext a
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
A B : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra (↑R : Type u) A
inst_3 : Algebra (↑R : Type u) B
f : A ≃ₐ[(↑R : Type u)] B
a : B
⊢ Eq (α := (↑(R.mkUnder B).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier)
            (Under.Hom.right ((↑f.symm : B →ₐ[(↑R : Type u)] A).toUnder ≫ (↑f : A →ₐ[(↑R : Type u)] B).toUnder)) :
          (a : (↑(R.mkUnder B).right : Type u)) → (↑(R.mkUnder B).right : Type u))
        a :
      (↑(R.mkUnder B).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Under.Hom.right (𝟙 (R.mkUnder B))) :
          (a : (↑(R.mkUnder B).right : Type u)) → (↑(R.mkUnder B).right : Type u))
        a :
      (↑(R.mkUnder B).right : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R : CommRingCat
A B : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra (↑R : Type u) A
inst_3 : Algebra (↑R : Type u) B
f : A ≃ₐ[(↑R : Type u)] B
a : A
⊢ Eq (α := (↑(R.mkUnder B).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Under.Hom.right f.toUnder.hom) :
          (a : (↑(R.mkUnder A).right : Type u)) → (↑(R.mkUnder B).right : Type u))
        a :
      (↑(R.mkUnder B).right : Type u))
    ((f : (a : A) → B) a : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R : CommRingCat
A B : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra (↑R : Type u) A
inst_3 : Algebra (↑R : Type u) B
f : A ≃ₐ[(↑R : Type u)] B
b : B
⊢ Eq (α := (↑(R.mkUnder A).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Under.Hom.right f.toUnder.inv) :
          (a : (↑(R.mkUnder B).right : Type u)) → (↑(R.mkUnder A).right : Type u))
        b :
      (↑(R.mkUnder A).right : Type u))
    ((f.symm : (a : B) → A) b : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R : CommRingCat
A B C : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra (↑R : Type u) A
inst_4 : Algebra (↑R : Type u) B
inst_5 : Algebra (↑R : Type u) C
f : A ≃ₐ[(↑R : Type u)] B
g : B ≃ₐ[(↑R : Type u)] C
⊢ (f.trans g).toUnder = f.toUnder ≪≫ g.toUnder

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.Under.homMk, AlgEquiv.toUnder, CategoryTheory.Iso.trans, AlgHom.toUnder, rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
X Y Z : Under R
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{u + 1} (α :=
    S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑X.right : Type u)) ⟶
      S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑Z.right : Type u)))
    (AlgHom.toUnder (Algebra.TensorProduct.map (AlgHom.id (↑S : Type u) (↑S : Type u)) (toAlgHom (f ≫ g))))
    (CategoryStruct.comp (Y := S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑Y.right : Type u)))
      (AlgHom.toUnder (Algebra.TensorProduct.map (AlgHom.id (↑S : Type u) (↑S : Type u)) (toAlgHom f)))
      (AlgHom.toUnder (Algebra.TensorProduct.map (AlgHom.id (↑S : Type u) (↑S : Type u)) (toAlgHom g))))

Tactic:
simp [Algebra.TensorProduct.map_id_comp]

Premises used: Algebra.TensorProduct.map_id_comp
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A : Under R
simp :
  Eq (α := S ⟶ pushout (Z := of (↑S : Type u)) A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    (pushout.inr (ofHom (algebraMap (↑R : Type u) (↑A.right : Type u)))
      (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    (pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
⊢ Eq (α := S ⟶ Under.right (X := S) (Functor.obj (Under.pushout (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) A))
    ((S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑A.right : Type u))).hom ≫ Iso.hom (IsPushout.isoPushout ⋯))
    (Under.hom (Functor.obj (Under.pushout (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) A))

Tactic:
simp only [Under.pushout_obj, Under.mk_right,
      mkUnder_hom, AlgHom.toRingHom_eq_coe, IsPushout.inr_isoPushout_hom, Under.mk_hom]

Premises used: CategoryTheory.Under.mk_hom, CommRingCat.mkUnder_hom, CategoryTheory.Under.mk_right, AlgHom.toRingHom_eq_coe, CategoryTheory.Under.pushout_obj, CategoryTheory.IsPushout.inr_isoPushout_hom
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A : Under R
⊢ Eq (α := S ⟶ pushout (Z := of (↑S : Type u)) A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    (pushout.inr (ofHom (algebraMap (↑R : Type u) (↑A.right : Type u)))
      (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    (pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A : Under R
⊢ Eq (α := A.right ⟶ (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑A.right : Type u))).right)
    (pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S A)))
    (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight))

Tactic:
simp [tensorProdObjIsoPushoutObj]

Premises used: CommRingCat.tensorProdObjIsoPushoutObj
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A : Under R
⊢ Eq (α := of (↑S : Type u) ⟶ (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑A.right : Type u))).right)
    (pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S A)))
    (ofHom Algebra.TensorProduct.includeLeftRingHom)

Tactic:
simp [tensorProdObjIsoPushoutObj]

Premises used: CommRingCat.tensorProdObjIsoPushoutObj
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
dsimp :
  (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B) =
    Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
      Under.homMk
        (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
          (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
        ⋯
⊢ Eq (α := (R.tensorProd S).obj A ⟶ Functor.obj (Under.pushout (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) B)
    ((R.tensorProd S).map f ≫
      Iso.hom
        ((fun (A : Under R) ↦
            (tensorProdObjIsoPushoutObj S A :
              S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑A.right : Type u)) ≅
                Functor.obj (Under.pushout (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) A))
          B))
    (Iso.hom
        ((fun (A : Under R) ↦
            (tensorProdObjIsoPushoutObj S A :
              S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑A.right : Type u)) ≅
                Functor.obj (Under.pushout (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) A))
          A) ≫
      CategoryTheory.Functor.map (Under.pushout (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) f)

Tactic:
dsimp