internlm/Lean-Github huggingface dataset:
Theorem: Equiv.exists_bijOn
Proof state before:
case h.refine_2
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy :
  (if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) =
    if hx : y ∈ s then ↑(e ⟨y, hx⟩) else Classical.arbitrary β
⊢ x = y
Tactic:
simpa [dif_pos hx, dif_pos hy, Subtype.coe_inj] using hxy
Proof state after:
no goals
Theorem: Equiv.exists_bijOn
Proof state before:
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
y : β
hy : y ∈ t
⊢ ↑(e.symm ⟨y, hy⟩) ∈ s ∧ (fun x => if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) ↑(e.symm ⟨y, hy⟩) = y
Tactic:
simp
Proof state after:
no goals
Theorem: Equiv.exists_bijOn
Proof state before:
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
⊢ ∀ (x : ↑s), ↑(e x) = if hx : ↑x ∈ s then ↑(e ⟨↑x, hx⟩) else Classical.arbitrary β
Tactic:
simp
Proof state after:
no goals
Theorem: Equiv.exists_bijOn
Proof state before:
case h.refine_1
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
⊢ (if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) ∈ t
Tactic:
rw [dif_pos hx]
Proof state after:
case h.refine_1
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
⊢ ↑(e ⟨x, hx⟩) ∈ t
Theorem: Equiv.exists_bijOn
Proof state before:
case h.refine_1
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
⊢ ↑(e ⟨x, hx⟩) ∈ t
Tactic:
exact Subtype.prop _
Proof state after:
no goals
Theorem: Set.Finite.encard_le_iff_nonempty_embedding
Proof state before:
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Tactic:
cases isEmpty_or_nonempty β
Proof state after:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)

case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Theorem: Set.Finite.encard_le_iff_nonempty_embedding
Proof state before:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Tactic:
refine ⟨fun h ↦ ?_, fun ⟨e⟩ ↦ e.enccard_le⟩
Proof state after:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
h : s.encard ≤ t.encard
⊢ Nonempty (↑s ↪ ↑t)
Theorem: Set.Finite.encard_le_iff_nonempty_embedding
Proof state before:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
h : s.encard ≤ t.encard
⊢ Nonempty (↑s ↪ ↑t)
Tactic:
obtain ⟨f, hst, hf⟩ := hs.exists_injOn_of_encard_le h
Proof state after:
case inr.intro.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f✝ : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
h : s.encard ≤ t.encard
f : α → β
hst : s ⊆ f ⁻¹' t
hf : InjOn f s
⊢ Nonempty (↑s ↪ ↑t)
Theorem: Set.Finite.encard_le_iff_nonempty_embedding
Proof state before:
case inr.intro.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f✝ : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
h : s.encard ≤ t.encard
f : α → β
hst : s ⊆ f ⁻¹' t
hf : InjOn f s
⊢ Nonempty (↑s ↪ ↑t)
Tactic:
exact ⟨codRestrict (s.restrict f) t (fun x ↦ by aesop), hf.injective.codRestrict _⟩
Proof state after:
no goals
Theorem: Set.Finite.encard_le_iff_nonempty_embedding
Proof state before:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Tactic:
simp only [t.eq_empty_of_isEmpty, encard_empty, nonpos_iff_eq_zero, encard_eq_zero]
Proof state after:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s = ∅ ↔ Nonempty (↑s ↪ ↑∅)
Theorem: Set.Finite.encard_le_iff_nonempty_embedding
Proof state before:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s = ∅ ↔ Nonempty (↑s ↪ ↑∅)
Tactic:
constructor
Proof state after:
case inl.mp
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s = ∅ → Nonempty (↑s ↪ ↑∅)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅
Theorem: Set.Finite.encard_le_iff_nonempty_embedding
Proof state before:
case inl.mp
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s = ∅ → Nonempty (↑s ↪ ↑∅)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅
Tactic:
rintro rfl
Proof state after:
case inl.mp
α : Type u_1
β : Type u_2
s s₁ s₂ t✝ t' : Set α
f : α → β
t : Set β
h✝ : IsEmpty β
hs : ∅.Finite
⊢ Nonempty (↑∅ ↪ ↑∅)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅
Theorem: Set.Finite.encard_le_iff_nonempty_embedding
Proof state before:
case inl.mp
α : Type u_1
β : Type u_2
s s₁ s₂ t✝ t' : Set α
f : α → β
t : Set β
h✝ : IsEmpty β
hs : ∅.Finite
⊢ Nonempty (↑∅ ↪ ↑∅)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅
Tactic:
exact ⟨Embedding.ofIsEmpty⟩
Proof state after:
case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅
Theorem: Set.Finite.encard_le_iff_nonempty_embedding
Proof state before:
case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅
Tactic:
rintro ⟨e⟩
Proof state after:
case inl.mpr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
e : ↑s ↪ ↑∅
⊢ s = ∅
Theorem: Set.Finite.encard_le_iff_nonempty_embedding
Proof state before:
case inl.mpr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
e : ↑s ↪ ↑∅
⊢ s = ∅
Tactic:
exact isEmpty_coe_sort.1 e.toFun.isEmpty
Proof state after:
no goals
Theorem: Set.Finite.encard_le_iff_nonempty_embedding
Proof state before:
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f✝ : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
h : s.encard ≤ t.encard
f : α → β
hst : s ⊆ f ⁻¹' t
hf : InjOn f s
x : ↑s
⊢ s.restrict f x ∈ t
Tactic:
aesop
Proof state after:
no goals
Theorem: Set.Finite.encard_le_iff_nonempty_embedding'
Proof state before:
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Tactic:
obtain (hs | hs) := s.finite_or_infinite
Proof state after:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Finite
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)

