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
i : ι
x : M
j : ι
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)
⊢ 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 (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
  (HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M))
Tactic: apply Submodule.sub_mem
-- 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
hx : Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
⊢ x ∈ Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
have mem : ∀ (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)))
Tactic: induction hx using Submodule.span_induction with
  | mem y hy =>
    obtain ⟨j, rfl⟩ := hy
    rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply_root]
    apply Submodule.sub_mem
    · exact Submodule.subset_span <| mem_range_self j
    · exact Submodule.smul_mem _ _ <| Submodule.subset_span <| mem_range_self i
  | zero => simp
  | add y z hy hz hy' hz' => simpa using Submodule.add_mem _ hy' hz'
  | smul y t hy hy' => simpa using Submodule.smul_mem _ _ hy'
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
i : ι
x : M
hx : Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
mem :
  ∀ (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)))
⊢ x ∈ Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
have zero : 0 ∈ Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
Tactic: induction hx using Submodule.span_induction with
  | mem y hy =>
    obtain ⟨j, rfl⟩ := hy
    rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply_root]
    apply Submodule.sub_mem
    · exact Submodule.subset_span <| mem_range_self j
    · exact Submodule.smul_mem _ _ <| Submodule.subset_span <| mem_range_self i
  | zero => simp
  | add y z hy hz hy' hz' => simpa using Submodule.add_mem _ hy' hz'
  | smul y t hy hy' => simpa using Submodule.smul_mem _ _ hy'
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
i : ι
x : M
hx : Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
mem :
  ∀ (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)))
zero :
  0 ∈ Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
⊢ x ∈ Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
have add : ∀ (y z : M)
  (hy : Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) y)
  (hz : Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) z)
  (hy' :
    y ∈
      Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
  (hz' :
    z ∈
      Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))),
  y + z ∈
    Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
Tactic: induction hx using Submodule.span_induction with
  | mem y hy =>
    obtain ⟨j, rfl⟩ := hy
    rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply_root]
    apply Submodule.sub_mem
    · exact Submodule.subset_span <| mem_range_self j
    · exact Submodule.smul_mem _ _ <| Submodule.subset_span <| mem_range_self i
  | zero => simp
  | add y z hy hz hy' hz' => simpa using Submodule.add_mem _ hy' hz'
  | smul y t hy hy' => simpa using Submodule.smul_mem _ _ hy'
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
i : ι
x : M
hx : Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
mem :
  ∀ (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)))
zero :
  0 ∈ Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
add :
  ∀ (y z : M)
    (hy : Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) y)
    (hz : Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) z)
    (hy' :
      y ∈
        Submodule.comap (↑(P.reflection i) : M →ₗ[R] M)
          (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (hz' :
      z ∈
        Submodule.comap (↑(P.reflection i) : M →ₗ[R] M)
          (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))),
    y + z ∈
      Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
⊢ x ∈ Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
have smul : ∀ (y : R) (t : M)
  (hy : Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) t)
  (hy' :
    t ∈
      Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))),
  y • t ∈
    Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
