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
w w' : P.Aut
hw' : w' ∈ range (Equiv.reflection P)
refine_2 :
  ∀ (i : ι),
    Membership.mem (α := (N ≃ₗ[R] N)ᵐᵒᵖ) (γ := Subgroup (N ≃ₗ[R] N)ᵐᵒᵖ)
      (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
      ((((Equiv.coweightHom P).restrict P.weylGroup : ↥P.weylGroup →* (N ≃ₗ[R] N)ᵐᵒᵖ) :
            (a : ↥P.weylGroup) → (N ≃ₗ[R] N)ᵐᵒᵖ)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯) :
        (N ≃ₗ[R] N)ᵐᵒᵖ)
⊢ Membership.mem (α := (N ≃ₗ[R] N)ᵐᵒᵖ) (γ := Subgroup (N ≃ₗ[R] N)ᵐᵒᵖ)
    (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
    ((((Equiv.coweightHom P).restrict P.weylGroup : ↥P.weylGroup →* (N ≃ₗ[R] N)ᵐᵒᵖ) :
          (a : ↥P.weylGroup) → (N ≃ₗ[R] N)ᵐᵒᵖ)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w' ⋯) :
      (N ≃ₗ[R] N)ᵐᵒᵖ)

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 (N ≃ₗ[R] N)ᵐᵒᵖ) (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
    (MulOpposite.op (P.coreflection i))
⊢ Membership.mem (α := (N ≃ₗ[R] N)ᵐᵒᵖ) (γ := Subgroup (N ≃ₗ[R] N)ᵐᵒᵖ)
    (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
    ((((Equiv.coweightHom P).restrict P.weylGroup : ↥P.weylGroup →* (N ≃ₗ[R] N)ᵐᵒᵖ) :
          (a : ↥P.weylGroup) → (N ≃ₗ[R] N)ᵐᵒᵖ)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯) :
      (N ≃ₗ[R] N)ᵐᵒᵖ)

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

Premises used: MonoidHom.restrict_apply, RootPairing.Equiv.coweightHom_apply, RootPairing.Equiv.reflection_coweightEquiv
-- 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 (N ≃ₗ[R] N)ᵐᵒᵖ) (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
    (MulOpposite.op (P.coreflection 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 (α := (N ≃ₗ[R] N)ᵐᵒᵖ) (γ := Subgroup (N ≃ₗ[R] N)ᵐᵒᵖ)
      (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
      ((((Equiv.coweightHom P).restrict P.weylGroup : ↥P.weylGroup →* (N ≃ₗ[R] N)ᵐᵒᵖ) :
            (a : ↥P.weylGroup) → (N ≃ₗ[R] N)ᵐᵒᵖ)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i)⁻¹ ⋯) :
        (N ≃ₗ[R] N)ᵐᵒᵖ)
⊢ Membership.mem (α := (N ≃ₗ[R] N)ᵐᵒᵖ) (γ := Subgroup (N ≃ₗ[R] N)ᵐᵒᵖ)
    (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
    ((((Equiv.coweightHom P).restrict P.weylGroup : ↥P.weylGroup →* (N ≃ₗ[R] N)ᵐᵒᵖ) :
          (a : ↥P.weylGroup) → (N ≃ₗ[R] N)ᵐᵒᵖ)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w'⁻¹ ⋯) :
      (N ≃ₗ[R] N)ᵐᵒᵖ)

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 (N ≃ₗ[R] N)ᵐᵒᵖ) (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
    (MulOpposite.op (P.coreflection i))
⊢ Membership.mem (α := (N ≃ₗ[R] N)ᵐᵒᵖ) (γ := Subgroup (N ≃ₗ[R] N)ᵐᵒᵖ)
    (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
    ((((Equiv.coweightHom P).restrict P.weylGroup : ↥P.weylGroup →* (N ≃ₗ[R] N)ᵐᵒᵖ) :
          (a : ↥P.weylGroup) → (N ≃ₗ[R] N)ᵐᵒᵖ)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i)⁻¹ ⋯) :
      (N ≃ₗ[R] N)ᵐᵒᵖ)

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

Premises used: MonoidHom.restrict_apply, RootPairing.Equiv.reflection_inv, RootPairing.Equiv.coweightHom_apply, RootPairing.Equiv.reflection_coweightEquiv
-- 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 (α := (N ≃ₗ[R] N)ᵐᵒᵖ) (γ := Subgroup (N ≃ₗ[R] N)ᵐᵒᵖ)
    (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
    ((((Equiv.coweightHom P).restrict P.weylGroup : ↥P.weylGroup →* (N ≃ₗ[R] N)ᵐᵒᵖ) :
          (a : ↥P.weylGroup) → (N ≃ₗ[R] N)ᵐᵒᵖ)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w₁ hw₁) :
      (N ≃ₗ[R] N)ᵐᵒᵖ)
h₂ :
  Membership.mem (α := (N ≃ₗ[R] N)ᵐᵒᵖ) (γ := Subgroup (N ≃ₗ[R] N)ᵐᵒᵖ)
    (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
    ((((Equiv.coweightHom P).restrict P.weylGroup : ↥P.weylGroup →* (N ≃ₗ[R] N)ᵐᵒᵖ) :
          (a : ↥P.weylGroup) → (N ≃ₗ[R] N)ᵐᵒᵖ)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w₂ hw₂) :
      (N ≃ₗ[R] N)ᵐᵒᵖ)
⊢ Membership.mem (α := (N ≃ₗ[R] N)ᵐᵒᵖ) (γ := Subgroup (N ≃ₗ[R] N)ᵐᵒᵖ)
    (Subgroup.closure (range (MulOpposite.op ∘ P.coreflection)))
    ((((Equiv.coweightHom P).restrict P.weylGroup : ↥P.weylGroup →* (N ≃ₗ[R] N)ᵐᵒᵖ) :
          (a : ↥P.weylGroup) → (N ≃ₗ[R] N)ᵐᵒᵖ)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (w₁ * w₂) ⋯) :
      (N ≃ₗ[R] N)ᵐᵒᵖ)

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

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.reflectionPerm ⊆ (↑P.weylGroupToPerm.range : Set (ι ≃ ι))
refine_2 : P.weylGroupToPerm.range ≤ Subgroup.closure (range P.reflectionPerm)
⊢ P.weylGroupToPerm.range = Subgroup.closure (range P.reflectionPerm)

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.indexHom P : (a : P.Aut) → ι ≃ ι) x = P.reflectionPerm i
⊢ P.reflectionPerm i ∈ (↑P.weylGroupToPerm.range : Set (ι ≃ ι))

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.indexHom P : (a : P.Aut) → ι ≃ ι) (Equiv.reflection P i) = P.reflectionPerm i
⊢ ∃ x ∈ P.weylGroup, (Equiv.indexHom P : (a : P.Aut) → ι ≃ ι) x = P.reflectionPerm 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.indexHom P : (a : P.Aut) → ι ≃ ι) (Equiv.reflection P i) = P.reflectionPerm 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.indexHom P : (a : P.Aut) → ι ≃ ι) (Equiv.reflection P i) = P.reflectionPerm 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 (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    (((Equiv.indexHom P).restrict P.weylGroup : (a : ↥P.weylGroup) → ι ≃ ι) 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 (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
      ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯) :
        ι ≃ ι)
⊢ Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w' ⋯) :
      ι ≃ ι)

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 (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm)) (P.reflectionPerm i)
⊢ Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯) :
      ι ≃ ι)

