internlm/Lean-Github huggingface dataset:
Theorem: orthSpace_eq
Proof state before:
case h.refine_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x✝ : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
x : η → R
h : ∃ y, (∀ w ∈ U, y w = 0) ∧ (Module.piEquiv η R R).symm y = x
⊢ ∀ y ∈ U, ∑ i : η, x i * y i = 0
Tactic:
obtain ⟨w, h, rfl⟩ := h
Proof state after:
case h.refine_2.intro.intro
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
⊢ ∀ y ∈ U, ∑ i : η, (Module.piEquiv η R R).symm w i * y i = 0
Theorem: orthSpace_eq
Proof state before:
case h.refine_2.intro.intro
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
⊢ ∀ y ∈ U, ∑ i : η, (Module.piEquiv η R R).symm w i * y i = 0
Tactic:
intro y hy
Proof state after:
case h.refine_2.intro.intro
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ i : η, (Module.piEquiv η R R).symm w i * y i = 0
Theorem: orthSpace_eq
Proof state before:
case h.refine_2.intro.intro
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ i : η, (Module.piEquiv η R R).symm w i * y i = 0
Tactic:
convert h y hy using 1
Proof state after:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ i : η, (Module.piEquiv η R R).symm w i * y i = w y
Theorem: orthSpace_eq
Proof state before:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ i : η, (Module.piEquiv η R R).symm w i * y i = w y
Tactic:
simp [Module.piEquiv_apply_symm]
Proof state after:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = w y
Theorem: orthSpace_eq
Proof state before:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = w y
Tactic:
convert DFunLike.congr_fun ((Pi.basisFun R η).sum_dual_apply_smul_coord w) y using 1
Proof state after:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = (∑ x : η, w ((Pi.basisFun R η) x) • (Pi.basisFun R η).coord x) y
Theorem: orthSpace_eq
Proof state before:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = (∑ x : η, w ((Pi.basisFun R η) x) • (Pi.basisFun R η).coord x) y
Tactic:
simp only [Pi.basisFun_apply, LinearMap.coeFn_sum, Finset.sum_apply, LinearMap.smul_apply,
  Basis.coord_apply, Pi.basisFun_repr, smul_eq_mul]
Proof state after:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = ∑ x : η, w ((LinearMap.stdBasis R (fun x => R) x) 1) * y x
Theorem: orthSpace_eq
Proof state before:
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = ∑ x : η, w ((LinearMap.stdBasis R (fun x => R) x) 1) * y x
Tactic:
rfl
Proof state after:
no goals
Theorem: orthSpace_eq
Proof state before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x✝ : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
x : η → R
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
⊢ (Module.piEquiv η R R).symm ((Module.piEquiv η R R) x) = x
Tactic:
simp
Proof state after:
no goals
Theorem: orthSpace_eq
Proof state before:
case h.refine_1
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x✝ : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
x : η → R
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
⊢ ∀ w ∈ U, ((Module.piEquiv η R R) x) w = 0
Tactic:
simpa [Module.piEquiv_apply_apply, h, mul_comm]
Proof state after:
no goals
Theorem: orthSpace_orthSpace
Proof state before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝¹ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
⊢ (orthSpace U).orthSpace = U
Tactic:
refine (FiniteDimensional.eq_of_le_of_finrank_le (fun x hxU ↦ ?_) (le_of_eq ?_)).symm
Proof state after:
case refine_1
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x✝ : η → R
U✝¹ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
x : η → K
hxU : x ∈ U
⊢ x ∈ (orthSpace U).orthSpace

case refine_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝¹ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
⊢ FiniteDimensional.finrank K ↥(orthSpace U).orthSpace = FiniteDimensional.finrank K ↥U
Theorem: orthSpace_orthSpace
Proof state before:
case refine_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝¹ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
⊢ FiniteDimensional.finrank K ↥(orthSpace U).orthSpace = FiniteDimensional.finrank K ↥U
Tactic:
rw [orthSpace_eq, orthSpace_eq, LinearEquiv.finrank_map_eq', LinearEquiv.dualAnnihilator_map_eq,
  LinearEquiv.finrank_map_eq', ← Subspace.finrank_dualCoannihilator_eq,
  Subspace.dualAnnihilator_dualCoannihilator_eq]
