awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (hypothesis)
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)
⊢ IsEmbedding (Y := (B ⟶ R) × (C ⟶ R)) fun (f : pushout φ ψ ⟶ R) ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)
have hfB : Function.Surjective (α := (↑PB : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom fB) : (a : (↑PB : Type u)) → (↑B : Type u))
Tactic: have hfB : Function.Surjective fB.hom := fun x ↦ ⟨.X x, by simp [PB, fB]⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (hypothesis)
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)
⊢ IsEmbedding (Y := (B ⟶ R) × (C ⟶ R)) fun (f : pushout φ ψ ⟶ R) ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)
have hfC : Function.Surjective (α := (↑PC : Type u)) (β := (↑C : Type u)) (⇑(Hom.hom fC) : (a : (↑PC : Type u)) → (↑C : Type u))
Tactic: have hfC : Function.Surjective fC.hom := fun x ↦ ⟨.X x, by simp [PC, fC]⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (hypothesis)
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))
⊢ IsEmbedding (Y := (B ⟶ R) × (C ⟶ R)) fun (f : pushout φ ψ ⟶ R) ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)
have 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)
Tactic: have := (isEmbedding_precomp_of_surjective (R := R) fB hfB).prodMap
    (isEmbedding_precomp_of_surjective (R := R) fC hfC)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
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)
⊢ IsEmbedding (Y := (B ⟶ R) × (C ⟶ R)) fun (f : pushout φ ψ ⟶ R) ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)
have rw : IsEmbedding.{u, u} (X := pushout φ ψ ⟶ R) (Y := (PB ⟶ R) × (PC ⟶ R))
  (Function.comp (β := (B ⟶ R) × (C ⟶ R)) (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
    fun (f : pushout φ ψ ⟶ R) ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f))
Tactic: rw [← IsEmbedding.of_comp_iff this]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
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))))
⊢ 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))
have rw : Set.range (ι := (↑B : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (Y := pushout φ ψ) (pushout.inl φ ψ)) :
        (a : (↑B : Type u)) → (↑(pushout φ ψ) : Type u)) ∪
    Set.range (ι := (↑C : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (Y := pushout φ ψ) (pushout.inr φ ψ)) :
        (a : (↑C : Type u)) → (↑(pushout φ ψ) : Type u)) ⊆
  (↑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
          fBC).range :
    Set (↑(pushout φ ψ) : Type u))
Tactic: rw [← RingHom.range_eq_top, ← top_le_iff,
      ← closure_range_union_range_eq_top_of_isPushout (.of_hasPushout _ _), Subring.closure_le]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (hypothesis)
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))))
⊢ IsEmbedding.{u, u} (X := pushout φ ψ ⟶ R) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Function.comp (β := (B ⟶ R) × (C ⟶ R)) (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
      fun (f : pushout φ ψ ⟶ R) ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f))
have 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))
Tactic: have hfBC : Function.Surjective fBC := by
    rw [← RingHom.range_eq_top, ← top_le_iff,
      ← closure_range_union_range_eq_top_of_isPushout (.of_hasPushout _ _), Subring.closure_le]
    simp only [Set.union_subset_iff, RingHom.coe_range, Set.range_subset_iff, Set.mem_range]
    exact ⟨fun x ↦ ⟨.X (.inl x), by simp [fBC, PBC]⟩, fun x ↦ ⟨.X (.inr x), by simp [fBC, PBC]⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (hypothesis)
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)
⊢ IsEmbedding.{u, u} (X := pushout φ ψ ⟶ R) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Function.comp (β := (B ⟶ R) × (C ⟶ R)) (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
      fun (f : pushout φ ψ ⟶ R) ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f))
have hF : IsEmbedding F
Tactic: have hF : IsEmbedding F := (Homeomorph.prodProdProdComm _ _ _ _).isEmbedding.comp
    ((isEmbedding_graph continuous_id).prodMap Homeomorph.sumArrowHomeomorphProdArrow.isEmbedding)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (hypothesis)
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
⊢ IsEmbedding.{u, u} (X := pushout φ ψ ⟶ R) (Y := (PB ⟶ R) × (PC ⟶ R))
    (Function.comp (β := (B ⟶ R) × (C ⟶ R)) (Prod.map (fun (x : B ⟶ R) ↦ fB ≫ x) fun (x : C ⟶ R) ↦ fC ≫ x)
      fun (f : pushout φ ψ ⟶ R) ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f))
have 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))
Tactic: have H := (mvPolynomialHomeomorph B R A).symm.isEmbedding.prodMap
    (mvPolynomialHomeomorph C R A).symm.isEmbedding
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (hypothesis)
Goal:
R S : CommRingCat
A B : Under R
f : A ⟶ B
a : (↑R : 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
have 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))
Tactic: have : (A.hom ≫ f.right) a = B.hom a := by simp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
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))
⊢ f = g
have 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))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
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
⊢ (R.mkUnder A).hom ≫ CommRingCat.ofHom f.toRingHom = (R.mkUnder B).hom
have 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))
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
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
⊢ (↑f : A →ₐ[(↑R : Type u)] B).toUnder ≫ (↑f.symm : B →ₐ[(↑R : Type u)] A).toUnder = 𝟙 (R.mkUnder A)
have 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))
Tactic: ext (a : (CommRingCat.mkUnder R A).right)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
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
⊢ (↑f.symm : B →ₐ[(↑R : Type u)] A).toUnder ≫ (↑f : A →ₐ[(↑R : Type u)] B).toUnder = 𝟙 (R.mkUnder B)
have 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))
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A : Under R
⊢ 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))
have 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))))
Tactic: simp only [Under.pushout_obj, Under.mk_right,
      mkUnder_hom, AlgHom.toRingHom_eq_coe, IsPushout.inr_isoPushout_hom, Under.mk_hom]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
⊢ 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)
have 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)))) sorry)
      sorry
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
⊢ (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)))) ⋯)
        ⋯
have rw : Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B) =
  Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
    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)))) sorry)
        sorry
Tactic: rw [← cancel_epi (tensorProdObjIsoPushoutObj S A).inv]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
⊢ Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B) =
    Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
      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)))) ⋯)
          ⋯
have h : Under.Hom.right
    (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
  Under.Hom.right
    (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
      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)))) sorry)
          sorry)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
⊢ Under.Hom.right
      (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
    Under.Hom.right
      (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
        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)))) ⋯)
            ⋯)
have h : pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
    Under.Hom.right
      (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
  pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
    Under.Hom.right
      (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
        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)))) sorry)
            sorry)
Tactic: apply pushout.hom_ext