awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
f : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
h : ¬f ≤ 0
⊢ 0 ≤ f
have refine_1 : ∀ (h' : 0 < f), 0 ≤ f
Tactic: rcases b.pos_or_neg_of_sum_smul_root_mem f hf hf₀ with h' | h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
f : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
h : ¬f ≤ 0
refine_1 : ∀ (h' : 0 < f), 0 ≤ f
⊢ 0 ≤ f
have refine_1₁ : ∀ (h' : f < 0), 0 ≤ f
Tactic: rcases b.pos_or_neg_of_sum_smul_root_mem f hf hf₀ with h' | h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
f : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
h : ¬f ≤ 0
h' : f < 0
⊢ 0 ≤ f
have refine_1 : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
f : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
h : ¬f ≤ 0
⊢ ∃ (i : ι), 0 i < f i
have refine_2 : ∀ (h : ∀ (i : ι), f i ≤ 0 i), f ≤ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
f : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) ((-f) j) ((P.root : (a : ι) → M) j : M))
have rw : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
  (-∑ j ∈ b.support, HSMul.hSMul (β := M) ((-f) j) ((P.root : (a : ι) → M) j : M))
Tactic: rw [← neg_mem_range_root_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
f : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
⊢ ¬0 ≤ f ↔ f < 0
have hf₁ : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
  (∑ j ∈ b.support, HSMul.hSMul (β := M) ((-f) j) ((P.root : (a : ι) → M) j : M))
Tactic: replace hf : ∑ j ∈ b.support, (-f) j • P.root j ∈ range P.root := by
    rw [← neg_mem_range_root_iff]; simpa
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) ((-f) j) ((P.root : (a : ι) → M) j : M))
⊢ ¬0 ≤ f ↔ f < 0
have this : ¬-f ≤ 0 ↔ 0 < -f
Tactic: have := b.not_nonpos_iff_pos_of_sum_mem_range_root (-f) hf (by simpa)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
⊢ HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
have inl : ∀ (hi : j ∈ b.support),
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) j : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
Tactic: rcases eq_or_ne j i with rfl | hij
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
inl :
  ∀ (hi : j ∈ b.support),
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) j : M) ∉
      range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
⊢ HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
have inr : ∀ (hij : j ≠ i),
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
Tactic: rcases eq_or_ne j i with rfl | hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
⊢ ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
have this : {i, j} ⊆ b.support
Tactic: have : {i, j} ⊆ b.support := by aesop (add simp Finset.insert_subset_iff)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
this : {i, j} ⊆ b.support
⊢ ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
have rw : HSMul.hSMul (β := M) (f i) ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) =
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
Tactic: rw [← Finset.sum_subset (s₁ := {i, j}) (s₂ := b.support) (by lia) (by aesop),
      Finset.sum_insert (by grind), Finset.sum_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
⊢ HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
have hf : ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
Tactic: have hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j := by
    have : {i, j} ⊆ b.support := by aesop (add simp Finset.insert_subset_iff)
    rw [← Finset.sum_subset (s₁ := {i, j}) (s₂ := b.support) (by lia) (by aesop),
      Finset.sum_insert (by grind), Finset.sum_singleton]
    simp [f, hij, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
hf :
  ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
contra :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
⊢ False
have inr : ∀ (pos : 0 < f), False
Tactic: rcases b.pos_or_neg_of_sum_smul_root_mem f (by rwa [hf]) (by aesop) with pos | neg
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0
hf :
  ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
contra :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
inr : ∀ (pos : 0 < f), False
⊢ False
have inr₁ : ∀ (neg : f < 0), False
Tactic: rcases b.pos_or_neg_of_sum_smul_root_mem f (by rwa [hf]) (by aesop) with pos | neg
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
inr inr₁ inr₂ :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
⊢ HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
have inr₃ : let f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0;
∀
  (hf :
    ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)),
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
Tactic: classical
  let f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
  have hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j := by
    have : {i, j} ⊆ b.support := by aesop (add simp Finset.insert_subset_iff)
    rw [← Finset.sum_subset (s₁ := {i, j}) (s₂ := b.support) (by lia) (by aesop),
      Finset.sum_insert (by grind), Finset.sum_singleton]
    simp [f, hij, sub_eq_add_neg]
  intro contra
  rcases b.pos_or_neg_of_sum_smul_root_mem f (by rwa [hf]) (by aesop) with pos | neg
  · simpa [hij, f] using le_of_lt pos j
  · simpa [hij, f] using le_of_lt neg i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
inr inr₁ inr₂ :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
inr₃ :
  let f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0;
  ∀
    (hf :
      ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)),
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
      range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
