awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseChange (hypothesis)
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
i : ι
⊢ Eq.{u_5 + 1} (α := K)
    ((((LinearMap.restrictScalarsRange₂
                  (Submodule.subtype (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
                  (Submodule.subtype (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
                  (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯ :
                (a : ↥(span K (range (⇑P.root : (a : ι) → M)))) → ↥(span K (range (⇑P.coroot : (a : ι) → N))) →ₗ[K] K)
              (({
                    toFun := fun (i : ι) ↦
                      Subtype.mk (p := fun (x : M) ↦
                        Membership.mem (γ := Submodule K M)
                          (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                        ((P.root : (a : ι) → M) i) ⋯,
                    inj' := ⋯ } :
                  (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))
                i) :
            LinearMap.{u_5, u_5, u_4, u_5} (RingHom.id K)
              (↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) K) :
          (a : ↥(span K (range (⇑P.coroot : (a : ι) → N)))) → K)
        (({
                toFun := fun (i : ι) ↦
                  Subtype.mk (p := fun (x : N) ↦
                    Membership.mem (γ := Submodule K N)
                      (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x)
                    ((P.coroot : (a : ι) → N) i) ⋯,
                inj' := ⋯ } :
              (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N))))
            i :
          ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) :
      K)
    (2 : K)
have this : Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) 2 : L) (2 : L)
Tactic: have : algebraMap K L 2 = 2 := by
      rw [← Int.cast_two (R := K), ← Int.cast_two (R := L), map_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseChange (goal)
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
⊢ Eq.{u_3 + 1} (α := Submodule K ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (span K
      (range.{u_3, u_1 + 1} (ι := ι)
        (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))))
    ⊤
have rw : Eq.{u_3 + 1} (α := Submodule K ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
  (span K
    (range.{u_3, u_1 + 1} (ι := ι)
      (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
        (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))))
  (span K
    {x : ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (↑x : M)})
Tactic: rw [← span_setOf_mem_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseChange (goal)
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
⊢ Eq.{u_3 + 1} (α := Submodule K ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (span K
      (range.{u_3, u_1 + 1} (ι := ι)
        (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))))
    (span K
      {x : ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) |
        Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (↑x : M)})
have e_s : Eq.{u_3 + 1} (α := Set ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
  (range.{u_3, u_1 + 1} (ι := ι)
    (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
      (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M)))))
  {x : ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (↑x : M)}
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseChange (goal)
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
⊢ Eq.{u_3 + 1} (α := Set ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (range.{u_3, u_1 + 1} (ι := ι)
      (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
        (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M)))))
    {x : ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (↑x : M)}
have e_s : ∀ (x : M) (hx : Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x),
  Membership.mem (γ := Set ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
      (range.{u_3, u_1 + 1} (ι := ι)
        (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M)))))
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x hx) ↔
    Membership.mem (γ := Set ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
      {x : ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) |
        Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (↑x : M)}
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x hx)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseChange (goal)
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
⊢ Eq.{u_4 + 1} (α := Submodule K ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
    (span K
      (range.{u_4, u_1 + 1} (ι := ι)
        (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N))))))
    ⊤
have rw : Eq.{u_4 + 1} (α := Submodule K ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
  (span K
    (range.{u_4, u_1 + 1} (ι := ι)
      (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
        (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N))))))
  (span K
    {x : ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) |
      Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (↑x : N)})
Tactic: rw [← span_setOf_mem_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseChange (goal)
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
⊢ Eq.{u_4 + 1} (α := Submodule K ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
    (span K
      (range.{u_4, u_1 + 1} (ι := ι)
        (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N))))))
    (span K
      {x : ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) |
        Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (↑x : N)})
have e_s : Eq.{u_4 + 1} (α := Set ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
  (range.{u_4, u_1 + 1} (ι := ι)
    (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
      (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N)))))
  {x : ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) |
    Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (↑x : N)}
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseChange (goal)
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
⊢ Eq.{u_4 + 1} (α := Set ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
    (range.{u_4, u_1 + 1} (ι := ι)
      (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
        (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N)))))
    {x : ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) |
      Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (↑x : N)}
