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

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.coweightHom P).restrict P.weylGroup) ⟨w, hw⟩ ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

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.coweightHom P).restrict P.weylGroup) ⟨(Equiv.reflection P i)⁻¹, ⋯⟩ ∈
    Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
simp only [Equiv.reflection_inv, MonoidHom.restrict_apply, Equiv.coweightHom_apply,
  Equiv.reflection_coweightEquiv]

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

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.coweightHom P) x = (MulOpposite.op ∘ P.coreflection) 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.coweightHom P) (Equiv.reflection P i) = (MulOpposite.op ∘ P.coreflection) i

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 : ι
⊢ (MulOpposite.op ∘ P.coreflection) i ∈ ↑((Equiv.coweightHom 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.coweightHom P) x = (MulOpposite.op ∘ P.coreflection) 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.coweightHom P).restrict P.weylGroup) 1 ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

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

Result:
no goals

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 (MulOpposite.op ∘ P.coreflection) ⊆ ↑((Equiv.coweightHom 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 : ι
⊢ (MulOpposite.op ∘ P.coreflection) i ∈ ↑((Equiv.coweightHom P).restrict P.weylGroup).range

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.coweightHom P).restrict P.weylGroup) ⟨w'⁻¹, ⋯⟩ ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

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.coweightHom P).restrict P.weylGroup) ⟨(Equiv.reflection P i)⁻¹, ⋯⟩ ∈
    Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

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.coweightHom P).restrict P.weylGroup) ⟨1, ⋯⟩ ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
change ((Equiv.coweightHom 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.coweightHom P).restrict P.weylGroup) 1 ∈ 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 : ι
⊢ ((Equiv.coweightHom P).restrict P.weylGroup) ⟨Equiv.reflection P i, ⋯⟩ ∈
    Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
simp only [MonoidHom.restrict_apply, Equiv.coweightHom_apply, Equiv.reflection_coweightEquiv]

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

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.coweightHom P).restrict P.weylGroup) ⟨w₁, hw₁⟩ ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))
h₂ : ((Equiv.coweightHom P).restrict P.weylGroup) ⟨w₂, hw₂⟩ ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))
⊢ ((Equiv.coweightHom P).restrict P.weylGroup) ⟨w₁ * w₂, ⋯⟩ ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

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 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.coweightHom P) (Equiv.reflection P i) = (MulOpposite.op ∘ P.coreflection) i

Tactic:
refine ⟨reflection_mem_weylGroup P i, by simp⟩

Result:
no goals