inr₄ :
  let f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0;
  ∀
    (hf :
      ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
    (contra :
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))),
    False
⊢ HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
have inr₅ : let f : ι → ℤ := fun (k : ι) ↦ if k = i then 1 else if k = j then -1 else 0;
∀
  (hf :
    ∑ k ∈ b.support, HSMul.hSMul (β := M) (f k) ((P.root : (a : ι) → M) k : M) =
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
  (contra :
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)))
  (pos : 0 < f), False
Tactic: classical
  let f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
  have hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j := by
    have : {i, j} ⊆ b.support := by aesop (add simp Finset.insert_subset_iff)
    rw [← Finset.sum_subset (s₁ := {i, j}) (s₂ := b.support) (by lia) (by aesop),
      Finset.sum_insert (by grind), Finset.sum_singleton]
    simp [f, hij, sub_eq_add_neg]
  intro contra
  rcases b.pos_or_neg_of_sum_smul_root_mem f (by rwa [hf]) (by aesop) with pos | neg
  · simpa [hij, f] using le_of_lt pos j
  · simpa [hij, f] using le_of_lt neg i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : P.IsCrystallographic
inst_8 : Finite ι
i j : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
⊢ P.pairingIn ℤ i j ≤ 0
have by_contra! : ∀ (h : 0 < P.pairingIn ℤ i j), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : P.IsCrystallographic
inst_8 : Finite ι
i j : ↥b.support
hij : i ≠ j
⊢ (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) (↑j : ι)) : ℤ) =
    -P.pairingIn ℤ (↑j : ι) (↑i : ι)
have rw : (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) (↑j : ι)) : ℤ) =
  HSub.hSub (α := ℤ) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) (↑j : ι)) : ℤ)
    (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) (↑j : ι)) : ℤ)
Tactic: rw [← chainTopCoeff_sub_chainBotCoeff (b.linearIndependent_pair_of_ne hij)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
inst_5 : P.IsRootSystem
⊢ LE.le.{u_3} (α := Submodule R M) ⊤
    (span R (range fun (x : (↑(↑b.support : Set ι) : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι)))
have change : LE.le.{u_3} (α := Submodule R M) ⊤
  (span R
    (range.{u_3, u_1 + 1} (ι := ↥b.support) ((⇑P.root : (a : ι) → M) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ b.support))))
Tactic: change ⊤ ≤ span R (range <| P.root ∘ ((↑) : b.support → ι))
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
i : ι
this :
  ∀ (m : M),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M) ∨
        Eq.{u_3 + 1} (α := M) (-(P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M))
have inl : ∀
  (hi :
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
      (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) ((P.root : (a : ι) → M) i : M)),
  ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M) ∨
        Eq.{u_3 + 1} (α := M) (-(P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M))
Tactic: rcases b.root_mem_or_neg_mem i with hi | hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
i : ι
this :
  ∀ (m : M),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
inl :
  ∀
    (hi :
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
        (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) ((P.root : (a : ι) → M) i : M)),
    ∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        (Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
            (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M) ∨
          Eq.{u_3 + 1} (α := M) (-(P.root : (a : ι) → M) i : M)
            (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M))
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M) ∨
        Eq.{u_3 + 1} (α := M) (-(P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M))
have inr : ∀
  (hi :
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
      (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (-(P.root : (a : ι) → M) i : M)),
  ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M) ∨
        Eq.{u_3 + 1} (α := M) (-(P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M))
Tactic: rcases b.root_mem_or_neg_mem i with hi | hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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.Base
i : ι
this :
  ∀ (m : M),
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
    (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) ((P.root : (a : ι) → M) i : M)
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M) ∨
        Eq.{u_3 + 1} (α := M) (-(P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M))
have inl : ∀ (f : ι → ℕ) (hf : Function.support f ⊆ (↑b.support : Set ι))
  (hf' :
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
      (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)),
  ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M) ∨
        Eq.{u_3 + 1} (α := M) (-(P.root : (a : ι) → M) i : M)
          (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M))
Tactic: obtain ⟨f, hf, hf'⟩ := this _ hi