-- 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 (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
    ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 ⋯) :
      M ≃ₗ[R] M)
refine_2₁ :
  ∀ (w' : P.Aut) (hw' : w' ∈ range (Equiv.reflection P)),
    Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
      ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w' ⋯) :
        M ≃ₗ[R] M)
refine_2₂ :
  ∀ (w' : P.Aut) (hw' : w' ∈ range (Equiv.reflection P)),
    Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
      ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w'⁻¹ ⋯) :
        M ≃ₗ[R] M)
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 (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
        ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
            (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w₁ hw₁) :
          M ≃ₗ[R] M))
    (h₂ :
      Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
        ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
            (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w₂ hw₂) :
          M ≃ₗ[R] M)),
    Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
      ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (w₁ * w₂) ⋯) :
        M ≃ₗ[R] M)
⊢ Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
    ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w hw) :
      M ≃ₗ[R] M)

Tactic:
induction hw using Subgroup.closure_induction'' with
    | one =>
      change ((Equiv.weightHom P).restrict P.weylGroup) 1 ∈ _
      simp only [map_one, one_mem]
    | mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [MonoidHom.restrict_apply, Equiv.weightHom_apply, Equiv.reflection_weightEquiv]
      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.weightHom_apply,
        Equiv.reflection_weightEquiv]
      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, MonoidHom.restrict, MonoidHom.restrict_apply, RootPairing.Equiv.weightHom_apply, RootPairing.reflection_mem_weylGroup, InvMemClass.inv_mem, map_mul, map_one, RootPairing.Equiv.reflection_inv, RootPairing.Equiv.weightHom, OneMemClass.one_mem, OfNat.ofNat, DFunLike.coe, RootPairing.Equiv.reflection_weightEquiv, rfl