internlm/Lean-Github huggingface dataset:
Theorem: isEmpty_fin_iff
Proof state before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
m n R : Type
inst✝ : Semiring R
b : ℕ
⊢ IsEmpty (Fin b) ↔ b = 0
Tactic:
cases b <;> simp [Fin.isEmpty]
Proof state after:
no goals
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
Tactic:
obtain ⟨r, hrss, hbij⟩ := exists_subset_bijOn ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t) f
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r (f '' ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t))
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r (f '' ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t))
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
Tactic:
rw [image_diff_preimage, image_inter_preimage] at hbij
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
Tactic:
refine ⟨s ∪ r, subset_union_left, ?_, ?_, ?_, fun y hyt' ↦ ?_⟩
Proof state after:
case intro.intro.refine_1
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ s ∪ r ⊆ s₁

case intro.intro.refine_2
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ MapsTo f (s ∪ r) t'

case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ InjOn f (s ∪ r)

case intro.intro.refine_4
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' (s ∪ r)
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
case intro.intro.refine_4
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' (s ∪ r)
Tactic:
rw [image_union, h.image_eq, hbij.image_eq, union_diff_self]
Proof state after:
case intro.intro.refine_4
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ t ∪ f '' s₁ ∩ t'
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
case intro.intro.refine_4
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ t ∪ f '' s₁ ∩ t'
Tactic:
exact .inr ⟨ht' hyt', hyt'⟩
Proof state after:
no goals
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
case intro.intro.refine_1
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ s ∪ r ⊆ s₁
Tactic:
exact union_subset hss₁ <| hrss.trans <| diff_subset.trans inter_subset_left
Proof state after:
no goals
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
case intro.intro.refine_2
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ MapsTo f (s ∪ r) t'
Tactic:
rw [mapsTo', image_union, hbij.image_eq, h.image_eq, union_subset_iff]
Proof state after:
case intro.intro.refine_2
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ t ⊆ t' ∧ (f '' s₁ ∩ t') \ t ⊆ t'
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
case intro.intro.refine_2
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ t ⊆ t' ∧ (f '' s₁ ∩ t') \ t ⊆ t'
Tactic:
exact ⟨htt', diff_subset.trans inter_subset_right⟩
Proof state after:
no goals
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ InjOn f (s ∪ r)
Tactic:
rw [injOn_union, and_iff_right h.injOn, and_iff_right hbij.injOn]
Proof state after:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∀ x ∈ s, ∀ y ∈ r, f x ≠ f y

