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

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