case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Theorem: Set.Finite.encard_le_iff_nonempty_embedding'
Proof state before:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Tactic:
rw [hs.encard_eq, top_le_iff, encard_eq_top_iff, Set.Infinite, iff_true_intro ht,
  not_true, false_iff]
Proof state after:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
⊢ ¬Nonempty (↑s ↪ ↑t)
Theorem: Set.Finite.encard_le_iff_nonempty_embedding'
Proof state before:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
⊢ ¬Nonempty (↑s ↪ ↑t)
Tactic:
rintro ⟨e⟩
Proof state after:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
e : ↑s ↪ ↑t
⊢ False
Theorem: Set.Finite.encard_le_iff_nonempty_embedding'
Proof state before:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
e : ↑s ↪ ↑t
⊢ False
Tactic:
have hle := e.enccard_le
Proof state after:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
e : ↑s ↪ ↑t
hle : s.encard ≤ t.encard
⊢ False
Theorem: Set.Finite.encard_le_iff_nonempty_embedding'
Proof state before:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
e : ↑s ↪ ↑t
hle : s.encard ≤ t.encard
⊢ False
Tactic:
rw [hs.encard_eq, top_le_iff, encard_eq_top_iff] at hle
Proof state after:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
e : ↑s ↪ ↑t
hle : t.Infinite
⊢ False
Theorem: Set.Finite.encard_le_iff_nonempty_embedding'
Proof state before:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
e : ↑s ↪ ↑t
hle : t.Infinite
⊢ False
Tactic:
exact hle ht
Proof state after:
no goals
Theorem: Set.Finite.encard_le_iff_nonempty_embedding'
Proof state before:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Finite
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Tactic:
exact hs.encard_le_iff_nonempty_embedding
Proof state after:
no goals
Theorem: encard_univ_fin
Proof state before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
a : ℕ
⊢ univ.encard = ↑a
Tactic:
simp [encard_eq_coe_toFinset_card]
Proof state after:
no goals
Theorem: Set.Finite.encard_eq_iff_nonempty_equiv
Proof state before:
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
⊢ s.encard = t.encard ↔ Nonempty (↑s ≃ ↑t)
Tactic:
cases isEmpty_or_nonempty α
Proof state after:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ s.encard = t.encard ↔ Nonempty (↑s ≃ ↑t)

