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 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
ht :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M))
obtain :
  ∀ (j : ι) (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)),
    ∃ (z : ℤ), (↑z : R) * t = 1
⊢ ∃ (z : ℤ), (↑z : R) * t = 1
have obtain₁ : ∀ (j : ι) (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)) (f : ↥b.support → ℤ)
  (hf :
    Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
      (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)),
  ∃ (z : ℤ), (↑z : R) * t = 1
Tactic: classical
  obtain ⟨j, hj⟩ := ht
  obtain ⟨f, hf⟩ : ∃ f : b.support → ℤ, P.coroot i = ∑ i, (t * f i) • P.coroot i := by
    have : P.coroot j ∈ span ℤ (P.coroot '' b.support) := b.coroot_mem_span_int j
    rw [image_eq_range, mem_span_range_iff_exists_fun] at this
    refine this.imp fun f hf ↦ ?_
    simp only [Finset.coe_sort_coe] at hf
    simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf,
      coroot_eq_smul_coroot_iff.mpr hj]
  use f ⟨i, h⟩
  replace hf : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k)
      (t • (linearEquivFunOnFinite R _ _).symm (fun x ↦ (f x : R))) := by
    rw [map_smul, linearCombination_eq_fintype_linearCombination_apply,
      Fintype.linearCombination_apply, hf]
    simp_rw [mul_smul, ← Finset.smul_sum]
  let g : b.support →₀ R := single ⟨i, h⟩ 1
  have hg : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k) g := by simp [g]
  rw [hg] at hf
  have : Injective (linearCombination R fun k : b.support ↦ P.coroot k) := b.linearIndepOn_coroot
  simpa [g, linearEquivFunOnFinite, mul_comm t] using (DFunLike.congr_fun (this hf) ⟨i, h⟩).symm
Cleared hypotheses: ht
-- 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 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
ht :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M))
obtain :
  ∀ (j : ι) (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)),
    ∃ (z : ℤ), (↑z : R) * t = 1
obtain₁ :
  ∀ (j : ι) (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)) (f : ↥b.support → ℤ)
    (hf :
      Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
        (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)),
    ∃ (z : ℤ), (↑z : R) * t = 1
⊢ ∃ (z : ℤ), (↑z : R) * t = 1
have h₁ : ∀ (j : ι) (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)) (f : ↥b.support → ℤ)
  (hf :
    Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
      (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)),
  (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h)) : R) * t = 1
Tactic: classical
  obtain ⟨j, hj⟩ := ht
  obtain ⟨f, hf⟩ : ∃ f : b.support → ℤ, P.coroot i = ∑ i, (t * f i) • P.coroot i := by
    have : P.coroot j ∈ span ℤ (P.coroot '' b.support) := b.coroot_mem_span_int j
    rw [image_eq_range, mem_span_range_iff_exists_fun] at this
    refine this.imp fun f hf ↦ ?_
    simp only [Finset.coe_sort_coe] at hf
    simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf,
      coroot_eq_smul_coroot_iff.mpr hj]
  use f ⟨i, h⟩
  replace hf : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k)
      (t • (linearEquivFunOnFinite R _ _).symm (fun x ↦ (f x : R))) := by
    rw [map_smul, linearCombination_eq_fintype_linearCombination_apply,
      Fintype.linearCombination_apply, hf]
    simp_rw [mul_smul, ← Finset.smul_sum]
  let g : b.support →₀ R := single ⟨i, h⟩ 1
  have hg : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k) g := by simp [g]
  rw [hg] at hf
  have : Injective (linearCombination R fun k : b.support ↦ P.coroot k) := b.linearIndepOn_coroot
  simpa [g, linearEquivFunOnFinite, mul_comm t] using (DFunLike.congr_fun (this hf) ⟨i, h⟩).symm
Cleared hypotheses: ht
-- 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 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
ht :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M))
⊢ t = 1 ∨ t = -1
have obtain : ∀ (z : ℤ) (hz : (↑z : R) * t = 1), t = 1 ∨ t = -1
Tactic: obtain ⟨z, hz⟩ := b.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux i h t ht
-- 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 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
ht :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M))
z : ℤ
hz : (↑z : R) * t = 1
⊢ Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
have obtain : ∀ (j : ι) (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)),
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
Tactic: obtain ⟨j, hj⟩ := ht
Cleared hypotheses: ht
-- 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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
ht :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M))
z : ℤ
hz : (↑z : R) * t = 1
⊢ t = 1 ∨ t = -1
have ht₁ : Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
  (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
Tactic: replace ht : (z : R) • P.coroot i ∈ range P.coroot := by
    obtain ⟨j, hj⟩ := ht
    simpa only [coroot_eq_smul_coroot_iff.mpr hj, smul_smul, hz, one_smul] using mem_range_self j
Cleared hypotheses: ht
-- 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 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
⊢ t = 1 ∨ t = -1
have obtain : ∀ (w : ℤ) (hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1), t = 1 ∨ t = -1
Tactic: obtain ⟨w, hw⟩ := b.flip.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux i h _ ht
-- 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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
⊢ t = 1 ∨ t = -1
have this : HMul.hMul (α := R) (↑z : R) (↑w : R) = 1
Tactic: have : (z : R) * w = 1 := by
    simpa [mul_mul_mul_comm _ t, mul_comm t, mul_comm _ (z : R), hz] using congr_arg₂ (· * ·) hz hw
-- 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 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
this_1 : HMul.hMul (α := R) (↑z : R) (↑w : R) = 1
this : z = 1 ∨ z = -1
⊢ t = 1 ∨ t = -1
have inl : ∀ (hz : (↑1 : R) * t = 1)
  (ht :
    Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑1 : R) ((P.coroot : (a : ι) → N) i : N)))
  (hw : HMul.hMul (α := R) (↑w : R) (↑1 : R) = 1) (this : HMul.hMul (α := R) (↑1 : R) (↑w : R) = 1), t = 1 ∨ t = -1
