-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
w : P.Aut
hw : w ∈ P.weylGroup
refine_2 :
  Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 ⋯) : ι ≃ ι)
refine_2₁ :
  ∀ (w' : P.Aut) (hw' : w' ∈ range (Equiv.reflection P)),
    Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
      ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w' ⋯) :
        ι ≃ ι)
refine_2₂ :
  ∀ (w' : P.Aut) (hw' : w' ∈ range (Equiv.reflection P)),
    Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
      ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w'⁻¹ ⋯) :
        ι ≃ ι)
refine_2₃ :
  ∀ (w₁ w₂ : P.Aut) (hw₁ : Membership.mem (γ := Subgroup P.Aut) (Subgroup.closure (range (Equiv.reflection P))) w₁)
    (hw₂ : Membership.mem (γ := Subgroup P.Aut) (Subgroup.closure (range (Equiv.reflection P))) w₂)
    (h₁ :
      Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
        ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w₁ hw₁) :
          ι ≃ ι))
    (h₂ :
      Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
        ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w₂ hw₂) :
          ι ≃ ι)),
    Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
      ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (w₁ * w₂) ⋯) :
        ι ≃ ι)
⊢ Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w hw) :
      ι ≃ ι)

Tactic:
induction hw using Subgroup.closure_induction'' with
    | one =>
      change ((Equiv.indexHom P).restrict P.weylGroup) 1 ∈ _
      simp only [map_one, one_mem]
    | mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [MonoidHom.restrict_apply, Equiv.indexHom_apply, Equiv.reflection_indexEquiv]
      simpa only [reflection_mem_weylGroup] using Subgroup.subset_closure (mem_range_self i)
    | inv_mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [Equiv.reflection_inv, MonoidHom.restrict_apply, Equiv.indexHom_apply,
        Equiv.reflection_indexEquiv]
      simpa only [reflection_mem_weylGroup] using Subgroup.subset_closure (mem_range_self i)
    | mul w₁ w₂ hw₁ hw₂ h₁ h₂ =>
      simpa only [← Submonoid.mk_mul_mk _ w₁ w₂ hw₁ hw₂, map_mul] using Subgroup.mul_mem _ h₁ h₂

Premises used: RootPairing.weylGroup, RootPairing.Equiv.indexHom, MonoidHom.restrict, MonoidHom.restrict_apply, RootPairing.reflection_mem_weylGroup, InvMemClass.inv_mem, map_mul, RootPairing.Equiv.indexHom_apply, map_one, RootPairing.Equiv.reflection_inv, RootPairing.Equiv.reflection_indexEquiv, OneMemClass.one_mem, OfNat.ofNat, DFunLike.coe, rfl