awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i j : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
this :
  ∀ (i j : ι),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)) →
      Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M) →
        Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
⊢ Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) i : M) ↔
    Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) j : M)
have aux : Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M) → Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
Tactic: have aux := this j i (by rwa [add_comm])
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i j : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
this :
  ∀ (i j : ι),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)) →
      Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M) →
        Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
aux :
  Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M) →
    Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
⊢ Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) i : M) ↔
    Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) j : M)
have inl : ∀ (aux : ((P.root : (a : ι) → M) j : M) ∉ q),
  Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) i : M) ↔
    Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) j : M)
Tactic: tauto
Cleared hypotheses: aux
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i j : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
this :
  ∀ (i j : ι),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)) →
      Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M) →
        Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
aux :
  Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M) →
    Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
inl :
  ∀ (aux : ((P.root : (a : ι) → M) j : M) ∉ q),
    Membership.mem («α» := M)
        (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
        ((P.root : (a : ι) → M) i : M) ↔
      Membership.mem («α» := M)
        (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
        ((P.root : (a : ι) → M) j : M)
⊢ Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) i : M) ↔
    Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) j : M)
have inr : ∀ (aux : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)),
  Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) i : M) ↔
    Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) j : M)
Tactic: tauto
Cleared hypotheses: aux
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i j : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
⊢ Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) i : M) ↔
    Membership.mem («α» := M)
      (↑(Subtype.mk (p := fun (x : Submodule K M) ↦ x ∈ P.invtRootSubmodule) q hq_1) : Submodule K M)
      ((P.root : (a : ι) → M) j : M)
have suffices : ∀ (i j : ι),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)) →
    Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M) →
      Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
Tactic: suffices ∀ i j, P.root i + P.root j ∈ range P.root → P.root i ∈ q → P.root j ∈ q by
    have aux := this j i (by rwa [add_comm]); tauto
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
have inl : ∀ (hij₀ : P.pairing i j = 0), Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
Tactic: rcases eq_or_ne (P.pairing i j) 0 with hij₀ | hij₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
inl : ∀ (hij₀ : P.pairing i j = 0), Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
have inr : ∀ (hij₀ : P.pairing i j ≠ 0), Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
Tactic: rcases eq_or_ne (P.pairing i j) 0 with hij₀ | hij₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
⊢ P.pairing i k ≠ 0
have rw : ¬Eq.{u_5 + 1} («α» := K)
    ((((P.toLinearMap : (a : M) → N →ₗ[K] K)
              (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)) :
            N →ₗ[K] K) :
          (a : N) → K)
        ((P.coroot : (a : ι) → N) i : N) :
      K)
    (0 : K)
Tactic: rw [ne_eq, P.pairing_eq_zero_iff, ← root_coroot_eq_pairing, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
have hik : P.pairing i k ≠ 0
Tactic: have hik : P.pairing i k ≠ 0 := by
      rw [ne_eq, P.pairing_eq_zero_iff, ← root_coroot_eq_pairing, hk]
      simpa [P.pairing_eq_zero_iff.mp hij₀] using two_ne_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
hik : P.pairing i k ≠ 0
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
have inl : Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)
Tactic: suffices P.root k ∈ q from (q.add_mem_iff_right hi).mp <| hk ▸ this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
hik : P.pairing i k ≠ 0
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)
have hq₁ : HSub.hSub («α» := M) ((P.root : (a : ι) → M) i : M)
    (HSMul.hSMul (β := M) (P.pairing i k) ((P.root : (a : ι) → M) k : M)) ∈
  q
Tactic: replace hq : P.root i - P.pairing i k • P.root k ∈ q := by
      simpa [reflection_apply_root] using hq k hi
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
hik : P.pairing i k ≠ 0
hq :
  HSub.hSub («α» := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairing i k) ((P.root : (a : ι) → M) k : M)) ∈
    q
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)
have inl : ∀ (hq : HSMul.hSMul (β := M) (P.pairing i k) ((P.root : (a : ι) → M) k : M) ∈ q),
  Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)
Tactic: rwa [q.sub_mem_iff_right hi, q.smul_mem_iff hik] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j = 0
hik : P.pairing i k ≠ 0
hq :
  HSub.hSub («α» := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairing i k) ((P.root : (a : ι) → M) k : M)) ∈
    q
inl :
  ∀ (hq : HSMul.hSMul (β := M) (P.pairing i k) ((P.root : (a : ι) → M) k : M) ∈ q),
    Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)
have inl₁ : ∀ (hq : Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)),
  Membership.mem («α» := M) q ((P.root : (a : ι) → M) k : M)
Tactic: rwa [q.sub_mem_iff_right hi, q.smul_mem_iff hik] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
hq : ∀ (i : ι), q ∈ Module.End.invtSubmodule (↑(P.reflection i) : M →ₗ[K] M)
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j ≠ 0
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
have hq₁ : HSub.hSub («α» := M) ((P.root : (a : ι) → M) i : M)
    (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) ∈
  q
Tactic: replace hq : P.root i - P.pairing i j • P.root j ∈ q := by
      simpa [reflection_apply_root] using hq j hi
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j ≠ 0
hq :
  HSub.hSub («α» := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) ∈
    q
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
have inr : ∀ (hq : HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) ∈ q),
  Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
Tactic: rwa [q.sub_mem_iff_right hi, q.smul_mem_iff hij₀] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
i_1 j_1 : ι
K : Type u_5
inst_2 : Field K
inst_3 : NeZero.{u_5} (R := K) 2
inst_4 : Module K M
inst_5 : Module K N
P : RootPairing ι K M N
hij :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i_1 : M) ((P.root : (a : ι) → M) j_1 : M))
q : Submodule K M
hq_1 : q ∈ P.invtRootSubmodule
i j k : ι
hk :
  (P.root : (a : ι) → M) k = HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hi : Membership.mem («α» := M) q ((P.root : (a : ι) → M) i : M)
hij₀ : P.pairing i j ≠ 0
hq :
  HSub.hSub («α» := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) ∈
    q
inr :
  ∀ (hq : HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) ∈ q),
    Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
⊢ Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
have inr₁ : ∀ (hq : Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)),
  Membership.mem («α» := M) q ((P.root : (a : ι) → M) j : M)
Tactic: rwa [q.sub_mem_iff_right hi, q.smul_mem_iff hij₀] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
B : P.InvariantForm
i j : ι
h : P.pairingIn ℤ i j ≠ 0
⊢ Eq.{u_2 + 1} («α» := R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) ∨
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) =
        HMul.hMul («α» := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R) ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) =
          HMul.hMul («α» := R) (β := R) (3 : R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) j : M) :
              R) ∨
        (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) =
            HMul.hMul («α» := R) (β := R) (2 : R)
              ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                  ((P.root : (a : ι) → M) i : M) :
                R) ∨
          (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) =
            HMul.hMul («α» := R) (β := R) (3 : R)
              ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                  ((P.root : (a : ι) → M) i : M) :
                R)
have h₁ : Membership.mem (γ := Set (ℤ × ℤ))
  {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
  (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
Tactic: have h₁ := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i j