-- Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean
lemma range_weylGroup_coweightHom :
    MonoidHom.range ((Equiv.coweightHom P).restrict P.weylGroup) =
      Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ ((Equiv.coweightHom P).restrict P.weylGroup).range = Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
refine (Subgroup.closure_eq_of_le _ ?_ ?_).symm

Result:
case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ range (MulOpposite.op ∘ P.coreflection) ⊆ ↑((Equiv.coweightHom P).restrict P.weylGroup).range

case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ ((Equiv.coweightHom P).restrict P.weylGroup).range ≤ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Proof state:
case refine_2.intro.mk
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
w : P.Aut
hw : w ∈ P.weylGroup
⊢ ((Equiv.coweightHom P).restrict P.weylGroup) ⟨w, hw⟩ ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
induction hw using Subgroup.closure_induction'' with
| one =>
  change ((Equiv.coweightHom P).restrict P.weylGroup) 1 ∈ _
  simpa only [map_one] using Subgroup.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₂

Result:
no goals

Proof state:
case refine_2.intro.mk.mem
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
w w' : P.Aut
hw' : w' ∈ range (Equiv.reflection P)
⊢ ((Equiv.coweightHom P).restrict P.weylGroup) ⟨w', ⋯⟩ ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
obtain ⟨i, rfl⟩ := hw'

Result:
case refine_2.intro.mk.mem.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
w : P.Aut
i : ι
⊢ ((Equiv.coweightHom P).restrict P.weylGroup) ⟨Equiv.reflection P i, ⋯⟩ ∈
    Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Proof state:
case refine_2.intro.mk.mem.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
w : P.Aut
i : ι
⊢ MulOpposite.op (P.coreflection i) ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
simpa only [reflection_mem_weylGroup] using Subgroup.subset_closure (mem_range_self i)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (Equiv.coweightHom P) (Equiv.reflection P i) = (MulOpposite.op ∘ P.coreflection) i

Tactic:
simp

Result:
no goals

Proof state:
case refine_2.intro.mk.inv_mem.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
w : P.Aut
i : ι
⊢ MulOpposite.op (P.coreflection i) ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
simpa only [reflection_mem_weylGroup] using Subgroup.subset_closure (mem_range_self i)

Result:
no goals