awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.RootPositive (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : Algebra S R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : IsStrictOrderedRing S
inl : ∀ (h : 0 < P.pairingIn S i j), 0 ≤ P.pairingIn S i j * P.pairingIn S j i
⊢ 0 ≤ P.pairingIn S i j * P.pairingIn S j i
have inr : ∀ (h : P.pairingIn S i j ≤ 0), 0 ≤ P.pairingIn S i j * P.pairingIn S j i
Tactic: rcases lt_or_ge 0 (P.pairingIn S i j) with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.RootPositive (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : Algebra S R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : IsStrictOrderedRing S
h : P.pairingIn S i j ≤ 0
⊢ P.pairingIn S j i ≤ 0
have rwa : ¬0 < P.pairingIn S j i
Tactic: rwa [← not_lt, ← zero_lt_pairingIn_iff B i j, not_lt]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.RootPositive (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : Algebra S R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : IsStrictOrderedRing S
h : P.pairingIn S i j ≤ 0
rwa : ¬0 < P.pairingIn S j i
⊢ P.pairingIn S j i ≤ 0
have rwa₁ : ¬0 < P.pairingIn S i j
Tactic: rwa [← not_lt, ← zero_lt_pairingIn_iff B i j, not_lt]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.RootPositive (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : Algebra S R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : IsStrictOrderedRing S
h : P.pairingIn S i j ≤ 0
⊢ 0 ≤ P.pairingIn S i j * P.pairingIn S j i
have hn : P.pairingIn S j i ≤ 0
Tactic: have hn : P.pairingIn S j i ≤ 0 := by rwa [← not_lt, ← zero_lt_pairingIn_iff B i j, not_lt]
-- 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
this : range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹
⊢ P.weylGroup.toSubmonoid = Submonoid.closure (range (Equiv.reflection P))
have rw : Eq (α := Submonoid P.Aut) (Subgroup.toSubmonoid (Subgroup.closure (range (Equiv.reflection P))))
  (Submonoid.closure (range (Equiv.reflection P)))
Tactic: rw [weylGroup, Subgroup.closure_toSubmonoid, ← this, union_self]
-- 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
this : range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹
rw :
  Eq (α := Submonoid P.Aut) (Subgroup.toSubmonoid (Subgroup.closure (range (Equiv.reflection P))))
    (Submonoid.closure (range (Equiv.reflection P)))
⊢ P.weylGroup.toSubmonoid = Submonoid.closure (range (Equiv.reflection P))
have rw₁ : Eq (α := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P) ∪ (range (Equiv.reflection P))⁻¹))
  (Submonoid.closure (range (Equiv.reflection P)))
Tactic: rw [weylGroup, Subgroup.closure_toSubmonoid, ← this, union_self]
-- 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
this : range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹
rw :
  Eq (α := Submonoid P.Aut) (Subgroup.toSubmonoid (Subgroup.closure (range (Equiv.reflection P))))
    (Submonoid.closure (range (Equiv.reflection P)))
rw₁ :
  Eq (α := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P) ∪ (range (Equiv.reflection P))⁻¹))
    (Submonoid.closure (range (Equiv.reflection P)))
⊢ P.weylGroup.toSubmonoid = Submonoid.closure (range (Equiv.reflection P))
have rw₂ : Eq (α := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P) ∪ range (Equiv.reflection P)))
  (Submonoid.closure (range (Equiv.reflection P)))
Tactic: rw [weylGroup, Subgroup.closure_toSubmonoid, ← this, union_self]
-- 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
this : range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹
rw :
  Eq (α := Submonoid P.Aut) (Subgroup.toSubmonoid (Subgroup.closure (range (Equiv.reflection P))))
    (Submonoid.closure (range (Equiv.reflection P)))
rw₁ :
  Eq (α := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P) ∪ (range (Equiv.reflection P))⁻¹))
    (Submonoid.closure (range (Equiv.reflection P)))
rw₂ :
  Eq (α := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P) ∪ range (Equiv.reflection P)))
    (Submonoid.closure (range (Equiv.reflection P)))
⊢ P.weylGroup.toSubmonoid = Submonoid.closure (range (Equiv.reflection P))
have rw₃ : Eq (α := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P)))
  (Submonoid.closure (range (Equiv.reflection P)))
Tactic: rw [weylGroup, Subgroup.closure_toSubmonoid, ← this, union_self]
-- 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
⊢ P.weylGroup.toSubmonoid = Submonoid.closure (range (Equiv.reflection P))
have suffices : range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹
Tactic: suffices range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹ by
    rw [weylGroup, Subgroup.closure_toSubmonoid, ← this, union_self]
