-- Mathlib/Algebra/Category/Ring/LinearAlgebra.lean
lemma nontrivial_of_isPushout_of_isField {A B C D : CommRingCat.{u}}
    (hA : IsField A) {f : A ⟶ B} {g : A ⟶ C} {inl : B ⟶ D} {inr : C ⟶ D}
    [Nontrivial B] [Nontrivial C]
    (h : IsPushout f g inl inr) : Nontrivial D

Proof state:
A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
algInst✝¹ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑A ↑C := (Hom.hom g).toAlgebra
e : D ≅ of (↑B ⊗[↑A] ↑C) := h.isColimit.coconePointUniqueUpToIso (pushoutCoconeIsColimit ↑A ↑B ↑C)
e' : ↑D ≃ ↑B ⊗[↑A] ↑C := e.commRingCatIsoToRingEquiv.toEquiv
⊢ Nontrivial ↑D

Tactic:
exact e'.nontrivial

Result:
no goals

Proof state:
A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
⊢ Nontrivial ↑D

Tactic:
letI : Field A := hA.toField

Result:
A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
⊢ Nontrivial ↑D

Proof state:
A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
⊢ Nontrivial ↑D

Tactic:
algebraize [f.hom, g.hom]

Result:
A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
algInst✝¹ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑A ↑C := (Hom.hom g).toAlgebra
⊢ Nontrivial ↑D

Proof state:
A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
algInst✝¹ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑A ↑C := (Hom.hom g).toAlgebra
⊢ Nontrivial ↑D

Tactic:
let e : D ≅ .of (B ⊗[A] C) :=
  IsColimit.coconePointUniqueUpToIso h.isColimit (CommRingCat.pushoutCoconeIsColimit A B C)

Result:
A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
algInst✝¹ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑A ↑C := (Hom.hom g).toAlgebra
e : D ≅ of (↑B ⊗[↑A] ↑C) := h.isColimit.coconePointUniqueUpToIso (pushoutCoconeIsColimit ↑A ↑B ↑C)
⊢ Nontrivial ↑D

Proof state:
A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
algInst✝¹ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑A ↑C := (Hom.hom g).toAlgebra
e : D ≅ of (↑B ⊗[↑A] ↑C) := h.isColimit.coconePointUniqueUpToIso (pushoutCoconeIsColimit ↑A ↑B ↑C)
⊢ Nontrivial ↑D

Tactic:
let e' : D ≃ B ⊗[A] C := e.commRingCatIsoToRingEquiv.toEquiv

Result:
A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
algInst✝¹ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑A ↑C := (Hom.hom g).toAlgebra
e : D ≅ of (↑B ⊗[↑A] ↑C) := h.isColimit.coconePointUniqueUpToIso (pushoutCoconeIsColimit ↑A ↑B ↑C)
e' : ↑D ≃ ↑B ⊗[↑A] ↑C := e.commRingCatIsoToRingEquiv.toEquiv
⊢ Nontrivial ↑D