Theorem: DividedPowerAlgebra.roby4.f_mem_I (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)
p : ↥I →₀ A
⊢ (f A I) p ∈ I
Tactic:
suffices LinearMap.range (f A I) ≤ Submodule.restrictScalars A I by
  apply this
  simp only [LinearMap.mem_range, exists_apply_eq_apply]
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)
p : ↥I →₀ A
⊢ LinearMap.range (f A I) ≤ Submodule.restrictScalars A I

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)
p : ↥I →₀ A
⊢ LinearMap.range (f A I) ≤ Submodule.restrictScalars A I
Tactic:
simp only [f, Basis.constr_range, Submodule.span_le]
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)
p : ↥I →₀ A
⊢ (Set.range fun i => ↑i) ⊆ ↑(Submodule.restrictScalars A I)

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)
p : ↥I →₀ A
⊢ (Set.range fun i => ↑i) ⊆ ↑(Submodule.restrictScalars A I)
Tactic:
rintro _ ⟨i, rfl⟩
State after:
case 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)
p : ↥I →₀ A
i : ↥I
⊢ (fun i => ↑i) i ∈ ↑(Submodule.restrictScalars A I)

State before:
case 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)
p : ↥I →₀ A
i : ↥I
⊢ (fun i => ↑i) i ∈ ↑(Submodule.restrictScalars A I)
Tactic:
simp only [Submodule.coe_restrictScalars, SetLike.mem_coe, SetLike.coe_mem]
State after:
no goals

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)
p : ↥I →₀ A
this : LinearMap.range (f A I) ≤ Submodule.restrictScalars A I
⊢ (f A I) p ∈ I
Tactic:
apply this
State after:
case a
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)
p : ↥I →₀ A
this : LinearMap.range (f A I) ≤ Submodule.restrictScalars A I
⊢ (f A I) p ∈ LinearMap.range (f A I)

State before:
case a
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)
p : ↥I →₀ A
this : LinearMap.range (f A I) ≤ Submodule.restrictScalars A I
⊢ (f A I) p ∈ LinearMap.range (f A I)
Tactic:
simp only [LinearMap.mem_range, exists_apply_eq_apply]
State after:
no goals