case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : Nonempty α
⊢ s.encard = t.encard ↔ Nonempty (↑s ≃ ↑t)
Theorem: Set.Finite.encard_eq_iff_nonempty_equiv
Proof state before:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : Nonempty α
⊢ s.encard = t.encard ↔ Nonempty (↑s ≃ ↑t)
Tactic:
refine ⟨fun h ↦ ?_, fun ⟨e⟩ ↦ encard_congr e⟩
Proof state after:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : Nonempty α
h : s.encard = t.encard
⊢ Nonempty (↑s ≃ ↑t)
Theorem: Set.Finite.encard_eq_iff_nonempty_equiv
Proof state before:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : Nonempty α
h : s.encard = t.encard
⊢ Nonempty (↑s ≃ ↑t)
Tactic:
obtain ⟨f, hf⟩ := ht.exists_bijOn_of_encard_eq h.symm
Proof state after:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f✝ : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : Nonempty α
h : s.encard = t.encard
f : β → α
hf : BijOn f t s
⊢ Nonempty (↑s ≃ ↑t)
Theorem: Set.Finite.encard_eq_iff_nonempty_equiv
Proof state before:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f✝ : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : Nonempty α
h : s.encard = t.encard
f : β → α
hf : BijOn f t s
⊢ Nonempty (↑s ≃ ↑t)
Tactic:
exact Nonempty.intro <| (hf.equiv _).symm
Proof state after:
no goals
Theorem: Set.Finite.encard_eq_iff_nonempty_equiv
Proof state before:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ s.encard = t.encard ↔ Nonempty (↑s ≃ ↑t)
Tactic:
simp only [s.eq_empty_of_isEmpty, eq_comm (a := (0 : ℕ∞)), encard_empty, encard_eq_zero]
Proof state after:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ t = ∅ ↔ Nonempty (↑∅ ≃ ↑t)
Theorem: Set.Finite.encard_eq_iff_nonempty_equiv
Proof state before:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ t = ∅ ↔ Nonempty (↑∅ ≃ ↑t)
Tactic:
constructor
Proof state after:
case inl.mp
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ t = ∅ → Nonempty (↑∅ ≃ ↑t)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ Nonempty (↑∅ ≃ ↑t) → t = ∅
Theorem: Set.Finite.encard_eq_iff_nonempty_equiv
Proof state before:
case inl.mp
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ t = ∅ → Nonempty (↑∅ ≃ ↑t)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ Nonempty (↑∅ ≃ ↑t) → t = ∅
Tactic:
rintro rfl
Proof state after:
case inl.mp
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t t' : Set α
f : α → β
s : Set α
h✝ : IsEmpty α
ht : ∅.Finite
⊢ Nonempty (↑∅ ≃ ↑∅)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ Nonempty (↑∅ ≃ ↑t) → t = ∅
Theorem: Set.Finite.encard_eq_iff_nonempty_equiv
Proof state before:
case inl.mp
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t t' : Set α
f : α → β
s : Set α
h✝ : IsEmpty α
ht : ∅.Finite
⊢ Nonempty (↑∅ ≃ ↑∅)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ Nonempty (↑∅ ≃ ↑t) → t = ∅
Tactic:
exact ⟨Equiv.equivOfIsEmpty _ _⟩
Proof state after:
case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ Nonempty (↑∅ ≃ ↑t) → t = ∅
Theorem: Set.Finite.encard_eq_iff_nonempty_equiv
Proof state before:
case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ Nonempty (↑∅ ≃ ↑t) → t = ∅
Tactic:
rintro ⟨e⟩
Proof state after:
case inl.mpr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
e : ↑∅ ≃ ↑t
⊢ t = ∅
Theorem: Set.Finite.encard_eq_iff_nonempty_equiv
Proof state before:
case inl.mpr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
e : ↑∅ ≃ ↑t
⊢ t = ∅
Tactic:
exact isEmpty_coe_sort.1 e.symm.toFun.isEmpty
Proof state after:
no goals
Theorem: Equiv.swap_image_eq_self
Proof state before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
hef : e ∈ S ↔ f ∈ S
⊢ ⇑(swap e f) '' S = S
Tactic:
ext x
Proof state after:
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
hef : e ∈ S ↔ f ∈ S
x : α
⊢ x ∈ ⇑(swap e f) '' S ↔ x ∈ S
Theorem: Equiv.swap_image_eq_self
Proof state before:
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
hef : e ∈ S ↔ f ∈ S
x : α
⊢ x ∈ ⇑(swap e f) '' S ↔ x ∈ S
Tactic:
rw [image_equiv_eq_preimage_symm, mem_preimage, Equiv.symm_swap, Equiv.swap_apply_def]
Proof state after:
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
hef : e ∈ S ↔ f ∈ S
x : α
⊢ (if x = e then f else if x = f then e else x) ∈ S ↔ x ∈ S
Theorem: Equiv.swap_image_eq_self
Proof state before:
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
hef : e ∈ S ↔ f ∈ S
x : α
⊢ (if x = e then f else if x = f then e else x) ∈ S ↔ x ∈ S
Tactic:
split_ifs with hxe hxf
Proof state after:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
hef : e ∈ S ↔ f ∈ S
x : α
hxe : x = e
⊢ f ∈ S ↔ x ∈ S

