Induction hypothesis in subgroup closure induction

Stream: new members

[Stepan Nesterov]

Here's an example of a proof using subgroup closure induction

import Mathlib.Algebra.Group.Subgroup.Lattice
import Mathlib.Algebra.Group.Subgroup.Map

variable (G : Type*) [Group G]

theorem exercise3_1_23 (ι : Type*) (H : ι → Subgroup G) : (∀ i : ι, (H i).Normal) → (⨆ (i : ι), H i).Normal := by
  intro hyp
  rw[Subgroup.iSup_eq_closure] at *
  constructor
  intro n hn g
  induction hn using Subgroup.closure_induction with
  | mem x hx =>
    rw[Set.mem_iUnion] at hx
    obtain ⟨i, hx⟩ := hx
    apply Subgroup.subset_closure
    rw[Set.mem_iUnion]
    use i
    specialize hyp i
    obtain ⟨hyp⟩ := hyp
    exact hyp x hx g
  | one => simp
  | mul x y _ _ hx hy =>
    rw[← conj_mul]
    exact mul_mem hx hy
  | inv x _ hx =>
    rw[← conj_inv]
    exact inv_mem hx

From the docstring I would expect the induction step to be just $P(x) \to P(y) \to P(xy)$, not $x \in \mathrm{closure} \to P(x) \to y \in \mathrm{closure} \to P(y) \to P(xy)$. I suppose there might be some exotic cases where you need to remember the assumption that $x$ and $y$ are in the closure, but usually that's not the case. Is there a way to apply induction in such a way that it gets rid of the assumptions $x \in \mathrm{closure}$, $y \in \mathrm{closure}$?

[Aaron Liu]

It's so that the motive can depend on the fact that xy is in the closure

[Aaron Liu]

I don't think there's a way to get rid of those hypotheses with induction, but you can choose not to use them

[Riccardo Brasca]

Note that in the current version the assumption is an implication with a stronger assumption that in your version, so the assumption is weaker and the theorem stronger.

[Riccardo Brasca]

As Aaron said, you can just ignore that x and y are in the closure.

[Kevin Buzzard]

(If you prove that the conjugate of the sup is the sup of the conjugates (which should be easy) then you don't need induction to prove this)