awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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)
⊢ Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w'⁻¹ ⋯) :
      ι ≃ ι)
have 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)⁻¹ sorry) :
      ι ≃ ι)
Tactic: obtain ⟨i, rfl⟩ := hw'
Cleared hypotheses: w', hw'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i)⁻¹ ⋯) :
      ι ≃ ι)
have refine_2 : Membership.mem (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm)) (P.reflectionPerm i)
Tactic: simp only [Equiv.reflection_inv, MonoidHom.restrict_apply, Equiv.indexHom_apply,
        Equiv.reflection_indexEquiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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
hw : w ∈ P.weylGroup
⊢ 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) :
      ι ≃ ι)
have refine_2 : Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
  ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 sorry) : ι ≃ ι)
Tactic: induction hw using Subgroup.closure_induction'' with
    | one =>
      change ((Equiv.indexHom P).restrict P.weylGroup) 1 ∈ _
      simp only [map_one, 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₂
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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
hw : w ∈ P.weylGroup
refine_2 :
  Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 ⋯) : ι ≃ ι)
⊢ 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) :
      ι ≃ ι)
have refine_2₁ : ∀ (w' : P.Aut) (hw' : w' ∈ range (Equiv.reflection P)),
  Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w' sorry) :
      ι ≃ ι)
Tactic: induction hw using Subgroup.closure_induction'' with
    | one =>
      change ((Equiv.indexHom P).restrict P.weylGroup) 1 ∈ _
      simp only [map_one, 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₂
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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
hw : w ∈ P.weylGroup
refine_2 :
  Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 ⋯) : ι ≃ ι)
refine_2₁ :
  ∀ (w' : P.Aut) (hw' : w' ∈ range (Equiv.reflection P)),
    Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
      ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w' ⋯) :
        ι ≃ ι)
⊢ 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) :
      ι ≃ ι)
have refine_2₂ : ∀ (w' : P.Aut) (hw' : w' ∈ range (Equiv.reflection P)),
  Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w'⁻¹ sorry) :
      ι ≃ ι)
Tactic: induction hw using Subgroup.closure_induction'' with
    | one =>
      change ((Equiv.indexHom P).restrict P.weylGroup) 1 ∈ _
      simp only [map_one, 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₂
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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
hw : w ∈ P.weylGroup
refine_2 :
  Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
    ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 ⋯) : ι ≃ ι)
refine_2₁ :
  ∀ (w' : P.Aut) (hw' : w' ∈ range (Equiv.reflection P)),
    Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
      ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w' ⋯) :
        ι ≃ ι)
refine_2₂ :
  ∀ (w' : P.Aut) (hw' : w' ∈ range (Equiv.reflection P)),
    Membership.mem (α := ι ≃ ι) (γ := Subgroup (ι ≃ ι)) (Subgroup.closure (range P.reflectionPerm))
      ((P.weylGroupToPerm : (a : ↥P.weylGroup) → ι ≃ ι) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) w'⁻¹ ⋯) :
        ι ≃ ι)
⊢ 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) :
      ι ≃ ι)
have refine_2₃ : ∀ (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₂) sorry) :
      ι ≃ ι)
Tactic: induction hw using Subgroup.closure_induction'' with
    | one =>
      change ((Equiv.indexHom P).restrict P.weylGroup) 1 ∈ _
      simp only [map_one, 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₂
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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
⊢ 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)
have 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)
Tactic: revert x y
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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),
    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)
have 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)
Tactic: obtain ⟨g, hg⟩ := g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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 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)
have mul : Eq.{u_2 + 1} (α := R)
  ((((B.form : (a : M) → M →ₗ[R] R)
            ((Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ *
                Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂) •
              x) :
          M →ₗ[R] R) :
        (a : M) → R)
      ((Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ *
          Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂) •
        y) :
    R)
  ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: rw [← Submonoid.mk_mul_mk _ _ _ hg₁ hg₂, mul_smul, mul_smul, hg₁', hg₂']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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 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
mul :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R)
              ((Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ *
                  Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂) •
                x) :
            M →ₗ[R] R) :
          (a : M) → R)
        ((Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ *
            Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂) •
          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) (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)
have mul₁ : Eq.{u_2 + 1} (α := R)
  ((((B.form : (a : M) → M →ₗ[R] R)
            (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ •
              Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂ • x) :
          M →ₗ[R] R) :
        (a : M) → R)
      ((Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ *
          Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂) •
        y) :
    R)
  ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: rw [← Submonoid.mk_mul_mk _ _ _ hg₁ hg₂, mul_smul, mul_smul, hg₁', hg₂']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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 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
mul :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R)
              ((Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ *
                  Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂) •
                x) :
            M →ₗ[R] R) :
          (a : M) → R)
        ((Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ *
            Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂) •
          y) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
mul₁ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R)
              (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ •
                Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂ • x) :
            M →ₗ[R] R) :
          (a : M) → R)
        ((Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ *
            Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂) •
          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) (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)
have mul₂ : Eq.{u_2 + 1} (α := R)
  ((((B.form : (a : M) → M →ₗ[R] R)
            (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ •
              Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂ • x) :
          M →ₗ[R] R) :
        (a : M) → R)
      (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ •
        Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂ • y) :
    R)
  ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: rw [← Submonoid.mk_mul_mk _ _ _ hg₁ hg₂, mul_smul, mul_smul, hg₁', hg₂']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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
⊢ ∀ (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)
have 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) sorry • x) :
            M →ₗ[R] R) :
          (a : M) → R)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (Equiv.reflection P i) sorry • 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₂']
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
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)
⊢ ∀ (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)
have 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 sorry) x) :
            M →ₗ[R] R) :
          (a : M) → R)
        (HSMul.hSMul (α := ↥P.weylGroup) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) 1 sorry) 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₂']
Cleared hypotheses: hg