awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
S_1 : Type u_3
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_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S N
inst_8 : Finite ι
⊢ Module.Finite.{u_6, u_5} S ↥(P.corootSpan S)

Tactic:
Finite.span_of_finite S <| finite_range _

Premises used: Set.Mem, Set.finite_range, Module.Finite.span_of_finite
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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 : ι
a : (↑(P.rootSpanMem S ((P.reflectionPerm i : (a : ι) → ι) i)) : M) = (↑(-P.rootSpanMem S i) : M)
⊢ Eq (α := ↥(P.rootSpan S)) (P.rootSpanMem S ((P.reflectionPerm i : (a : ι) → ι) i)) (-P.rootSpanMem S i)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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 : ι
⊢ (↑(P.rootSpanMem S ((P.reflectionPerm i : (a : ι) → ι) i)) : M) = (↑(-P.rootSpanMem S i) : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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 : ι
a : (↑(P.corootSpanMem S ((P.reflectionPerm i : (a : ι) → ι) i)) : N) = (↑(-P.corootSpanMem S i) : N)
⊢ Eq (α := ↥(P.corootSpan S)) (P.corootSpanMem S ((P.reflectionPerm i : (a : ι) → ι) i)) (-P.corootSpanMem S i)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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 : ι
⊢ (↑(P.corootSpanMem S ((P.reflectionPerm i : (a : ι) → ι) i)) : N) = (↑(-P.corootSpanMem S i) : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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)
rw₃ rw₄ : Eq.{u_2 + 1} (α := R) ((P.root' i : (a : N) → R) (↑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)

Tactic:
rw [root'In, ← Algebra.linearMap_apply, LinearMap.restrictScalarsRange_apply,
    Submodule.subtype_apply]

Premises used: Submodule.subtype_apply, Algebra.linearMap_apply, LinearMap.restrictScalarsRange_apply, RootPairing.root'In
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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_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
⊢ (P.root'In S i : (a : ↥(P.corootSpan S)) → S) (P.corootSpanMem S j) = P.pairingIn S i j

Tactic:
rfl

Premises used: RootPairing.pairing, RootPairing.pairingIn, Classical.choose, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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 : FaithfulSMul S R
inst_10 : P.IsValuedIn S
i : ι
x : ↥(P.rootSpan S)
⊢ Eq.{u_2 + 1} (α := R) ((algebraMap S R : (a : S) → R) ((P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) x : S) : R)
    ((P.coroot' i : (a : M) → R) (↑x : M) : R)

Tactic:
P.flip.algebraMap_root'In_apply S i x

Premises used: RootPairing.flip, RootPairing.algebraMap_root'In_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : FaithfulSMul S R
inst_10 : P.IsValuedIn S
⊢ (P.coroot'In S i : (a : ↥(P.rootSpan S)) → S) (P.rootSpanMem S j) = P.pairingIn S j i

Tactic:
rfl

Premises used: RootPairing.pairing, RootPairing.pairingIn, Classical.choose, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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
inst_7 : Nonempty ι
inst_8 : NeZero.{u_2} (R := R) 2
⊢ Ne (α := Submodule S M) (P.rootSpan S) ⊥

Tactic:
simpa [rootSpan] using P.exists_ne_zero

Premises used: RootPairing.rootSpan, RootPairing.exists_ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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
inst_7 : Nonempty ι
inst_8 : NeZero.{u_2} (R := R) 2
⊢ Ne (α := Submodule S N) (P.corootSpan S) ⊥

Tactic:
P.flip.rootSpan_ne_bot S

Premises used: RootPairing.flip, RootPairing.rootSpan_ne_bot
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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
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)
⊢ y ∈ Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))

Tactic:
obtain ⟨j, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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 (γ := 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)))
⊢ 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:
rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply_root]

Premises used: Submodule.mem_comap, LinearEquiv.coe_coe, RootPairing.reflection_apply_root
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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)
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))
⊢ 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:
apply Submodule.sub_mem

Premises used: Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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.{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:
Submodule.subset_span <| mem_range_self j

Premises used: Set.mem_range_self, Set.Mem, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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.{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:
exact Submodule.subset_span <| mem_range_self j

Premises used: Set.mem_range_self, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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)))
    (HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M))

