Theorem: DividedPowerAlgebra.condQ_and_condTFree_imply_condT (DividedPowers/DPAlgebra/Dpow.lean)

State before:
R : Type u
inst✝¹ : CommRing R
A : Type u_1
inst✝ : CommRing A
hQ : CondQ A
hT_free : CondTFree A
⊢ CondT A
Tactic:
intro R' _ _ I' hI' S' _ _ J' hJ'
State after:
R : Type u
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
hQ : CondQ A
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'
⊢ Condτ A hI' hJ'

State before:
R : Type u
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
hQ : CondQ A
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'
⊢ Condτ A hI' hJ'
Tactic:
simp only [CondQ] at hQ
State after:
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'
⊢ Condτ A hI' hJ'

State before:
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'
⊢ Condτ A hI' hJ'
Tactic:
obtain ⟨R, _, _, hR_free, f, I, hI, hfDP, hfI, hf⟩ := hQ R' I' hI'
State after:
case 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
⊢ Condτ A hI' hJ'

State before:
case 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
⊢ Condτ A hI' hJ'
Tactic:
obtain ⟨S, _, _, hS_free, g, J, hJ, hgDP, hgJ, hg⟩ := hQ S' J' hJ'
State after:
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'

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
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

State before:
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)
Tactic:
rw [Algebra.TensorProduct.map_ker _ _ hf hg]
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
⊢ (Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f) ⊔
        Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)) ⊓
      K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)

State before:
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
⊢ (Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f) ⊔
        Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)) ⊓
      K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)
Tactic:
sorry
State after:
no goals

State before:
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
Tactic:
apply hT_free
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hRS.x
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
⊢ Module.Free A R

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hRS.x
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
⊢ Module.Free A S

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hRS.x
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
⊢ Module.Free A R

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hRS.x
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
⊢ Module.Free A S
Tactic:
exact hR_free
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hRS.x
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
⊢ Module.Free A S

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hRS.x
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
⊢ Module.Free A S
Tactic:
exact hS_free
State after:
no goals