awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
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
hi :
  Membership.mem.{u_4, u_4} (α := M) (γ := Submodule S M)
    (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) ((P.root : (a : ι) → M) i : M)
hj :
  Membership.mem.{u_4, u_4} (α := M) (γ := Submodule S M)
    (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) ((P.root : (a : ι) → M) j : M)
ri : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) i) hi
rj : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) j) hj
⊢ Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        (HMul.hMul (α := S) (β := S) (2 : S)
          ((((B.posForm :
                      (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) →
                        ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                    ri :
                  LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                    (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
              rj :
            S)) :
      R)
    ((algebraMap S R : (a : S) → R)
        (HMul.hMul (β := S) (P.pairingIn S i j)
          ((((B.posForm :
                      (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) →
                        ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                    rj :
                  LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                    (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
              rj :
            S)) :
      R)

Tactic:
simpa [map_ofNat] using B.toInvariantForm.two_mul_apply_root_root i j

Premises used: map_ofNat, RootPairing.InvariantForm.two_mul_apply_root_root, RootPairing.RootPositiveForm.toInvariantForm
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
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
hi :
  Membership.mem.{u_4, u_4} (α := M) (γ := Submodule S M)
    (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) ((P.root : (a : ι) → M) i : M)
hj :
  Membership.mem.{u_4, u_4} (α := M) (γ := Submodule S M)
    (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) ((P.root : (a : ι) → M) j : M)
ri : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) i) hi
rj : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) j) hj
⊢ HMul.hMul (α := S) (β := S) (2 : S)
      ((((B.posForm :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                ri :
              LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
          rj :
        S) =
    HMul.hMul (β := S) (P.pairingIn S i j)
      ((((B.posForm :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                rj :
              LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
          rj :
        S)

Tactic:
have : 2 * B.posForm ri rj = P.pairingIn S i j * B.posForm rj rj := by
    apply FaithfulSMul.algebraMap_injective S R
    simpa [map_ofNat] using B.toInvariantForm.two_mul_apply_root_root i j
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
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
hi :
  Membership.mem.{u_4, u_4} (α := M) (γ := Submodule S M)
    (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) ((P.root : (a : ι) → M) i : M)
hj :
  Membership.mem.{u_4, u_4} (α := M) (γ := Submodule S M)
    (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) ((P.root : (a : ι) → M) j : M)
ri : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) i) hi
rj : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) j) hj
this :
  HMul.hMul (α := S) (β := S) (2 : S)
      ((((B.posForm :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                ri :
              LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
          rj :
        S) =
    HMul.hMul (β := S) (P.pairingIn S i j)
      ((((B.posForm :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                rj :
              LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
          rj :
        S)
rw rw₁ : 0 < P.pairingIn S i j ↔ 0 < P.pairingIn S i j
⊢ 0 <
      HMul.hMul (β := S) (P.pairingIn S i j)
        ((((B.posForm :
                    (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                  rj :
                LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                  (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
            rj :
          S) ↔
    0 < P.pairingIn S i j

Tactic:
rw [mul_pos_iff_of_pos_right (B.zero_lt_posForm_apply_root j)]

Premises used: Set.mem_range_self, RootPairing.RootPositiveForm.zero_lt_posForm_apply_root, mul_pos_iff_of_pos_right, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
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
dsimp : 0 ≤ P.pairingIn S i j * P.pairingIn S j i
⊢ 0 ≤ P.coxeterWeightIn S i j

Tactic:
dsimp [coxeterWeightIn]

Premises used: RootPairing.coxeterWeightIn
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
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
inr : ∀ (h : P.pairingIn S i j ≤ 0), 0 ≤ P.pairingIn S i j * P.pairingIn S j i
⊢ 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

Premises used: RootPairing.pairingIn, lt_or_ge, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
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 : 0 < P.pairingIn S i j
⊢ 0 ≤ P.pairingIn S i j * P.pairingIn S j i

Tactic:
le_of_lt <| mul_pos h ((zero_lt_pairingIn_iff B i j).mp h)

Premises used: le_of_lt, RootPairing.zero_lt_pairingIn_iff, mul_pos, Iff.mp
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
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 : 0 < P.pairingIn S i j
⊢ 0 ≤ P.pairingIn S i j * P.pairingIn S j i

Tactic:
exact le_of_lt <| mul_pos h ((zero_lt_pairingIn_iff B i j).mp h)

Premises used: le_of_lt, RootPairing.zero_lt_pairingIn_iff, mul_pos, Iff.mp
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
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
rwa₁ : ¬0 < P.pairingIn S i j
rwa₂ rwa₃ rwa₄ rwa₅ : P.pairingIn S i j ≤ 0
⊢ P.pairingIn S j i ≤ 0

Tactic:
rwa [← not_lt, ← zero_lt_pairingIn_iff B i j, not_lt]

Premises used: RootPairing.zero_lt_pairingIn_iff, not_lt
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
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

Tactic:
have hn : P.pairingIn S j i ≤ 0 := by rwa [← not_lt, ← zero_lt_pairingIn_iff B i j, not_lt]
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
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
hn : P.pairingIn S j i ≤ 0
⊢ 0 ≤ P.pairingIn S i j * P.pairingIn S j i

Tactic:
mul_nonneg_of_nonpos_of_nonpos h hn

Premises used: mul_nonneg_of_nonpos_of_nonpos
-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
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
hn : P.pairingIn S j i ≤ 0
⊢ 0 ≤ P.pairingIn S i j * P.pairingIn S j i

Tactic:
exact mul_nonneg_of_nonpos_of_nonpos h hn

Premises used: mul_nonneg_of_nonpos_of_nonpos
-- 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

Tactic:
Subgroup.subset_closure <| mem_range_self i

Premises used: Set.mem_range_self, Set.Mem, 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
i : ι
m : M
⊢ ofIdx P i • m = Equiv.reflection P i • m

Tactic:
rfl

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
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)))
rw₃ rw₄ :
  Eq (α := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P)))
    (Submonoid.closure (range (Equiv.reflection P)))
⊢ P.weylGroup.toSubmonoid = Submonoid.closure (range (Equiv.reflection P))

Tactic:
rw [weylGroup, Subgroup.closure_toSubmonoid, ← this, union_self]

Premises used: RootPairing.weylGroup, Subgroup.closure_toSubmonoid, Set.union_self
-- 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
suffices : range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹
⊢ P.weylGroup.toSubmonoid = Submonoid.closure (range (Equiv.reflection P))

Tactic:
suffices range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹ by
    rw [weylGroup, Subgroup.closure_toSubmonoid, ← this, union_self]
-- 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
h : ∀ (x : P.Aut), x ∈ range (Equiv.reflection P) ↔ x ∈ (range (Equiv.reflection P))⁻¹
⊢ range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹

Tactic:
ext
-- 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
x : P.Aut
⊢ x ∈ range (Equiv.reflection P) ↔ x ∈ (range (Equiv.reflection P))⁻¹

Tactic:
simp [← inv_eq_iff_eq_inv]

Premises used: inv_eq_iff_eq_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
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
g : P.Aut
hg : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) g
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) g
⊢ g ∈ P.weylGroup.toSubmonoid

Tactic:
rwa [weylGroup_toSubmonoid]

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 : P.Aut
hx : x ∈ P.weylGroup
let : pred x hx
⊢ pred x hx

Tactic:
let pred' : (g : Aut P) → g ∈ Submonoid.closure (range (Equiv.reflection P)) → Prop :=
    fun g hg ↦ pred g <| by change g ∈ P.weylGroup.toSubmonoid; rwa [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 : 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 ⋯
rwa rwa₁ rwa₂ rwa₃ : x ∈ P.weylGroup.toSubmonoid
⊢ Membership.mem (γ := Submonoid P.Aut) (Submonoid.closure (range (Equiv.reflection P))) x

Tactic:
rwa [← weylGroup_toSubmonoid]

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

Tactic:
have hx' : x ∈ Submonoid.closure (range (Equiv.reflection P)) := by rwa [← 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 : 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
suffices : pred' x hx'
⊢ pred x hx

Tactic:
suffices pred' x hx' from this
-- 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
mem₁ : ∀ (x : P.Aut) (h : x ∈ range (Equiv.reflection P)), pred' x ⋯
one₁ : pred' 1 ⋯
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) ⋯
⊢ pred' x hx'

Tactic:
apply Submonoid.closure_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
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
i : ι
⊢ pred' (Equiv.reflection P i) ⋯

Tactic:
mem 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
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
i : ι
⊢ pred' (Equiv.reflection P i) ⋯

Tactic:
exact mem i