case intro
R✝ : Type ?u.243597
M✝ : Type ?u.243600
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
P✝ : Type ?u.243636
inst✝⁴ : AddCommMonoid P✝
inst✝³ : Module R✝ P✝
f : M✝ →ₗ[R✝] P✝
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M → Prop
h₁ : ∀ (x : M), P (span R {x})
h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂)
s : Finset M
⊢ P (span R ↑s)
R✝ : Type ?u.243597
M✝ : Type ?u.243600
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
P✝ : Type ?u.243636
inst✝⁴ : AddCommMonoid P✝
inst✝³ : Module R✝ P✝
f : M✝ →ₗ[R✝] P✝
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M → Prop
h₁ : ∀ (x : M), P (span R {x})
h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂)
N : Submodule R M
hN : FG N
⊢ P N
obtain ⟨s, rfl⟩ := hN
case intro.empty
R✝ : Type ?u.243597
M✝ : Type ?u.243600
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
P✝ : Type ?u.243636
inst✝⁴ : AddCommMonoid P✝
inst✝³ : Module R✝ P✝
f : M✝ →ₗ[R✝] P✝
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M → Prop
h₁ : ∀ (x : M), P (span R {x})
h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂)
⊢ P (span R ↑∅)

case intro.insert
R✝ : Type ?u.243597
M✝ : Type ?u.243600
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
P✝ : Type ?u.243636
inst✝⁴ : AddCommMonoid P✝
inst✝³ : Module R✝ P✝
f : M✝ →ₗ[R✝] P✝
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M → Prop
h₁ : ∀ (x : M), P (span R {x})
h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂)
a✝² : M
s✝ : Finset M
a✝¹ : ¬a✝² ∈ s✝
a✝ : P (span R ↑s✝)
⊢ P (span R ↑(insert a✝² s✝))
case intro
R✝ : Type ?u.243597
M✝ : Type ?u.243600
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
P✝ : Type ?u.243636
inst✝⁴ : AddCommMonoid P✝
inst✝³ : Module R✝ P✝
f : M✝ →ₗ[R✝] P✝
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M → Prop
h₁ : ∀ (x : M), P (span R {x})
h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂)
s : Finset M
⊢ P (span R ↑s)
induction s using Finset.induction
case intro.empty
R✝ : Type ?u.243597
M✝ : Type ?u.243600
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
P✝ : Type ?u.243636
inst✝⁴ : AddCommMonoid P✝
inst✝³ : Module R✝ P✝
f : M✝ →ₗ[R✝] P✝
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M → Prop
h₁ : ∀ (x : M), P (span R {x})
h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂)
⊢ P (span R {0})
case intro.empty
R✝ : Type ?u.243597
M✝ : Type ?u.243600
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
P✝ : Type ?u.243636
inst✝⁴ : AddCommMonoid P✝
inst✝³ : Module R✝ P✝
f : M✝ →ₗ[R✝] P✝
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M → Prop
h₁ : ∀ (x : M), P (span R {x})
h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂)
⊢ P (span R ↑∅)
rw [Finset.coe_empty, Submodule.span_empty, ← Submodule.span_zero_singleton]
no goals
case intro.empty
R✝ : Type ?u.243597
M✝ : Type ?u.243600
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
P✝ : Type ?u.243636
inst✝⁴ : AddCommMonoid P✝
inst✝³ : Module R✝ P✝
f : M✝ →ₗ[R✝] P✝
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M → Prop
h₁ : ∀ (x : M), P (span R {x})
h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂)
⊢ P (span R {0})
apply h₁
case intro.insert
R✝ : Type ?u.243597
M✝ : Type ?u.243600
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
P✝ : Type ?u.243636
inst✝⁴ : AddCommMonoid P✝
inst✝³ : Module R✝ P✝
f : M✝ →ₗ[R✝] P✝
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M → Prop
h₁ : ∀ (x : M), P (span R {x})
h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂)
a✝² : M
s✝ : Finset M
a✝¹ : ¬a✝² ∈ s✝
a✝ : P (span R ↑s✝)
⊢ P (span R {a✝²} ⊔ span R ↑s✝)
case intro.insert
R✝ : Type ?u.243597
M✝ : Type ?u.243600
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
P✝ : Type ?u.243636
inst✝⁴ : AddCommMonoid P✝
inst✝³ : Module R✝ P✝
f : M✝ →ₗ[R✝] P✝
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M → Prop
h₁ : ∀ (x : M), P (span R {x})
h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂)
a✝² : M
s✝ : Finset M
a✝¹ : ¬a✝² ∈ s✝
a✝ : P (span R ↑s✝)
⊢ P (span R ↑(insert a✝² s✝))
rw [Finset.coe_insert, Submodule.span_insert]
no goals
case intro.insert
R✝ : Type ?u.243597
M✝ : Type ?u.243600
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
P✝ : Type ?u.243636
inst✝⁴ : AddCommMonoid P✝
inst✝³ : Module R✝ P✝
f : M✝ →ₗ[R✝] P✝
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M → Prop
h₁ : ∀ (x : M), P (span R {x})
h₂ : ∀ (M₁ M₂ : Submodule R M), P M₁ → P M₂ → P (M₁ ⊔ M₂)
a✝² : M
s✝ : Finset M
a✝¹ : ¬a✝² ∈ s✝
a✝ : P (span R ↑s✝)
⊢ P (span R {a✝²} ⊔ span R ↑s✝)
apply h₂ <;> apply_assumption