internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Basis.cl_inter_basis_cl
Proof state before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
h : X ⊆ M.cl (X ∩ I)
hI : M.Indep I
⊢ M.cl X ⊆ M.cl (M.cl X ∩ I)
Tactic:
exact (M.cl_subset_cl_of_subset_cl h).trans (M.cl_subset_cl
  (inter_subset_inter_left _ (h.trans (M.cl_subset_cl inter_subset_left))))
Proof state after:
no goals
Theorem: Equiv.ofInjective_image
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
f : α → β
hf : Injective f
s : Set α
⊢ ↑(⇑(ofInjective f hf) '' s) = f '' s
Tactic:
ext
Proof state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
f : α → β
hf : Injective f
s : Set α
x✝ : β
⊢ x✝ ∈ ↑(⇑(ofInjective f hf) '' s) ↔ x✝ ∈ f '' s
Theorem: Equiv.ofInjective_image
Proof state before:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
f : α → β
hf : Injective f
s : Set α
x✝ : β
⊢ x✝ ∈ ↑(⇑(ofInjective f hf) '' s) ↔ x✝ ∈ f '' s
Tactic:
simp
Proof state after:
no goals
Theorem: Set.embeddingOfSubset_image
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f : ↑s✝ ↪ β
s t : Set α
hst : s ⊆ t
r : Set ↑s
⊢ ⇑(s.embeddingOfSubset t hst) '' r = {x | ↑x ∈ ↑r}
Tactic:
ext ⟨x,h⟩
Proof state after:
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f : ↑s✝ ↪ β
s t : Set α
hst : s ⊆ t
r : Set ↑s
x : α
h : x ∈ t
⊢ ⟨x, h⟩ ∈ ⇑(s.embeddingOfSubset t hst) '' r ↔ ⟨x, h⟩ ∈ {x | ↑x ∈ ↑r}
Theorem: Set.embeddingOfSubset_image
Proof state before:
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f : ↑s✝ ↪ β
s t : Set α
hst : s ⊆ t
r : Set ↑s
x : α
h : x ∈ t
⊢ ⟨x, h⟩ ∈ ⇑(s.embeddingOfSubset t hst) '' r ↔ ⟨x, h⟩ ∈ {x | ↑x ∈ ↑r}
Tactic:
simp [embeddingOfSubset_apply]
Proof state after:
no goals
Theorem: Set.embeddingOfSubset_preimage
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f : ↑s✝ ↪ β
s t : Set α
hst : s ⊆ t
r : Set ↑t
⊢ ⇑(s.embeddingOfSubset t hst) ⁻¹' r = {x | ↑x ∈ ↑r}
Tactic:
ext ⟨x,h⟩
Proof state after:
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f : ↑s✝ ↪ β
s t : Set α
hst : s ⊆ t
r : Set ↑t
x : α
h : x ∈ s
⊢ ⟨x, h⟩ ∈ ⇑(s.embeddingOfSubset t hst) ⁻¹' r ↔ ⟨x, h⟩ ∈ {x | ↑x ∈ ↑r}
Theorem: Set.embeddingOfSubset_preimage
Proof state before:
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f : ↑s✝ ↪ β
s t : Set α
hst : s ⊆ t
r : Set ↑t
x : α
h : x ∈ s
⊢ ⟨x, h⟩ ∈ ⇑(s.embeddingOfSubset t hst) ⁻¹' r ↔ ⟨x, h⟩ ∈ {x | ↑x ∈ ↑r}
Tactic:
simp [hst h, embeddingOfSubset_apply]
Proof state after:
no goals
Theorem: image_val_image_comp_inclusion
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
s : Set α
r : Set ↑s
t t' : Set β
ht : t ⊆ t'
f : ↑s → ↑t
⊢ ↑((fun x => inclusion ht (f x)) '' r) = ↑(f '' r)
Tactic:
simp_rw [image_image, coe_inclusion]
Proof state after:
no goals
Theorem: image_val_range_comp_inclusion
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
s : Set α
t t' : Set β
ht : t ⊆ t'
f : ↑s → ↑t
⊢ ↑(range fun x => inclusion ht (f x)) = ↑(range f)
Tactic:
rw [← image_univ, image_val_image_comp_inclusion]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
s : Set α
t t' : Set β
ht : t ⊆ t'
f : ↑s → ↑t
⊢ ↑((fun x => f x) '' univ) = ↑(range f)
Theorem: image_val_range_comp_inclusion
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
s : Set α
t t' : Set β
ht : t ⊆ t'
f : ↑s → ↑t
⊢ ↑((fun x => f x) '' univ) = ↑(range f)
Tactic:
simp
Proof state after:
no goals
Theorem: Subtype.embeddingInsert_apply_mem
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : ↑(insert a s)
hx : ↑x ∈ s
⊢ (embeddingInsert f ha hb) x = f ⟨↑x, hx⟩
Tactic:
nth_rw 1 [show x = inclusion (subset_insert a s) ⟨x,hx⟩ from rfl]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : ↑(insert a s)
hx : ↑x ∈ s
⊢ (embeddingInsert f ha hb) (inclusion ⋯ ⟨↑x, hx⟩) = f ⟨↑x, hx⟩
Theorem: Subtype.embeddingInsert_apply_mem
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : ↑(insert a s)
hx : ↑x ∈ s
⊢ (embeddingInsert f ha hb) (inclusion ⋯ ⟨↑x, hx⟩) = f ⟨↑x, hx⟩
Tactic:
simp only [embeddingInsert,  Embedding.coeFn_mk]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : ↑(insert a s)
hx : ↑x ∈ s
⊢ extend (inclusion ⋯) (⇑f) (fun x => b) (inclusion ⋯ ⟨↑x, hx⟩) = f ⟨↑x, hx⟩
Theorem: Subtype.embeddingInsert_apply_mem
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : ↑(insert a s)
hx : ↑x ∈ s
⊢ extend (inclusion ⋯) (⇑f) (fun x => b) (inclusion ⋯ ⟨↑x, hx⟩) = f ⟨↑x, hx⟩
Tactic:
rw [(inclusion_injective (subset_insert a s)).extend_apply]
Proof state after:
no goals
Theorem: Subtype.embeddingInsert_apply
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ (embeddingInsert f ha hb) ⟨a, ⋯⟩ = b
Tactic:
simp only [embeddingInsert, Embedding.coeFn_mk]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ extend (inclusion ⋯) (⇑f) (fun x => b) ⟨a, ⋯⟩ = b
Theorem: Subtype.embeddingInsert_apply
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ extend (inclusion ⋯) (⇑f) (fun x => b) ⟨a, ⋯⟩ = b
Tactic:
rw [extend_apply' _ _ _ (by simpa [embeddingOfSubset])]
Proof state after:
no goals
Theorem: Subtype.embeddingInsert_apply
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ ¬∃ a_1, inclusion ⋯ a_1 = ⟨a, ⋯⟩
Tactic:
simpa [embeddingOfSubset]
Proof state after:
no goals
Theorem: Subtype.embeddingInsert_apply'
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : ↑(insert a s)
hx : ↑x ∉ s
⊢ (embeddingInsert f ha hb) x = b
Tactic:
obtain ⟨x, (rfl | h)⟩ := x
Proof state after:
case mk.inl
α : Type u_1
β : Type u_2
γ : Type u_3
b : β
s : Set α
f✝ f : ↑s ↪ β
hb : b ∉ range ⇑f
x : α
ha : x ∉ s
hx : ↑⟨x, ⋯⟩ ∉ s
⊢ (embeddingInsert f ha hb) ⟨x, ⋯⟩ = b

case mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : α
h : x ∈ s
hx : ↑⟨x, ⋯⟩ ∉ s
⊢ (embeddingInsert f ha hb) ⟨x, ⋯⟩ = b
Theorem: Subtype.embeddingInsert_apply'
Proof state before:
case mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : α
h : x ∈ s
hx : ↑⟨x, ⋯⟩ ∉ s
⊢ (embeddingInsert f ha hb) ⟨x, ⋯⟩ = b
Tactic:
exact (hx h).elim
Proof state after:
no goals
Theorem: Subtype.embeddingInsert_apply'
Proof state before:
case mk.inl
α : Type u_1
β : Type u_2
γ : Type u_3
b : β
s : Set α
f✝ f : ↑s ↪ β
hb : b ∉ range ⇑f
x : α
ha : x ∉ s
hx : ↑⟨x, ⋯⟩ ∉ s
⊢ (embeddingInsert f ha hb) ⟨x, ⋯⟩ = b
Tactic:
rw [Subtype.embeddingInsert_apply]
Proof state after:
no goals
Theorem: Subtype.embeddingInsert_apply_eq_ite
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : ↑(insert a s)
inst✝ : DecidablePred fun x => x ∈ s
⊢ (embeddingInsert f ha hb) x = if hx : ↑x ∈ s then f ⟨↑x, hx⟩ else b
Tactic:
split_ifs with h
Proof state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : ↑(insert a s)
inst✝ : DecidablePred fun x => x ∈ s
h : ↑x ∈ s
⊢ (embeddingInsert f ha hb) x = f ⟨↑x, h⟩

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : ↑(insert a s)
inst✝ : DecidablePred fun x => x ∈ s
h : ↑x ∉ s
⊢ (embeddingInsert f ha hb) x = b
Theorem: Subtype.embeddingInsert_apply_eq_ite
Proof state before:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : ↑(insert a s)
inst✝ : DecidablePred fun x => x ∈ s
h : ↑x ∉ s
⊢ (embeddingInsert f ha hb) x = b
Tactic:
rwa [embeddingInsert_apply']
Proof state after:
no goals
Theorem: Subtype.embeddingInsert_apply_eq_ite
Proof state before:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : ↑(insert a s)
inst✝ : DecidablePred fun x => x ∈ s
h : ↑x ∈ s
⊢ (embeddingInsert f ha hb) x = f ⟨↑x, h⟩
Tactic:
rw [embeddingInsert_apply_mem]
Proof state after:
no goals
Theorem: Subtype.range_embeddingInsert
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ range ⇑(embeddingInsert f ha hb) = insert b (range ⇑f)
Tactic:
simp only [embeddingInsert, Embedding.coeFn_mk]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ range (extend (inclusion ⋯) ⇑f fun x => b) = insert b (range ⇑f)
Theorem: Subtype.range_embeddingInsert
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ range (extend (inclusion ⋯) ⇑f fun x => b) = insert b (range ⇑f)
Tactic:
rw [range_extend (inclusion_injective (subset_insert a s)), range_inclusion]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ range ⇑f ∪ (fun x => b) '' {x | ↑x ∈ s}ᶜ = insert b (range ⇑f)
Theorem: Subtype.range_embeddingInsert
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ range ⇑f ∪ (fun x => b) '' {x | ↑x ∈ s}ᶜ = insert b (range ⇑f)
Tactic:
simp_rw [← union_singleton]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ range ⇑f ∪ (fun x => b) '' {x | ↑x ∈ s}ᶜ = range ⇑f ∪ {b}
Theorem: Subtype.range_embeddingInsert
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ range ⇑f ∪ (fun x => b) '' {x | ↑x ∈ s}ᶜ = range ⇑f ∪ {b}
Tactic:
convert rfl
Proof state after:
case h.e'_3.h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ {b} = (fun x => b) '' {x | ↑x ∈ s}ᶜ
Theorem: Subtype.range_embeddingInsert
Proof state before:
case h.e'_3.h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
⊢ {b} = (fun x => b) '' {x | ↑x ∈ s}ᶜ
Tactic:
ext x
Proof state after:
case h.e'_3.h.e'_4.h
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : β
⊢ x ∈ {b} ↔ x ∈ (fun x => b) '' {x | ↑x ∈ s}ᶜ
Theorem: Subtype.range_embeddingInsert
Proof state before:
case h.e'_3.h.e'_4.h
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s : Set α
f✝ f : ↑s ↪ β
ha : a ∉ s
hb : b ∉ range ⇑f
x : β
⊢ x ∈ {b} ↔ x ∈ (fun x => b) '' {x | ↑x ∈ s}ᶜ
Tactic:
simp [ha, eq_comm (a := x)]
Proof state after:
no goals
Theorem: Equiv.subsetEquivSubset_image_val
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
⊢ ↑(⇑(e.subsetEquivSubset has hbt h_eq) '' u) = ↑(⇑e '' (inclusion has '' u))
Tactic:
ext x
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ x ∈ ↑(⇑(e.subsetEquivSubset has hbt h_eq) '' u) ↔ x ∈ ↑(⇑e '' (inclusion has '' u))
Theorem: Equiv.subsetEquivSubset_image_val
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ x ∈ ↑(⇑(e.subsetEquivSubset has hbt h_eq) '' u) ↔ x ∈ ↑(⇑e '' (inclusion has '' u))
Tactic:
simp only [mem_image, mem_image_equiv, Subtype.exists, exists_and_right, exists_eq_right,
  inclusion_mk, Subtype.mk.injEq, exists_and_right, exists_eq_right, exists_and_left,
  subsetEquivSubset, coe_fn_mk, Subtype.mk.injEq, exists_prop]
Proof state after:
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ (x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x) ↔
    ∃ (x_1 : x ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨x, ⋯⟩
Theorem: Equiv.subsetEquivSubset_image_val
Proof state before:
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ (x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x) ↔
    ∃ (x_1 : x ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨x, ⋯⟩
Tactic:
constructor
Proof state after:
case h.mp
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ (x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x) →
    ∃ (x_1 : x ∈ t), ∃ a_2, (∃ (x : a_2 ∈ a), ⟨a_2, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_2 ∈ s), e ⟨a_2, ⋯⟩ = ⟨x, ⋯⟩

case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ (∃ (x_1 : x ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨x, ⋯⟩) →
    x ∈ b ∧ ∃ a_2, ∃ (h : a_2 ∈ a), ⟨a_2, ⋯⟩ ∈ u ∧ ↑(e ⟨a_2, ⋯⟩) = x
Theorem: Equiv.subsetEquivSubset_image_val
Proof state before:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ (∃ (x_1 : x ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨x, ⋯⟩) →
    x ∈ b ∧ ∃ a_2, ∃ (h : a_2 ∈ a), ⟨a_2, ⋯⟩ ∈ u ∧ ↑(e ⟨a_2, ⋯⟩) = x
Tactic:
simp only [forall_exists_index, and_imp]
Proof state after:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ ∀ (x_1 : x ∈ t) (x_2 : α) (x_3 : x_2 ∈ a),
    ⟨x_2, ⋯⟩ ∈ u →
      ∀ (x_4 : x_2 ∈ s), e ⟨x_2, ⋯⟩ = ⟨x, ⋯⟩ → x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x
Theorem: Equiv.subsetEquivSubset_image_val
Proof state before:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ ∀ (x_1 : x ∈ t) (x_2 : α) (x_3 : x_2 ∈ a),
    ⟨x_2, ⋯⟩ ∈ u →
      ∀ (x_4 : x_2 ∈ s), e ⟨x_2, ⋯⟩ = ⟨x, ⋯⟩ → x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x
Tactic:
rintro hxt v hva hvu hvs hvx
Proof state after:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
⊢ x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x
Theorem: Equiv.subsetEquivSubset_image_val
Proof state before:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
⊢ x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x
Tactic:
refine ⟨?_, ⟨v, hva, hvu, by rw [hvx]⟩⟩
Proof state after:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
⊢ x ∈ b
Theorem: Equiv.subsetEquivSubset_image_val
Proof state before:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
⊢ x ∈ b
Tactic:
specialize h_eq ⟨v, hvs⟩
Proof state after:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
h_eq : ↑(e ⟨v, hvs⟩) ∈ b ↔ ↑⟨v, hvs⟩ ∈ a
⊢ x ∈ b
Theorem: Equiv.subsetEquivSubset_image_val
Proof state before:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
h_eq : ↑(e ⟨v, hvs⟩) ∈ b ↔ ↑⟨v, hvs⟩ ∈ a
⊢ x ∈ b
Tactic:
rw [hvx, Subtype.coe_mk, Subtype.coe_mk] at h_eq
Proof state after:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
h_eq : x ∈ b ↔ v ∈ a
⊢ x ∈ b
Theorem: Equiv.subsetEquivSubset_image_val
Proof state before:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
h_eq : x ∈ b ↔ v ∈ a
⊢ x ∈ b
Tactic:
rwa [h_eq]
Proof state after:
no goals
Theorem: Equiv.subsetEquivSubset_image_val
Proof state before:
case h.mp
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ (x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x) →
    ∃ (x_1 : x ∈ t), ∃ a_2, (∃ (x : a_2 ∈ a), ⟨a_2, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_2 ∈ s), e ⟨a_2, ⋯⟩ = ⟨x, ⋯⟩
Tactic:
rintro ⟨hxb, ⟨v, hva, hvu, rfl⟩⟩
Proof state after:
case h.mp.intro.intro.intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hxb : ↑(e ⟨v, ⋯⟩) ∈ b
⊢ ∃ (x : ↑(e ⟨v, ⋯⟩) ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_1 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨↑(e ⟨v, ⋯⟩), ⋯⟩
Theorem: Equiv.subsetEquivSubset_image_val
Proof state before:
case h.mp.intro.intro.intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hxb : ↑(e ⟨v, ⋯⟩) ∈ b
⊢ ∃ (x : ↑(e ⟨v, ⋯⟩) ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_1 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨↑(e ⟨v, ⋯⟩), ⋯⟩
Tactic:
simp [has hva, hva, hvu]
Proof state after:
no goals
Theorem: Equiv.subsetEquivSubset_image_val
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
⊢ ↑(e ⟨v, ⋯⟩) = x
Tactic:
rw [hvx]
Proof state after:
no goals
Theorem: Module.piEquiv_apply_symm
Proof state before:
α : Type u_1
R : Type u_2
η : Type u_3
ι : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype α
inst✝ : DecidableEq α
y : Dual R (α → R)
i : α
⊢ (piEquiv α R R).symm y i = y (Pi.single i 1)
Tactic:
simp only [piEquiv, Basis.constr, Pi.basisFun_apply, LinearMap.stdBasis_apply,
  LinearEquiv.coe_symm_mk]
Proof state after:
α : Type u_1
R : Type u_2
η : Type u_3
ι : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype α
inst✝ : DecidableEq α
y : Dual R (α → R)
i : α
⊢ y (update 0 i 1) = y (Pi.single i 1)
Theorem: Module.piEquiv_apply_symm
Proof state before:
α : Type u_1
R : Type u_2
η : Type u_3
ι : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype α
inst✝ : DecidableEq α
y : Dual R (α → R)
i : α
⊢ y (update 0 i 1) = y (Pi.single i 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Module.Dual.sum_update
Proof state before:
α : Type u_1
R : Type u_2
η : Type u_3
ι : Type u_4
inst✝² : Field R
inst✝¹ : Fintype α
inst✝ : DecidableEq α
y : Dual R (α → R)
x : α → R
⊢ ∑ i : α, y (update 0 i 1) * x i = y x
Tactic:
rw [← LinearMap.congr_fun ((Pi.basisFun R α).sum_dual_apply_smul_coord y) x]
Proof state after:
α : Type u_1
R : Type u_2
η : Type u_3
ι : Type u_4
inst✝² : Field R
inst✝¹ : Fintype α
inst✝ : DecidableEq α
y : Dual R (α → R)
x : α → R
⊢ ∑ i : α, y (update 0 i 1) * x i = (∑ x : α, y ((Pi.basisFun R α) x) • (Pi.basisFun R α).coord x) x
Theorem: Module.Dual.sum_update
Proof state before:
α : Type u_1
R : Type u_2
η : Type u_3
ι : Type u_4
inst✝² : Field R
inst✝¹ : Fintype α
inst✝ : DecidableEq α
y : Dual R (α → R)
x : α → R
⊢ ∑ i : α, y (update 0 i 1) * x i = (∑ x : α, y ((Pi.basisFun R α) x) • (Pi.basisFun R α).coord x) x
Tactic:
simp [LinearMap.stdBasis_apply]
Proof state after:
no goals
Theorem: Function.ExtendByZero.linearMap_injective
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
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
⊢ Injective ⇑(linearMap R s)
Tactic:
intro x x' h
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 α
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'
⊢ x = x'
Theorem: Function.ExtendByZero.linearMap_injective
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
ι η : Type u_7
inst✝ : Semiring R
s : ι → η
hs : Injective s
x x' : ι → R
h : (linearMap R s) x = (linearMap R s) x'
⊢ 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
ι η : 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