awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : IsDomain R
S : Type u_6
inst_7 : LinearOrder S
inst_8 : CommRing S
inst_9 : IsStrictOrderedRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsValuedIn S
inst_17 : P.IsCrystallographic
f : Dual S M
hf : ∀ (i : ι), Ne.{u_6 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
this_1 : CharZero R
this : Fintype ι
M₀ : Submodule S M := span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) → ↥M₀ :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦ P.rootSpanMem S (↑i : ι)
f' : Dual.{u_6, u_3} S ↥M₀ := f ∘ₗ M₀.subtype
B : RootPositiveForm S P
hB :
  QuadraticMap.PosDef (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (LinearMap.BilinMap.toQuadraticMap B.posForm)
hp :
  ∀ (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)),
    LT.lt.{u_6} (α := S) (0 : S) ((f' : (a : ↥M₀) → S) (v i) : S)
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) i
j : ι
hj : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) j
hij :
  Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) i hi ≠
    Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) j hj
⊢ LE.le.{u_6} (α := S)
    ((((B.posForm : (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              (v
                (Subtype.mk (p := fun (x : ι) ↦
                  Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x) i hi)) :
            LinearMap.{u_6, u_6, u_3, u_6} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        (v
          (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x)
            j hj)) :
      S)
    (0 : S)
have rw : LE.le (α := S)
  ((algebraMap ℤ S : (a : ℤ) → S)
      (P.pairingIn ℤ
        (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x)
              i hi) :
          ι)
        (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x)
              j hj) :
          ι)) :
    S)
  (0 : S)
Tactic: rw [B.posForm_apply_root_root_le_zero_iff, ← P.algebraMap_pairingIn' S ℤ]
-- 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 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : IsDomain R
S : Type u_6
inst_7 : LinearOrder S
inst_8 : CommRing S
inst_9 : IsStrictOrderedRing S
inst_10 : Algebra S R
inst_11 : FaithfulSMul S R
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsValuedIn S
inst_17 : P.IsCrystallographic
f : Dual S M
hf : ∀ (i : ι), Ne.{u_6 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
this_1 : CharZero R
this : Fintype ι
M₀ : Submodule S M := span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) → ↥M₀ :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦ P.rootSpanMem S (↑i : ι)
f' : Dual.{u_6, u_3} S ↥M₀ := f ∘ₗ M₀.subtype
B : RootPositiveForm S P
hB :
  QuadraticMap.PosDef (M := ↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (LinearMap.BilinMap.toQuadraticMap B.posForm)
hp :
  ∀ (i : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)),
    LT.lt.{u_6} (α := S) (0 : S) ((f' : (a : ↥M₀) → S) (v i) : S)
⊢ LinearIndependent S v
have hn : Pairwise fun (i j : (↑(baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) : Type u_1)) ↦
  LE.le.{u_6} (α := S)
    ((((B.posForm : (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              (v i) :
            LinearMap.{u_6, u_6, u_3, u_6} (RingHom.id S)
              (↥(span S (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
          (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
        (v j) :
      S)
    (0 : S)
Tactic: have hn : Pairwise fun (i j : baseOf P.root (f : M →+ S)) ↦ B.posForm (v i) (v j) ≤ 0 := by
    rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
    rw [B.posForm_apply_root_root_le_zero_iff, ← P.algebraMap_pairingIn' S ℤ]
    simpa using P.baseOf_pairwise_pairing_le_zero _ hf (by simpa) (by simpa) (by aesop : i ≠ j)
-- 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 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
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)
⊢ LE.le.{u_3} (α := Submodule R M) ⊤ (span R (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι)))
have rw : range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M) ⊆
  (↑(span R (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)) : Set M)
Tactic: rw [← IsRootSystem.span_root_eq_top (P := P), span_le, ← span_span_of_tower (R := ℤ)]
-- 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 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
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 : ι
⊢ Membership.mem (α := M)
    (↑(span R (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)) : Set M)
    ((P.root : (a : ι) → M) i : M)
have a : Membership.mem (α := M) (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)
  ((P.root : (a : ι) → M) i : M)
Tactic: apply subset_span
-- 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 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
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 : ι
⊢ Membership.mem (α := M) (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)
    ((P.root : (a : ι) → M) i : M)
have a : ∀
  (hi :
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
      ((P.root : (a : ι) → M) i : M)),
  Membership.mem (α := M) (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)
    ((P.root : (a : ι) → M) i : M)
Tactic: rcases hsp i with hi | hi
-- 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 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
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 : ι
a :
  ∀
    (hi :
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M)),
    Membership.mem (α := M) (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)
      ((P.root : (a : ι) → M) i : M)
⊢ Membership.mem (α := M) (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)
    ((P.root : (a : ι) → M) i : M)
have a₁ : ∀
  (hi :
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
      (-(P.root : (a : ι) → M) i : M)),
  Membership.mem (α := M) (↑(span ℤ (range fun (x : (↑s : Type u_1)) ↦ (P.root : (a : ι) → M) (↑x : ι))) : Set M)
    ((P.root : (a : ι) → M) i : M)
Tactic: rcases hsp i with hi | hi
-- 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 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
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)
b : Basis.{u_1, u_2, u_3} (↑s : Type u_1) R M := Basis.mk hli ⋯
⊢ s.ncard = finrank R M
have have : ∀ (_i : Fintype (↑s : Type u_1)), s.ncard = finrank R M
Tactic: have _i : Fintype s := Fintype.ofFinite s
-- 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 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsRootSystem
inst_7 : Nontrivial R
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)
b : Basis.{u_1, u_2, u_3} (↑s : Type u_1) R M := Basis.mk hli ⋯
_i : Fintype (↑s : Type u_1)
⊢ s.ncard = finrank R M
have rw : sorry.toFinset (s := s).card = finrank R M
Tactic: rw [ncard_eq_toFinset_card]
-- 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
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this : InvolutiveNeg ι := P.indexNeg
⊢ LinearIndepOn.{u_1, u_2, u_3} (ι := ι) R (M := M) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)
have have : ∀ (this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)),
  LinearIndepOn.{u_1, u_2, u_3} (ι := ι) R (M := M) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)
Tactic: have : Fintype (baseOf P.root f) := Fintype.ofFinite _
-- 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
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
⊢ LinearIndepOn.{u_1, u_2, u_3} (ι := ι) R (M := M) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)
have change : LinearIndependent R (M := M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v)
Tactic: change LinearIndependent R ((P.rootSpan ℚ).subtype ∘ v)
-- 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
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
this : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) (span ℚ (range (P.rootSpanMem ℚ)))
⊢ Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) ⊤
have rw : LE.le (α := Submodule ℚ M) (map (M := ↥(P.rootSpan ℚ)) (Submodule.subtype (P.rootSpan ℚ)) ⊤)
  (span ℚ
    (comp (β := ↥(P.rootSpan ℚ)) (⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) (P.rootSpanMem ℚ) ''
      univ))
