internlm/Lean-Github huggingface dataset:
Theorem: Function.ExtendByZero.linearMap_injective
Proof state before:
case h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
h : (linearMap R s) x = (linearMap R s) x'
i : ι
⊢ x i = x' i
Tactic:
replace h := _root_.congr_fun h (s i)
Proof state after:
case h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
i : ι
h : (linearMap R s) x (s i) = (linearMap R s) x' (s i)
⊢ x i = x' i
Theorem: Function.ExtendByZero.linearMap_injective
Proof state before:
case h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
i : ι
h : (linearMap R s) x (s i) = (linearMap R s) x' (s i)
⊢ x i = x' i
Tactic:
simp only [linearMap_apply, exists_apply_eq_apply, not_true] at h
Proof state after:
case h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
i : ι
h : extend s x 0 (s i) = extend s x' 0 (s i)
⊢ x i = x' i
Theorem: Function.ExtendByZero.linearMap_injective
Proof state before:
case h
α : Type u_1
R✝¹ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
i : ι
h : extend s x 0 (s i) = extend s x' 0 (s i)
⊢ x i = x' i
Tactic:
rwa [hs.extend_apply, hs.extend_apply] at h
Proof state after:
no goals
Theorem: LinearMap.extendSubtype_apply
Proof state before:
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set α
f : ↑s → R
y : ↑s
⊢ (extendSubtype R s) f ↑y = f y
Tactic:
rw [extendSubtype, Function.ExtendByZero.linearMap_apply, Subtype.coe_injective.extend_apply]
Proof state after:
no goals
Theorem: LinearMap.extendSubtype_apply_not_mem
Proof state before:
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set α
f : ↑s → R
i : α
hi : i ∉ s
⊢ (extendSubtype R s) f i = 0
Tactic:
rw [extendSubtype, ExtendByZero.linearMap_apply, extend_apply', Pi.zero_apply]
Proof state after:
case hb
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set α
f : ↑s → R
i : α
hi : i ∉ s
⊢ ¬∃ a, s.incl a = i
Theorem: LinearMap.extendSubtype_apply_not_mem
Proof state before:
case hb
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set α
f : ↑s → R
i : α
hi : i ∉ s
⊢ ¬∃ a, s.incl a = i
Tactic:
rintro ⟨a, rfl⟩
Proof state after:
case hb.intro
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set α
f : ↑s → R
a : ↑s
hi : s.incl a ∉ s
⊢ False
Theorem: LinearMap.extendSubtype_apply_not_mem
Proof state before:
case hb.intro
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set α
f : ↑s → R
a : ↑s
hi : s.incl a ∉ s
⊢ False
Tactic:
exact hi a.2
Proof state after:
no goals
Theorem: LinearMap.extendSubtype_eq_ite
Proof state before:
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝² : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝¹ : Semiring R
s : Set η
x : ↑s → R
inst✝ : DecidablePred fun x => x ∈ s
⊢ (extendSubtype R s) x = fun i => if h : i ∈ s then x ⟨i, h⟩ else 0
Tactic:
ext i
Proof state after:
case h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝² : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝¹ : Semiring R
s : Set η
x : ↑s → R
inst✝ : DecidablePred fun x => x ∈ s
i : η
⊢ (extendSubtype R s) x i = if h : i ∈ s then x ⟨i, h⟩ else 0
Theorem: LinearMap.extendSubtype_eq_ite
Proof state before:
case h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝² : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝¹ : Semiring R
s : Set η
x : ↑s → R
inst✝ : DecidablePred fun x => x ∈ s
i : η
⊢ (extendSubtype R s) x i = if h : i ∈ s then x ⟨i, h⟩ else 0
Tactic:
split_ifs with h
Proof state after:
case pos
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝² : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝¹ : Semiring R
s : Set η
x : ↑s → R
inst✝ : DecidablePred fun x => x ∈ s
i : η
h : i ∈ s
⊢ (extendSubtype R s) x i = x ⟨i, h⟩

case neg
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝² : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝¹ : Semiring R
s : Set η
x : ↑s → R
inst✝ : DecidablePred fun x => x ∈ s
i : η
h : i ∉ s
⊢ (extendSubtype R s) x i = 0
Theorem: LinearMap.extendSubtype_eq_ite
Proof state before:
case neg
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝² : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝¹ : Semiring R
s : Set η
x : ↑s → R
inst✝ : DecidablePred fun x => x ∈ s
i : η
h : i ∉ s
⊢ (extendSubtype R s) x i = 0
Tactic:
exact extendSubtype_apply_not_mem _ h
Proof state after:
no goals
Theorem: LinearMap.extendSubtype_eq_ite
Proof state before:
case pos
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝² : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝¹ : Semiring R
s : Set η
x : ↑s → R
inst✝ : DecidablePred fun x => x ∈ s
i : η
h : i ∈ s
⊢ (extendSubtype R s) x i = x ⟨i, h⟩
Tactic:
exact extendSubtype_apply x ⟨i,h⟩
Proof state after:
no goals
Theorem: LinearMap.extendSubtype_restrict
Proof state before:
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
⊢ s.restrict ((extendSubtype R s) x) = x
Tactic:
ext
Proof state after:
case h
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
x✝ : ↑s
⊢ s.restrict ((extendSubtype R s) x) x✝ = x x✝
Theorem: LinearMap.extendSubtype_restrict
Proof state before:
case h
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
x✝ : ↑s
⊢ s.restrict ((extendSubtype R s) x) x✝ = x x✝
Tactic:
simp
Proof state after:
no goals
Theorem: LinearMap.extendSubtype_support_subset
Proof state before:
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
⊢ support ((extendSubtype R s) x) ⊆ s
Tactic:
classical
refine fun i (hi : _ ≠ 0) ↦ by_contra fun his ↦ ?_
simp_rw [LinearMap.extendSubtype_eq_ite, dif_neg his] at hi
exact hi rfl
Proof state after:
no goals
Theorem: LinearMap.extendSubtype_support_subset
Proof state before:
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
⊢ support ((extendSubtype R s) x) ⊆ s
Tactic:
refine fun i (hi : _ ≠ 0) ↦ by_contra fun his ↦ ?_
Proof state after:
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
i : α
hi : (extendSubtype R s) x i ≠ 0
his : i ∉ s
⊢ False
Theorem: LinearMap.extendSubtype_support_subset
Proof state before:
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
i : α
hi : (extendSubtype R s) x i ≠ 0
his : i ∉ s
⊢ False
Tactic:
simp_rw [LinearMap.extendSubtype_eq_ite, dif_neg his] at hi
Proof state after:
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
i : α
his : i ∉ s
hi : 0 ≠ 0
⊢ False
Theorem: LinearMap.extendSubtype_support_subset
Proof state before:
α : Type u_1
R✝ : Type u_2
η : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Semiring R
s : Set α
x : ↑s → R
i : α
his : i ∉ s
hi : 0 ≠ 0
⊢ False
Tactic:
exact hi rfl
Proof state after:
no goals
Theorem: LinearMap.funSubtype_extendSubtype
Proof state before:
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set α
⊢ funSubtype R s ∘ₗ extendSubtype R s = id
Tactic:
ext
Proof state after:
case h.h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set α
x✝¹ : ↑s → R
x✝ : ↑s
⊢ (funSubtype R s ∘ₗ extendSubtype R s) x✝¹ x✝ = id x✝¹ x✝
Theorem: LinearMap.funSubtype_extendSubtype
Proof state before:
case h.h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set α
x✝¹ : ↑s → R
x✝ : ↑s
⊢ (funSubtype R s ∘ₗ extendSubtype R s) x✝¹ x✝ = id x✝¹ x✝
Tactic:
simp
Proof state after:
no goals
Theorem: LinearMap.funSubtype_extendSubtype_apply
Proof state before:
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set α
x : ↑s → R
⊢ (funSubtype R s) ((extendSubtype R s) x) = x
Tactic:
ext
Proof state after:
case h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set α
x : ↑s → R
x✝ : ↑s
⊢ (funSubtype R s) ((extendSubtype R s) x) x✝ = x x✝
Theorem: LinearMap.funSubtype_extendSubtype_apply
Proof state before:
case h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set α
x : ↑s → R
x✝ : ↑s
⊢ (funSubtype R s) ((extendSubtype R s) x) x✝ = x x✝
Tactic:
simp
Proof state after:
no goals
Theorem: LinearMap.extendSubtype_funSubtype_apply
Proof state before:
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
⊢ (extendSubtype R s) ((funSubtype R s) x) = x
Tactic:
classical
ext i
simp only [extendSubtype_eq_ite, fun_Subtype_apply, dite_eq_ite, ite_eq_left_iff]
exact fun his ↦ Eq.symm <| by simpa using mt (support_subset_iff.1 hx i) his
Proof state after:
no goals
Theorem: LinearMap.extendSubtype_funSubtype_apply
Proof state before:
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
⊢ (extendSubtype R s) ((funSubtype R s) x) = x
Tactic:
ext i
Proof state after:
case h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
i : η
⊢ (extendSubtype R s) ((funSubtype R s) x) i = x i
Theorem: LinearMap.extendSubtype_funSubtype_apply
Proof state before:
case h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
i : η
⊢ (extendSubtype R s) ((funSubtype R s) x) i = x i
Tactic:
simp only [extendSubtype_eq_ite, fun_Subtype_apply, dite_eq_ite, ite_eq_left_iff]
Proof state after:
case h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
i : η
⊢ i ∉ s → 0 = x i
Theorem: LinearMap.extendSubtype_funSubtype_apply
Proof state before:
case h
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
i : η
⊢ i ∉ s → 0 = x i
Tactic:
exact fun his ↦ Eq.symm <| by simpa using mt (support_subset_iff.1 hx i) his
Proof state after:
no goals
Theorem: LinearMap.extendSubtype_funSubtype_apply
Proof state before:
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s : Set η
x : η → R
hx : support x ⊆ s
i : η
his : i ∉ s
⊢ x i = 0
Tactic:
simpa using mt (support_subset_iff.1 hx i) his
Proof state after:
no goals
Theorem: LinearMap.extendSubset_apply
Proof state before:
α : Type u_1
R✝¹ : Type u_2
η : Type u_3
ι : Type u_4
R✝ : Type u_5
inst✝¹ : Semiring R✝
s✝ : Set α
R : Type u_6
inst✝ : Semiring R
s t : Set α
hst : s ⊆ t
f : ↑s → R
x : ↑s
⊢ (extendSubset R hst) f (Set.inclusion hst x) = f x
Tactic:
rw [extendSubset, Function.ExtendByZero.linearMap_apply, (inclusion_injective hst).extend_apply]
Proof state after:
no goals
Theorem: mem_supportedFun_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
⊢ x ∈ s.supportedFun R ↔ support x ⊆ s
Tactic:
simp only [supportedFun, LinearMap.mem_range, ne_eq]
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
⊢ (∃ y, (LinearMap.extendSubtype R s) y = x) ↔ support x ⊆ s
Theorem: mem_supportedFun_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
⊢ (∃ y, (LinearMap.extendSubtype R s) y = x) ↔ support x ⊆ s
Tactic:
refine ⟨?_, fun h ↦ ?_⟩
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
⊢ (∃ y, (LinearMap.extendSubtype R s) y = x) → support x ⊆ s

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
h : support x ⊆ s
⊢ ∃ y, (LinearMap.extendSubtype R s) y = x
Theorem: mem_supportedFun_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
h : support x ⊆ s
⊢ ∃ y, (LinearMap.extendSubtype R s) y = x
Tactic:
exact ⟨LinearMap.funSubtype R s x, LinearMap.extendSubtype_funSubtype_apply h⟩
Proof state after:
no goals
Theorem: mem_supportedFun_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
⊢ (∃ y, (LinearMap.extendSubtype R s) y = x) → support x ⊆ s
Tactic:
rintro ⟨y, rfl⟩ i hi
Proof state after:
case refine_1.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 η
y : ↑s → R
i : η
hi : i ∈ support ((LinearMap.extendSubtype R s) y)
⊢ i ∈ s
Theorem: mem_supportedFun_iff
Proof state before:
case refine_1.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 η
y : ↑s → R
i : η
hi : i ∈ support ((LinearMap.extendSubtype R s) y)
⊢ i ∈ s
Tactic:
simp only [mem_support, ne_eq, LinearMap.extendSubtype_eq_ite, dite_eq_right_iff,
  not_forall] at hi
Proof state after:
case refine_1.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 η
y : ↑s → R
i : η
hi : ∃ (x : i ∈ s), ¬y ⟨i, x⟩ = 0
⊢ i ∈ s
Theorem: mem_supportedFun_iff
Proof state before:
case refine_1.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 η
y : ↑s → R
i : η
hi : ∃ (x : i ∈ s), ¬y ⟨i, x⟩ = 0
⊢ i ∈ s
Tactic:
obtain ⟨h,-⟩ := hi
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 η
y : ↑s → R
i : η
h : i ∈ s
⊢ i ∈ s
Theorem: mem_supportedFun_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 η
y : ↑s → R
i : η
h : i ∈ s
⊢ i ∈ s
Tactic:
exact h
Proof state after:
no goals
Theorem: supportedFun_univ
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✝
R : Type u_7
η : Type u_8
inst✝ : Semiring R
⊢ univ.supportedFun R = ⊤
Tactic:
ext
Proof state after:
case 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✝
R : Type u_7
η : Type u_8
inst✝ : Semiring R
x✝ : η → R
⊢ x✝ ∈ univ.supportedFun R ↔ x✝ ∈ ⊤
Theorem: supportedFun_univ
Proof state before:
case 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✝
R : Type u_7
η : Type u_8
inst✝ : Semiring R
x✝ : η → R
⊢ x✝ ∈ univ.supportedFun R ↔ x✝ ∈ ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: supportedFun_empty
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✝
R : Type u_7
η : Type u_8
inst✝ : Semiring R
⊢ ∅.supportedFun R = ⊥
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
η✝ : Type u_6
inst✝¹ : Semiring R✝
s : Set η✝
x✝ : η✝ → R✝
R : Type u_7
η : Type u_8
inst✝ : Semiring R
x : η → R
⊢ x ∈ ∅.supportedFun R ↔ x ∈ ⊥
Theorem: supportedFun_empty
Proof state before:
case 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✝
R : Type u_7
η : Type u_8
inst✝ : Semiring R
x : η → R
⊢ x ∈ ∅.supportedFun R ↔ x ∈ ⊥
Tactic:
simp only [mem_supportedFun_iff, support_subset_iff, ne_eq, mem_empty_iff_false, mem_bot,
  imp_false, not_not]
Proof state after:
case 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✝
R : Type u_7
η : Type u_8
inst✝ : Semiring R
x : η → R
⊢ (∀ (x_1 : η), x x_1 = 0) ↔ x = 0
Theorem: supportedFun_empty
Proof state before:
case 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✝
R : Type u_7
η : Type u_8
inst✝ : Semiring R
x : η → R
⊢ (∀ (x_1 : η), x x_1 = 0) ↔ x = 0
Tactic:
exact Iff.symm funext_iff
Proof state after:
no goals
Theorem: Set.supportedFunEquiv_apply_symm
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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : ↥(s.supportedFun R)
⊢ (s.supportedFunEquiv R).symm x = (LinearMap.funSubtype R s) ↑x
Tactic:
classical
obtain ⟨x, hx⟩ := x
rw [(s.supportedFunEquiv R).symm_apply_eq]
ext i
simp only [supportedFunEquiv_apply, LinearMap.extendSubtype_eq_ite, LinearMap.fun_Subtype_apply,
  dite_eq_ite]
rw [eq_comm, ite_eq_left_iff, not_imp_comm, eq_comm]
rw [mem_supportedFun_iff, support_subset_iff] at hx
apply hx
Proof state after:
no goals
Theorem: Set.supportedFunEquiv_apply_symm
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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : ↥(s.supportedFun R)
⊢ (s.supportedFunEquiv R).symm x = (LinearMap.funSubtype R s) ↑x
Tactic:
obtain ⟨x, hx⟩ := x
Proof state after:
case mk
α : 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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
⊢ (s.supportedFunEquiv R).symm ⟨x, hx⟩ = (LinearMap.funSubtype R s) ↑⟨x, hx⟩
Theorem: Set.supportedFunEquiv_apply_symm
Proof state before:
case mk
α : 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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
⊢ (s.supportedFunEquiv R).symm ⟨x, hx⟩ = (LinearMap.funSubtype R s) ↑⟨x, hx⟩
Tactic:
rw [(s.supportedFunEquiv R).symm_apply_eq]
Proof state after:
case mk
α : 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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
⊢ ⟨x, hx⟩ = (s.supportedFunEquiv R) ((LinearMap.funSubtype R s) ↑⟨x, hx⟩)
Theorem: Set.supportedFunEquiv_apply_symm
Proof state before:
case mk
α : 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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
⊢ ⟨x, hx⟩ = (s.supportedFunEquiv R) ((LinearMap.funSubtype R s) ↑⟨x, hx⟩)
Tactic:
ext i
Proof state after:
case mk.a.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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ ↑⟨x, hx⟩ i = ↑((s.supportedFunEquiv R) ((LinearMap.funSubtype R s) ↑⟨x, hx⟩)) i
Theorem: Set.supportedFunEquiv_apply_symm
Proof state before:
case mk.a.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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ ↑⟨x, hx⟩ i = ↑((s.supportedFunEquiv R) ((LinearMap.funSubtype R s) ↑⟨x, hx⟩)) i
Tactic:
simp only [supportedFunEquiv_apply, LinearMap.extendSubtype_eq_ite, LinearMap.fun_Subtype_apply,
  dite_eq_ite]
Proof state after:
case mk.a.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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ x i = if i ∈ s then x i else 0
Theorem: Set.supportedFunEquiv_apply_symm
Proof state before:
case mk.a.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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ x i = if i ∈ s then x i else 0
Tactic:
rw [eq_comm, ite_eq_left_iff, not_imp_comm, eq_comm]
Proof state after:
case mk.a.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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ ¬x i = 0 → i ∈ s
Theorem: Set.supportedFunEquiv_apply_symm
Proof state before:
case mk.a.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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : x ∈ s.supportedFun R
i : η
⊢ ¬x i = 0 → i ∈ s
Tactic:
rw [mem_supportedFun_iff, support_subset_iff] at hx
Proof state after:
case mk.a.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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
i : η
⊢ ¬x i = 0 → i ∈ s
Theorem: Set.supportedFunEquiv_apply_symm
Proof state before:
case mk.a.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✝
s : Set η
R : Type u_7
inst✝ : Semiring R
x : η → R
hx : ∀ (x_1 : η), x x_1 ≠ 0 → x_1 ∈ s
i : η
⊢ ¬x i = 0 → i ∈ s
Tactic:
apply hx
Proof state after:
no goals
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 ∈ ↑((s.subtypeFunEquiv R) U) ↔ support x ⊆ s ∧ s.restrict x ∈ U
Tactic:
change (x ∈ (MapSubtype.relIso _ _).1 ↔ _)
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)
⊢ 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