awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
one : pred 1 ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
pred' : (g : P.Aut) → Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) g → Prop :=
  fun (g : P.Aut) (hg : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) g) ↦
    pred g ⋯
hx' : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) x
⊢ pred' 1 ⋯

Tactic:
one
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
one : pred 1 ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
pred' : (g : P.Aut) → Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) g → Prop :=
  fun (g : P.Aut) (hg : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) g) ↦
    pred g ⋯
hx' : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) x
⊢ pred' 1 ⋯

Tactic:
exact one
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
one : pred 1 ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x_1 : P.Aut
hx_1 : x_1 ∈ P.weylGroup
pred' : (g : P.Aut) → Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) g → Prop :=
  fun (g : P.Aut) (hg : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) g) ↦
    pred g ⋯
hx'_1 : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) x_1
x y : P.Aut
hx : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) x
hy : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) y
hx' : pred' x hx
hy' : pred' y hy
mul₁ :
  ∀ (hx_2 : x ∈ P.weylGroup.toSubmonoid)
    (hy : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) y)
    (hy_1 : y ∈ P.weylGroup.toSubmonoid) (hx' : pred' x hx) (hy' : pred' y hy), pred' (x * y) ⋯
⊢ pred' (x * y) ⋯

Tactic:
rw [← weylGroup_toSubmonoid] at hx hy

Premises used: RootPairing.weylGroup_toSubmonoid
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
one : pred 1 ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x_1 : P.Aut
hx_1 : x_1 ∈ P.weylGroup
pred' : (g : P.Aut) → Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) g → Prop :=
  fun (g : P.Aut) (hg : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) g) ↦
    pred g ⋯
hx'_1 : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) x_1
x y : P.Aut
hx_2 : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) x
hx : x ∈ P.weylGroup.toSubmonoid
hy_1 : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) y
hy : y ∈ P.weylGroup.toSubmonoid
hx' : pred' x hx_2
hy' : pred' y hy_1
⊢ pred' (x * y) ⋯

Tactic:
mul x y hx hy hx' hy'
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
one : pred 1 ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x_1 : P.Aut
hx_1 : x_1 ∈ P.weylGroup
pred' : (g : P.Aut) → Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) g → Prop :=
  fun (g : P.Aut) (hg : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) g) ↦
    pred g ⋯
hx'_1 : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) x_1
x y : P.Aut
hx_2 : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) x
hx : x ∈ P.weylGroup.toSubmonoid
hy_1 : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) y
hy : y ∈ P.weylGroup.toSubmonoid
hx' : pred' x hx_2
hy' : pred' y hy_1
⊢ pred' (x * y) ⋯

Tactic:
exact mul x y hx hy hx' hy'
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nonempty ι
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
⊢ pred x hx

Tactic:
weylGroup.induction P mem ?_ mul hx

Premises used: RootPairing.weylGroup.induction
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nonempty ι
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
refine : pred 1 ⋯
⊢ pred x hx

Tactic:
refine weylGroup.induction P mem ?_ mul hx
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nonempty ι
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
⊢ Nonempty ι

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nonempty ι
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
obtain : ∀ (i : ι), pred 1 ⋯
⊢ pred 1 ⋯

Tactic:
obtain ⟨i⟩ : Nonempty ι := inferInstance

Premises used: Nonempty
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nonempty ι
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
i : ι
rw : Equiv.reflection P i * Equiv.reflection P i = 1
rw₁ : (Equiv.reflection P i)⁻¹ = Equiv.reflection P i
rw₂ rw₃ : Equiv.reflection P i = Equiv.reflection P i
⊢ HPow.hPow (β := ℕ) (Equiv.reflection P i) 2 = 1

Tactic:
rw [sq, mul_eq_one_iff_inv_eq, Equiv.reflection_inv P i]

Premises used: mul_eq_one_iff_inv_eq, sq, RootPairing.Equiv.reflection_inv
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nonempty ι
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
i : ι
have : ∀ (this : HPow.hPow (β := ℕ) (Equiv.reflection P i) 2 = 1), pred 1 ⋯
⊢ pred 1 ⋯

Tactic:
have : (Equiv.reflection P i) ^ 2 = 1 := by
    rw [sq, mul_eq_one_iff_inv_eq, Equiv.reflection_inv P i]
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nonempty ι
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
i : ι
this : HPow.hPow (β := ℕ) (Equiv.reflection P i) 2 = 1
⊢ pred 1 ⋯

Tactic:
simpa [sq, ← this] using mul _ _ _ _ (mem i) (mem i)

Premises used: sq
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup) = Subgroup.closure (range P.reflection)

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

Premises used: Subgroup.closure_eq_of_le, Eq.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
refine_1 : range P.reflection ⊆ (↑(MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup)) : Set (M ≃ₗ[R] M))
refine_2 : MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup) ≤ Subgroup.closure (range P.reflection)
⊢ MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup) = Subgroup.closure (range P.reflection)

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

Premises used: Subgroup.closure_eq_of_le, Eq.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i : ι
refine_1 : ∃ x ∈ P.weylGroup, Equiv.weightEquiv P P x = P.reflection i
⊢ P.reflection i ∈ (↑(MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup)) : Set (M ≃ₗ[R] M))

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

Premises used: Subgroup.coe_map, Set.mem_image, MonoidHom.restrict_range, RootPairing.Equiv.weightHom_apply, SetLike.mem_coe
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i : ι
h : Equiv.reflection P i ∈ P.weylGroup ∧ Equiv.weightEquiv P P (Equiv.reflection P i) = P.reflection i
⊢ ∃ x ∈ P.weylGroup, Equiv.weightEquiv P P x = P.reflection i

Tactic:
use Equiv.reflection P i

