Theorem: DividedPowerAlgebra.roby4.Algebra.mem_bot_of_subalgebra_iff (DividedPowers/DPAlgebra/Dpow.lean)

State before:
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ s ∈ ⊥ ↔ s ∈ S₀
Tactic:
simp only [Algebra.mem_bot, Set.mem_range, Subtype.exists]
State after:
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ (∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s) ↔ s ∈ S₀

State before:
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ (∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s) ↔ s ∈ S₀
Tactic:
constructor
State after:
case mp
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ (∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s) → s ∈ S₀

case mpr
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ s ∈ S₀ → ∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s

State before:
case mp
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ (∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s) → s ∈ S₀
Tactic:
rintro ⟨s, hs, rfl⟩
State after:
case mp.intro.intro
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
hs : s ∈ S₀
⊢ (algebraMap (↥S₀) S) ⟨s, hs⟩ ∈ S₀

State before:
case mp.intro.intro
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
hs : s ∈ S₀
⊢ (algebraMap (↥S₀) S) ⟨s, hs⟩ ∈ S₀
Tactic:
exact hs
State after:
no goals

State before:
case mpr
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ s ∈ S₀ → ∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s
Tactic:
intro hs
State after:
case mpr
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
hs : s ∈ S₀
⊢ ∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s

State before:
case mpr
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
hs : s ∈ S₀
⊢ ∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s
Tactic:
exact ⟨s, hs, rfl⟩
State after:
no goals