internlm/Lean-Github huggingface dataset:
Theorem: Set.update_injOn_iff
Proof state before:
case refine_2
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn (update f a b) s
⊢ a ∈ s → ∀ x ∈ s, f x = b → x = a
Tactic:
rintro has x hxs rfl
Proof state after:
case refine_2
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
⊢ x = a
Theorem: Set.update_injOn_iff
Proof state before:
case refine_2
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
⊢ x = a
Tactic:
by_contra! hne
Proof state after:
case refine_2
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
hne : x ≠ a
⊢ False
Theorem: Set.update_injOn_iff
Proof state before:
case refine_2
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
hne : x ≠ a
⊢ False
Tactic:
have h' := h hxs has
Proof state after:
case refine_2
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
hne : x ≠ a
h' : update f a (f x) x = update f a (f x) a → x = a
⊢ False
Theorem: Set.update_injOn_iff
Proof state before:
case refine_2
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
hne : x ≠ a
h' : update f a (f x) x = update f a (f x) a → x = a
⊢ False
Tactic:
rw [update_noteq hne, update_same] at h'
Proof state after:
case refine_2
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
hne : x ≠ a
h' : f x = f x → x = a
⊢ False
Theorem: Set.update_injOn_iff
Proof state before:
case refine_2
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a✝ : α
b : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
hne : x ≠ a
h' : f x = f x → x = a
⊢ False
Tactic:
exact hne <| h' rfl
Proof state after:
no goals
Theorem: Set.update_injOn_iff
Proof state before:
case refine_3.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : update f x b x = update f x b y
⊢ x = y
Tactic:
by_contra! hne
Proof state after:
case refine_3.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : update f x b x = update f x b y
hne : x ≠ y
⊢ False
Theorem: Set.update_injOn_iff
Proof state before:
case refine_3.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : update f x b x = update f x b y
hne : x ≠ y
⊢ False
Tactic:
rw [update_same, update_noteq hne.symm] at hxy
Proof state after:
case refine_3.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : b = f y
hne : x ≠ y
⊢ False
Theorem: Set.update_injOn_iff
Proof state before:
case refine_3.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : b = f y
hne : x ≠ y
⊢ False
Tactic:
exact hne.symm <| h.2 hx y hy hxy.symm
Proof state after:
no goals
Theorem: Set.update_injOn_iff
Proof state before:
case refine_3.inr.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {y}) ∧ (y ∈ s → ∀ x ∈ s, f x = b → x = y)
hxy : update f y b x = update f y b y
hxa : x ≠ y
⊢ x = y
Tactic:
rw [update_noteq hxa, update_same] at hxy
Proof state after:
case refine_3.inr.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {y}) ∧ (y ∈ s → ∀ x ∈ s, f x = b → x = y)
hxy : f x = b
hxa : x ≠ y
⊢ x = y
Theorem: Set.update_injOn_iff
Proof state before:
case refine_3.inr.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {y}) ∧ (y ∈ s → ∀ x ∈ s, f x = b → x = y)
hxy : f x = b
hxa : x ≠ y
⊢ x = y
Tactic:
exact h.2 hy x hx hxy
Proof state after:
no goals
Theorem: Set.update_id_injOn_iff
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b✝ : β
a b : α
s : Set α
⊢ InjOn (update id a b) s ↔ a ∈ s → b ∈ s → a = b
Tactic:
rw [update_injOn_iff, and_iff_right injective_id.injOn]
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b✝ : β
a b : α
s : Set α
⊢ (a ∈ s → ∀ x ∈ s, id x = b → x = a) ↔ a ∈ s → b ∈ s → a = b
Theorem: Set.update_id_injOn_iff
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b✝ : β
a b : α
s : Set α
⊢ (a ∈ s → ∀ x ∈ s, id x = b → x = a) ↔ a ∈ s → b ∈ s → a = b
Tactic:
refine ⟨fun h has hbs ↦ (h has b hbs rfl).symm, ?_⟩
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b✝ : β
a b : α
s : Set α
⊢ (a ∈ s → b ∈ s → a = b) → a ∈ s → ∀ x ∈ s, id x = b → x = a
Theorem: Set.update_id_injOn_iff
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b✝ : β
a b : α
s : Set α
⊢ (a ∈ s → b ∈ s → a = b) → a ∈ s → ∀ x ∈ s, id x = b → x = a
Tactic:
rintro h has _ hbs rfl
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
a : α
s : Set α
has : a ∈ s
x✝ : α
hbs : x✝ ∈ s
h : a ∈ s → id x✝ ∈ s → a = id x✝
⊢ x✝ = a
Theorem: Set.update_id_injOn_iff
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a✝ : α
b : β
a : α
s : Set α
has : a ∈ s
x✝ : α
hbs : x✝ ∈ s
h : a ∈ s → id x✝ ∈ s → a = id x✝
⊢ x✝ = a
Tactic:
exact (h has hbs).symm
Proof state after:
no goals
Theorem: infinite_iUnion
Proof state before:
α : Type u_1
s✝ : Set α
ι : Type u_2
inst✝ : Infinite ι
s : ι → Set α
hs : Function.Injective s
hfin : (⋃ i, s i).Finite
i j : ι
h_eq : (fun i => ⟨s i, ⋯⟩) i = (fun i => ⟨s i, ⋯⟩) j
⊢ s i = s j
Tactic:
simpa using h_eq
Proof state after:
no goals
Theorem: Set.Infinite.biUnion
Proof state before:
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ i ∈ a, s i).Infinite
Tactic:
rw [biUnion_eq_iUnion]
Proof state after:
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ x, s ↑x).Infinite
Theorem: Set.Infinite.biUnion
Proof state before:
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ x, s ↑x).Infinite
Tactic:
have _ := ha.to_subtype
Proof state after:
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
x✝ : Infinite ↑a
⊢ (⋃ x, s ↑x).Infinite
Theorem: Set.Infinite.biUnion
Proof state before:
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
x✝ : Infinite ↑a
⊢ (⋃ x, s ↑x).Infinite
Tactic:
exact infinite_iUnion fun ⟨i,hi⟩ ⟨j,hj⟩ hij ↦ by simp [hs hi hj hij]
Proof state after:
no goals
Theorem: Set.Infinite.biUnion
Proof state before:
α : Type u_1
s✝ : Set α
ι : Type u_2
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
x✝² : Infinite ↑a
x✝¹ x✝ : ↑a
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
hij : s ↑⟨i, hi⟩ = s ↑⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Tactic:
simp [hs hi hj hij]
Proof state after:
no goals
Theorem: Set.Infinite.sUnion
Proof state before:
α : Type u_1
s✝ : Set α
s : Set (Set α)
hs : s.Infinite
⊢ (⋃₀ s).Infinite
Tactic:
rw [sUnion_eq_iUnion]
Proof state after:
α : Type u_1
s✝ : Set α
s : Set (Set α)
hs : s.Infinite
⊢ (⋃ i, ↑i).Infinite
Theorem: Set.Infinite.sUnion
Proof state before:
α : Type u_1
s✝ : Set α
s : Set (Set α)
hs : s.Infinite
⊢ (⋃ i, ↑i).Infinite
Tactic:
have _ := hs.to_subtype
Proof state after:
α : Type u_1
s✝ : Set α
s : Set (Set α)
hs : s.Infinite
x✝ : Infinite ↑s
⊢ (⋃ i, ↑i).Infinite
Theorem: Set.Infinite.sUnion
Proof state before:
α : Type u_1
s✝ : Set α
s : Set (Set α)
hs : s.Infinite
x✝ : Infinite ↑s
⊢ (⋃ i, ↑i).Infinite
Tactic:
exact infinite_iUnion Subtype.coe_injective
Proof state after:
no goals
Theorem: Set.Finite.subset_sUnion_directedOn_iff
Proof state before:
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
⊢ s ⊆ ⋃₀ C ↔ ∃ t ∈ C, s ⊆ t
Tactic:
refine ⟨fun h ↦ ?_, fun ⟨t, ht, hst⟩ ↦ subset_sUnion_of_subset _ _ hst ht⟩
Proof state after:
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
⊢ ∃ t ∈ C, s ⊆ t
Theorem: Set.Finite.subset_sUnion_directedOn_iff
Proof state before:
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
⊢ ∃ t ∈ C, s ⊆ t
Tactic:
apply hs.induction_on' (C := fun x ↦ ∃ u ∈ C, x ⊆ u) ⟨_, hne.some_mem,empty_subset _⟩
Proof state after:
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
⊢ ∀ {a : α} {s_1 : Set α}, a ∈ s → s_1 ⊆ s → a ∉ s_1 → (∃ u ∈ C, s_1 ⊆ u) → ∃ u ∈ C, insert a s_1 ⊆ u
Theorem: Set.Finite.subset_sUnion_directedOn_iff
Proof state before:
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
⊢ ∀ {a : α} {s_1 : Set α}, a ∈ s → s_1 ⊆ s → a ∉ s_1 → (∃ u ∈ C, s_1 ⊆ u) → ∃ u ∈ C, insert a s_1 ⊆ u
Tactic:
rintro a t has - - ⟨u, huC, htu⟩
Proof state after:
case intro.intro
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
a : α
t : Set α
has : a ∈ s
u : Set α
huC : u ∈ C
htu : t ⊆ u
⊢ ∃ u ∈ C, insert a t ⊆ u
Theorem: Set.Finite.subset_sUnion_directedOn_iff
Proof state before:
case intro.intro
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
a : α
t : Set α
has : a ∈ s
u : Set α
huC : u ∈ C
htu : t ⊆ u
⊢ ∃ u ∈ C, insert a t ⊆ u
Tactic:
obtain ⟨v, hvC, hav⟩ := h has
Proof state after:
case intro.intro.intro.intro
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
a : α
t : Set α
has : a ∈ s
u : Set α
huC : u ∈ C
htu : t ⊆ u
v : Set α
hvC : v ∈ C
hav : a ∈ v
⊢ ∃ u ∈ C, insert a t ⊆ u
Theorem: Set.Finite.subset_sUnion_directedOn_iff
Proof state before:
case intro.intro.intro.intro
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
a : α
t : Set α
has : a ∈ s
u : Set α
huC : u ∈ C
htu : t ⊆ u
v : Set α
hvC : v ∈ C
hav : a ∈ v
⊢ ∃ u ∈ C, insert a t ⊆ u
Tactic:
obtain ⟨z, hzC, huz, hvz⟩ := hC _ huC _ hvC
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
a : α
t : Set α
has : a ∈ s
u : Set α
huC : u ∈ C
htu : t ⊆ u
v : Set α
hvC : v ∈ C
hav : a ∈ v
z : Set α
hzC : z ∈ C
huz : u ⊆ z
hvz : v ⊆ z
⊢ ∃ u ∈ C, insert a t ⊆ u
Theorem: Set.Finite.subset_sUnion_directedOn_iff
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
s : Set α
hs : s.Finite
C : Set (Set α)
hC : DirectedOn (fun x x_1 => x ⊆ x_1) C
hne : C.Nonempty
h : s ⊆ ⋃₀ C
a : α
t : Set α
has : a ∈ s
u : Set α
huC : u ∈ C
htu : t ⊆ u
v : Set α
hvC : v ∈ C
hav : a ∈ v
z : Set α
hzC : z ∈ C
huz : u ⊆ z
hvz : v ⊆ z
⊢ ∃ u ∈ C, insert a t ⊆ u
Tactic:
exact ⟨z, hzC, insert_subset (hvz hav) (htu.trans huz)⟩
Proof state after:
no goals
Theorem: Set.Finite.subset_biUnion_mono_iff
Proof state before:
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
doimage : DirectedOn (fun x x_1 => x ⊆ x_1) (v '' a)
⊢ s ⊆ ⋃ i ∈ a, v i ↔ ∃ i ∈ a, s ⊆ v i
Tactic:
simpa using hs.subset_sUnion_directedOn_iff doimage (hne.image v)
Proof state after:
no goals
Theorem: Set.Finite.subset_biUnion_mono_iff
Proof state before:
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
⊢ DirectedOn (fun x x_1 => x ⊆ x_1) (v '' a)
Tactic:
rintro _ ⟨i, hi, rfl⟩ _ ⟨j, hj, rfl⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
⊢ ∃ z ∈ v '' a, (fun x x_1 => x ⊆ x_1) (v i) z ∧ (fun x x_1 => x ⊆ x_1) (v j) z
Theorem: Set.Finite.subset_biUnion_mono_iff
Proof state before:
case intro.intro.intro.intro
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
⊢ ∃ z ∈ v '' a, (fun x x_1 => x ⊆ x_1) (v i) z ∧ (fun x x_1 => x ⊆ x_1) (v j) z
Tactic:
obtain ⟨k, hka, hik, hjk⟩ := ha i hi j hj
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
k : ι
hka : k ∈ a
hik : i ≤ k
hjk : j ≤ k
⊢ ∃ z ∈ v '' a, (fun x x_1 => x ⊆ x_1) (v i) z ∧ (fun x x_1 => x ⊆ x_1) (v j) z
Theorem: Set.Finite.subset_biUnion_mono_iff
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
s : Set α
ι : Type u_2
inst✝ : LE ι
v : ι → Set α
a : Set ι
hs : s.Finite
ha : DirectedOn (fun x x_1 => x ≤ x_1) a
hne : a.Nonempty
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
k : ι
hka : k ∈ a
hik : i ≤ k
hjk : j ≤ k
⊢ ∃ z ∈ v '' a, (fun x x_1 => x ⊆ x_1) (v i) z ∧ (fun x x_1 => x ⊆ x_1) (v j) z
Tactic:
exact ⟨v k, ⟨k, hka, rfl⟩, hv hik, hv hjk⟩
Proof state after:
no goals
Theorem: Set.Finite.subset_iUnion_mono_iff
Proof state before:
α : Type u_1
s : Set α
ι : Type u_2
inst✝² : LE ι
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : Nonempty ι
v : ι → Set α
hs : s.Finite
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
⊢ s ⊆ ⋃ i, v i ↔ ∃ i, s ⊆ v i
Tactic:
simp [← biUnion_univ, hs.subset_biUnion_mono_iff directedOn_univ univ_nonempty hv]
Proof state after:
no goals
Theorem: Matroid.cl_def'
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.cl X = ⋂₀ {F | M.Flat F ∧ X ⊆ F}
Tactic:
nth_rw 2 [← inter_eq_self_of_subset_left hX]
Proof state after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.cl X = ⋂₀ {F | M.Flat F ∧ X ∩ M.E ⊆ F}
Theorem: Matroid.cl_def'
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.cl X = ⋂₀ {F | M.Flat F ∧ X ∩ M.E ⊆ F}
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.ground_subset_cl_iff
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.E ⊆ M.cl X ↔ M.cl X = M.E
Tactic:
simp [M.cl_subset_ground X, subset_antisymm_iff]
Proof state after:
no goals
Theorem: Matroid.cl_eq_sInter_of_subset
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.cl X = ⋂₀ {F | M.Flat F ∧ X ⊆ F}
Tactic:
rw [cl, inter_eq_self_of_subset_left hX]
Proof state after:
no goals
Theorem: Matroid.cl_inter_ground
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X : Set α
⊢ M.cl (X ∩ M.E) = M.cl X
Tactic:
simp_rw [cl_def, inter_assoc, inter_self]
Proof state after:
no goals
Theorem: Matroid.inter_ground_subset_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 : α
M : Matroid α
X : Set α
⊢ X ∩ M.E ⊆ M.cl X
Tactic:
simp_rw [cl_def, subset_sInter_iff]
Proof state after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X : Set α
⊢ ∀ t' ∈ {F | M.Flat F ∧ X ∩ M.E ⊆ F}, X ∩ M.E ⊆ t'
Theorem: Matroid.inter_ground_subset_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 : α
M : Matroid α
X : Set α
⊢ ∀ t' ∈ {F | M.Flat F ∧ X ∩ M.E ⊆ F}, X ∩ M.E ⊆ t'
Tactic:
aesop
Proof state after:
no goals
Theorem: Matroid.mem_cl_iff_forall_mem_flat
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ e ∈ M.cl X ↔ ∀ (F : Set α), M.Flat F → X ⊆ F → e ∈ F
Tactic:
simp_rw [cl_eq_sInter_of_subset X, mem_sInter, mem_setOf, and_imp]
Proof state after:
no goals
Theorem: Matroid.subset_cl_iff_forall_subset_flat
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ Y ⊆ M.cl X ↔ ∀ (F : Set α), M.Flat F → X ⊆ F → Y ⊆ F
Tactic:
simp_rw [cl_eq_sInter_of_subset X, subset_sInter_iff, mem_setOf, and_imp]
Proof state after:
no goals
Theorem: Matroid.subset_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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X ⊆ M.cl X
Tactic:
rw [cl_eq_sInter_of_subset X, subset_sInter_iff]
Proof state after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ∀ t' ∈ {F | M.Flat F ∧ X ⊆ F}, X ⊆ t'
Theorem: Matroid.subset_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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ∀ t' ∈ {F | M.Flat F ∧ X ⊆ F}, X ⊆ t'
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Flat.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 : α
hF : M.Flat F
⊢ F ∈ {F_1 | M.Flat F_1 ∧ F ∩ M.E ⊆ F_1}
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.cl_univ
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
M : Matroid α
⊢ M.cl univ = M.E
Tactic:
rw [← cl_inter_ground, univ_inter, cl_ground]
Proof state after:
no goals
Theorem: Matroid.subset_cl_of_subset'
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
M : Matroid α
hXY : X ⊆ Y
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X ⊆ M.cl Y
Tactic:
rw [← cl_inter_ground]
Proof state after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
M : Matroid α
hXY : X ⊆ Y
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X ⊆ M.cl (Y ∩ M.E)
Theorem: Matroid.subset_cl_of_subset'
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
M : Matroid α
hXY : X ⊆ Y
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X ⊆ M.cl (Y ∩ M.E)
Tactic:
exact M.subset_cl_of_subset (subset_inter hXY hX)
Proof state after:
no goals
Theorem: Matroid.exists_of_cl_ssubset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hXY : M.cl X ⊂ M.cl Y
⊢ ∃ e ∈ Y, e ∉ M.cl X
Tactic:
by_contra! hcon
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hXY : M.cl X ⊂ M.cl Y
hcon : ∀ e ∈ Y, e ∈ M.cl X
⊢ False
Theorem: Matroid.exists_of_cl_ssubset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hXY : M.cl X ⊂ M.cl Y
hcon : ∀ e ∈ Y, e ∈ M.cl X
⊢ False
Tactic:
exact hXY.not_subset (M.cl_subset_cl_of_subset_cl hcon)
Proof state after:
no goals
Theorem: Matroid.mem_cl_of_mem'
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
M : Matroid α
heX : e ∈ X
h : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M.cl X
Tactic:
rw [← cl_inter_ground]
Proof state after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
M : Matroid α
heX : e ∈ X
h : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M.cl (X ∩ M.E)
Theorem: Matroid.mem_cl_of_mem'
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
M : Matroid α
heX : e ∈ X
h : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M.cl (X ∩ M.E)
Tactic:
exact M.mem_cl_of_mem ⟨heX, h⟩
Proof state after:
no goals
Theorem: Matroid.cl_iUnion_cl_eq_cl_iUnion
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
M : Matroid α
Xs : ι → Set α
⊢ M.cl (⋃ i, M.cl (Xs i)) = M.cl (⋃ i, Xs i)
Tactic:
refine (M.cl_subset_cl_of_subset_cl
  (iUnion_subset (fun i ↦ M.cl_subset_cl (subset_iUnion _ _)))).antisymm ?_
Proof state after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
M : Matroid α
Xs : ι → Set α
⊢ M.cl (⋃ i, Xs i) ⊆ M.cl (⋃ i, M.cl (Xs i))