Commit 2024-10-15 22:29 f44f4685

refactor: migrate to dependent induction lemmas (#17543) Many of the existing induction lemmas for subobjects (e.g., Subsemigroup.closure_induction) were written with a motive that does not depend on the induction argument (e.g., x ∈ Subsemigroup.closure s), like so:

theorem Subsemigroup.closure_induction {M : Type u_1} [Mul M] {s : Set M}
    {p : M → Prop} {x : M} (h : x ∈ Subsemigroup.closure s)
    (mem : ∀ x ∈ s, p x) (mul : ∀ (x y : M), p x → p y → p (x * y)) :
    p x

This prevents Lean from correctly inferring the motive when applying the induction tactic. As such, these lemmas don't serve much purpose, and we gradually acquired their dependent counterparts as variations with a ', like this one:

theorem Subsemigroup.closure_induction' {M : Type u_1} [Mul M] (s : Set M)
    {p : (x : M) → x ∈ Subsemigroup.closure s → Prop}
    (mem : ∀ (x : M) (h : x ∈ s), p x ⋯)
    (mul : ∀ (x : M) (hx : x ∈ Subsemigroup.closure s) (y : M)
    (hy : y ∈ Subsemigroup.closure s), p x hx → p y hy → p (x * y) (mul_mem hx hy))
    {x : M} (hx : x ∈ Subsemigroup.closure s) :
    p x hx

This PR moves the primed versions to the un-primed names, and removes the non-dependent lemmas, while also ensuring the dependent versions exist and are uniform for all these various subobjects. Moves:

• Subsemigroup.closure_induction' -> Subsemigroup.closure_induction
• AddSubsemigroup.closure_induction' -> AddSubsemigroup.closure_induction
• Submonoid.closure_induction' -> Submonoid.closure_induction
• AddSubmonoid.closure_induction' -> AddSubmonoid.closure_induction
• Subgroup.closure_induction' -> Subgroup.closure_induction
• AddSubgroup.closure_induction' -> AddSubgroup.closure_induction
• Submodule.span_induction' -> Submodule.span_induction
• Submodule.closure_induction' -> Submodule.closure_induction
• NonUnitalAlgebra.adjoin_induction' -> NonUnitalAlgebra.adjoin_induction
• NonUnitalStarAlgebra.adjoin_induction' -> NonUnitalStarAlgebra.adjoin_induction
• Subsemiring.closure_induction' -> Subsemiring.closure_induction
• Subring.closure_induction' -> Subring.closure_induction
• Algebra.adjoin_induction'' -> Algebra.adjoin_induction