-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem fg_induction (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]
    (P : Submodule R M → Prop) (h₁ : ∀ x, P (Submodule.span R {x}))
    (h₂ : ∀ M₁ M₂, P M₁ → P M₂ → P (M₁ ⊔ M₂)) (N : Submodule R M) (hN : N.FG) : P N

Proof state:
R : Type u_4
M : Type u_5
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 : N.FG
⊢ P N

Tactic:
obtain ⟨s, rfl⟩ := hN

Result:
case intro
R : Type u_4
M : Type u_5
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)

Proof state:
case intro.insert
R : Type u_4
M : Type u_5
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✝
ih : P (span R ↑s✝)
⊢ P (span R ↑(insert a✝¹ s✝))

Tactic:
rw [Finset.coe_insert, Submodule.span_insert]

Result:
case intro.insert
R : Type u_4
M : Type u_5
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✝
ih : P (span R ↑s✝)
⊢ P (span R {a✝¹} ⊔ span R ↑s✝)

Proof state:
R : Type u_4
M : Type u_5
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 : N.FG
⊢ P N

Tactic:
classical
  obtain ⟨s, rfl⟩ := hN
  induction s using Finset.induction with
  | empty =>
    rw [Finset.coe_empty, Submodule.span_empty, ← Submodule.span_zero_singleton]
    exact h₁ _
  | insert _ ih =>
    rw [Finset.coe_insert, Submodule.span_insert]
    exact h₂ _ _ (h₁ _) ih

Result:
no goals

Proof state:
case intro.insert
R : Type u_4
M : Type u_5
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✝
ih : P (span R ↑s✝)
⊢ P (span R {a✝¹} ⊔ span R ↑s✝)

Tactic:
exact h₂ _ _ (h₁ _) ih

Result:
no goals

Proof state:
case intro
R : Type u_4
M : Type u_5
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)

Tactic:
induction s using Finset.induction with
| empty =>
  rw [Finset.coe_empty, Submodule.span_empty, ← Submodule.span_zero_singleton]
  exact h₁ _
| insert _ ih =>
  rw [Finset.coe_insert, Submodule.span_insert]
  exact h₂ _ _ (h₁ _) ih

Result:
no goals

Proof state:
case intro.empty
R : Type u_4
M : Type u_5
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})

Tactic:
exact h₁ _

Result:
no goals

Proof state:
case intro.empty
R : Type u_4
M : Type u_5
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 ↑∅)

Tactic:
rw [Finset.coe_empty, Submodule.span_empty, ← Submodule.span_zero_singleton]

Result:
case intro.empty
R : Type u_4
M : Type u_5
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})