Tactic: rcases this with rfl | rfl
Cleared hypotheses: z, hz, ht, hw, this_1, 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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
this_1 : HMul.hMul (α := R) (↑z : R) (↑w : R) = 1
this : z = 1 ∨ z = -1
inl :
  ∀ (hz : (↑1 : R) * t = 1)
    (ht :
      Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑1 : R) ((P.coroot : (a : ι) → N) i : N)))
    (hw : HMul.hMul (α := R) (↑w : R) (↑1 : R) = 1) (this : HMul.hMul (α := R) (↑1 : R) (↑w : R) = 1), t = 1 ∨ t = -1
⊢ t = 1 ∨ t = -1
have inr : ∀ (hz : (↑(-1) : R) * t = 1)
  (ht :
    Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(-1) : R) ((P.coroot : (a : ι) → N) i : N)))
  (hw : HMul.hMul (α := R) (↑w : R) (↑(-1) : R) = 1) (this : HMul.hMul (α := R) (↑(-1) : R) (↑w : R) = 1),
  t = 1 ∨ t = -1
Tactic: rcases this with rfl | rfl
Cleared hypotheses: z, hz, ht, hw, this_1, 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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
w : ℤ
hz : (↑1 : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑1 : R) ((P.coroot : (a : ι) → N) i : N))
hw : HMul.hMul (α := R) (↑w : R) (↑1 : R) = 1
this : HMul.hMul (α := R) (↑1 : R) (↑w : R) = 1
⊢ t = 1 ∨ t = -1
have inl : t = 1
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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
w : ℤ
hz : (↑(-1) : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(-1) : R) ((P.coroot : (a : ι) → N) i : N))
hw : HMul.hMul (α := R) (↑w : R) (↑(-1) : R) = 1
this : HMul.hMul (α := R) (↑(-1) : R) (↑w : R) = 1
⊢ t = 1 ∨ t = -1
have inr : t = -1
Tactic: right
-- 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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
this : HMul.hMul (α := R) (↑z : R) (↑w : R) = 1
⊢ z = 1 ∨ z = -1
have this₁ : z * w = 1
Tactic: norm_cast at this
Cleared hypotheses: this
-- 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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
this : z * w = 1
⊢ z = 1 ∨ z = -1
have this₁ : z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
Tactic: rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at this
Cleared hypotheses: 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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
this : z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
⊢ z = 1 ∨ z = -1
have inl : z = 1 → w = 1 → z = 1 ∨ z = -1
Tactic: tauto
Cleared hypotheses: 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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
this : z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
inl : z = 1 → w = 1 → z = 1 ∨ z = -1
⊢ z = 1 ∨ z = -1
have inr : z = -1 → w = -1 → z = 1 ∨ z = -1
Tactic: tauto
Cleared hypotheses: 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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
this : z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
inl : z = 1 → w = 1 → z = 1 ∨ z = -1
inr : z = -1 → w = -1 → z = 1 ∨ z = -1
inl₁ : z = 1 → w = 1 → z = 1 ∨ z = -1
inr₁ : z = -1 → w = -1 → z = 1 ∨ z = -1
⊢ z = 1 ∨ z = -1
have inl₂ : z = 1 → w = 1 → ¬z = 1 → z = -1
Tactic: tauto
Cleared hypotheses: 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
inst_6 : Finite ι
inst_7 : IsAddTorsionFree M
inst_8 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : (↑z : R) * t = 1
ht :
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑z : R) ((P.coroot : (a : ι) → N) i : N))
w : ℤ
hw : HMul.hMul (α := R) (↑w : R) (↑z : R) = 1
this : z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
inl : z = 1 → w = 1 → z = 1 ∨ z = -1
inr : z = -1 → w = -1 → z = 1 ∨ z = -1
inl₁ : z = 1 → w = 1 → z = 1 ∨ z = -1
inr₁ : z = -1 → w = -1 → z = 1 ∨ z = -1
inl₂ : z = 1 → w = 1 → ¬z = 1 → z = -1
⊢ z = 1 ∨ z = -1
have inr₂ : z = -1 → w = -1 → ¬z = 1 → z = -1
Tactic: tauto
Cleared hypotheses: 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 : ι → ℤ
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 ι)
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
⊢ 0 < f ∨ f < 0
have obtain : ∀ (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)),
  0 < f ∨ f < 0
Tactic: obtain ⟨k, hk⟩ := 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 : ι → ℤ
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)
⊢ 0 < f ∨ f < 0
have hf' : f ≠ 0
Tactic: have hf' : f ≠ 0 := by rintro rfl; exact P.ne_zero k <| by simp [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
⊢ 0 < f ∨ f < 0
have inl : ∀
  (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
Tactic: rcases b.root_mem_or_neg_mem k with hk' | 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
inl :
  ∀
    (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
⊢ 0 < f ∨ f < 0
have inr : ∀
  (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
Tactic: rcases b.root_mem_or_neg_mem k with hk' | hk'
-- 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'