case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ Disjoint s r
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ Disjoint s r
Tactic:
exact (subset_diff.1 hrss).2.symm.mono_left h.mapsTo
Proof state after:
no goals
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∀ x ∈ s, ∀ y ∈ r, f x ≠ f y
Tactic:
refine fun x hxs y hyr hxy ↦ (hrss hyr).2 ?_
Proof state after:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' t
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' t
Tactic:
rw [← h.image_eq]
Proof state after:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' (f '' s)
Theorem: Set.BijOn.exists_extend_of_subset
Proof state before:
case intro.intro.refine_3
α : Type u_1
β : Type u_2
r✝ s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' (f '' s)
Tactic:
exact ⟨x, hxs, hxy⟩
Proof state after:
no goals
Theorem: Set.BijOn.exists_extend
Proof state before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ ∃ s', s ⊆ s' ∧ BijOn f s' t'
Tactic:
simpa using h.exists_extend_of_subset (subset_univ s) htt' (by simpa [SurjOn])
Proof state after:
no goals
Theorem: Set.BijOn.exists_extend
Proof state before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ SurjOn f univ t'
Tactic:
simpa [SurjOn]
Proof state after:
no goals
Theorem: Set.InjOn.exists_subset_injOn_subset_range_eq
Proof state before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
hinj : InjOn f r
hrs : r ⊆ s
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
Tactic:
obtain ⟨u, hru, hus, h⟩ := hinj.bijOn_image.exists_extend_of_subset hrs
  (image_subset f hrs) Subset.rfl
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
hinj : InjOn f r
hrs : r ⊆ s
u : Set α
hru : r ⊆ u
hus : u ⊆ s
h : BijOn f u (f '' s)
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
Theorem: Set.InjOn.exists_subset_injOn_subset_range_eq
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
hinj : InjOn f r
hrs : r ⊆ s
u : Set α
hru : r ⊆ u
hus : u ⊆ s
h : BijOn f u (f '' s)
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
Tactic:
exact ⟨u, hru, hus, h.image_eq, h.injOn⟩
Proof state after:
no goals
Theorem: Set.surjOn_empty_iff
Proof state before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t✝ t' t₁ t₂ : Set β
f✝ f : α → β
t : Set β
⊢ SurjOn f ∅ t ↔ t = ∅
Tactic:
simp [SurjOn, subset_empty_iff]
Proof state after:
no goals
Theorem: Set.mapsTo_empty_iff
Proof state before:
α : Type u_1
β : Type u_2
r s✝ s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f✝ f : α → β
s : Set α
⊢ MapsTo f s ∅ ↔ s = ∅
Tactic:
simp [mapsTo', subset_empty_iff]
Proof state after:
no goals
Theorem: Set.bijOn_empty_iff_left
Proof state before:
α : Type u_1
β : Type u_2
r s✝ s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f✝ f : α → β
s : Set α
h : BijOn f s ∅
⊢ s = ∅
Tactic:
simpa using h.mapsTo
Proof state after:
no goals
Theorem: Set.bijOn_empty_iff_left
Proof state before:
α : Type u_1
β : Type u_2
r s✝ s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f✝ f : α → β
s : Set α
⊢ s = ∅ → BijOn f s ∅
Tactic:
rintro rfl
Proof state after:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f✝ f : α → β
⊢ BijOn f ∅ ∅
Theorem: Set.bijOn_empty_iff_left
Proof state before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f✝ f : α → β
⊢ BijOn f ∅ ∅
Tactic:
exact bijOn_empty f
Proof state after:
no goals
Theorem: Set.bijOn_empty_iff_right
Proof state before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t✝ t' t₁ t₂ : Set β
f✝ f : α → β
t : Set β
h : BijOn f ∅ t
⊢ t = ∅
Tactic:
simpa using h.surjOn
Proof state after:
no goals
Theorem: Set.bijOn_empty_iff_right
Proof state before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t✝ t' t₁ t₂ : Set β
f✝ f : α → β
t : Set β
⊢ t = ∅ → BijOn f ∅ t
Tactic:
rintro rfl
Proof state after:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f✝ f : α → β
⊢ BijOn f ∅ ∅
Theorem: Set.bijOn_empty_iff_right
Proof state before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f✝ f : α → β
⊢ BijOn f ∅ ∅
Tactic:
exact bijOn_empty f
Proof state after:
no goals
Theorem: Set.image_update
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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
⊢ update f a b '' s = if a ∈ s then insert b (f '' (s \ {a})) else f '' s
Tactic:
split_ifs with h
Proof state after:
case pos
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
⊢ update f a b '' s = insert b (f '' (s \ {a}))

case neg
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
⊢ update f a b '' s = f '' s
Theorem: Set.image_update
Proof state before:
case neg
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
⊢ update f a b '' s = f '' s
Tactic:
rw [subset_antisymm_iff, image_subset_iff, image_subset_iff]
Proof state after:
case neg
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
⊢ s ⊆ update f a b ⁻¹' (f '' s) ∧ s ⊆ f ⁻¹' (update f a b '' s)
Theorem: Set.image_update
Proof state before:
case neg
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
⊢ s ⊆ update f a b ⁻¹' (f '' s) ∧ s ⊆ f ⁻¹' (update f a b '' s)
Tactic:
refine ⟨fun x hxs ↦ ⟨x, hxs, ?_⟩, fun x hxs ↦ ⟨x, hxs, ?_⟩⟩
Proof state after:
case neg.refine_1
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ f x = update f a b x

case neg.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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ update f a b x = f x
Theorem: Set.image_update
Proof state before:
case neg.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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ update f a b x = f x
Tactic:
rw [update_noteq]
Proof state after:
case neg.refine_2.h
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ x ≠ a
Theorem: Set.image_update
Proof state before:
case neg.refine_2.h
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ x ≠ a
Tactic:
rintro rfl
Proof state after:
case neg.refine_2.h
α✝ : 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 : α
hxs : x ∈ s
inst✝ : Decidable (x ∈ s)
h : x ∉ s
⊢ False
Theorem: Set.image_update
Proof state before:
case neg.refine_2.h
α✝ : 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 : α
hxs : x ∈ s
inst✝ : Decidable (x ∈ s)
h : x ∉ s
⊢ False
Tactic:
exact h hxs
Proof state after:
no goals
Theorem: Set.image_update
Proof state before:
case pos
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
⊢ update f a b '' s = insert b (f '' (s \ {a}))
Tactic:
rw [subset_antisymm_iff, image_subset_iff]
Proof state after:
case pos
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
⊢ s ⊆ update f a b ⁻¹' insert b (f '' (s \ {a})) ∧ insert b (f '' (s \ {a})) ⊆ update f a b '' s
Theorem: Set.image_update
Proof state before:
case pos
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
⊢ s ⊆ update f a b ⁻¹' insert b (f '' (s \ {a})) ∧ insert b (f '' (s \ {a})) ⊆ update f a b '' s
Tactic:
refine ⟨fun x hxs ↦ (em (x = a)).elim (fun heq ↦ ?_) (fun hne ↦ Or.inr ?_), fun x ↦ ?_⟩
Proof state after:
case pos.refine_1
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
heq : x = a
⊢ x ∈ update f a b ⁻¹' insert b (f '' (s \ {a}))

case pos.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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
hne : ¬x = a
⊢ update f a b x ∈ f '' (s \ {a})

case pos.refine_3
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : β
⊢ x ∈ insert b (f '' (s \ {a})) → x ∈ update f a b '' s
Theorem: Set.image_update
Proof state before:
case pos.refine_3
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : β
⊢ x ∈ insert b (f '' (s \ {a})) → x ∈ update f a b '' s
Tactic:
rintro (rfl | ⟨x, hx, rfl⟩)
Proof state after:
case pos.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 : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
h : a ∈ s
x : β
⊢ x ∈ update f a x '' s

case pos.refine_3.inr.intro.intro
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hx : x ∈ s \ {a}
⊢ f x ∈ update f a b '' s
Theorem: Set.image_update
Proof state before:
case pos.refine_3.inr.intro.intro
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hx : x ∈ s \ {a}
⊢ f x ∈ update f a b '' s
Tactic:
exact ⟨x, hx.1, update_noteq hx.2 _ _⟩
Proof state after:
no goals
Theorem: Set.image_update
Proof state before:
case pos.refine_1
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
heq : x = a
⊢ x ∈ update f a b ⁻¹' insert b (f '' (s \ {a}))
Tactic:
rw [mem_preimage, update_apply, if_pos heq]
Proof state after:
case pos.refine_1
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
heq : x = a
⊢ b ∈ insert b (f '' (s \ {a}))
Theorem: Set.image_update
Proof state before:
case pos.refine_1
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
heq : x = a
⊢ b ∈ insert b (f '' (s \ {a}))
Tactic:
exact mem_insert _ _
Proof state after:
no goals
Theorem: Set.image_update
Proof state before:
case pos.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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
hne : ¬x = a
⊢ update f a b x ∈ f '' (s \ {a})
Tactic:
exact ⟨x, ⟨hxs, hne⟩, by rw [update_noteq hne]⟩
Proof state after:
no goals
Theorem: Set.image_update
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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
hne : ¬x = a
⊢ f x = update f a b x
Tactic:
rw [update_noteq hne]
Proof state after:
no goals
Theorem: Set.image_update
Proof state before:
case pos.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 : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
h : a ∈ s
x : β
⊢ x ∈ update f a x '' s
Tactic:
use a
Proof state after:
case h
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
h : a ∈ s
x : β
⊢ a ∈ s ∧ update f a x a = x
Theorem: Set.image_update
Proof state before:
case h
α✝ : 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 : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
h : a ∈ s
x : β
⊢ a ∈ s ∧ update f a x a = x
Tactic:
simpa
Proof state after:
no goals