awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
inst_9 : Module S M
inst_10 : IsScalarTower S R M
i j k l : ι
x y : S
h :
  (P.root : (a : ι) → M) k =
    HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) l : M)
⊢ P.pairingIn S k j = x • P.pairingIn S i j + y • P.pairingIn S l j
have a : Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S k j) : R)
  ((algebraMap S R : (a : S) → R) (x • P.pairingIn S i j + y • P.pairingIn S l j) : R)
Tactic: apply FaithfulSMul.algebraMap_injective S R
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
inst_9 : Module S M
inst_10 : IsScalarTower S R M
i j k l : ι
x y : S
h :
  (P.root : (a : ι) → M) k =
    HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) l : M)
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) (P.pairingIn S k j) : R)
    ((algebraMap S R : (a : S) → R) (x • P.pairingIn S i j + y • P.pairingIn S l j) : R)
have h₁ : (P.root : (a : ι) → M) k =
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M) ((algebraMap S R : (a : S) → R) x : R) ((P.root : (a : ι) → M) i : M) +
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M) ((algebraMap S R : (a : S) → R) y : R) ((P.root : (a : ι) → M) l : M)
Tactic: replace h : P.root k = (algebraMap S R x) • P.root i + (algebraMap S R y) • P.root l := by simpa
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
i j k : ι
⊢ P.pairingIn S j ((P.reflectionPerm i : (a : ι) → ι) k) = P.pairingIn S ((P.reflectionPerm i : (a : ι) → ι) j) k
have simp : P.pairing j ((P.reflectionPerm i : (a : ι) → ι) k) = P.pairing ((P.reflectionPerm i : (a : ι) → ι) j) k
Tactic: simp only [← (FaithfulSMul.algebraMap_injective S R).eq_iff, algebraMap_pairingIn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
T : Type u_7
inst_7 : CommRing T
inst_8 : Algebra T S
inst_9 : Algebra T R
inst_10 : IsScalarTower T S R
inst_11 : P.IsValuedIn T
i j : ι
⊢ ∃ (s : S), (algebraMap S R : (a : S) → R) s = P.pairing i j
have h : (algebraMap S R : (a : S) → R) ((algebraMap T S : (a : T) → S) (P.pairingIn T i j) : S) = P.pairing i j
Tactic: use algebraMap T S (P.pairingIn T i j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
T : Type u_7
inst_7 : CommRing T
inst_8 : Algebra T S
inst_9 : Algebra T R
inst_10 : IsScalarTower T S R
inst_11 : P.IsValuedIn T
inst_12 : P.IsValuedIn S
inst_13 : FaithfulSMul S R
i j : ι
⊢ (algebraMap T S : (a : T) → S) (P.pairingIn T i j) = P.pairingIn S i j
have a : Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) ((algebraMap T S : (a : T) → S) (P.pairingIn T i j) : S) : R)
  ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
Tactic: apply FaithfulSMul.algebraMap_injective S R
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
T : Type u_7
inst_7 : CommRing T
inst_8 : Algebra T S
inst_9 : Algebra T R
inst_10 : IsScalarTower T S R
inst_11 : P.IsValuedIn T
inst_12 : P.IsValuedIn S
inst_13 : FaithfulSMul S R
i j : ι
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) ((algebraMap T S : (a : T) → S) (P.pairingIn T i j) : S) : R)
    ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
have a : Eq.{u_2 + 1} (α := R) ((algebraMap T R : (a : T) → R) (P.pairingIn T i j) : R)
  ((algebraMap S R : (a : S) → R) (P.pairingIn S i j) : R)
