internlm/Lean-Github huggingface dataset:
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
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, ⋯⟩ = 0
Tactic:
simp only [Finsupp.total_mapDomain, and_imp]
Proof state after:
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 (↑s) K K (x ∘ s.incl)) l = 0
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
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 (↑s) K K (x ∘ s.incl)) l = 0
Tactic:
exact fun _ _ hyU ↦ hl _ hyU
Proof state after:
no goals
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
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
Tactic:
rintro ⟨l, rfl, h⟩
Proof state after:
case h.refine_1.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 K (↑s → K)
l : ↥(Finsupp.supported K K s)
h : ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
⊢ support ⇑↑l ⊆ s ∧ ∃ l_1, ⇑l_1 = s.restrict ⇑↑l ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l_1 = 0
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_1.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 K (↑s → K)
l : ↥(Finsupp.supported K K s)
h : ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
⊢ support ⇑↑l ⊆ s ∧ ∃ l_1, ⇑l_1 = s.restrict ⇑↑l ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l_1 = 0
Tactic:
rw [Finsupp.fun_support_eq]
Proof state after:
case h.refine_1.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 K (↑s → K)
l : ↥(Finsupp.supported K K s)
h : ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
⊢ ↑(↑l).support ⊆ s ∧ ∃ l_1, ⇑l_1 = s.restrict ⇑↑l ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l_1 = 0
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_1.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 K (↑s → K)
l : ↥(Finsupp.supported K K s)
h : ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
⊢ ↑(↑l).support ⊆ s ∧ ∃ l_1, ⇑l_1 = s.restrict ⇑↑l ∧ ∀ y ∈ U, (Finsupp.total (↑s) K K y) l_1 = 0
Tactic:
refine ⟨l.2, Finsupp.restrictSupportEquiv s _ l, ?_, fun y hy ↦ ?_⟩
Proof state after:
case h.refine_1.intro.intro.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)
l : ↥(Finsupp.supported K K s)
h : ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
⊢ ⇑((Finsupp.restrictSupportEquiv s K) l) = s.restrict ⇑↑l