Tactic:
simp only [MonoidHom.restrict_apply, Equiv.indexHom_apply, Equiv.reflection_indexEquiv]

Premises used: MonoidHom.restrict_apply, RootPairing.Equiv.indexHom_apply, RootPairing.Equiv.reflection_indexEquiv
-- 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 (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm)) (P.reflectionPerm 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 (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
      ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i)⁻¹ ⋯) :
        ι ≃ ι)
⊢ Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w'⁻¹ ⋯) :
      ι ≃ ι)

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 (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm)) (P.reflectionPerm i)
⊢ Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i)⁻¹ ⋯) :
      ι ≃ ι)

Tactic:
simp only [Equiv.reflection_inv, MonoidHom.restrict_apply, Equiv.indexHom_apply,
        Equiv.reflection_indexEquiv]

Premises used: MonoidHom.restrict_apply, RootPairing.Equiv.indexHom_apply, RootPairing.Equiv.reflection_inv, RootPairing.Equiv.reflection_indexEquiv
-- 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 (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w₁ hw₁) :
      ι ≃ ι)
h₂ :
  Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w₂ hw₂) :
      ι ≃ ι)
⊢ Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (w₁ * w₂) ⋯) :
      ι ≃ ι)

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
g : ↥P.weylGroup
i : ι
⊢ HSMul.hSMul (β := M) g ((P.root : (a : ι) → M) i : M) =
    (P.root : (a : ι) → M) ((((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) g : ι ≃ ι) : (a : ι) → ι) i : ι)

Tactic:
Hom.root_weightMap_apply _ _ _ _

