awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
⊢ False
have h₁ : 0 ≤ P.pairingIn ℤ k i
Tactic: have h₁ : 0 ≤ P.pairingIn ℤ k i := by
    have := P.root_add_root_mem_of_pairingIn_neg (i := k) (j := i)
    contrapose! this
    exact ⟨this, hki_ne, hki_notMem⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
h₁ : 0 ≤ P.pairingIn ℤ k i
⊢ P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
have a : Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ k i) : R)
  ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ j i + r * 2) : R)
Tactic: apply algebraMap_injective ℤ R
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
h₁ : 0 ≤ P.pairingIn ℤ k i
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ k i) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ j i + r * 2) : R)
have a : (P.coroot' i : (a : M) → R)
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))) =
  P.pairing j i +
    HMul.hMul (α := R) (β := R) ((algebraMap ℤ R : (a : ℤ) → R) r : R) ((algebraMap ℤ R : (a : ℤ) → R) 2 : R)
Tactic: rw [algebraMap_pairingIn, map_add, map_mul, algebraMap_pairingIn, ← root_coroot'_eq_pairing, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
h₁ : 0 ≤ P.pairingIn ℤ k i
⊢ False
have h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
Tactic: have h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2 := by
    apply algebraMap_injective ℤ R
    rw [algebraMap_pairingIn, map_add, map_mul, algebraMap_pairingIn, ← root_coroot'_eq_pairing, hk]
    simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
⊢ P.pairingIn ℤ l i ≤ 0
have this : ∀ (h : 0 < P.pairingIn ℤ l i) (h' : l ≠ i),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M))
Tactic: have := P.root_sub_root_mem_of_pairingIn_pos (i := l) (j := i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
this :
  ∀ (h : 0 < P.pairingIn ℤ l i) (h' : l ≠ i),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M))
⊢ P.pairingIn ℤ l i ≤ 0
have contrapose! : ∀ (this : 0 < P.pairingIn ℤ l i),
  0 < P.pairingIn ℤ l i ∧
    l ≠ i ∧
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
        range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
⊢ False
have h₃ : P.pairingIn ℤ l i ≤ 0
Tactic: have h₃ : P.pairingIn ℤ l i ≤ 0 := by
    have := P.root_sub_root_mem_of_pairingIn_pos (i := l) (j := i)
    contrapose! this
    exact ⟨this, fun x ↦ hli_ne (congrArg P.root x), hli_notMem⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
h₃ : P.pairingIn ℤ l i ≤ 0
⊢ P.pairingIn ℤ l i = P.pairingIn ℤ j i + s * 2
have a : Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ l i) : R)
  ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ j i + s * 2) : R)
Tactic: apply algebraMap_injective ℤ R
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
h₃ : P.pairingIn ℤ l i ≤ 0
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ l i) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ j i + s * 2) : R)
have a : (P.coroot' i : (a : M) → R)
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))) =
  P.pairing j i +
    HMul.hMul (α := R) (β := R) ((algebraMap ℤ R : (a : ℤ) → R) s : R) ((algebraMap ℤ R : (a : ℤ) → R) 2 : R)
Tactic: rw [algebraMap_pairingIn, map_add, map_mul, algebraMap_pairingIn, ← root_coroot'_eq_pairing, hl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
S : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S_def :
  S =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
h₃ : P.pairingIn ℤ l i ≤ 0
⊢ False
have h₄ : P.pairingIn ℤ l i = P.pairingIn ℤ j i + s * 2
Tactic: have h₄ : P.pairingIn ℤ l i = P.pairingIn ℤ j i + s * 2 := by
    apply algebraMap_injective ℤ R
    rw [algebraMap_pairingIn, map_add, map_mul, algebraMap_pairingIn, ← root_coroot'_eq_pairing, hl]
    simp