Tactic: induction hx using Submodule.span_induction with
  | mem y hy =>
    obtain ⟨j, rfl⟩ := hy
    rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply_root]
    apply Submodule.sub_mem
    · exact Submodule.subset_span <| mem_range_self j
    · exact Submodule.smul_mem _ _ <| Submodule.subset_span <| mem_range_self i
  | zero => simp
  | add y z hy hz hy' hz' => simpa using Submodule.add_mem _ hy' hz'
  | smul y t hy hy' => simpa using Submodule.smul_mem _ _ hy'
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
⊢ (↑(Submodule.map (↑P.flip.toPerfPair.symm : Dual R M →ₗ[R] N) (Submodule.dualAnnihilator (P.rootSpan R))) : Set N) =
    (↑(⨅ (i : ι), LinearMap.ker (P.root' i)) : Set N)
have h : ∀ (x : N),
  x ∈
      (↑(Submodule.map (↑P.flip.toPerfPair.symm : Dual R M →ₗ[R] N) (Submodule.dualAnnihilator (P.rootSpan R))) :
        Set N) ↔
    x ∈ (↑(⨅ (i : ι), LinearMap.ker (P.root' i)) : Set 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
⊢ (↑(Submodule.map (↑P.flip.toPerfPair.symm : Dual R M →ₗ[R] N) (Submodule.dualAnnihilator (P.rootSpan R))) : Set N) =
    (↑(Submodule.dualCoannihilator (span R (range P.root'))) : Set N)
have h : ∀ (x : N),
  x ∈
      (↑(Submodule.map (↑P.flip.toPerfPair.symm : Dual R M →ₗ[R] N) (Submodule.dualAnnihilator (P.rootSpan R))) :
        Set N) ↔
    x ∈ (↑(Submodule.dualCoannihilator (span R (range P.root'))) : Set 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
⊢ ⨅ (i : ι), LinearMap.ker (P.root' i) = Submodule.dualCoannihilator (span R (range P.root'))
have rw : ⨅ (i : ι), LinearMap.ker (P.root' i) =
  Submodule.map (↑P.flip.toPerfPair.symm : Dual R M →ₗ[R] N) (Submodule.dualAnnihilator (P.rootSpan R))
Tactic: rw [← rootSpan_dualAnnihilator_map_eq, rootSpan_dualAnnihilator_map_eq_iInf_ker_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
rw :
  ⨅ (i : ι), LinearMap.ker (P.root' i) =
    Submodule.map (↑P.flip.toPerfPair.symm : Dual R M →ₗ[R] N) (Submodule.dualAnnihilator (P.rootSpan R))
⊢ ⨅ (i : ι), LinearMap.ker (P.root' i) = Submodule.dualCoannihilator (span R (range P.root'))
have rw₁ : Eq.{u_5 + 1} (α := Submodule R N) (⨅ (i : ι), LinearMap.ker (P.root' i)) (⨅ (i : ι), LinearMap.ker (P.root' i))
Tactic: rw [← rootSpan_dualAnnihilator_map_eq, rootSpan_dualAnnihilator_map_eq_iInf_ker_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
⊢ Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (P.rootSpan R) = span R (range P.root')
have rw : Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) =
  span R (range P.root')
Tactic: rw [rootSpan, Submodule.map_span, ← image_univ, ← image_comp, image_univ, LinearEquiv.coe_coe,
    toPerfPair_comp_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
rw :
  Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) =
    span R (range P.root')
⊢ Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (P.rootSpan R) = span R (range P.root')
have rw₁ : Eq (α := Submodule R (Dual R N))
  (span R
    (image (α := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
  (span R (range P.root'))
Tactic: rw [rootSpan, Submodule.map_span, ← image_univ, ← image_comp, image_univ, LinearEquiv.coe_coe,
    toPerfPair_comp_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
rw :
  Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) =
    span R (range P.root')
rw₁ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (image (α := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N)
        (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (span R (range P.root'))
⊢ Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (P.rootSpan R) = span R (range P.root')
have rw₂ : Eq (α := Submodule R (Dual R N))
  (span R
    (image (α := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N)
      (image.{u_1, u_4} (α := ι) (⇑P.root : (a : ι) → M) univ)))
  (span R (range P.root'))
Tactic: rw [rootSpan, Submodule.map_span, ← image_univ, ← image_comp, image_univ, LinearEquiv.coe_coe,
    toPerfPair_comp_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
rw :
  Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) =
    span R (range P.root')
rw₁ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (image (α := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N)
        (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (span R (range P.root'))
rw₂ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (image (α := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N)
        (image.{u_1, u_4} (α := ι) (⇑P.root : (a : ι) → M) univ)))
    (span R (range P.root'))
⊢ Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (P.rootSpan R) = span R (range P.root')
have rw₃ : Eq (α := Submodule R (Dual R N))
  (span R
    (image (α := ι) (comp (β := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N) (⇑P.root : (a : ι) → M))
      univ))
  (span R (range P.root'))
Tactic: rw [rootSpan, Submodule.map_span, ← image_univ, ← image_comp, image_univ, LinearEquiv.coe_coe,
    toPerfPair_comp_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
rw :
  Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) =
    span R (range P.root')
rw₁ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (image (α := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N)
        (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (span R (range P.root'))
rw₂ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (image (α := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N)
        (image.{u_1, u_4} (α := ι) (⇑P.root : (a : ι) → M) univ)))
    (span R (range P.root'))
rw₃ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (image (α := ι) (comp (β := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N) (⇑P.root : (a : ι) → M))
        univ))
    (span R (range P.root'))
⊢ Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (P.rootSpan R) = span R (range P.root')
have rw₄ : Eq (α := Submodule R (Dual R N))
  (span R
    (range (ι := ι) (comp (β := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N) (⇑P.root : (a : ι) → M))))
  (span R (range P.root'))
Tactic: rw [rootSpan, Submodule.map_span, ← image_univ, ← image_comp, image_univ, LinearEquiv.coe_coe,
    toPerfPair_comp_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
rw :
  Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) =
    span R (range P.root')
rw₁ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (image (α := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N)
        (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (span R (range P.root'))
rw₂ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (image (α := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N)
        (image.{u_1, u_4} (α := ι) (⇑P.root : (a : ι) → M) univ)))
    (span R (range P.root'))
rw₃ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (image (α := ι) (comp (β := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N) (⇑P.root : (a : ι) → M))
        univ))
    (span R (range P.root'))
rw₄ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (range (ι := ι)
        (comp (β := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N) (⇑P.root : (a : ι) → M))))
    (span R (range P.root'))
⊢ Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (P.rootSpan R) = span R (range P.root')
have rw₅ : Eq (α := Submodule R (Dual R N))
  (span R (range (ι := ι) (comp (β := M) (⇑P.toPerfPair : (a : M) → Dual R N) (⇑P.root : (a : ι) → M))))
  (span R (range P.root'))
Tactic: rw [rootSpan, Submodule.map_span, ← image_univ, ← image_comp, image_univ, LinearEquiv.coe_coe,
    toPerfPair_comp_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
rw :
  Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) =
    span R (range P.root')
rw₁ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (image (α := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N)
        (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (span R (range P.root'))
rw₂ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (image (α := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N)
        (image.{u_1, u_4} (α := ι) (⇑P.root : (a : ι) → M) univ)))
    (span R (range P.root'))
rw₃ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (image (α := ι) (comp (β := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N) (⇑P.root : (a : ι) → M))
        univ))
    (span R (range P.root'))
rw₄ :
  Eq (α := Submodule R (Dual R N))
    (span R
      (range (ι := ι)
        (comp (β := M) (⇑(↑P.toPerfPair : M →ₗ[R] Dual R N) : (a : M) → Dual R N) (⇑P.root : (a : ι) → M))))
    (span R (range P.root'))
rw₅ :
  Eq (α := Submodule R (Dual R N))
    (span R (range (ι := ι) (comp (β := M) (⇑P.toPerfPair : (a : M) → Dual R N) (⇑P.root : (a : ι) → M))))
    (span R (range P.root'))
⊢ Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (P.rootSpan R) = span R (range P.root')
have rw₆ : Eq (α := Submodule R (Dual R N)) (span R (range P.root')) (span R (range P.root'))
Tactic: rw [rootSpan, Submodule.map_span, ← image_univ, ← image_comp, image_univ, LinearEquiv.coe_coe,
    toPerfPair_comp_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 j : ι
S : Type u_7
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
⊢ (P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) j : M) =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M))
have rw : HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
    (HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M)) =
  HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
    (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M))
Tactic: rw [reflection_apply_root, ← P.algebraMap_pairingIn S, algebraMap_smul]
-- 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 j : ι
S : Type u_7
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
rw :
  HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M)) =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M))
⊢ (P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) j : M) =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M))
have rw₁ : HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R)
      ((P.root : (a : ι) → M) i : M)) =
  HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
    (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M))
Tactic: rw [reflection_apply_root, ← P.algebraMap_pairingIn S, algebraMap_smul]
-- 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 j : ι
S : Type u_7
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
rw :
  HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M)) =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M))
rw₁ :
  HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M))
⊢ (P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) j : M) =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M))
have rw₂ : HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
    (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M)) =
  HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
    (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M))
Tactic: rw [reflection_apply_root, ← P.algebraMap_pairingIn S, algebraMap_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.IsValuedIn (goal)
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_7
L : Type u_8
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module L M
inst_6 : Module L N
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
Q : RootPairing ι L M N
inst_11 : Q.IsRootSystem
inst_12 : Q.IsValuedIn K
⊢ finrank.{u_7, u_4} K ↥(Q.rootSpan K) = finrank L M
have hM : Eq (α := Submodule L M) (span L (↑(Q.rootSpan K) : Set M)) ⊤
Tactic: rw [LinearMap.finrank_eq_of_isPerfPair Q.toLinearMap (Q.rootSpan K) (Q.corootSpan K)]