-- 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:
simpa only [map_one] using Subgroup.one_mem _

Result:
no goals

Proof state:
case refine_2.intro.mk.mul
ι : 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₁ w₂ : P.Aut
hw₁ : w₁ ∈ Subgroup.closure (range (Equiv.reflection P))
hw₂ : w₂ ∈ Subgroup.closure (range (Equiv.reflection P))
h₁ : ((Equiv.weightHom P).restrict P.weylGroup) ⟨w₁, hw₁⟩ ∈ Subgroup.closure (range P.reflection)
h₂ : ((Equiv.weightHom P).restrict P.weylGroup) ⟨w₂, hw₂⟩ ∈ Subgroup.closure (range P.reflection)
⊢ ((Equiv.weightHom P).restrict P.weylGroup) ⟨w₁ * w₂, ⋯⟩ ∈ Subgroup.closure (range P.reflection)

Tactic:
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
ι : 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.weightHom P).restrict P.weylGroup) ⟨w, hw⟩ ∈ Subgroup.closure (range P.reflection)

Tactic:
induction hw using Subgroup.closure_induction'' with
| one =>
  change ((Equiv.weightHom 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.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₂

Result:
no goals

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 : ι
⊢ P.reflection i ∈ Subgroup.closure (range P.reflection)

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

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 : ι
⊢ P.reflection i ∈ Subgroup.closure (range P.reflection)

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

Result:
no goals

Proof state:
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)

Tactic:
rintro fg ⟨⟨w, hw⟩, rfl⟩

Result:
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.weightHom P).restrict P.weylGroup) ⟨w, hw⟩ ∈ Subgroup.closure (range P.reflection)

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

Tactic:
simp only [MonoidHom.restrict_apply, Equiv.weightHom_apply, Equiv.reflection_weightEquiv]

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 : ι
⊢ P.reflection i ∈ Subgroup.closure (range P.reflection)

Proof state:
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

Tactic:
rintro - ⟨i, rfl⟩

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

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

Tactic:
simp only [Equiv.reflection_inv, MonoidHom.restrict_apply, Equiv.weightHom_apply,
  Equiv.reflection_weightEquiv]

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

Tactic:
use Equiv.reflection P i

Result:
case h
ι : 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.reflection P i ∈ P.weylGroup ∧ Equiv.weightEquiv P P (Equiv.reflection P i) = P.reflection i

Proof state:
case h
ι : 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.reflection P i ∈ P.weylGroup ∧ Equiv.weightEquiv P P (Equiv.reflection P i) = P.reflection i

Tactic:
exact ⟨reflection_mem_weylGroup P i, Equiv.reflection_weightEquiv P i⟩

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.weightHom P).restrict P.weylGroup) ⟨w', ⋯⟩ ∈ Subgroup.closure (range P.reflection)

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