internlm/Lean-Github huggingface dataset:
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
⊢ x ∈
      ↑((MapSubtype.relIso (LinearMap.range (LinearMap.extendSubtype R s)))
          ((orderIsoMapComap (LinearEquiv.ofInjective (LinearMap.extendSubtype R s) ⋯)).toEquiv U)) ↔
    support x ⊆ s ∧ s.restrict x ∈ U
Tactic:
simp only [RelIso.coe_fn_toEquiv, orderIsoMapComap_apply, MapSubtype.relIso_apply, mem_map,
  coeSubtype, exists_exists_and_eq_and, LinearEquiv.ofInjective_apply, support_subset_iff,
  LinearMap.extendSubtype_eq_ite]
Proof state after:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
⊢ (∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = x) ↔ (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
⊢ (∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = x) ↔ (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
Tactic:
refine ⟨?_, fun ⟨hxs, hxU⟩ ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
⊢ (∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = x) → (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U

case refine_2
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
⊢ ∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = x
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
case refine_2
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
⊢ ∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = x
Tactic:
refine ⟨_, hxU, ?_⟩
Proof state after:
case refine_2
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
⊢ (fun i => if h : i ∈ s then s.restrict x ⟨i, h⟩ else 0) = x
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
case refine_2
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
⊢ (fun i => if h : i ∈ s then s.restrict x ⟨i, h⟩ else 0) = x
Tactic:
ext i
Proof state after:
case refine_2.h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ (if h : i ∈ s then s.restrict x ⟨i, h⟩ else 0) = x i
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
case refine_2.h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ (if h : i ∈ s then s.restrict x ⟨i, h⟩ else 0) = x i
Tactic:
simp_rw [restrict_apply, dite_eq_ite, ite_eq_left_iff, eq_comm (b := x i)]
Proof state after:
case refine_2.h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ i ∉ s → x i = 0
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
case refine_2.h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ i ∉ s → x i = 0
Tactic:
rw [not_imp_comm]
Proof state after:
case refine_2.h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ ¬x i = 0 → i ∈ s
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
case refine_2.h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
x✝ : (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
hxs : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
hxU : s.restrict x ∈ U
i : η
⊢ ¬x i = 0 → i ∈ s
Tactic:
apply hxs
Proof state after:
no goals
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
case refine_1
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
U : Submodule R (↑s → R)
⊢ (∃ a ∈ U, (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = x) → (∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s) ∧ s.restrict x ∈ U
Tactic:
rintro ⟨a, ha, rfl⟩
Proof state after:
case refine_1.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (∀ (x : η), (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x ≠ 0 → x ∈ s) ∧
    (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) ∈ U
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
case refine_1.intro.intro
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (∀ (x : η), (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x ≠ 0 → x ∈ s) ∧
    (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) ∈ U
Tactic:
constructor
Proof state after:
case refine_1.intro.intro.left
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ ∀ (x : η), (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x ≠ 0 → x ∈ s

case refine_1.intro.intro.right
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) ∈ U
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
case refine_1.intro.intro.right
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) ∈ U
Tactic:
convert ha
Proof state after:
case h.e'_4
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = a
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
case h.e'_4
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ (s.restrict fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) = a
Tactic:
ext
Proof state after:
case h.e'_4.h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
x✝ : ↑s
⊢ s.restrict (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x✝ = a x✝
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
case h.e'_4.h
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
x✝ : ↑s
⊢ s.restrict (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x✝ = a x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
case refine_1.intro.intro.left
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ ∀ (x : η), (fun i => if h : i ∈ s then a ⟨i, h⟩ else 0) x ≠ 0 → x ∈ s
Tactic:
simp only [ne_eq, dite_eq_right_iff, not_forall, forall_exists_index]
Proof state after:
case refine_1.intro.intro.left
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ ∀ (x : η) (x_1 : x ∈ s), ¬a ⟨x, x_1⟩ = 0 → x ∈ s
Theorem: Set.mem_subtypeFunEquiv_iff
Proof state before:
case refine_1.intro.intro.left
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι : Type u_4
R : Type u_5
η : Type u_6
inst✝ : Semiring R
s : Set η
U : Submodule R (↑s → R)
a : ↑s → R
ha : a ∈ U
⊢ ∀ (x : η) (x_1 : x ∈ s), ¬a ⟨x, x_1⟩ = 0 → x ∈ s
Tactic:
exact fun i hi _ ↦ hi
Proof state after:
no goals
Theorem: mem_orthSpace'_iff
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 U : Submodule R (η → R)
l : η →₀ R
⊢ l ∈ U.orthSpace' ↔ ∀ x ∈ U, (Finsupp.total η R R x) l = 0
Tactic:
simp [orthSpace']
Proof state after:
no goals
Theorem: mem_orthSpace_iff'
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 η
⊢ x ∈ U.orthSpace ↔ ∀ y ∈ U, ∑ i : η, x i * y i = 0
Tactic:
simp only [orthSpace, orthSpace', mem_map, mem_comap, Finsupp.toDualLin_coe, mem_dualAnnihilator,
  Finsupp.toDual_apply, Finsupp.total_apply, Finsupp.sum, smul_eq_mul]
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)
inst✝ : Fintype η
⊢ (∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x) ↔ ∀ y ∈ U, ∑ i : η, x i * y i = 0
Theorem: mem_orthSpace_iff'
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 η
⊢ (∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x) ↔ ∀ y ∈ U, ∑ i : η, x i * y i = 0
Tactic:
refine ⟨fun h y hyU ↦ ?_, fun h ↦ ?_⟩
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)
inst✝ : Fintype η
h : ∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x
y : η → R
hyU : y ∈ U
⊢ ∑ i : η, x i * y i = 0

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)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
⊢ ∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x
Theorem: mem_orthSpace_iff'
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)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
⊢ ∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x
Tactic:
refine ⟨Finsupp.equivFunOnFinite.2 x, fun w hw ↦ ?_, by ext; simp⟩
Proof state after:
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)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ (Finsupp.equivFunOnFinite.invFun x).support, (Finsupp.equivFunOnFinite.invFun x) x_1 * w x_1 = 0
Theorem: mem_orthSpace_iff'
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)
inst✝ : Fintype η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ (Finsupp.equivFunOnFinite.invFun x).support, (Finsupp.equivFunOnFinite.invFun x) x_1 * w x_1 = 0
Tactic:
convert h w hw 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 η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ (Finsupp.equivFunOnFinite.invFun x).support, (Finsupp.equivFunOnFinite.invFun x) x_1 * w x_1 =
    ∑ i : η, x i * w i
Theorem: mem_orthSpace_iff'
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 η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ (Finsupp.equivFunOnFinite.invFun x).support, (Finsupp.equivFunOnFinite.invFun x) x_1 * w x_1 =
    ∑ i : η, x i * w i
Tactic:
simp only [Equiv.invFun_as_coe, Finsupp.equivFunOnFinite_symm_apply_support,
  Finite.toFinset_setOf, ne_eq, Finset.mem_univ, forall_true_left, not_not,
  Finsupp.equivFunOnFinite_symm_apply_toFun]
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 η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ Finset.filter (fun x_1 => ¬x x_1 = 0) Finset.univ, x x_1 * w x_1 = ∑ i : η, x i * w i
Theorem: mem_orthSpace_iff'
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 η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∑ x_1 ∈ Finset.filter (fun x_1 => ¬x x_1 = 0) Finset.univ, x x_1 * w x_1 = ∑ i : η, x i * w i
Tactic:
apply Finset.sum_subset (Finset.subset_univ _)
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 η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∀ x_1 ∈ Finset.univ, x_1 ∉ Finset.filter (fun x_2 => ¬x x_2 = 0) Finset.univ → x x_1 * w x_1 = 0
Theorem: mem_orthSpace_iff'
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 η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∀ x_1 ∈ Finset.univ, x_1 ∉ Finset.filter (fun x_2 => ¬x x_2 = 0) Finset.univ → x x_1 * w x_1 = 0
Tactic:
simp only [Finset.mem_univ, forall_true_left, not_not, Finset.mem_filter, true_and]
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 η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∀ (x_1 : η), x x_1 = 0 → x x_1 * w x_1 = 0
Theorem: mem_orthSpace_iff'
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 η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
w : η → R
hw : w ∈ U
⊢ ∀ (x_1 : η), x x_1 = 0 → x x_1 * w x_1 = 0
Tactic:
exact fun x hx ↦ by simp [hx]
Proof state after:
no goals
Theorem: mem_orthSpace_iff'
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)
inst✝ : Fintype η
h : ∃ y, (∀ w ∈ U, ∑ x ∈ y.support, y x * w x = 0) ∧ Finsupp.lcoeFun y = x
y : η → R
hyU : y ∈ U
⊢ ∑ i : η, x i * y i = 0
Tactic:
obtain ⟨c, hc, rfl⟩ := h
Proof state after:
case refine_1.intro.intro
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ i : η, Finsupp.lcoeFun c i * y i = 0
Theorem: mem_orthSpace_iff'
Proof state before:
case refine_1.intro.intro
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ i : η, Finsupp.lcoeFun c i * y i = 0
Tactic:
simp only [Finsupp.lcoeFun_apply]
Proof state after:
case refine_1.intro.intro
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ x : η, c x * y x = 0
Theorem: mem_orthSpace_iff'
Proof state before:
case refine_1.intro.intro
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ x : η, c x * y x = 0
Tactic:
convert hc y hyU 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
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ x : η, c x * y x = ∑ x ∈ c.support, c x * y x
Theorem: mem_orthSpace_iff'
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
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∑ x : η, c x * y x = ∑ x ∈ c.support, c x * y x
Tactic:
rw [eq_comm, Finset.sum_subset (Finset.subset_univ _)]
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
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∀ x ∈ Finset.univ, x ∉ c.support → c x * y x = 0
Theorem: mem_orthSpace_iff'
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
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∀ x ∈ Finset.univ, x ∉ c.support → c x * y x = 0
Tactic:
simp only [Finset.mem_univ, Finsupp.mem_support_iff, ne_eq, not_not, forall_true_left]
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
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∀ (x : η), c x = 0 → c x * y x = 0
Theorem: mem_orthSpace_iff'
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
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
⊢ ∀ (x : η), c x = 0 → c x * y x = 0
Tactic:
exact fun x hx ↦ by simp [hx]
Proof state after:
no goals
Theorem: mem_orthSpace_iff'
Proof state before:
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
U V : Submodule R (η → R)
inst✝ : Fintype η
y : η → R
hyU : y ∈ U
c : η →₀ R
hc : ∀ w ∈ U, ∑ x ∈ c.support, c x * w x = 0
x : η
hx : c x = 0
⊢ c x * y x = 0
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: mem_orthSpace_iff'
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 η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
⊢ Finsupp.lcoeFun (Finsupp.equivFunOnFinite.invFun x) = x
Tactic:
ext
Proof state after:
case h
α : 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 η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
x✝ : η
⊢ Finsupp.lcoeFun (Finsupp.equivFunOnFinite.invFun x) x✝ = x x✝
Theorem: mem_orthSpace_iff'
Proof state before:
case h
α : 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 η
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
x✝ : η
⊢ Finsupp.lcoeFun (Finsupp.equivFunOnFinite.invFun x) x✝ = x x✝
Tactic:
simp
Proof state after:
no goals
Theorem: mem_orthSpace_iff'
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 η
h : ∀ y ∈ U, ∑ i : η, x✝ i * y i = 0
w : η → R
hw : w ∈ U
x : η
hx : x✝ x = 0
⊢ x✝ x * w x = 0
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: mem_orthSpace_iff''
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)
U : Submodule R (ι → R)
w : ι → R
⊢ w ∈ U.orthSpace ↔ ∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0
Tactic:
simp_rw [orthSpace, mem_map, mem_orthSpace'_iff]
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)
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ y, (∀ x ∈ U, (Finsupp.total ι R R x) y = 0) ∧ Finsupp.lcoeFun y = w) ↔
    ∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0