case h.refine_1.intro.intro.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)
l : ↥(Finsupp.supported K K s)
h : ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
y : ↑s → K
hy : y ∈ U
⊢ (Finsupp.total (↑s) K K y) ((Finsupp.restrictSupportEquiv s K) l) = 0
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_1.intro.intro.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)
l : ↥(Finsupp.supported K K s)
h : ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
y : ↑s → K
hy : y ∈ U
⊢ (Finsupp.total (↑s) K K y) ((Finsupp.restrictSupportEquiv s K) l) = 0
Tactic:
specialize h (LinearMap.extendSubtype K s y)
Proof state after:
case h.refine_1.intro.intro.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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h :
  support ((LinearMap.extendSubtype K s) y) ⊆ s ∧ s.restrict ((LinearMap.extendSubtype K s) y) ∈ U →
    (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
⊢ (Finsupp.total (↑s) K K y) ((Finsupp.restrictSupportEquiv s K) l) = 0
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_1.intro.intro.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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h :
  support ((LinearMap.extendSubtype K s) y) ⊆ s ∧ s.restrict ((LinearMap.extendSubtype K s) y) ∈ U →
    (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
⊢ (Finsupp.total (↑s) K K y) ((Finsupp.restrictSupportEquiv s K) l) = 0
Tactic:
simp only [LinearMap.extendSubtype_restrict, hy, and_true,
  LinearMap.extendSubtype_support_subset, forall_true_left] at h
Proof state after:
case h.refine_1.intro.intro.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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
⊢ (Finsupp.total (↑s) K K y) ((Finsupp.restrictSupportEquiv s K) l) = 0
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_1.intro.intro.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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
⊢ (Finsupp.total (↑s) K K y) ((Finsupp.restrictSupportEquiv s K) l) = 0
Tactic:
convert h
Proof state after:
case h.e'_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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
⊢ (Finsupp.total (↑s) K K y) ((Finsupp.restrictSupportEquiv s K) l) =
    (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.e'_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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
⊢ (Finsupp.total (↑s) K K y) ((Finsupp.restrictSupportEquiv s K) l) =
    (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l
Tactic:
simp only [Finsupp.restrictSupportEquiv, Equiv.coe_fn_mk, Finsupp.total_apply, Finsupp.sum,
  Finsupp.subtypeDomain_apply, smul_eq_mul]
Proof state after:
case h.e'_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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
⊢ ∑ x ∈ (Finsupp.subtypeDomain (fun x => x ∈ s) ↑l).support, ↑l ↑x * y x =
    ∑ x ∈ (↑l).support, ↑l x * (LinearMap.extendSubtype K s) y x
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.e'_3.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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
⊢ (↑l).support = Finset.map (Embedding.subtype fun x => x ∈ s) (Finsupp.subtypeDomain (fun x => x ∈ s) ↑l).support
Tactic:
ext i
Proof state after:
case h.e'_3.h.a
α : 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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
i : ι
⊢ i ∈ (↑l).support ↔
    i ∈ Finset.map (Embedding.subtype fun x => x ∈ s) (Finsupp.subtypeDomain (fun x => x ∈ s) ↑l).support
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.e'_3.h.a
α : 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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
i : ι
⊢ i ∈ (↑l).support ↔
    i ∈ Finset.map (Embedding.subtype fun x => x ∈ s) (Finsupp.subtypeDomain (fun x => x ∈ s) ↑l).support
Tactic:
simp only [Finsupp.mem_support_iff, ne_eq, Finset.mem_map, Finsupp.subtypeDomain_apply,
  Embedding.coe_subtype, Subtype.exists, exists_and_left, exists_prop, exists_eq_right_right,
  iff_self_and]
Proof state after:
case h.e'_3.h.a
α : 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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
i : ι
⊢ ¬↑l i = 0 → i ∈ s
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.e'_3.h.a
α : 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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
i : ι
⊢ ¬↑l i = 0 → i ∈ s
Tactic:
rw [not_imp_comm]
Proof state after:
case h.e'_3.h.a
α : 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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
i : ι
⊢ i ∉ s → ↑l i = 0
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.e'_3.h.a
α : 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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
i : ι
⊢ i ∉ s → ↑l i = 0
Tactic:
exact (Finsupp.mem_supported' _ _).1 l.2 _
Proof state after:
no goals
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_1.intro.intro.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)
l : ↥(Finsupp.supported K K s)
h : ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
⊢ ⇑((Finsupp.restrictSupportEquiv s K) l) = s.restrict ⇑↑l
Tactic:
ext
Proof state after:
case h.refine_1.intro.intro.refine_1.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)
l : ↥(Finsupp.supported K K s)
h : ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
x✝ : ↑s
⊢ ((Finsupp.restrictSupportEquiv s K) l) x✝ = s.restrict (⇑↑l) x✝
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_1.intro.intro.refine_1.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)
l : ↥(Finsupp.supported K K s)
h : ∀ (x : ι → K), support x ⊆ s ∧ s.restrict x ∈ U → (Finsupp.total ι K K x) ↑l = 0
x✝ : ↑s
⊢ ((Finsupp.restrictSupportEquiv s K) l) x✝ = s.restrict (⇑↑l) x✝
Tactic:
simp [Finsupp.restrictSupportEquiv]
Proof state after:
no goals
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.e'_2.a
α : 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)
l : ↥(Finsupp.supported K K s)
y : ↑s → K
hy : y ∈ U
h : (Finsupp.total ι K K ((LinearMap.extendSubtype K s) y)) ↑l = 0
x✝ : ↑s
a✝ : x✝ ∈ (Finsupp.subtypeDomain (fun x => x ∈ s) ↑l).support
⊢ ↑l ↑x✝ * y x✝ =
    ↑l ((Embedding.subtype fun x => x ∈ s) x✝) * (LinearMap.extendSubtype K s) y ((Embedding.subtype fun x => x ∈ s) x✝)
Tactic:
simp only [Embedding.coe_subtype, LinearMap.extendSubtype_apply]
Proof state after:
no goals
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
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
Tactic:
rw [Finsupp.mem_supported']
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
⊢ ∀ x ∉ s, (Finsupp.mapDomain s.incl l) x = 0
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
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
⊢ ∀ x ∉ s, (Finsupp.mapDomain s.incl l) x = 0
Tactic:
intro i hi
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
i : ι
hi : i ∉ s
⊢ (Finsupp.mapDomain s.incl l) i = 0
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
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
i : ι
hi : i ∉ s
⊢ (Finsupp.mapDomain s.incl l) i = 0
Tactic:
rw [Finsupp.mapDomain_notin_range _ _ (by 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)
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
i : ι
hi : i ∉ s
⊢ i ∉ range s.incl
Tactic:
simpa
Proof state after:
no goals
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
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, ⋯⟩ = x
Tactic:
ext i
Proof state after:
case h.refine_2.refine_2.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✝ : 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
i : ι
⊢ ↑⟨Finsupp.mapDomain s.incl l, ⋯⟩ i = x i
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_2.refine_2.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✝ : 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
i : ι
⊢ ↑⟨Finsupp.mapDomain s.incl l, ⋯⟩ i = x i
Tactic:
simp only
Proof state after:
case h.refine_2.refine_2.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✝ : 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
i : ι
⊢ (Finsupp.mapDomain s.incl l) i = x i
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_2.refine_2.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✝ : 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
i : ι
⊢ (Finsupp.mapDomain s.incl l) i = x i
Tactic:
obtain (his | his) := em (i ∈ s)
Proof state after:
case h.refine_2.refine_2.h.inl
α : 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
i : ι
his : i ∈ s
⊢ (Finsupp.mapDomain s.incl l) i = x i

case h.refine_2.refine_2.h.inr
α : 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
i : ι
his : i ∉ s
⊢ (Finsupp.mapDomain s.incl l) i = x i
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_2.refine_2.h.inr
α : 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
i : ι
his : i ∉ s
⊢ (Finsupp.mapDomain s.incl l) i = x i
Tactic:
rw [Finsupp.mapDomain_notin_range, eq_comm]
Proof state after:
case h.refine_2.refine_2.h.inr
α : 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
i : ι
his : i ∉ s
⊢ x i = 0

case h.refine_2.refine_2.h.inr.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✝ : 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
i : ι
his : i ∉ s
⊢ i ∉ range s.incl
Theorem: Set.relOrthSpace_subtypeFunEquiv
Proof state before:
case h.refine_2.refine_2.h.inr.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✝ : 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
i : ι
his : i ∉ s
⊢ i ∉ range s.incl
Tactic:
simpa
Proof state after:
no goals