Tactic: rw [← RingHom.comp_apply, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
i : ι
⊢ range.{u_2, u_6 + 1} (ι := S) (⇑(algebraMap S R) : (a : S) → R) = (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
have h : ∀ (x : R),
  Membership.mem (γ := Set R) (range.{u_2, u_6 + 1} (ι := S) (⇑(algebraMap S R) : (a : S) → R)) x ↔
    x ∈ (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
i : ι
⊢ Membership.mem.{u_2, u_2} (α := R) (γ := Set R) (range.{u_2, u_6 + 1} (ι := S) (⇑(algebraMap S R) : (a : S) → R))
    ((P.coroot' i : (a : M) → R) x : R)
have rw : Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
Tactic: rw [show range (algebraMap S R) = LinearMap.range (Algebra.linearMap S R) by ext; simp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x_1 : M
i : ι
x : M
hx : Membership.mem (γ := Set M) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
⊢ Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
have mem : ∀ (k : ι),
  Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
    ((P.coroot' i : (a : M) → R) ((P.root : (a : ι) → M) k : M) : R)
Tactic: obtain ⟨k, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
i : ι
⊢ Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
have mem : ∀ (x : M) (hx : Membership.mem (γ := Set M) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x),
  Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
Tactic: induction hx using Submodule.span_induction with
  | mem x hx =>
    obtain ⟨k, rfl⟩ := hx
    simpa using RootPairing.exists_value k i
  | zero => simp
  | add x y _ _ hx hy => simpa only [map_add] using add_mem hx hy
  | smul t x _ hx => simpa only [LinearMap.map_smul_of_tower] using Submodule.smul_mem _ t hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
i : ι
mem :
  ∀ (x : M) (hx : Membership.mem (γ := Set M) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x),
    Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
⊢ Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
have zero : Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) 0 : R)
Tactic: induction hx using Submodule.span_induction with
  | mem x hx =>
    obtain ⟨k, rfl⟩ := hx
    simpa using RootPairing.exists_value k i
  | zero => simp
  | add x y _ _ hx hy => simpa only [map_add] using add_mem hx hy
  | smul t x _ hx => simpa only [LinearMap.map_smul_of_tower] using Submodule.smul_mem _ t hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
i : ι
mem :
  ∀ (x : M) (hx : Membership.mem (γ := Set M) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x),
    Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
zero : Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) 0 : R)
⊢ Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
have add : ∀ (x y : M),
  Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
    Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) y →
      ∀
        (hx :
          Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
            ((P.coroot' i : (a : M) → R) x : R))
        (hy :
          Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
            ((P.coroot' i : (a : M) → R) y : R)),
        Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
          ((P.coroot' i : (a : M) → R) (x + y) : R)
Tactic: induction hx using Submodule.span_induction with
  | mem x hx =>
    obtain ⟨k, rfl⟩ := hx
    simpa using RootPairing.exists_value k i
  | zero => simp
  | add x y _ _ hx hy => simpa only [map_add] using add_mem hx hy
  | smul t x _ hx => simpa only [LinearMap.map_smul_of_tower] using Submodule.smul_mem _ t hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
i : ι
mem :
  ∀ (x : M) (hx : Membership.mem (γ := Set M) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x),
    Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
zero : Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) 0 : R)
add :
  ∀ (x y : M),
    Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
      Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) y →
        ∀
          (hx :
            Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
              ((P.coroot' i : (a : M) → R) x : R))
          (hy :
            Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
              ((P.coroot' i : (a : M) → R) y : R)),
          Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
            ((P.coroot' i : (a : M) → R) (x + y) : R)
⊢ Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R) ((P.coroot' i : (a : M) → R) x : R)
have smul : ∀ (t : S) (x : M),
  Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
    ∀
      (hx :
        Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
          ((P.coroot' i : (a : M) → R) x : R)),
      Membership.mem (α := R) (↑(LinearMap.range (Algebra.linearMap S R)) : Set R)
        ((P.coroot' i : (a : M) → R) (t • x) : R)
Tactic: induction hx using Submodule.span_induction with
  | mem x hx =>
    obtain ⟨k, rfl⟩ := hx
    simpa using RootPairing.exists_value k i
  | zero => simp
  | add x y _ _ hx hy => simpa only [map_add] using add_mem hx hy
  | smul t x _ hx => simpa only [LinearMap.map_smul_of_tower] using Submodule.smul_mem _ t hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Module S M
i : ι
⊢ Eq (α := ↥(P.rootSpan S)) (P.rootSpanMem S ((P.reflectionPerm i : (a : ι) → ι) i)) (-P.rootSpanMem S i)
have a : (↑(P.rootSpanMem S ((P.reflectionPerm i : (a : ι) → ι) i)) : M) = (↑(-P.rootSpanMem S i) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Module S N
i : ι
⊢ Eq (α := ↥(P.corootSpan S)) (P.corootSpanMem S ((P.reflectionPerm i : (a : ι) → ι) i)) (-P.corootSpanMem S i)
have a : (↑(P.corootSpanMem S ((P.reflectionPerm i : (a : ι) → ι) i)) : N) = (↑(-P.corootSpanMem S i) : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : FaithfulSMul S R
inst_10 : P.IsValuedIn S
i : ι
x : ↥(P.corootSpan S)
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) ((P.root'In S i : (a : ↥(P.corootSpan S)) → S) x : S) : R)
    ((P.root' i : (a : N) → R) (↑x : N) : R)
have rw : Eq.{u_2 + 1} (α := R)
  ((algebraMap S R : (a : S) → R)
      ((LinearMap.restrictScalarsRange (Submodule.subtype (P.corootSpan S)) (Algebra.linearMap S R) sorry (P.root' i) sorry :
            (a : ↥(P.corootSpan S)) → S)
          x :
        S) :
    R)
  ((P.root' i : (a : N) → R) (↑x : N) : R)
Tactic: rw [root'In, ← Algebra.linearMap_apply, LinearMap.restrictScalarsRange_apply,
    Submodule.subtype_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : FaithfulSMul S R
inst_10 : P.IsValuedIn S
i : ι
x : ↥(P.corootSpan S)
rw :
  Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((LinearMap.restrictScalarsRange (Submodule.subtype (P.corootSpan S)) (Algebra.linearMap S R) ⋯ (P.root' i) ⋯ :
              (a : ↥(P.corootSpan S)) → S)
            x :
          S) :
      R)
    ((P.root' i : (a : N) → R) (↑x : N) : R)
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) ((P.root'In S i : (a : ↥(P.corootSpan S)) → S) x : S) : R)
    ((P.root' i : (a : N) → R) (↑x : N) : R)
have rw₁ : Eq.{u_2 + 1} (α := R)
  ((Algebra.linearMap S R : (a : S) → R)
      ((LinearMap.restrictScalarsRange (Submodule.subtype (P.corootSpan S)) (Algebra.linearMap S R) sorry (P.root' i) sorry :
            (a : ↥(P.corootSpan S)) → S)
          x :
        S) :
    R)
  ((P.root' i : (a : N) → R) (↑x : N) : R)
Tactic: rw [root'In, ← Algebra.linearMap_apply, LinearMap.restrictScalarsRange_apply,
    Submodule.subtype_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : FaithfulSMul S R
inst_10 : P.IsValuedIn S
i : ι
x : ↥(P.corootSpan S)
rw :
  Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((LinearMap.restrictScalarsRange (Submodule.subtype (P.corootSpan S)) (Algebra.linearMap S R) ⋯ (P.root' i) ⋯ :
              (a : ↥(P.corootSpan S)) → S)
            x :
          S) :
      R)
    ((P.root' i : (a : N) → R) (↑x : N) : R)
rw₁ :
  Eq.{u_2 + 1} (α := R)
    ((Algebra.linearMap S R : (a : S) → R)
        ((LinearMap.restrictScalarsRange (Submodule.subtype (P.corootSpan S)) (Algebra.linearMap S R) ⋯ (P.root' i) ⋯ :
              (a : ↥(P.corootSpan S)) → S)
            x :
          S) :
      R)
    ((P.root' i : (a : N) → R) (↑x : N) : R)
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) ((P.root'In S i : (a : ↥(P.corootSpan S)) → S) x : S) : R)
    ((P.root' i : (a : N) → R) (↑x : N) : R)
have rw₂ : Eq.{u_2 + 1} (α := R)
  ((P.root' i : (a : N) → R) ((Submodule.subtype (P.corootSpan S) : (a : ↥(P.corootSpan S)) → N) x : N) : R)
  ((P.root' i : (a : N) → R) (↑x : N) : R)
Tactic: rw [root'In, ← Algebra.linearMap_apply, LinearMap.restrictScalarsRange_apply,
    Submodule.subtype_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : IsScalarTower S R N
inst_9 : FaithfulSMul S R
inst_10 : P.IsValuedIn S
i : ι
x : ↥(P.corootSpan S)
rw :
  Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((LinearMap.restrictScalarsRange (Submodule.subtype (P.corootSpan S)) (Algebra.linearMap S R) ⋯ (P.root' i) ⋯ :
              (a : ↥(P.corootSpan S)) → S)
            x :
          S) :
      R)
    ((P.root' i : (a : N) → R) (↑x : N) : R)
rw₁ :
  Eq.{u_2 + 1} (α := R)
    ((Algebra.linearMap S R : (a : S) → R)
        ((LinearMap.restrictScalarsRange (Submodule.subtype (P.corootSpan S)) (Algebra.linearMap S R) ⋯ (P.root' i) ⋯ :
              (a : ↥(P.corootSpan S)) → S)
            x :
          S) :
      R)
    ((P.root' i : (a : N) → R) (↑x : N) : R)
rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((P.root' i : (a : N) → R) ((Submodule.subtype (P.corootSpan S) : (a : ↥(P.corootSpan S)) → N) x : N) : R)
    ((P.root' i : (a : N) → R) (↑x : N) : R)
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) ((P.root'In S i : (a : ↥(P.corootSpan S)) → S) x : S) : R)
    ((P.root' i : (a : N) → R) (↑x : N) : R)
have rw₃ : Eq.{u_2 + 1} (α := R) ((P.root' i : (a : N) → R) (↑x : N) : R) ((P.root' i : (a : N) → R) (↑x : N) : R)
Tactic: rw [root'In, ← Algebra.linearMap_apply, LinearMap.restrictScalarsRange_apply,
    Submodule.subtype_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i : ι
x y : M
hy : Membership.mem (γ := Set M) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) y
⊢ y ∈ Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
have mem : ∀ (j : ι),
  Membership.mem (α := M)
    (Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    ((P.root : (a : ι) → M) j : M)
Tactic: obtain ⟨j, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i : ι
x : M
j : ι
⊢ Membership.mem (α := M)
    (Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    ((P.root : (a : ι) → M) j : M)
have mem : Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
  (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
    (HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M)))
Tactic: rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply_root]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i : ι
x : M
j : ι
⊢ Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
    (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M)))
have mem : Membership.mem.{u_4, u_4} (α := M) (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
  ((P.root : (a : ι) → M) j : M)
Tactic: apply Submodule.sub_mem