-- 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
⊢ range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹
have h : ∀ (x : P.Aut), x ∈ range (Equiv.reflection P) ↔ x ∈ (range (Equiv.reflection P))⁻¹
Tactic: ext
-- 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
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 ⋯
⊢ Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) x
have rwa : x ∈ P.weylGroup.toSubmonoid
Tactic: rwa [← weylGroup_toSubmonoid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (hypothesis)
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 ⋯
⊢ pred x hx
have hx' : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) x
Tactic: have hx' : x ∈ Submonoid.closure (range (Equiv.reflection P)) := by rwa [← weylGroup_toSubmonoid]
-- 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
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' x hx'
have mem₁ : ∀ (x : P.Aut) (h : x ∈ range (Equiv.reflection P)), pred' x sorry
Tactic: apply Submonoid.closure_induction
-- 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
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
mem₁ : ∀ (x : P.Aut) (h : x ∈ range (Equiv.reflection P)), pred' x ⋯
one₁ : pred' 1 ⋯
⊢ pred' x hx'
have mul₁ : ∀ (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),
  pred' x hx → pred' y hy → pred' (x * y) sorry
Tactic: apply Submonoid.closure_induction
-- 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
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
⊢ pred' (x * y) ⋯
have 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) sorry
Tactic: rw [← weylGroup_toSubmonoid] at hx hy
Cleared hypotheses: hy, hx', hy'
-- 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
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
have refine : pred 1 sorry
Tactic: refine weylGroup.induction P mem ?_ mul hx
-- 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
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 1 ⋯
have obtain : ∀ (i : ι), pred 1 sorry
Tactic: obtain ⟨i⟩ : Nonempty ι := inferInstance
-- 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
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 : ι
⊢ HPow.hPow (β := ℕ) (Equiv.reflection P i) 2 = 1
have rw : Equiv.reflection P i * Equiv.reflection P i = 1
Tactic: rw [sq, mul_eq_one_iff_inv_eq, Equiv.reflection_inv P i]
-- 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
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
⊢ HPow.hPow (β := ℕ) (Equiv.reflection P i) 2 = 1
have rw₁ : (Equiv.reflection P i)⁻¹ = Equiv.reflection P i
Tactic: rw [sq, mul_eq_one_iff_inv_eq, Equiv.reflection_inv P i]
-- 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
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
⊢ HPow.hPow (β := ℕ) (Equiv.reflection P i) 2 = 1
have rw₂ : Equiv.reflection P i = Equiv.reflection P i
Tactic: rw [sq, mul_eq_one_iff_inv_eq, Equiv.reflection_inv P i]
-- 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
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 : ι
⊢ pred 1 ⋯
have have : ∀ (this : HPow.hPow (β := ℕ) (Equiv.reflection P i) 2 = 1), pred 1 sorry
Tactic: have : (Equiv.reflection P i) ^ 2 = 1 := by
    rw [sq, mul_eq_one_iff_inv_eq, Equiv.reflection_inv P i]
-- 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
⊢ MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup) = Subgroup.closure (range P.reflection)
have refine_1 : range P.reflection ⊆ (↑(MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup)) : Set (M ≃ₗ[R] M))
Tactic: refine (Subgroup.closure_eq_of_le _ ?_ ?_).symm
-- 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
refine_1 : range P.reflection ⊆ (↑(MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup)) : Set (M ≃ₗ[R] M))
⊢ MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup) = Subgroup.closure (range P.reflection)
have refine_2 : MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup) ≤ Subgroup.closure (range P.reflection)
Tactic: refine (Subgroup.closure_eq_of_le _ ?_ ?_).symm
-- 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
i : ι
⊢ P.reflection i ∈ (↑(MonoidHom.range ((Equiv.weightHom P).restrict P.weylGroup)) : Set (M ≃ₗ[R] M))
have refine_1 : ∃ x ∈ P.weylGroup, Equiv.weightEquiv P P x = P.reflection i
Tactic: simp only [MonoidHom.restrict_range, Subgroup.coe_map, Equiv.weightHom_apply, mem_image,
      SetLike.mem_coe]
-- 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
i : ι
⊢ ∃ x ∈ P.weylGroup, Equiv.weightEquiv P P x = P.reflection i
have h : Equiv.reflection P i ∈ P.weylGroup ∧ Equiv.weightEquiv P P (Equiv.reflection P i) = P.reflection i
Tactic: use Equiv.reflection P i
-- 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 (α := 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)
have 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) sorry) :
      M ≃ₗ[R] M)
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 (α := 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)
have refine_2 : Membership.mem (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection)) (P.reflection i)
Tactic: simp only [MonoidHom.restrict_apply, Equiv.weightHom_apply, Equiv.reflection_weightEquiv]
-- 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 (α := 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)
have 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)⁻¹ sorry) :
      M ≃ₗ[R] M)
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 (α := 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)
have refine_2 : Membership.mem (γ := Subgroup (M ≃ₗ[R] M)) (Subgroup.closure (range P.reflection)) (P.reflection i)
Tactic: simp only [Equiv.reflection_inv, MonoidHom.restrict_apply, Equiv.weightHom_apply,
        Equiv.reflection_weightEquiv]