Theorem: mem_orthSpace_iff''
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)
U : Submodule R (ι → R)
w : ι → R
⊢ (∃ y, (∀ x ∈ U, (Finsupp.total ι R R x) y = 0) ∧ Finsupp.lcoeFun y = w) ↔
    ∃ l, ⇑l = w ∧ ∀ y ∈ U, (Finsupp.total ι R R y) l = 0
Tactic:
aesop
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)
⊢ U.orthSpace = map (Module.piEquiv η R R).symm U.dualAnnihilator
Tactic:
ext x
Proof state after:
case h
α : 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
⊢ x ∈ U.orthSpace ↔ x ∈ map (Module.piEquiv η R R).symm U.dualAnnihilator
Theorem: orthSpace_eq
Proof state before:
case h
α : 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
⊢ x ∈ U.orthSpace ↔ x ∈ map (Module.piEquiv η R R).symm U.dualAnnihilator
Tactic:
simp only [mem_orthSpace_iff', mem_map, mem_dualAnnihilator]
Proof state after:
case h
α : 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
⊢ (∀ y ∈ U, ∑ i : η, x i * y i = 0) ↔ ∃ y, (∀ w ∈ U, y w = 0) ∧ (Module.piEquiv η R R).symm y = x
Theorem: orthSpace_eq
Proof state before:
case h
α : 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
⊢ (∀ y ∈ U, ∑ i : η, x i * y i = 0) ↔ ∃ y, (∀ w ∈ U, y w = 0) ∧ (Module.piEquiv η R R).symm y = x
Tactic:
refine ⟨fun h ↦ ⟨Module.piEquiv η R R x, ?_, by simp⟩, fun h ↦ ?_⟩
Proof state after:
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

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