awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
    (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (-(P.root : (a : ι) → M) k : M)
⊢ 0 < f ∨ f < 0
have hk'₁ : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
  (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
Tactic: rw [hk] at hk'
Cleared hypotheses: hk'
-- 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₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
⊢ 0 < f ∨ f < 0
have inl : 0 < f
Tactic: left
-- 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₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
⊢ 0 < f ∨ f < 0
have inr : f < 0
Tactic: right
-- 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₀ : Function.support f ⊆ (↑b.support : Set ι)
this :
  ∀ (f : ι → ℤ)
    (hf :
      Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
    (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M) : M)
hf' : f ≠ 0
hk' :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) ((-f) j) ((P.root : (a : ι) → M) j : M))
have h : Eq.{u_3 + 1} (α := M) (∑ j ∈ b.support, HSMul.hSMul (β := M) ((-f) j) ((P.root : (a : ι) → M) j : M))
  (-∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
Tactic: convert! hk'
-- 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 ι)
⊢ 0 < f ∨ f < 0
have suffices : ∀ (f : ι → ℤ)
  (hf :
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
      (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)))
  (hf₀ : Function.support f ⊆ (↑b.support : Set ι)) (hf' : f ≠ 0), 0 < f
Tactic: suffices ∀ (f : ι → ℤ)
      (hf : ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (P.root '' b.support))
      (hf₀ : f.support ⊆ b.support) (hf' : f ≠ 0), 0 < f by
    obtain ⟨k, hk⟩ := hf
    have hf' : f ≠ 0 := by rintro rfl; exact P.ne_zero k <| by simp [hk]
    rcases b.root_mem_or_neg_mem k with hk' | hk' <;> rw [hk] at hk'
    · left; exact this f hk' hf₀ hf'
    · right; simpa using this (-f) (by convert! hk'; simp) (by simpa only [support_neg]) (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
f_1 : ι → ℤ
hf_1 :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
have suffices : Eq.{u_3 + 1} (α := M) (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
  (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
Tactic: suffices ∑ j, f' j • P.root j = ∑ j ∈ b.support, f j • P.root j by rwa [this]
-- 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_1 : ι → ℤ
hf_1 :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
⊢ Eq.{u_3 + 1} (α := M) (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
have rw : Eq.{u_3 + 1} (α := M) (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
  (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (f (↑i : ι)) ((P.root : (a : ι) → M) (↑i : ι) : M))
Tactic: rw [← b.support.sum_finset_coe]
-- 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_1 : ι → ℤ
hf_1 :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M))
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
⊢ 0 < f
have hf₁ : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
  (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
Tactic: replace hf : ∑ j, f' j • P.root j ∈ AddSubmonoid.closure (P.root '' b.support) := by
    suffices ∑ j, f' j • P.root j = ∑ j ∈ b.support, f j • P.root j by rwa [this]
    rw [← b.support.sum_finset_coe]; rfl
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_1 : ι → ℤ
hf_1 :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
hf :
  Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
⊢ 0 < f
have hf₁ : ∃ (c : (↑(↑b.support : Set ι) : Type u_1) → ℕ),
  Eq.{u_3 + 1} (α := M)
    (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (c i) ((P.root : (a : ι) → M) (↑i : ι) : M))
    (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
Tactic: rw [← span_nat_eq_addSubmonoidClosure, mem_toAddSubmonoid,
    Fintype.mem_span_image_iff_exists_fun] at hf
Cleared hypotheses: hf
-- 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_1 : ι → ℤ
hf_1 :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
hf :
  ∃ (c : (↑(↑b.support : Set ι) : Type u_1) → ℕ),
    Eq.{u_3 + 1} (α := M)
      (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (c i) ((P.root : (a : ι) → M) (↑i : ι) : M))
      (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
⊢ 0 < f
have obtain : ∀ (c : (↑(↑b.support : Set ι) : Type u_1) → ℕ)
  (hc :
    Eq.{u_3 + 1} (α := M)
      (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (c i) ((P.root : (a : ι) → M) (↑i : ι) : M))
      (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))),
  0 < f
Tactic: obtain ⟨c, hc⟩ := hf
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_1 : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc :
  Eq.{u_3 + 1} (α := M)
    (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := M) (c i) ((P.root : (a : ι) → M) (↑i : ι) : M))
    (∑ j : ↥b.support, HSMul.hSMul (β := M) (f' j) ((P.root : (a : ι) → M) (↑j : ι) : M))
⊢ 0 < f
have hc₁ : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
Tactic: replace hc (i : b.support) : c i = f' i := Fintype.linearIndependent_iffₛ.mp
    (b.linearIndepOn_root.restrict_scalars' ℤ) (Int.ofNat ∘ c) f' (by simpa) i
Cleared hypotheses: hc
-- 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_1 : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
⊢ 0 i ≤ f i
have pos : ∀ (hi : i ∈ b.support), 0 i ≤ f i
Tactic: by_cases hi : i ∈ 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
inst_5 : CharZero R
f_1 : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
pos : ∀ (hi : i ∈ b.support), 0 i ≤ f i
⊢ 0 i ≤ f i
have neg : ∀ (hi : i ∉ b.support), 0 i ≤ f i
Tactic: by_cases hi : i ∈ 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
inst_5 : CharZero R
f_1 : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
hi : i ∈ b.support
⊢ 0 i ≤ f i
have pos : 0 ≤ f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i hi)
Tactic: change 0 ≤ f' ⟨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
f_1 : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
hi : i ∉ b.support
⊢ i ∉ Function.support f
have contrapose : ∀ (hi : i ∈ Function.support f), i ∈ b.support
Tactic: contrapose hi
Cleared hypotheses: hi
-- 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_1 : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
i : ι
hi : i ∉ b.support
⊢ 0 i ≤ f i
have hi₁ : i ∉ Function.support f
Tactic: replace hi : i ∉ f.support := by contrapose hi; exact hf₀ hi
Cleared hypotheses: hi
-- 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_1 : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
⊢ 0 < f
have aux : 0 ≤ f
Tactic: have aux : 0 ≤ f := by
    intro i
    by_cases hi : i ∈ b.support
    · change 0 ≤ f' ⟨i, hi⟩
      simp [← hc]
    · replace hi : i ∉ f.support := by contrapose hi; exact hf₀ hi
      simp_all
-- 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_1 : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
aux : 0 ≤ f
⊢ 0 < f
have refine : ∃ (i : ι), 0 i < f i
Tactic: refine Pi.lt_def.mpr ⟨aux, ?_⟩
-- 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_1 : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
aux : 0 ≤ f
⊢ ∃ (i : ι), 0 i < f i
have by_contra! : ∀ (contra : ∀ (i : ι), f i ≤ 0 i), False
Tactic: by_contra! contra
-- 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_1 : ι → ℤ
hf :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ j ∈ b.support, HSMul.hSMul (β := M) (f_1 j) ((P.root : (a : ι) → M) j : M))
hf₀_1 : Function.support f_1 ⊆ (↑b.support : Set ι)
f : ι → ℤ
hf₀ : Function.support f ⊆ (↑b.support : Set ι)
hf' : f ≠ 0
f' : ↥b.support → ℤ := fun (i : ↥b.support) ↦ f (↑i : ι)
c : (↑(↑b.support : Set ι) : Type u_1) → ℕ
hc : ∀ (i : ↥b.support), (↑(c i) : ℤ) = f' i
aux : 0 ≤ f
contra : ∀ (i : ι), f i ≤ 0 i
⊢ False
have contra₁ : f = 0
Tactic: replace contra : f = 0 := le_antisymm contra aux
Cleared hypotheses: contra
-- 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 ι)
⊢ ¬f ≤ 0 ↔ 0 < f
have rw : ¬f ≤ 0 ↔ 0 ≤ f ∧ ∃ (i : ι), 0 i < f i
Tactic: rw [Pi.lt_def]
-- 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 ι)
⊢ ¬f ≤ 0 ↔ 0 ≤ f ∧ ∃ (i : ι), 0 i < f i
have refine_1 : ∀ (h : ¬f ≤ 0), 0 ≤ f
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, ⟨i, hi⟩⟩ contra ↦ by simp [le_antisymm contra h] at 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
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 ι)
refine_1 : ∀ (h : ¬f ≤ 0), 0 ≤ f
⊢ ¬f ≤ 0 ↔ 0 ≤ f ∧ ∃ (i : ι), 0 i < f i
have refine_2 : ∀ (h : ¬f ≤ 0), ∃ (i : ι), 0 i < f i
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, ⟨i, hi⟩⟩ contra ↦ by simp [le_antisymm contra h] at hi⟩