Tactic: rw [this, eq_top_iff, ← (P.rootSpan ℚ).subtype.map_le_map_iff' (by simp), map_span,
        ← image_univ, ← image_comp]
-- 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
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
⊢ Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) ⊤
have suffices : Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) (span ℚ (range (P.rootSpanMem ℚ)))
Tactic: suffices span ℚ (range v) = span ℚ (range (P.rootSpanMem ℚ)) by
      rw [this, eq_top_iff, ← (P.rootSpan ℚ).subtype.map_le_map_iff' (by simp), map_span,
        ← image_univ, ← image_comp]
      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
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
⊢ Eq (α := Submodule ℚ ↥(P.rootSpan ℚ)) (span ℚ (range v)) (span ℚ (range (P.rootSpanMem ℚ)))
have apply : range (P.rootSpanMem ℚ) ⊆ (↑(span ℚ (range v)) : Set ↥(P.rootSpan ℚ))
Tactic: apply le_antisymm (span_mono fun x i ↦ by aesop) (span_le.mpr ?_)
-- 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
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
i : ι
this :
  Membership.mem (γ := Submodule ℚ M)
    (span ℚ (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
    (↑(P.rootSpanMem ℚ i) : M)
⊢ P.rootSpanMem ℚ i ∈ (↑(span ℚ (range v)) : Set ↥(P.rootSpan ℚ))
have rw : Membership.mem (α := M) (γ := Submodule ℚ M)
  (span ℚ ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v '' univ))
  ((Submodule.subtype (P.rootSpan ℚ) : (a : ↥(P.rootSpan ℚ)) → M) (P.rootSpanMem ℚ i) : M)
Tactic: rw [← (injective_subtype (P.rootSpan ℚ)).mem_set_image, ← map_coe, SetLike.mem_coe, map_span,
        ← image_univ, ← image_comp]
-- 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
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
i : ι
this :
  Membership.mem (γ := Submodule ℚ M)
    (span ℚ (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
    (↑(P.rootSpanMem ℚ i) : M)
⊢ Membership.mem (α := M) (γ := Submodule ℚ M)
    (span ℚ ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v '' univ))
    ((Submodule.subtype (P.rootSpan ℚ) : (a : ↥(P.rootSpan ℚ)) → M) (P.rootSpanMem ℚ i) : M)
have h : Eq (α := Set M) ((⇑(Submodule.subtype (P.rootSpan ℚ)) : (a : ↥(P.rootSpan ℚ)) → M) ∘ v '' univ)
  (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f))
Tactic: convert! this
-- 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
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
i : ι
⊢ P.rootSpanMem ℚ i ∈ (↑(span ℚ (range v)) : Set ↥(P.rootSpan ℚ))
have suffices : Membership.mem (γ := Submodule ℚ M)
  (span ℚ (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
  (↑(P.rootSpanMem ℚ i) : M)
Tactic: suffices (P.rootSpanMem ℚ i : M) ∈ span ℚ (P.root '' baseOf P.root f) by
      rw [← (injective_subtype (P.rootSpan ℚ)).mem_set_image, ← map_coe, SetLike.mem_coe, map_span,
        ← image_univ, ← image_comp]
      convert! this
      aesop
-- 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
f : M →+ ℚ
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this_1 : InvolutiveNeg ι := P.indexNeg
this : Fintype (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)
v : (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) → ↥(P.rootSpan ℚ) :=
  fun (i : (↑(baseOf (⇑P.root : (a : ι) → M) f) : Type u_1)) ↦ P.rootSpanMem ℚ (↑i : ι)
i : ι
⊢ Membership.mem (γ := Submodule ℚ M)
    (span ℚ (image.{u_1, u_3} (α := ι) (⇑P.root : (a : ι) → M) (baseOf (⇑P.root : (a : ι) → M) f)))
    (↑(P.rootSpanMem ℚ i) : M)
have rw : Membership.mem (γ := Submodule ℚ M)
  (span ℚ (↑(AddSubgroup.closure (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) : Set M))
  (↑(P.rootSpanMem ℚ i) : M)
Tactic: rw [← span_span_of_tower ℤ, ← Submodule.coe_toAddSubgroup, span_int_eq_addSubgroupClosure,
      AddSubgroup.closure_image_isAddIndecomposable_baseOf P.root (by simp) f (by simpa)]