have e_s : ∀ (x : N)
  (hx : Membership.mem (γ := Submodule K N) (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x),
  Membership.mem (γ := Set ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
      (range.{u_4, u_1 + 1} (ι := ι)
        (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N)))))
      (Subtype.mk (p := fun (x : N) ↦
        Membership.mem (γ := Submodule K N) (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x) x
        hx) ↔
    Membership.mem (γ := Set ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
      {x : ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) |
        Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (↑x : N)}
      (Subtype.mk (p := fun (x : N) ↦
        Membership.mem (γ := Submodule K N) (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x) x hx)
Tactic: ext ⟨x, hx⟩
-- 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
S : Type u_5
inst_6 : LinearOrder S
inst_7 : AddCommGroup S
inst_8 : IsOrderedAddMonoid S
f : M →+ S
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsCrystallographic
hf : ∀ (i : ι), Ne.{u_5 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
_i : InvolutiveNeg ι := P.indexNeg
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) j
hne : i ≠ j
⊢ P.pairingIn ℤ i j ≤ 0
have this : (fun (i j : ι) ↦
    HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
      range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
  i j
Tactic: have := IsAddIndecomposable.pairwise_baseOf_sub_notMem P.root (by simp) f hf hi hj hne
-- 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
S : Type u_5
inst_6 : LinearOrder S
inst_7 : AddCommGroup S
inst_8 : IsOrderedAddMonoid S
f : M →+ S
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsCrystallographic
hf : ∀ (i : ι), Ne.{u_5 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
_i : InvolutiveNeg ι := P.indexNeg
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) j
hne : i ≠ j
this :
  (fun (i j : ι) ↦
      HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) ∉
        range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    i j
⊢ P.pairingIn ℤ i j ≤ 0
have contrapose! : ∀ (this : 0 < P.pairingIn ℤ i j),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
Tactic: contrapose! this
Cleared hypotheses: this
-- 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)
⊢ LinearIndepOn.{u_1, u_6, u_3} (ι := ι) S (M := M) (⇑P.root : (a : ι) → M)
    (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S))
have this : CharZero R
Tactic: have : CharZero R := Algebra.charZero_of_charZero S 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 : 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 : CharZero R
⊢ LinearIndepOn.{u_1, u_6, u_3} (ι := ι) S (M := M) (⇑P.root : (a : ι) → M)
    (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S))
have have : ∀ (this : Fintype ι),
  LinearIndepOn.{u_1, u_6, u_3} (ι := ι) S (M := M) (⇑P.root : (a : ι) → M)
    (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S))
Tactic: have : Fintype ι := 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 : 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 : ι)
⊢ LinearIndepOn.{u_1, u_6, u_3} (ι := ι) S (M := M) (⇑P.root : (a : ι) → M)
    (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S))
have change : LinearIndependent S (M := M) ((⇑M₀.subtype : (a : ↥M₀) → M) ∘ v)
Tactic: change LinearIndependent S (M₀.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 : 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 : ι)
⊢ LinearIndependent S (M := M) ((⇑M₀.subtype : (a : ↥M₀) → M) ∘ v)
have suffices : LinearIndependent S v
Tactic: suffices LinearIndependent S v by
    rwa [LinearMap.linearIndependent_iff_of_disjoint M₀.subtype (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 : 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
⊢ LinearIndependent S v
have obtain : ∀ (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)),
  LinearIndependent S v
Tactic: obtain ⟨B, hB⟩ : ∃ B : P.RootPositiveForm S, B.posForm.toQuadraticMap.PosDef :=
    ⟨P.posRootForm S, by simpa using P.posRootForm_rootFormIn_posDef 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 : 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)
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)
have obtain : ∀ (i : ι)
  (left :
    Membership.mem (γ := Set ι)
      {i : ι | LT.lt.{u_6} (α := S) (0 : S) (((↑f : M →+ S) : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S)} i)
  (hi :
    ∀ (j : ι),
      Membership.mem (γ := Set ι)
          {i : ι | LT.lt.{u_6} (α := S) (0 : S) (((↑f : M →+ S) : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S)} j →
        ∀ (k : ι),
          Membership.mem (γ := Set ι)
              {i : ι | LT.lt.{u_6} (α := S) (0 : S) (((↑f : M →+ S) : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S)}
              k →
            (P.root : (a : ι) → M) i =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : 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)),
  LT.lt.{u_6} (α := S) (0 : S)
    ((f' : (a : ↥M₀) → S)
        (v
          (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ S)) x)
            i sorry)) :
      S)
Tactic: obtain ⟨i, -, hi⟩ := i
Cleared hypotheses: i
-- 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)
⊢ LinearIndependent S v
have 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)
Tactic: have hp (i : baseOf P.root (f : M →+ S)) : 0 < f' (v i) := by obtain ⟨i, -, hi⟩ := i; simpa