case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
hef : e ∈ S ↔ f ∈ S
x : α
hxe : ¬x = e
hxf : x = f
⊢ e ∈ S ↔ x ∈ S

case neg
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
hef : e ∈ S ↔ f ∈ S
x : α
hxe : ¬x = e
hxf : ¬x = f
⊢ x ∈ S ↔ x ∈ S
Theorem: Equiv.swap_image_eq_self
Proof state before:
case neg
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
hef : e ∈ S ↔ f ∈ S
x : α
hxe : ¬x = e
hxf : ¬x = f
⊢ x ∈ S ↔ x ∈ S
Tactic:
rfl
Proof state after:
no goals
Theorem: Equiv.swap_image_eq_self
Proof state before:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
hef : e ∈ S ↔ f ∈ S
x : α
hxe : x = e
⊢ f ∈ S ↔ x ∈ S
Tactic:
rwa [hxe, Iff.comm]
Proof state after:
no goals
Theorem: Equiv.swap_image_eq_self
Proof state before:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
hef : e ∈ S ↔ f ∈ S
x : α
hxe : ¬x = e
hxf : x = f
⊢ e ∈ S ↔ x ∈ S
Tactic:
rwa [hxf]
Proof state after:
no goals
Theorem: Equiv.swap_image_eq_exchange
Proof state before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
⊢ ⇑(swap e f) '' S = insert f (S \ {e})
Tactic:
ext x
Proof state after:
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
⊢ x ∈ ⇑(swap e f) '' S ↔ x ∈ insert f (S \ {e})
Theorem: Equiv.swap_image_eq_exchange
Proof state before:
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
⊢ x ∈ ⇑(swap e f) '' S ↔ x ∈ insert f (S \ {e})
Tactic:
rw [image_equiv_eq_preimage_symm, mem_preimage, Equiv.symm_swap, Equiv.swap_apply_def,
  mem_insert_iff, mem_diff]
Proof state after:
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
⊢ (if x = e then f else if x = f then e else x) ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}
Theorem: Equiv.swap_image_eq_exchange
Proof state before:
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
⊢ (if x = e then f else if x = f then e else x) ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}
Tactic:
split_ifs with hxe hxf
Proof state after:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
hxe : x = e
⊢ f ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}

case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
hxe : ¬x = e
hxf : x = f
⊢ e ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}