Proof state after:
no goals
Theorem: orthSpace_orthSpace
Proof state before:
case refine_1
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x✝ : η → R
U✝¹ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
x : η → K
hxU : x ∈ U
⊢ x ∈ (orthSpace U).orthSpace
Tactic:
simp_rw [mem_orthSpace_iff']
Proof state after:
case refine_1
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x✝ : η → R
U✝¹ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
x : η → K
hxU : x ∈ U
⊢ ∀ (y : η → K), (∀ y_1 ∈ U, ∑ i : η, y i * y_1 i = 0) → ∑ i : η, x i * y i = 0
Theorem: orthSpace_orthSpace
Proof state before:
case refine_1
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x✝ : η → R
U✝¹ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
x : η → K
hxU : x ∈ U
⊢ ∀ (y : η → K), (∀ y_1 ∈ U, ∑ i : η, y i * y_1 i = 0) → ∑ i : η, x i * y i = 0
Tactic:
intro y hy
Proof state after:
case refine_1
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x✝ : η → R
U✝¹ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
x : η → K
hxU : x ∈ U
y : η → K
hy : ∀ y_1 ∈ U, ∑ i : η, y i * y_1 i = 0
⊢ ∑ i : η, x i * y i = 0
Theorem: orthSpace_orthSpace
Proof state before:
case refine_1
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x✝ : η → R
U✝¹ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U✝ V U : Subspace K (η → K)
x : η → K
hxU : x ∈ U
y : η → K
hy : ∀ y_1 ∈ U, ∑ i : η, y i * y_1 i = 0
⊢ ∑ i : η, x i * y i = 0
Tactic:
simpa [mul_comm] using hy x hxU
Proof state after:
no goals
Theorem: orthSpace_injective
Proof state before:
α : Type u_1
R : Type u_2
η✝¹ : Type u_3
ι : Type u_4
η✝ : Type u_5
inst✝⁴ : CommRing R
x : η✝ → R
U✝¹ V✝ : Submodule R (η✝ → R)
K✝ : Type u_6
inst✝³ : Field K✝
inst✝² : Fintype η✝
U✝ V : Subspace K✝ (η✝ → K✝)
η : Type u_7
K : Type u_8
inst✝¹ : Fintype η
inst✝ : Field K
U U' : Submodule K (η → K)
h : U.orthSpace = U'.orthSpace
⊢ U = U'
Tactic:
simpa using congr_arg Submodule.orthSpace h
Proof state after:
no goals
Theorem: eq_orthSpace_comm
Proof state before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U V : Subspace K (η → K)
h : U = orthSpace V
⊢ V = orthSpace U
Tactic:
rw [h, orthSpace_orthSpace]
Proof state after:
no goals
Theorem: eq_orthSpace_comm
Proof state before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U V : Subspace K (η → K)
h : V = orthSpace U
⊢ U = orthSpace V
Tactic:
rw [h, orthSpace_orthSpace]
Proof state after:
no goals
Theorem: orthSpace_bot
Proof state before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U V : Subspace K (η → K)
⊢ orthSpace ⊥ = ⊤
Tactic:
rw [orthSpace_eq]
Proof state after:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U V : Subspace K (η → K)
⊢ map (Module.piEquiv η K K).symm (dualAnnihilator ⊥) = ⊤
Theorem: orthSpace_bot
Proof state before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U V : Subspace K (η → K)
⊢ map (Module.piEquiv η K K).symm (dualAnnihilator ⊥) = ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: orthSpace_top
Proof state before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U V : Subspace K (η → K)
⊢ orthSpace ⊤ = ⊥
Tactic:
rw [orthSpace_eq]
Proof state after:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U V : Subspace K (η → K)
⊢ map (Module.piEquiv η K K).symm (dualAnnihilator ⊤) = ⊥
Theorem: orthSpace_top
Proof state before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U V : Subspace K (η → K)
⊢ map (Module.piEquiv η K K).symm (dualAnnihilator ⊤) = ⊥
Tactic:
simp
Proof state after:
no goals
Theorem: Set.mem_relOrthSpace_iff
Proof state before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ w ∈ s.relOrthSpace U ↔ ∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
Tactic:
rw [relOrthSpace, mem_inf, mem_orthSpace_iff'', mem_supportedFun_iff]
Proof state after:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s ↔
    ∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
Theorem: Set.mem_relOrthSpace_iff
Proof state before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s ↔
    ∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s →
    ∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0

case mpr
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0) →
    (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s
Theorem: Set.mem_relOrthSpace_iff
Proof state before:
case mpr
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0) →
    (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s
Tactic:
rintro ⟨l, rfl, hl⟩
Proof state after:
case mpr.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ↥(Finsupp.supported R R s)
hl : ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
⊢ (∃ l_1, ⇑l_1 = ⇑↑l ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l_1 = 0) ∧ support ⇑↑l ⊆ s
Theorem: Set.mem_relOrthSpace_iff
Proof state before:
case mpr.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ↥(Finsupp.supported R R s)
hl : ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
⊢ (∃ l_1, ⇑l_1 = ⇑↑l ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l_1 = 0) ∧ support ⇑↑l ⊆ s
Tactic:
refine ⟨⟨l, rfl, hl⟩, ?_⟩
Proof state after:
case mpr.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ↥(Finsupp.supported R R s)
hl : ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
⊢ support ⇑↑l ⊆ s
Theorem: Set.mem_relOrthSpace_iff
Proof state before:
case mpr.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ↥(Finsupp.supported R R s)
hl : ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
⊢ support ⇑↑l ⊆ s
Tactic:
rw [Finsupp.fun_support_eq]
Proof state after:
case mpr.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ↥(Finsupp.supported R R s)
hl : ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
⊢ ↑(↑l).support ⊆ s
Theorem: Set.mem_relOrthSpace_iff
Proof state before:
case mpr.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ↥(Finsupp.supported R R s)
hl : ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
⊢ ↑(↑l).support ⊆ s
Tactic:
exact l.2
Proof state after:
no goals
Theorem: Set.mem_relOrthSpace_iff
Proof state before:
case mp
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0) ∧ support w ⊆ s →
    ∃ l, ⇑↑l = w ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l = 0