Premises used: RootPairing.Hom.root_weightMap_apply
-- 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
B : P.InvariantForm
g : ↥P.weylGroup
x y : M
revert :
  ∀ (x y : M),
    Eq.{u_2 + 1} (α := R) ((((B.form : (a : M) → M →ₗ[R] R) (g • x) : M →ₗ[R] R) : (a : M) → R) (g • y) : R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ Eq.{u_2 + 1} (α := R) ((((B.form : (a : M) → M →ₗ[R] R) (g • x) : M →ₗ[R] R) : (a : M) → R) (g • y) : R)
    ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
revert x y
-- 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
B : P.InvariantForm
g : ↥P.weylGroup
obtain :
  ∀ (g : P.Aut) (hg : g ∈ P.weylGroup) (x y : M),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g hg • x) : M →ₗ[R] R) :
            (a : M) → R)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g hg • y) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ ∀ (x y : M),
    Eq.{u_2 + 1} (α := R) ((((B.form : (a : M) → M →ₗ[R] R) (g • x) : M →ₗ[R] R) : (a : M) → R) (g • y) : R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
obtain ⟨g, hg⟩ := g
-- 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
B : P.InvariantForm
g : P.Aut
i : ι
⊢ ∀ (x y : M),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R)
                (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯ • x) :
              M →ₗ[R] R) :
            (a : M) → R)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯ • y) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

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
B : P.InvariantForm
g : P.Aut
⊢ ∀ (x y : M),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R)
                (HSMul.hSMul (α := ↥P.weylGroup) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 ⋯) x) :
              M →ₗ[R] R) :
            (a : M) → R)
          (HSMul.hSMul (α := ↥P.weylGroup) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 ⋯) y) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

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
B : P.InvariantForm
g : P.Aut
hg : g ∈ P.weylGroup
mem :
  ∀ (i : ι) (x y : M),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R)
                (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯ • x) :
              M →ₗ[R] R) :
            (a : M) → R)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) ⋯ • y) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
one :
  ∀ (x y : M),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R)
                (HSMul.hSMul (α := ↥P.weylGroup) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 ⋯) x) :
              M →ₗ[R] R) :
            (a : M) → R)
          (HSMul.hSMul (α := ↥P.weylGroup) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 ⋯) y) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
mul :
  ∀ (g₁ g₂ : P.Aut) (hg₁ : g₁ ∈ P.weylGroup) (hg₂ : g₂ ∈ P.weylGroup)
    (hg₁' :
      ∀ (x y : M),
        Eq.{u_2 + 1} (α := R)
          ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g₁ hg₁ • x) :
                  M →ₗ[R] R) :
                (a : M) → R)
              (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g₁ hg₁ • y) :
            R)
          ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R))
    (hg₂' :
      ∀ (x y : M),
        Eq.{u_2 + 1} (α := R)
          ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g₂ hg₂ • x) :
                  M →ₗ[R] R) :
                (a : M) → R)
              (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g₂ hg₂ • y) :
            R)
          ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R))
    (x y : M),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (g₁ * g₂) ⋯ • x) :
              M →ₗ[R] R) :
            (a : M) → R)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (g₁ * g₂) ⋯ • y) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ ∀ (x y : M),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g hg • x) : M →ₗ[R] R) :
            (a : M) → R)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g hg • y) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
induction hg using weylGroup.induction with
  | mem i => simp
  | one => simp
  | mul g₁ g₂ hg₁ hg₂ hg₁' hg₂' =>
    intro x y
    rw [← Submonoid.mk_mul_mk _ _ _ hg₁ hg₂, mul_smul, mul_smul, hg₁', hg₂']

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
⊢ x ≡ y [SMOD U] ↔ Eq (α := M ⧸ U) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y)

Tactic:
Iff.rfl

Premises used: Iff.rfl, SModEq
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R M
x y : M
rw : Eq (α := M ⧸ U) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y) ↔ x - y ∈ U
rw₁ rw₂ : x - y ∈ U ↔ x - y ∈ U
⊢ x ≡ y [SMOD U] ↔ x - y ∈ U

Tactic:
rw [SModEq.def, Submodule.Quotient.eq]

Premises used: Submodule.Quotient.eq, SModEq.def
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
⊢ SModEq.{u_1, u_4} (R := R) ⊤ x y

Tactic:
(Submodule.Quotient.eq ⊤).2 mem_top

Premises used: Submodule.Quotient.eq, Iff.mpr, Top.top, Submodule.mem_top, SModEq
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
rw : Eq (α := HasQuotient.Quotient M (B := Submodule R M) ⊥) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y) ↔ x = y
rw₁ : Membership.mem (γ := Submodule R M) ⊥ (x - y) ↔ x = y
rw₂ : x - y = 0 ↔ x = y
rw₃ rw₄ : x = y ↔ x = y
⊢ SModEq.{u_1, u_4} (R := R) ⊥ x y ↔ x = y

Tactic:
rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]

Premises used: Submodule.Quotient.eq, sub_eq_zero, Submodule.mem_bot, SModEq.def
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
U₁ U₂ : Submodule R M
x y : M
HU : U₁ ≤ U₂
hxy : x ≡ y [SMOD U₁]
⊢ x ≡ y [SMOD U₂]

Tactic:
(Submodule.Quotient.eq U₂).2 <| HU <| (Submodule.Quotient.eq U₁).1 hxy

Premises used: Submodule.Quotient.eq, Iff.mpr, Iff.mp, SModEq
-- Module: Mathlib.LinearAlgebra.SModEq.Basic
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : Ring S
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module S M
U : Submodule R M
V : Submodule S M
h : U.toAddSubgroup ≤ V.toAddSubgroup
x y : M
hxy : x ≡ y [SMOD U]
simp : ∀ (hxy : x - y ∈ U), x - y ∈ V
⊢ x ≡ y [SMOD V]

Tactic:
simp only [SModEq, Submodule.Quotient.eq] at hxy ⊢

Premises used: Submodule.Quotient.eq, SModEq