Premises used: RootPairing.Equiv.reflection
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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:
⟨reflection_mem_weylGroup P i, Equiv.reflection_weightEquiv P i⟩

Premises used: RootPairing.reflection_mem_weylGroup, And.intro, RootPairing.Equiv.reflection_weightEquiv
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : 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⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
w : P.Aut
⊢ Membership.mem (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
    (((Equiv.weightHom P).restrict P.weylGroup : (a : ↥P.weylGroup) → M ≃ₗ[R] M) 1)

Tactic:
simp only [map_one, one_mem]

Premises used: map_one, OneMemClass.one_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
w w' : P.Aut
hw' : w' ∈ range (Equiv.reflection P)
refine_2 :
  ∀ (i : ι),
    Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
      ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯) :
        M ≃ₗ[R] M)
⊢ Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
    ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w' ⋯) :
      M ≃ₗ[R] M)

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

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
w : P.Aut
i : ι
refine_2 : Membership.mem (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection)) (P.reflection i)
⊢ Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
    ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯) :
      M ≃ₗ[R] M)

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

Premises used: MonoidHom.restrict_apply, RootPairing.Equiv.weightHom_apply, RootPairing.Equiv.reflection_weightEquiv
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
w : P.Aut
i : ι
⊢ Membership.mem (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection)) (P.reflection i)

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

Premises used: Set.mem_range_self, RootPairing.reflection_mem_weylGroup, Subgroup.subset_closure
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
w w' : P.Aut
hw' : w' ∈ range (Equiv.reflection P)
refine_2 :
  ∀ (i : ι),
    Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
      ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i)⁻¹ ⋯) :
        M ≃ₗ[R] M)
⊢ Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
    ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w'⁻¹ ⋯) :
      M ≃ₗ[R] M)

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

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
w : P.Aut
i : ι
refine_2 : Membership.mem (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection)) (P.reflection i)
⊢ Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
    ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i)⁻¹ ⋯) :
      M ≃ₗ[R] M)

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

Premises used: MonoidHom.restrict_apply, RootPairing.Equiv.weightHom_apply, RootPairing.Equiv.reflection_inv, RootPairing.Equiv.reflection_weightEquiv
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
w w₁ w₂ : P.Aut
hw₁ : Membership.mem (γ := Subgroup P.Aut) (Subgroup.closure (range (Equiv.reflection P))) w₁
hw₂ : Membership.mem (γ := Subgroup P.Aut) (Subgroup.closure (range (Equiv.reflection P))) w₂
h₁ :
  Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
    ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w₁ hw₁) :
      M ≃ₗ[R] M)
h₂ :
  Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
    ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w₂ hw₂) :
      M ≃ₗ[R] M)
⊢ Membership.mem (α := M ≃ₗ[R] M) (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection))
    ((((Equiv.weightHom P).restrict P.weylGroup : ↥P.weylGroup →* M ≃ₗ[R] M) : (a : ↥P.weylGroup) → M ≃ₗ[R] M)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (w₁ * w₂) ⋯) :
      M ≃ₗ[R] M)

Tactic:
simpa only [← Submonoid.mk_mul_mk _ w₁ w₂ hw₁ hw₂, map_mul] using Subgroup.mul_mem _ h₁ h₂

Premises used: Submonoid.mk_mul_mk, map_mul, Subgroup.mul_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ MonoidHom.range ((Equiv.coweightHom P).restrict P.weylGroup) =
    Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

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

Premises used: Subgroup.closure_eq_of_le, Eq.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
refine_1 :
  range (MulOpposite.op ∘ P.coreflection) ⊆
    (↑(MonoidHom.range ((Equiv.coweightHom P).restrict P.weylGroup)) : Set (N ≃ₗ[R] N)ᵐᵒᵖ)
refine_2 :
  MonoidHom.range ((Equiv.coweightHom P).restrict P.weylGroup) ≤
    Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))
⊢ MonoidHom.range ((Equiv.coweightHom P).restrict P.weylGroup) =
    Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

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

Premises used: Subgroup.closure_eq_of_le, Eq.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i : ι
refine_1 :
  ∃ x ∈ P.weylGroup, (Equiv.coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) x = (MulOpposite.op ∘ P.coreflection) i
⊢ (MulOpposite.op ∘ P.coreflection) i ∈
    (↑(MonoidHom.range ((Equiv.coweightHom P).restrict P.weylGroup)) : Set (N ≃ₗ[R] N)ᵐᵒᵖ)

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

Premises used: Subgroup.coe_map, Set.mem_image, MonoidHom.restrict_range, SetLike.mem_coe
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i : ι
h :
  Equiv.reflection P i ∈ P.weylGroup ∧
    (Equiv.coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (Equiv.reflection P i) = (MulOpposite.op ∘ P.coreflection) i
⊢ ∃ x ∈ P.weylGroup, (Equiv.coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) x = (MulOpposite.op ∘ P.coreflection) i

Tactic:
use Equiv.reflection P i

Premises used: RootPairing.Equiv.reflection
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i : ι
⊢ (Equiv.coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (Equiv.reflection P i) = (MulOpposite.op ∘ P.coreflection) i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i : ι
⊢ Equiv.reflection P i ∈ P.weylGroup ∧
    (Equiv.coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (Equiv.reflection P i) = (MulOpposite.op ∘ P.coreflection) i

Tactic:
refine ⟨reflection_mem_weylGroup P i, by simp⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
w : P.Aut
⊢ Membership.mem (γ := Subgroup (N ≃ₗ[R] N)ᵐᵒᵖ) (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
    (((Equiv.coweightHom P).restrict P.weylGroup : (a : ↥P.weylGroup) → (N ≃ₗ[R] N)ᵐᵒᵖ) 1)

Tactic:
simp only [map_one, one_mem]

Premises used: map_one, OneMemClass.one_mem