awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)
obtain :
  ∀ (n : ℤ) (hn : Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) j : M) : ℚ) ((↑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)
⊢ 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)

Tactic:
obtain ⟨n, hn⟩ := hsp j
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 : ℚ) : ℚ)
obtain :
  ∀ (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)
⊢ 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)

Tactic:
obtain ⟨m, hm⟩ := hsp k
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 : ℚ) : ℚ)
⊢ 0 < n

Tactic:
simpa [hn] using hj
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 : ℚ) : ℚ)
⊢ 0 < n

Tactic:
replace hj : 0 < n := by simpa [hn] using hj
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
⊢ 0 < m

Tactic:
simpa [hm] using hk
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
⊢ 0 < m

Tactic:
replace hk : 0 < m := by simpa [hm] using hk
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 (α := ℚ) ((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)
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
rwa₆ rwa₇ rwa₈ rwa₉ : ∀ (contra : 1 = n + m), 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

Premises used: Int.cast_inj, Int.cast_add, map_add, Int.cast_one
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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

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
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 : 1 = n + 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)

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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)

Tactic:
⟨?_, fun ⟨hli, sp⟩ ↦ P.eq_baseOf_of_linearIndepOn_of_mem_or_neg_mem_closure s hli sp f hf⟩

Premises used: _private.0.RootPairing.eq_baseOf_iff.match_1, RootPairing.eq_baseOf_of_linearIndepOn_of_mem_or_neg_mem_closure, RootPairing.root, Iff.intro, IsAddIndecomposable.baseOf, Eq, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
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)
⊢ 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⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
f : M →+ ℚ
hf' : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
this : InvolutiveNeg ι := P.indexNeg
hf :
  ∀ (i : ι),
    Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i →
      Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
i : ι
⊢ Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
f : M →+ ℚ
hf' : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
this : InvolutiveNeg ι := P.indexNeg
hf :
  ∀ (i : ι),
    Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i →
      Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
i : ι
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) (-i) : M) (-(P.root : (a : ι) → M) i : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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
f : M →+ ℚ
hf' : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
this : InvolutiveNeg ι := P.indexNeg
hf :
  ∀ (i : ι),
    Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i →
      Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
⊢ LinearIndepOn.{u_1, u_2, u_3} (ι := ι) R (M := M) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f) ∧
    ∀ (i : ι),
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
          (AddSubmonoid.closure (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
          ((P.root : (a : ι) → M) i : M) ∨
        Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
          (AddSubmonoid.closure (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
          (-(P.root : (a : ι) → M) i : M)

Tactic:
exact ⟨P.linearIndepOn_root_baseOf f hf', fun i ↦
    mem_or_neg_mem_closure_baseOf P.root f i (by simp_all) (by simp)⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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) : ℚ)
have :
  ∀ (_i : Fintype ι), Subset.{u_1} (α := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) (baseOf (⇑P.coroot : (a : ι) → N) g)
⊢ Subset.{u_1} (α := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) (baseOf (⇑P.coroot : (a : ι) → N) g)

Tactic:
have _i : Fintype ι := Fintype.ofFinite _
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)} i

Tactic:
obtain ⟨hi, -⟩ := hi
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
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 ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)} i
⊢ Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    i

Tactic:
aesop