Tactic:
Submodule.smul_mem _ _ <| Submodule.subset_span <| mem_range_self i

Premises used: Set.mem_range_self, Set.Mem, Submodule.subset_span, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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)))
    (HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M))

Tactic:
exact Submodule.smul_mem _ _ <| Submodule.subset_span <| mem_range_self i

Premises used: Set.mem_range_self, Submodule.subset_span, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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
⊢ 0 ∈ Submodule.comap (↑(P.reflection i) : M →ₗ[R] M) (span R (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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 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:
simpa using Submodule.add_mem _ hy' hz'

Premises used: Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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
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:
simpa using Submodule.smul_mem _ _ hy'

Premises used: Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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)))
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)))
⊢ x ∈ 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'

Premises used: Set.mem_range_self, Submodule.mem_comap, Submodule.subset_span, rfl, Submodule.sub_mem, LinearEquiv.coe_coe, Submodule.smul_mem, RootPairing.reflection_apply_root
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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 : ι
⊢ P.corootSpan R ∈ End.invtSubmodule (↑(P.coreflection i) : N →ₗ[R] N)

Tactic:
P.flip.rootSpan_mem_invtSubmodule_reflection i

Premises used: Set.Mem, RootPairing.flip, setOf, RootPairing.rootSpan_mem_invtSubmodule_reflection
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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
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)
⊢ (↑(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)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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
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:
simp [LinearEquiv.symm_apply_eq, subset_def]

Premises used: Set.subset_def, LinearEquiv.symm_apply_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R)) =
    ⨅ (i : ι), LinearMap.ker (P.coroot' i)

Tactic:
P.flip.rootSpan_dualAnnihilator_map_eq_iInf_ker_root'

Premises used: RootPairing.flip, LinearMap.mk₂'ₛₗ, LinearMap.flip, RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root'
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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
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)
⊢ (↑(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)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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
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:
simp [LinearEquiv.symm_apply_eq, subset_def]

Premises used: Set.subset_def, LinearEquiv.symm_apply_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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.symm : Dual R N →ₗ[R] M) (Submodule.dualAnnihilator (P.corootSpan R)) =
    Submodule.dualCoannihilator (span R (range P.coroot'))

Tactic:
P.flip.rootSpan_dualAnnihilator_map_eq

Premises used: RootPairing.flip, LinearMap.mk₂'ₛₗ, LinearMap.flip, RootPairing.rootSpan_dualAnnihilator_map_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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))
rw₁ rw₂ :
  Eq.{u_5 + 1} (α := Submodule R N) (⨅ (i : ι), LinearMap.ker (P.root' i)) (⨅ (i : ι), LinearMap.ker (P.root' i))
⊢ ⨅ (i : ι), LinearMap.ker (P.root' i) = Submodule.dualCoannihilator (span R (range P.root'))

Tactic:
rw [← rootSpan_dualAnnihilator_map_eq, rootSpan_dualAnnihilator_map_eq_iInf_ker_root']

Premises used: RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root', RootPairing.rootSpan_dualAnnihilator_map_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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.coroot' i) = Submodule.dualCoannihilator (span R (range P.coroot'))

Tactic:
P.flip.iInf_ker_root'_eq

Premises used: RootPairing.flip, RootPairing.iInf_ker_root'_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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'))
rw₆ rw₇ : Eq (α := Submodule R (Dual R N)) (span R (range P.root')) (span R (range P.root'))
⊢ Submodule.map (↑P.toPerfPair : M →ₗ[R] Dual R N) (P.rootSpan R) = span R (range P.root')

Tactic:
rw [rootSpan, Submodule.map_span, ← image_univ, ← image_comp, image_univ, LinearEquiv.coe_coe,
    toPerfPair_comp_root]

Premises used: Set.image_univ, RootPairing.toPerfPair_comp_root, RootPairing.rootSpan, Set.image_comp, Submodule.map_span, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
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 : N →ₗ[R] Dual R M) (P.corootSpan R) = span R (range P.coroot')

Tactic:
P.flip.rootSpan_map_toPerfPair

Premises used: RootPairing.flip, RootPairing.rootSpan_map_toPerfPair, LinearMap.mk₂'ₛₗ, LinearMap.flip