-- Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean
lemma range_weylGroupToPerm :
    P.weylGroupToPerm.range = Subgroup.closure (range P.reflection_perm)

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
⊢ P.weylGroupToPerm ⟨w, hw⟩ ∈ Subgroup.closure (range P.reflection_perm)

Tactic:
induction hw using Subgroup.closure_induction'' with
| one =>
  change ((Equiv.indexHom 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.indexHom_apply, Equiv.reflection_indexEquiv]
  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.indexHom_apply,
    Equiv.reflection_indexEquiv]
  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.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
⊢ P.weylGroupToPerm ⟨1, ⋯⟩ ∈ Subgroup.closure (range P.reflection_perm)

Tactic:
change ((Equiv.indexHom 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.indexHom P).restrict P.weylGroup) 1 ∈ Subgroup.closure (range P.reflection_perm)

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)
⊢ P.weylGroupToPerm ⟨w', ⋯⟩ ∈ Subgroup.closure (range P.reflection_perm)

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

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
⊢ P.weylGroupToPerm.range ≤ Subgroup.closure (range P.reflection_perm)

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
⊢ P.weylGroupToPerm ⟨w, hw⟩ ∈ Subgroup.closure (range P.reflection_perm)

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_perm ⊆ ↑P.weylGroupToPerm.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_perm i ∈ ↑P.weylGroupToPerm.range

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.indexHom P) (Equiv.reflection P i) = P.reflection_perm i

Tactic:
refine ⟨reflection_mem_weylGroup P i, by simp⟩

Result:
no goals

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)
⊢ P.weylGroupToPerm ⟨w'⁻¹, ⋯⟩ ∈ Subgroup.closure (range P.reflection_perm)

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

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
⊢ P.weylGroupToPerm.range = Subgroup.closure (range P.reflection_perm)

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_perm ⊆ ↑P.weylGroupToPerm.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
⊢ P.weylGroupToPerm.range ≤ Subgroup.closure (range P.reflection_perm)

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₁ : P.weylGroupToPerm ⟨w₁, hw₁⟩ ∈ Subgroup.closure (range P.reflection_perm)
h₂ : P.weylGroupToPerm ⟨w₂, hw₂⟩ ∈ Subgroup.closure (range P.reflection_perm)
⊢ P.weylGroupToPerm ⟨w₁ * w₂, ⋯⟩ ∈ Subgroup.closure (range P.reflection_perm)

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_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.indexHom P) x = P.reflection_perm 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.indexHom P) (Equiv.reflection P i) = P.reflection_perm i

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.indexHom P).restrict P.weylGroup) 1 ∈ Subgroup.closure (range P.reflection_perm)

Tactic:
simpa only [map_one] using Subgroup.one_mem _

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_perm i ∈ Subgroup.closure (range P.reflection_perm)

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

Result:
no goals