-- Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean
lemma range_weylGroup_weightHom :
    MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup) =
      Subgroup.closure (range P.reflection)

Proof state:
case refine_2.intro.mk.one
ι : 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
⊢ ((Equiv.weightHom P).restrict P.weylGroup) ⟨1, ⋯⟩ ∈ Subgroup.closure (range P.reflection)

Tactic:
change ((Equiv.weightHom P).restrict P.weylGroup) 1 ∈ _

Result:
case refine_2.intro.mk.one
ι : 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
⊢ ((Equiv.weightHom P).restrict P.weylGroup) 1 ∈ Subgroup.closure (range P.reflection)

Proof state:
case refine_2.intro.mk.inv_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.weightHom P).restrict P.weylGroup) ⟨w'⁻¹, ⋯⟩ ∈ Subgroup.closure (range P.reflection)

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

Result:
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 : ι
⊢ ((Equiv.weightHom P).restrict P.weylGroup) ⟨(Equiv.reflection P i)⁻¹, ⋯⟩ ∈ Subgroup.closure (range P.reflection)

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.weightHom P).restrict P.weylGroup).range = Subgroup.closure (range P.reflection)

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 P.reflection ⊆ ↑((Equiv.weightHom 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.weightHom P).restrict P.weylGroup).range ≤ Subgroup.closure (range P.reflection)

Proof state:
case refine_1.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
i : ι
⊢ P.reflection i ∈ ↑((Equiv.weightHom P).restrict P.weylGroup).range

Tactic:
simp only [MonoidHom.restrict_range, Subgroup.coe_map, Equiv.weightHom_apply, mem_image,
  SetLike.mem_coe]

Result:
case refine_1.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
i : ι
⊢ ∃ x ∈ P.weylGroup, Equiv.weightEquiv P P x = P.reflection i