Theorem: DividedPowerAlgebra.condQ_and_condTFree_imply_condT
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R✝ : Type u
inst✝⁵ : CommRing R✝
A : Type u_1
inst✝⁴ : CommRing A
hQ :
  ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra A R] (I : Ideal R) (hI : DividedPowers I),
    ∃ T x x_1,
      ∃ (_ : Module.Free A T), ∃ f J hJ, ∃ (_ : hJ.isDPMorphism hI ↑f), I = Ideal.map f J ∧ Function.Surjective ⇑f
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
R : Type u_1
w✝³ : CommRing R
w✝² : Algebra A R
hR_free : Module.Free A R
f : R →ₐ[A] R'
I : Ideal R
hI : DividedPowers I
hfDP : hI.isDPMorphism hI' ↑f
hfI : I' = Ideal.map f I
hf : Function.Surjective ⇑f
S : Type u_1
w✝¹ : CommRing S
w✝ : Algebra A S
hS_free : Module.Free A S
g : S →ₐ[A] S'
J : Ideal S
hJ : DividedPowers J
hgDP : hJ.isDPMorphism hJ' ↑g
hgJ : J' = Ideal.map g J
hg : Function.Surjective ⇑g
⊢ Condτ A hI' hJ'
Tactic:
apply condτ_rel A f hf hI hI' hfDP hfI g  hg hJ hJ' hgDP hgJ
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.roby
R✝ : Type u
inst✝⁵ : CommRing R✝
A : Type u_1
inst✝⁴ : CommRing A
hQ :
  ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra A R] (I : Ideal R) (hI : DividedPowers I),
    ∃ T x x_1,
      ∃ (_ : Module.Free A T), ∃ f J hJ, ∃ (_ : hJ.isDPMorphism hI ↑f), I = Ideal.map f J ∧ Function.Surjective ⇑f
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
R : Type u_1
w✝³ : CommRing R
w✝² : Algebra A R
hR_free : Module.Free A R
f : R →ₐ[A] R'
I : Ideal R
hI : DividedPowers I
hfDP : hI.isDPMorphism hI' ↑f
hfI : I' = Ideal.map f I
hf : Function.Surjective ⇑f
S : Type u_1
w✝¹ : CommRing S
w✝ : Algebra A S
hS_free : Module.Free A S
g : S →ₐ[A] S'
J : Ideal S
hJ : DividedPowers J
hgDP : hJ.isDPMorphism hJ' ↑g
hgJ : J' = Ideal.map g J
hg : Function.Surjective ⇑g
⊢ RingHom.ker (Algebra.TensorProduct.map f g) ⊓ K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hRS
R✝ : Type u
inst✝⁵ : CommRing R✝
A : Type u_1
inst✝⁴ : CommRing A
hQ :
  ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra A R] (I : Ideal R) (hI : DividedPowers I),
    ∃ T x x_1,
      ∃ (_ : Module.Free A T), ∃ f J hJ, ∃ (_ : hJ.isDPMorphism hI ↑f), I = Ideal.map f J ∧ Function.Surjective ⇑f
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
R : Type u_1
w✝³ : CommRing R
w✝² : Algebra A R
hR_free : Module.Free A R
f : R →ₐ[A] R'
I : Ideal R
hI : DividedPowers I
hfDP : hI.isDPMorphism hI' ↑f
hfI : I' = Ideal.map f I
hf : Function.Surjective ⇑f
S : Type u_1
w✝¹ : CommRing S
w✝ : Algebra A S
hS_free : Module.Free A S
g : S →ₐ[A] S'
J : Ideal S
hJ : DividedPowers J
hgDP : hJ.isDPMorphism hJ' ↑g
hgJ : J' = Ideal.map g J
hg : Function.Surjective ⇑g
⊢ Condτ A hI hJ