Tactic:
rintro ⟨⟨l, rfl, hl⟩, hsupp⟩
Proof state after:
case mp.intro.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ι →₀ R
hl : ∀ y ∈ U, (Finsupp.total ι R R y) l = 0
hsupp : support ⇑l ⊆ s
⊢ ∃ l_1, ⇑↑l_1 = ⇑l ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l_1 = 0
Theorem: Set.mem_relOrthSpace_iff
Proof state before:
case mp.intro.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ι →₀ R
hl : ∀ y ∈ U, (Finsupp.total ι R R y) l = 0
hsupp : support ⇑l ⊆ s
⊢ ∃ l_1, ⇑↑l_1 = ⇑l ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑l_1 = 0
Tactic:
exact ⟨⟨l, by simpa using hsupp⟩, by simpa⟩
Proof state after:
no goals
Theorem: Set.mem_relOrthSpace_iff
Proof state before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ι →₀ R
hl : ∀ y ∈ U, (Finsupp.total ι R R y) l = 0
hsupp : support ⇑l ⊆ s
⊢ l ∈ Finsupp.supported R R s
Tactic:
simpa using hsupp
Proof state after:
no goals
Theorem: Set.mem_relOrthSpace_iff
Proof state before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule R (ι → R)
l : ι →₀ R
hl : ∀ y ∈ U, (Finsupp.total ι R R y) l = 0
hsupp : support ⇑l ⊆ s
⊢ ⇑↑⟨l, ⋯⟩ = ⇑l ∧ ∀ x ∈ U, (Finsupp.total ι R R x) ↑⟨l, ⋯⟩ = 0
Tactic:
simpa
Proof state after:
no goals
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
⊢ s.relOrthSpace ↑((s.subtypeFunEquiv K) U) = ↑((s.subtypeFunEquiv K) U.orthSpace)
Tactic:
ext x
Proof state after:
case h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
⊢ x ∈ s.relOrthSpace ↑((s.subtypeFunEquiv K) U) ↔ x ∈ ↑((s.subtypeFunEquiv K) U.orthSpace)
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
⊢ x ∈ s.relOrthSpace ↑((s.subtypeFunEquiv K) U) ↔ x ∈ ↑((s.subtypeFunEquiv K) U.orthSpace)
Tactic:
simp_rw [mem_relOrthSpace_iff, mem_subtypeFunEquiv_iff, mem_orthSpace_iff'']
Proof state after:
case h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
⊢ (∃ l, ⇑↑l = x ∧ ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0) ↔
    support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
⊢ (∃ l, ⇑↑l = x ∧ ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0) ↔
    support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
Tactic:
refine ⟨?_, fun ⟨hsupp, l, hlrs, hl⟩ ↦ ?_⟩
Proof state after:
case h.refine_1
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
⊢ (∃ l, ⇑↑l = x ∧ ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0) →
    support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0

case h.refine_2
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
x✝ : support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
hsupp : support x ⊆ s
l : ↑s →₀ K
hlrs : ⇑l = s.restrict x
hl : ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
⊢ ∃ l, ⇑↑l = x ∧ ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_2
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
x✝ : support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
hsupp : support x ⊆ s
l : ↑s →₀ K
hlrs : ⇑l = s.restrict x
hl : ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
⊢ ∃ l, ⇑↑l = x ∧ ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
Tactic:
refine ⟨⟨Finsupp.mapDomain s.incl l, ?_⟩, ?_, ?_⟩
Proof state after:
case h.refine_2.refine_1
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
x✝ : support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
hsupp : support x ⊆ s
l : ↑s →₀ K
hlrs : ⇑l = s.restrict x
hl : ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
⊢ Finsupp.mapDomain s.incl l ∈ Finsupp.supported K K s

case h.refine_2.refine_2
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
x✝ : support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
hsupp : support x ⊆ s
l : ↑s →₀ K
hlrs : ⇑l = s.restrict x
hl : ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
⊢ ⇑↑⟨Finsupp.mapDomain s.incl l, ?h.refine_2.refine_1⟩ = x

case h.refine_2.refine_3
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
U : Submodule K (↑s → K)
x : ι → K
x✝ : support x ⊆ s ∧ ∃ l, ⇑l = s.restrict x ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
hsupp : support x ⊆ s
l : ↑s →₀ K
hlrs : ⇑l = s.restrict x
hl : ∀ y ∈ U, (Finsupp.total (↑s) K K y) l = 0
⊢ ∀ (x : ι → K),
    support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑⟨Finsupp.mapDomain s.incl l, ?h.refine_2.refine_1⟩ = 0