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
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
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk :
  ∀ {l : ι} (hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)),
    ∃ (c : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ),
      Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), c x • (↑x : M) : M)
        ((P.root : (a : ι) → M) l : M)
a : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
ha :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), a x • (↑x : M) : M)
    ((P.root : (a : ι) → M) j : M)
b : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
hb :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), b x • (↑x : M) : M)
    ((P.root : (a : ι) → M) k : M)
ri : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x)
    ((P.root : (a : ι) → M) i) ⋯
huv :
  HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) u (Nat.cast ∘ a) +
      HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) v (Nat.cast ∘ b) =
    Pi.single (M := fun (j : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1
q : ℚ
hq : q > 0
hq' : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) q ((P.root : (a : ι) → M) i : M)
⊢ i = j
have hij : ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
Tactic: have hij : ¬ LinearIndependent R ![P.root i, P.root j] := by
    simp_rw [LinearIndependent.pair_iff, not_forall]
    exact ⟨q, -1, by simp [Rat.cast_smul_eq_qsmul, hq'], by simp⟩
-- 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) : ℚ)
_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
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk :
  ∀ {l : ι} (hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)),
    ∃ (c : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ),
      Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), c x • (↑x : M) : M)
        ((P.root : (a : ι) → M) l : M)
a : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
ha :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), a x • (↑x : M) : M)
    ((P.root : (a : ι) → M) j : M)
b : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
hb :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), b x • (↑x : M) : M)
    ((P.root : (a : ι) → M) k : M)
ri : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x)
    ((P.root : (a : ι) → M) i) ⋯
huv :
  HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) u (Nat.cast ∘ a) +
      HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) v (Nat.cast ∘ b) =
    Pi.single (M := fun (j : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1
q : ℚ
hq : q > 0
hq' : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) q ((P.root : (a : ι) → M) i : M)
hij :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ i = j
have inl : ∀ (hij : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)), i = j
Tactic: rcases IsReduced.eq_or_eq_neg i j hij with hij | hij
-- 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) : ℚ)
_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
j : ι
hj :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    j
k : ι
hk :
  Membership.mem (γ := Set ι) {i : ι | LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ)}
    k
contra :
  (P.coroot : (a : ι) → N) i =
    HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) k : N)
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk :
  ∀ {l : ι} (hl : LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) l : N) : ℚ)),
    ∃ (c : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ),
      Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), c x • (↑x : M) : M)
        ((P.root : (a : ι) → M) l : M)
a : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
ha :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), a x • (↑x : M) : M)
    ((P.root : (a : ι) → M) j : M)
b : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℕ
hb :
  Eq.{u_3 + 1} (α := M) (∑ x : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3), b x • (↑x : M) : M)
    ((P.root : (a : ι) → M) k : M)
ri : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) ((⇑P.root : (a : ι) → M) '' s) x)
    ((P.root : (a : ι) → M) i) ⋯
huv :
  HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) u (Nat.cast ∘ a) +
      HSMul.hSMul (β := (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3) → ℚ) v (Nat.cast ∘ b) =
    Pi.single (M := fun (j : (↑((⇑P.root : (a : ι) → M) '' s) : Type u_3)) ↦ ℚ) ri 1
q : ℚ
hq : q > 0
hq' : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) q ((P.root : (a : ι) → M) i : M)
hij :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
inl : ∀ (hij : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)), i = j
⊢ i = j
have inr : ∀ (hij : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)), i = j
Tactic: rcases IsReduced.eq_or_eq_neg i j hij with hij | hij
-- 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (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)
i : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      ((P.coroot : (a : ι) → N) i : N) ∨
    Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      (-(P.coroot : (a : ι) → N) i : N)
have obtain : ∀ (f : Dual ℚ M) (hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)),
  Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      ((P.coroot : (a : ι) → N) i : N) ∨
    Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      (-(P.coroot : (a : ι) → N) i : N)
Tactic: obtain ⟨f, hf'⟩ := exists_dual_forall_apply_eq_one (hli.restrict_scalars' ℚ)
-- 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (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)
i : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      ((P.coroot : (a : ι) → N) i : N) ∨
    Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      (-(P.coroot : (a : ι) → N) i : N)
have hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
Tactic: have hf := P.eq_baseOf_of_linearIndepOn_of_mem_or_neg_mem_closure s hli hsp f hf'
-- 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (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)
i : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      ((P.coroot : (a : ι) → N) i : N) ∨
    Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      (-(P.coroot : (a : ι) → N) i : N)
have hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
Tactic: have hf₀ (i : ι) : f (P.root i) ≠ 0 :=
    AddSubmonoid.apply_ne_zero_of_mem_or_neg_mem_closure P.root (f : M →+ ℚ) s (by simp_all) i
      (P.ne_zero i) (by simp) (hsp i)
-- 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (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)
i_1 : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
i : ι
⊢ ∃ (q : ℚ),
    0 < q ∧
      (↑q : R) =
        HDiv.hDiv (α := R) (β := R) (2 : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) i : M) :
            R)
have refine_1 : 0 <
  HDiv.hDiv (α := ℚ) (β := ℚ) (2 : ℚ)
    ((((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
            ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
          (a : ↥(P.rootSpan ℚ)) → ℚ)
        (P.rootSpanMem ℚ i) :
      ℚ)
Tactic: refine ⟨2 / P.RootFormIn ℚ (P.rootSpanMem ℚ i) (P.rootSpanMem ℚ i), ?_, ?_⟩
-- 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (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)
i_1 : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
i : ι
refine_1 :
  0 <
    HDiv.hDiv (α := ℚ) (β := ℚ) (2 : ℚ)
      ((((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
              ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
            (a : ↥(P.rootSpan ℚ)) → ℚ)
          (P.rootSpanMem ℚ i) :
        ℚ)
⊢ ∃ (q : ℚ),
    0 < q ∧
      (↑q : R) =
        HDiv.hDiv (α := R) (β := R) (2 : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) i : M) :
            R)
have refine_2 : (↑(HDiv.hDiv (α := ℚ) (β := ℚ) (2 : ℚ)
        ((((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
                ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
              (a : ↥(P.rootSpan ℚ)) → ℚ)
            (P.rootSpanMem ℚ i) :
          ℚ)) :
    R) =
  HDiv.hDiv (α := R) (β := R) (2 : R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
Tactic: refine ⟨2 / P.RootFormIn ℚ (P.rootSpanMem ℚ i) (P.rootSpanMem ℚ i), ?_, ?_⟩
-- 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (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)
i_1 : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
i : ι
⊢ 0 <
    HDiv.hDiv (α := ℚ) (β := ℚ) (2 : ℚ)
      ((((P.RootFormIn ℚ : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) (P.rootSpanMem ℚ i) :
              ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
            (a : ↥(P.rootSpan ℚ)) → ℚ)
          (P.rootSpanMem ℚ i) :
        ℚ)
have refine_1 : LT.lt (α := ℚ) (0 : ℚ)
  ((((RootPositiveForm.posForm (P.posRootForm ℚ) : (a : ↥(P.rootSpan ℚ)) → ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ)
            (P.rootSpanMem ℚ i) :
          ↥(P.rootSpan ℚ) →ₗ[ℚ] ℚ) :
        (a : ↥(P.rootSpan ℚ)) → ℚ)
      (P.rootSpanMem ℚ i) :
    ℚ)
Tactic: simp only [Nat.ofNat_pos, div_pos_iff_of_pos_left, ← posRootForm_eq]
-- 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (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)
i : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      ((P.coroot : (a : ι) → N) i : N) ∨
    Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      (-(P.coroot : (a : ι) → N) i : N)
have aux : ∀ (i : ι),
  ∃ (q : ℚ),
    0 < q ∧
      (↑q : R) =
        HDiv.hDiv (α := R) (β := R) (2 : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) i : M) :
            R)
Tactic: have aux (i : ι) : ∃ q : ℚ, 0 < q ∧ q = 2 / P.RootForm (P.root i) (P.root i) := by
    refine ⟨2 / P.RootFormIn ℚ (P.rootSpanMem ℚ i) (P.rootSpanMem ℚ i), ?_, ?_⟩
    · simp only [Nat.ofNat_pos, div_pos_iff_of_pos_left, ← posRootForm_eq]
      exact (P.posRootForm ℚ).zero_lt_posForm_apply_root i (P.rootSpanMem ℚ i).property
    · simp [← P.algebraMap_rootFormIn ℚ (P.rootSpanMem ℚ i) (P.rootSpanMem ℚ i)]
-- 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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (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)
i_1 : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          HDiv.hDiv (α := R) (β := R) (2 : R)
            ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) i : M) :
              R)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
i : ι
⊢ Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)
have obtain : ∀ (q : ℚ) (hq₀ : 0 < q)
  (hq :
    (↑q : R) =
      HDiv.hDiv (α := R) (β := R) (2 : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)),
  Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)
Tactic: obtain ⟨q, hq₀, hq⟩ := aux i