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
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 inr : ∀ (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
-- 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 : ι
⊢ ∃ (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 suffices : ∀ (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)
Tactic: suffices ∀ m ∈ AddSubmonoid.closure (P.root '' b.support),
    ∃ f : ι → ℕ, f.support ⊆ b.support ∧ m = ∑ j ∈ b.support, f j • P.root j by
    rcases b.root_mem_or_neg_mem i with hi | hi
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inl hf'⟩
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inr 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
i : ι
m : M
hm : 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)
have refine_1 : ∀ (x : M) (h : Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)) x),
  ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
Tactic: refine AddSubmonoid.closure_induction ?_ ⟨0, by simp⟩ ?_ hm
-- 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 : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
refine_1 :
  ∀ (x : M) (h : Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)) x),
    ∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      m = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
have refine_2 : ∀ (x y : M)
  (hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x)
  (hy :
    Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y),
  (∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
    (∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
Tactic: refine AddSubmonoid.closure_induction ?_ ⟨0, by simp⟩ ?_ hm
-- 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 : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
x y : M
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y
⊢ (∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
    (∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
      ∃ (f : ι → ℕ),
        Function.support f ⊆ (↑b.support : Set ι) ∧
          x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
have refine_2 : ∀ (f : ι → ℕ) (hf : Function.support f ⊆ (↑b.support : Set ι))
  (hf' : x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)),
  (∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
    ∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
Tactic: ⟨f, hf, 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
i : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
x y : M
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y
f : ι → ℕ
hf : Function.support f ⊆ (↑b.support : Set ι)
hf' : x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
⊢ (∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)) →
    ∃ (f : ι → ℕ),
      Function.support f ⊆ (↑b.support : Set ι) ∧
        x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
have refine_2 : ∀ (g : ι → ℕ) (hg : Function.support g ⊆ (↑b.support : Set ι))
  (hg' : y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M)),
  ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
Tactic: ⟨g, hg, hg'⟩
-- 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 : ι
m : M
hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m
x y : M
hx : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) x
hy : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) y
f : ι → ℕ
hf : Function.support f ⊆ (↑b.support : Set ι)
hf' : x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
g : ι → ℕ
hg : Function.support g ⊆ (↑b.support : Set ι)
hg' : y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (g j) ((P.root : (a : ι) → M) j : M)
⊢ ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      x + y = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
have refine_2 : Function.support (f + g) ⊆ (↑b.support : Set ι)
Tactic: refine ⟨f + g, ?_, by simp [hf', hg', add_smul, Finset.sum_add_distrib]⟩
-- 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 : ι
⊢ ∃ (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 simp_rw : ∃ (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: classical
  simp_rw [← neg_eq_iff_eq_neg]
  suffices ∀ m ∈ AddSubmonoid.closure (P.root '' b.support),
    ∃ f : ι → ℕ, f.support ⊆ b.support ∧ m = ∑ j ∈ b.support, f j • P.root j by
    rcases b.root_mem_or_neg_mem i with hi | hi
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inl hf'⟩
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inr hf'⟩
  intro m hm
  refine AddSubmonoid.closure_induction ?_ ⟨0, by simp⟩ ?_ hm
  · rintro - ⟨j, hj, rfl⟩
    exact ⟨Pi.single j 1, by simpa, by aesop (add simp Pi.single_apply)⟩
  · intro _ _ _ _ ⟨f, hf, hf'⟩ ⟨g, hg, hg'⟩
    refine ⟨f + g, ?_, by simp [hf', hg', add_smul, Finset.sum_add_distrib]⟩
    exact (support_add f g).trans <| union_subset_iff.mpr ⟨hf, hg⟩
-- 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 : ι
simp_rw :
  ∃ (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 simp_rw₁ : ∀ (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)
Tactic: classical
  simp_rw [← neg_eq_iff_eq_neg]
  suffices ∀ m ∈ AddSubmonoid.closure (P.root '' b.support),
    ∃ f : ι → ℕ, f.support ⊆ b.support ∧ m = ∑ j ∈ b.support, f j • P.root j by
    rcases b.root_mem_or_neg_mem i with hi | hi
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inl hf'⟩
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inr hf'⟩
  intro m hm
  refine AddSubmonoid.closure_induction ?_ ⟨0, by simp⟩ ?_ hm
  · rintro - ⟨j, hj, rfl⟩
    exact ⟨Pi.single j 1, by simpa, by aesop (add simp Pi.single_apply)⟩
  · intro _ _ _ _ ⟨f, hf, hf'⟩ ⟨g, hg, hg'⟩
    refine ⟨f + g, ?_, by simp [hf', hg', add_smul, Finset.sum_add_distrib]⟩
    exact (support_add f g).trans <| union_subset_iff.mpr ⟨hf, hg⟩
-- 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 : ι
simp_rw :
  ∃ (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))
simp_rw₁ simp_rw₂ :
  ∀ (m : M)
    (hm :
      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 refine_1 : ∀ (m : M)
  (hm : Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) m)
  (x : M) (h : Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)) x),
  ∃ (f : ι → ℕ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      x = ∑ j ∈ b.support, HSMul.hSMul (β := M) (f j) ((P.root : (a : ι) → M) j : M)
Tactic: classical
  simp_rw [← neg_eq_iff_eq_neg]
  suffices ∀ m ∈ AddSubmonoid.closure (P.root '' b.support),
    ∃ f : ι → ℕ, f.support ⊆ b.support ∧ m = ∑ j ∈ b.support, f j • P.root j by
    rcases b.root_mem_or_neg_mem i with hi | hi
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inl hf'⟩
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inr hf'⟩
  intro m hm
  refine AddSubmonoid.closure_induction ?_ ⟨0, by simp⟩ ?_ hm
  · rintro - ⟨j, hj, rfl⟩
    exact ⟨Pi.single j 1, by simpa, by aesop (add simp Pi.single_apply)⟩
  · intro _ _ _ _ ⟨f, hf, hf'⟩ ⟨g, hg, hg'⟩
    refine ⟨f + g, ?_, by simp [hf', hg', add_smul, Finset.sum_add_distrib]⟩
    exact (support_add f g).trans <| union_subset_iff.mpr ⟨hf, hg⟩
-- 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 : ι
⊢ ∃ (f : ι → ℤ),
    Function.support f ⊆ (↑b.support : Set ι) ∧
      (0 < f ∨ f < 0) ∧
        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 ι) ∧
      (0 < f ∨ f < 0) ∧
        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' | hf'⟩ := b.exists_root_eq_sum_nat_or_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 : ι
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 ι) ∧
        (0 < f ∨ f < 0) ∧
          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 ι) ∧
      (0 < f ∨ f < 0) ∧
        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 : ∀ (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 ι) ∧
      (0 < f ∨ f < 0) ∧
        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' | hf'⟩ := b.exists_root_eq_sum_nat_or_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 : ι
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 ι) ∧
      (0 < f ∨ f < 0) ∧
        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 : ∃ (i : ι), LT.lt (α := ℤ) (0 i) ((Nat.cast ∘ f) i)
Tactic: refine ⟨Nat.cast ∘ f, by simpa, Or.inl <| Pi.lt_def.mpr ⟨fun _ ↦ by simp, ?_⟩, by simp [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
i : ι
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)
⊢ ∃ (i : ι), LT.lt (α := ℤ) (0 i) ((Nat.cast ∘ f) i)
have inl : ∀ (contra : ∀ (i : ι), LE.le (α := ℤ) ((Nat.cast ∘ f) i) (0 i)), False
Tactic: by_contra! 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
i : ι
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)
contra : ∀ (i : ι), LE.le (α := ℤ) ((Nat.cast ∘ f) i) (0 i)
⊢ f = 0
have h : ∀ (i : ι), f i = 0 i
Tactic: ext i
-- 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 : ι
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)
contra : ∀ (i : ι), LE.le (α := ℤ) ((Nat.cast ∘ f) i) (0 i)
⊢ False
have contra₁ : f = 0
Tactic: replace contra : f = 0 := by ext i; simpa using contra i
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
i : ι
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 ι) ∧
      (0 < f ∨ f < 0) ∧
        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 : ∃ (i : ι), LT.lt (α := ℤ) ((-Nat.cast ∘ f) i) (0 i)
Tactic: refine ⟨-Nat.cast ∘ f, by simpa, Or.inr <| Pi.lt_def.mpr ⟨fun _ ↦ by simp, ?_⟩, by simp [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
i : ι
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)
⊢ ∃ (i : ι), LT.lt (α := ℤ) ((-Nat.cast ∘ f) i) (0 i)
have inr : ∀ (contra : ∀ (i : ι), LE.le (α := ℤ) (0 i) ((-Nat.cast ∘ f) i)), False
Tactic: by_contra! 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
i : ι
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)
contra : ∀ (i : ι), LE.le (α := ℤ) (0 i) ((-Nat.cast ∘ f) i)
⊢ f = 0
have h : ∀ (i : ι), f i = 0 i
Tactic: ext i