awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)} j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)} k
contra :
  (P.root : (a : ι) → M) i = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ) ((↑m : ℚ) : ℚ)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (0 : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (0 : M)
have hj₁ : 0 < n
Tactic: replace hj : 0 < n := by simpa [hn] using hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)} k
contra :
  (P.root : (a : ι) → M) i = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ) ((↑m : ℚ) : ℚ)
hj : 0 < n
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (0 : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (0 : M)
have hk₁ : 0 < m
Tactic: replace hk : 0 < m := by simpa [hm] using hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j k : ι
contra :
  (P.root : (a : ι) → M) i = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ) ((↑m : ℚ) : ℚ)
hj : 0 < n
hk : 0 < m
⊢ 1 = n + m
have contra₁ : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
  ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) : ℚ)
Tactic: replace contra := congr(f $contra)
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j k : ι
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ) ((↑m : ℚ) : ℚ)
hj : 0 < n
hk : 0 < m
contra :
  Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
    ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) : ℚ)
⊢ 1 = n + m
have rwa : ∀
  (contra :
    Eq (α := ℚ) (1 : ℚ)
      ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) :
        ℚ)),
  1 = n + m
Tactic: rwa [hf i hi, map_add, hn, hm, ← Int.cast_add, ← Int.cast_one, Int.cast_inj] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j k : ι
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ) ((↑m : ℚ) : ℚ)
hj : 0 < n
hk : 0 < m
contra :
  Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
    ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) : ℚ)
rwa :
  ∀
    (contra :
      Eq (α := ℚ) (1 : ℚ)
        ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) :
          ℚ)),
    1 = n + m
⊢ 1 = n + m
have rwa₁ : ∀
  (contra :
    1 =
      HAdd.hAdd (α := ℚ) (β := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ)
        ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ)),
  1 = n + m
Tactic: rwa [hf i hi, map_add, hn, hm, ← Int.cast_add, ← Int.cast_one, Int.cast_inj] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j k : ι
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ) ((↑m : ℚ) : ℚ)
hj : 0 < n
hk : 0 < m
contra :
  Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
    ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) : ℚ)
rwa :
  ∀
    (contra :
      Eq (α := ℚ) (1 : ℚ)
        ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) :
          ℚ)),
    1 = n + m
rwa₁ :
  ∀
    (contra :
      1 =
        HAdd.hAdd (α := ℚ) (β := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ)
          ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ)),
    1 = n + m
⊢ 1 = n + m
have rwa₂ : ∀ (contra : 1 = HAdd.hAdd (α := ℚ) (β := ℚ) ((↑n : ℚ) : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ)),
  1 = n + m
Tactic: rwa [hf i hi, map_add, hn, hm, ← Int.cast_add, ← Int.cast_one, Int.cast_inj] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j k : ι
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ) ((↑m : ℚ) : ℚ)
hj : 0 < n
hk : 0 < m
contra :
  Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
    ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) : ℚ)
rwa :
  ∀
    (contra :
      Eq (α := ℚ) (1 : ℚ)
        ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) :
          ℚ)),
    1 = n + m
rwa₁ :
  ∀
    (contra :
      1 =
        HAdd.hAdd (α := ℚ) (β := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ)
          ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ)),
    1 = n + m
rwa₂ :
  ∀ (contra : 1 = HAdd.hAdd (α := ℚ) (β := ℚ) ((↑n : ℚ) : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ)),
    1 = n + m
⊢ 1 = n + m
have rwa₃ : ∀ (contra : 1 = HAdd.hAdd (α := ℚ) (↑n : ℚ) (↑m : ℚ)), 1 = n + m
Tactic: rwa [hf i hi, map_add, hn, hm, ← Int.cast_add, ← Int.cast_one, Int.cast_inj] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j k : ι
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ) ((↑m : ℚ) : ℚ)
hj : 0 < n
hk : 0 < m
contra :
  Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
    ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) : ℚ)
rwa :
  ∀
    (contra :
      Eq (α := ℚ) (1 : ℚ)
        ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) :
          ℚ)),
    1 = n + m
rwa₁ :
  ∀
    (contra :
      1 =
        HAdd.hAdd (α := ℚ) (β := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ)
          ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ)),
    1 = n + m
rwa₂ :
  ∀ (contra : 1 = HAdd.hAdd (α := ℚ) (β := ℚ) ((↑n : ℚ) : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ)),
    1 = n + m
rwa₃ : ∀ (contra : 1 = HAdd.hAdd (α := ℚ) (↑n : ℚ) (↑m : ℚ)), 1 = n + m
⊢ 1 = n + m
have rwa₄ : ∀ (contra : Eq (α := ℚ) 1 (↑(n + m) : ℚ)), 1 = n + m
Tactic: rwa [hf i hi, map_add, hn, hm, ← Int.cast_add, ← Int.cast_one, Int.cast_inj] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j k : ι
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ) ((↑m : ℚ) : ℚ)
hj : 0 < n
hk : 0 < m
contra :
  Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
    ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) : ℚ)