case neg
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
hxe : ¬x = e
hxf : ¬x = f
⊢ x ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}
Theorem: Equiv.swap_image_eq_exchange
Proof state before:
case neg
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
hxe : ¬x = e
hxf : ¬x = f
⊢ x ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}
Tactic:
simp [hxe, iff_false_intro hxf]
Proof state after:
no goals
Theorem: Equiv.swap_image_eq_exchange
Proof state before:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
hxe : x = e
⊢ f ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}
Tactic:
subst hxe
Proof state after:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
f : α
inst✝ : DecidableEq α
S : Set α
hf : f ∉ S
x : α
he : x ∈ S
⊢ f ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {x}
Theorem: Equiv.swap_image_eq_exchange
Proof state before:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
f : α
inst✝ : DecidableEq α
S : Set α
hf : f ∉ S
x : α
he : x ∈ S
⊢ f ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {x}
Tactic:
simp [he, hf, (show x ≠ f by rintro rfl; exact hf he)]
Proof state after:
no goals
Theorem: Equiv.swap_image_eq_exchange
Proof state before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
f : α
inst✝ : DecidableEq α
S : Set α
hf : f ∉ S
x : α
he : x ∈ S
⊢ x ≠ f
Tactic:
rintro rfl
Proof state after:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
inst✝ : DecidableEq α
S : Set α
x : α
he : x ∈ S
hf : x ∉ S
⊢ False
Theorem: Equiv.swap_image_eq_exchange
Proof state before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
inst✝ : DecidableEq α
S : Set α
x : α
he : x ∈ S
hf : x ∉ S
⊢ False
Tactic:
exact hf he
Proof state after:
no goals
Theorem: Equiv.swap_image_eq_exchange
Proof state before:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
hxe : ¬x = e
hxf : x = f
⊢ e ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}
Tactic:
subst hxf
Proof state after:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
e : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
x : α
hxe : ¬x = e
hf : x ∉ S
⊢ e ∈ S ↔ x = x ∨ x ∈ S ∧ x ∉ {e}
Theorem: Equiv.swap_image_eq_exchange
Proof state before:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
e : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
x : α
hxe : ¬x = e
hf : x ∉ S
⊢ e ∈ S ↔ x = x ∨ x ∈ S ∧ x ∉ {e}
Tactic:
simp [he]
Proof state after:
no goals
Theorem: exists_eq_image_subset_of_subset_image
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
⊢ ∃ t₀ ⊆ s, t = f '' t₀
Tactic:
refine ⟨f ⁻¹' t ∩ s, inter_subset_right, subset_antisymm (fun x hxt ↦ ?_) ?_⟩
Proof state after:
case refine_1
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
x : β
hxt : x ∈ t
⊢ x ∈ f '' (f ⁻¹' t ∩ s)

case refine_2
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
⊢ f '' (f ⁻¹' t ∩ s) ⊆ t
Theorem: exists_eq_image_subset_of_subset_image
Proof state before:
case refine_2
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
⊢ f '' (f ⁻¹' t ∩ s) ⊆ t
Tactic:
simp [image_subset_iff, inter_subset_left]
Proof state after:
no goals
Theorem: exists_eq_image_subset_of_subset_image
Proof state before:
case refine_1
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
x : β
hxt : x ∈ t
⊢ x ∈ f '' (f ⁻¹' t ∩ s)
Tactic:
obtain ⟨a, ha, rfl⟩ := hst hxt
Proof state after:
case refine_1.intro.intro
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
a : α
ha : a ∈ s
hxt : f a ∈ t
⊢ f a ∈ f '' (f ⁻¹' t ∩ s)
Theorem: exists_eq_image_subset_of_subset_image
Proof state before:
case refine_1.intro.intro
α✝ : Type u_1
β✝ : Type u_2
s✝ s₁ s₂ t✝ t' : Set α✝
f✝ : α✝ → β✝
m n R : Type
inst✝ : Semiring R
α : Type u_3
β : Type u_4
f : α → β
s : Set α
t : Set β
hst : t ⊆ f '' s
a : α
ha : a ∈ s
hxt : f a ∈ t
⊢ f a ∈ f '' (f ⁻¹' t ∩ s)
Tactic:
exact ⟨a, mem_inter hxt ha, rfl⟩
Proof state after:
no goals