rwa :
  ∀
    (contra :
      Eq (α := ℚ) (1 : ℚ)
        ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) :
          ℚ)),
    1 = n + m
rwa₁ :
  ∀
    (contra :
      1 =
        HAdd.hAdd (α := ℚ) (β := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ)
          ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ)),
    1 = n + m
rwa₂ :
  ∀ (contra : 1 = HAdd.hAdd (α := ℚ) (β := ℚ) ((↑n : ℚ) : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ)),
    1 = n + m
rwa₃ : ∀ (contra : 1 = HAdd.hAdd (α := ℚ) (↑n : ℚ) (↑m : ℚ)), 1 = n + m
rwa₄ : ∀ (contra : Eq (α := ℚ) 1 (↑(n + m) : ℚ)), 1 = n + m
⊢ 1 = n + m
have rwa₅ : ∀ (contra : Eq (α := ℚ) (↑1 : ℚ) (↑(n + m) : ℚ)), 1 = n + m
Tactic: rwa [hf i hi, map_add, hn, hm, ← Int.cast_add, ← Int.cast_one, Int.cast_inj] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j k : ι
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ) ((↑m : ℚ) : ℚ)
hj : 0 < n
hk : 0 < m
contra :
  Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
    ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) : ℚ)
rwa :
  ∀
    (contra :
      Eq (α := ℚ) (1 : ℚ)
        ((f : (a : M) → ℚ) (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)) :
          ℚ)),
    1 = n + m
rwa₁ :
  ∀
    (contra :
      1 =
        HAdd.hAdd (α := ℚ) (β := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ)
          ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ)),
    1 = n + m
rwa₂ :
  ∀ (contra : 1 = HAdd.hAdd (α := ℚ) (β := ℚ) ((↑n : ℚ) : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ)),
    1 = n + m
rwa₃ : ∀ (contra : 1 = HAdd.hAdd (α := ℚ) (↑n : ℚ) (↑m : ℚ)), 1 = n + m
rwa₄ : ∀ (contra : Eq (α := ℚ) 1 (↑(n + m) : ℚ)), 1 = n + m
rwa₅ : ∀ (contra : Eq (α := ℚ) (↑1 : ℚ) (↑(n + m) : ℚ)), 1 = n + m
⊢ 1 = n + m
have rwa₆ : ∀ (contra : 1 = n + m), 1 = n + m
Tactic: rwa [hf i hi, map_add, hn, hm, ← Int.cast_add, ← Int.cast_one, Int.cast_inj] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
_i : InvolutiveNeg ι := P.indexNeg
h_card : ncard.{u_1} (α := ι) (baseOf (⇑P.root : (a : ι) → M) f) = s.ncard
hsp : ∀ (i : ι), ∃ (z : ℤ), Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ((↑z : ℚ) : ℚ)
i : ι
hi : i ∈ s
j k : ι
contra :
  (P.root : (a : ι) → M) i = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℤ
hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑n : ℚ) : ℚ)
m : ℤ
hm : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) k : M) : ℚ) ((↑m : ℚ) : ℚ)
hj : 0 < n
hk : 0 < m
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (0 : M) ∨
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (0 : M)
have contra₁ : 1 = n + m
Tactic: replace contra : 1 = n + m := by
    replace contra := congr(f $contra)
    rwa [hf i hi, map_add, hn, hm, ← Int.cast_add, ← Int.cast_one, Int.cast_inj] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
s : Set ι
f : M →+ ℚ
hf : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf' : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
this : InvolutiveNeg ι := P.indexNeg
⊢ s = baseOf (⇑P.root : (a : ι) → M) f ↔
    LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s ∧
      ∀ (i : ι),
        Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
            ((P.root : (a : ι) → M) i : M) ∨
          Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
            (-(P.root : (a : ι) → M) i : M)
have refine : s = baseOf (⇑P.root : (a : ι) → M) f →
  LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s ∧
    ∀ (i : ι),
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
          ((P.root : (a : ι) → M) i : M) ∨
        Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
          (-(P.root : (a : ι) → M) i : M)
Tactic: refine ⟨?_, fun ⟨hli, sp⟩ ↦ P.eq_baseOf_of_linearIndepOn_of_mem_or_neg_mem_closure s hli sp f hf⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
⊢ Subset.{u_1} (α := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) (baseOf (⇑P.coroot : (a : ι) → N) g)
have have : ∀ (_i : Fintype ι), Subset.{u_1} (α := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) (baseOf (⇑P.coroot : (a : ι) → N) g)
Tactic: have _i : Fintype ι := Fintype.ofFinite _
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
hfg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)
_i_1 : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root : (a : ι) → M) f
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
⊢ Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    i
have hi₁ : Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)} i
Tactic: obtain ⟨hi, -⟩ := hi
Cleared hypotheses: hi