awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
h : T ⊆ S
⊢ Disjoint (S \ T) T

Tactic:
exact disjoint_sdiff_self_left

Premises used: disjoint_sdiff_self_left
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
h : #(↑S : Type u) < #(↑T : Type u)
rw : #(↑(T \ S) : Type u) ≠ 0
⊢ (T \ S).Nonempty

Tactic:
rw [← mk_set_ne_zero_iff]

Premises used: Cardinal.mk_set_ne_zero_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
h : #(↑S : Type u) < #(↑T : Type u)
h' : #(↑(T \ S) : Type u) = 0
⊢ #(↑(T \ S) : Type u) + #(↑S : Type u) ≤ #(↑S : Type u)

Tactic:
simp [h']
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S T : Set α
h : #(↑S : Type u) < #(↑T : Type u)
h' : #(↑(T \ S) : Type u) = 0
⊢ False

Tactic:
exact h.not_ge ((le_mk_diff_add_mk T S).trans (by simp [h']))

Premises used: Cardinal.le_mk_diff_add_mk, LE.le.trans, LT.lt.not_ge
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S : Set α
h : #(↑S : Type u) < #α
⊢ #(↑S : Type u) < #(↑univ : Type u)

Tactic:
rw [← mk_univ (α := α)] at h

Premises used: Cardinal.mk_univ
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
S : Set α
h : #(↑S : Type u) < #(↑univ : Type u)
⊢ Sᶜ.Nonempty

Tactic:
simpa [Set.compl_eq_univ_diff] using diff_nonempty_of_mk_lt_mk h

Premises used: Cardinal.diff_nonempty_of_mk_lt_mk, Set.compl_eq_univ_diff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
P Q : Set α
⊢ #(↑(P ∪ Q) : Type u_1) ≤ ℵ₀ ↔ #(↑P : Type u_1) ≤ ℵ₀ ∧ #(↑Q : Type u_1) ≤ ℵ₀

Tactic:
simp only [le_aleph0_iff_subtype_countable, setOf_mem_eq, Set.union_def,
    ← countable_union]

Premises used: Set.countable_union, Set.setOf_mem_eq, Cardinal.le_aleph0_iff_subtype_countable, Set.union_def
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
t : α → Prop
⊢ #(↑{x : α | x ∈ s ∧ t x} : Type u) = #(↑{x : (↑s : Type u) | t (↑x : α)} : Type u)

Tactic:
mk_congr (Equiv.Set.sep s t)

Premises used: Equiv.Set.sep, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
rw : Nonempty (Embedding.{u + 1, v + 1} (↑(f ⁻¹' s) : Type u) (↑s : Type v))
⊢ lift.{v, u} #(↑(f ⁻¹' s) : Type u) ≤ lift.{u, v} #(↑s : Type v)

Tactic:
rw [lift_mk_le.{0}]

Premises used: Cardinal.lift_mk_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
inj' :
  Injective.{u + 1, v + 1} (α := (↑(f ⁻¹' s) : Type u)) (β := (↑s : Type v))
    (Subtype.coind fun (x : (↑(f ⁻¹' s) : Type u)) ↦ f (↑x : α) (p := fun (x : β) ↦ x ∈ s) ⋯)
⊢ Nonempty (Embedding.{u + 1, v + 1} (↑(f ⁻¹' s) : Type u) (↑s : Type v))

Tactic:
use Subtype.coind (fun x => f x.1) fun x => mem_preimage.mp x.2

Premises used: Subtype.coind, Iff.mp, Set.mem_preimage
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
inj' : Injective.{u + 1, v + 1} (β := β) fun (x : (↑(f ⁻¹' s) : Type u)) ↦ f (↑x : α)
⊢ Injective.{u + 1, v + 1} (α := (↑(f ⁻¹' s) : Type u)) (β := (↑s : Type v))
    (Subtype.coind fun (x : (↑(f ⁻¹' s) : Type u)) ↦ f (↑x : α) (p := fun (x : β) ↦ x ∈ s) ⋯)

Tactic:
apply Subtype.coind_injective

Premises used: Subtype.coind_injective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective.{u + 1, v + 1} (β := β) fun (x : (↑(f ⁻¹' s) : Type u)) ↦ f (↑x : α)

Tactic:
h.comp Subtype.val_injective

Premises used: Subtype.val_injective, Function.Injective.comp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective.{u + 1, v + 1} (β := β) fun (x : (↑(f ⁻¹' s) : Type u)) ↦ f (↑x : α)

Tactic:
exact h.comp Subtype.val_injective

Premises used: Subtype.val_injective, Function.Injective.comp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ f '' f ⁻¹' s = s

Tactic:
rw [← image_preimage_eq_iff] at h

Premises used: Set.image_preimage_eq_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : f '' f ⁻¹' s = s
nth_rewrite : lift.{u, v} #(↑(f '' f ⁻¹' s) : Type v) ≤ lift.{v, u} #(↑(f ⁻¹' s) : Type u)
⊢ lift.{u, v} #(↑s : Type v) ≤ lift.{v, u} #(↑(f ⁻¹' s) : Type u)

Tactic:
nth_rewrite 1 [← h]
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : f '' f ⁻¹' s = s
⊢ lift.{u, v} #(↑(f '' f ⁻¹' s) : Type v) ≤ lift.{v, u} #(↑(f ⁻¹' s) : Type u)

Tactic:
apply mk_image_le_lift

Premises used: Cardinal.mk_image_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ lift.{v, u} #(↑(f ⁻¹' s) : Type u) = lift.{u, v} #(↑s : Type v)

Tactic:
le_antisymm (mk_preimage_of_injective_lift f s h) (mk_preimage_of_subset_range_lift f s h2)

Premises used: Cardinal.mk_preimage_of_subset_range_lift, le_antisymm, Cardinal.mk_preimage_of_injective_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ lift.{u, u} #(↑(f ⁻¹' s) : Type u) = lift.{u, u} #(↑s : Type u)

Tactic:
mk_preimage_of_injective_of_subset_range_lift.{u, u} f s h h2

Premises used: Cardinal.mk_preimage_of_injective_of_subset_range_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
h₁ : #(↑(f ⁻¹' s) : Type u) = lift.{u, u} #(↑(f ⁻¹' s) : Type u)
h₂ : #(↑s : Type u) = lift.{u, u} #(↑s : Type u)
⊢ #(↑(f ⁻¹' s) : Type u) = #(↑s : Type u)

Tactic:
convert! mk_preimage_of_injective_of_subset_range_lift.{u, u} f s h h2 using 1
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
h₁ h₂ : #(↑(f ⁻¹' s) : Type u) = #(↑(f ⁻¹' s) : Type u)
⊢ #(↑(f ⁻¹' s) : Type u) = lift.{u, u} #(↑(f ⁻¹' s) : Type u)

Tactic:
rw [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
h₁ h₂ : #(↑s : Type u) = #(↑s : Type u)
⊢ #(↑s : Type u) = lift.{u, u} #(↑s : Type u)

Tactic:
rw [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α ≃ β
s : Set β
apply : s ⊆ range.{v, u + 1} (ι := α) (⇑f : (a : α) → β)
⊢ lift.{v, u} #(↑((⇑f : (a : α) → β) ⁻¹' s) : Type u) = lift.{u, v} #(↑s : Type v)

Tactic:
apply mk_preimage_of_injective_of_subset_range_lift _ _ f.injective

Premises used: Cardinal.mk_preimage_of_injective_of_subset_range_lift, Equiv.injective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α ≃ β
s : Set β
rw : s ⊆ univ
⊢ s ⊆ range.{v, u + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
rw [f.range_eq_univ]

Premises used: Equiv.range_eq_univ
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ s ⊆ univ

Tactic:
fun _ _ ↦ ⟨⟩

Premises used: Set.Mem, Set.univ, setOf, Set.Subset, True.intro
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ s ⊆ univ

Tactic:
exact fun _ _ ↦ ⟨⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α ≃ β
s : Set β
⊢ #(↑((⇑f : (a : α) → β) ⁻¹' s) : Type u) = #(↑s : Type u)

Tactic:
simpa using mk_preimage_equiv_lift f s

Premises used: Cardinal.mk_preimage_equiv_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set β
h : Injective f
rw : lift.{u, u} #(↑(f ⁻¹' s) : Type u) ≤ lift.{u, u} #(↑s : Type u)
⊢ #(↑(f ⁻¹' s) : Type u) ≤ #(↑s : Type u)

Tactic:
rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]

Premises used: Cardinal.mk, Set.Elem, Set.preimage, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ lift.{u, u} #(↑(f ⁻¹' s) : Type u) ≤ lift.{u, u} #(↑s : Type u)

Tactic:
mk_preimage_of_injective_lift f s h

Premises used: Cardinal.mk_preimage_of_injective_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ lift.{u, u} #(↑(f ⁻¹' s) : Type u) ≤ lift.{u, u} #(↑s : Type u)

Tactic:
exact mk_preimage_of_injective_lift f s h

Premises used: Cardinal.mk_preimage_of_injective_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
rw : lift.{u, u} #(↑s : Type u) ≤ lift.{u, u} #(↑(f ⁻¹' s) : Type u)
⊢ #(↑s : Type u) ≤ #(↑(f ⁻¹' s) : Type u)

Tactic:
rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]

Premises used: Cardinal.mk, Set.Elem, Set.preimage, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift.{u, u} #(↑s : Type u) ≤ lift.{u, u} #(↑(f ⁻¹' s) : Type u)

Tactic:
mk_preimage_of_subset_range_lift f s h

Premises used: Cardinal.mk_preimage_of_subset_range_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift.{u, u} #(↑s : Type u) ≤ lift.{u, u} #(↑(f ⁻¹' s) : Type u)

Tactic:
exact mk_preimage_of_subset_range_lift f s h

Premises used: Cardinal.mk_preimage_of_subset_range_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)

Tactic:
rw [image_eq_range] at h

Premises used: Set.image_eq_range
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
⊢ lift.{u, v} #(↑t : Type v) ≤ lift.{v, u} #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)

Tactic:
mk_preimage_of_subset_range_lift _ _ h

Premises used: Cardinal.mk_preimage_of_subset_range_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
h₁ :
  lift.{v, u} #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u) =
    lift.{v, u} #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)
⊢ lift.{u, v} #(↑t : Type v) ≤ lift.{v, u} #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u)

Tactic:
convert! mk_preimage_of_subset_range_lift _ _ h using 1

Premises used: Cardinal.mk_preimage_of_subset_range_lift
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
h₁ :
  lift.{v, u} #(↑{x : (↑s : Type u) | f (↑x : α) ∈ t} : Type u) =
    lift.{v, u} #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)
⊢ lift.{v, u} #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u) =
    lift.{v, u} #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)

Tactic:
rw [mk_sep]

Premises used: Cardinal.mk_sep
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
⊢ lift.{v, u} #(↑{x : (↑s : Type u) | f (↑x : α) ∈ t} : Type u) =
    lift.{v, u} #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)

Tactic:
rw [image_eq_range] at h

Premises used: Set.image_eq_range
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
⊢ #(↑t : Type u) ≤ #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)

Tactic:
mk_preimage_of_subset_range _ _ h

Premises used: Cardinal.mk_preimage_of_subset_range
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
h₁ : #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u) = #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)
⊢ #(↑t : Type u) ≤ #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u)

Tactic:
convert! mk_preimage_of_subset_range _ _ h using 1

Premises used: Cardinal.mk_preimage_of_subset_range
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
h₁ : #(↑{x : (↑s : Type u) | f (↑x : α) ∈ t} : Type u) = #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)
⊢ #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u) = #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)

Tactic:
rw [mk_sep]

Premises used: Cardinal.mk_sep
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
⊢ #(↑{x : (↑s : Type u) | f (↑x : α) ∈ t} : Type u) = #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u}
α : Type u
s : Set α
rw :
  (∃ (p : Set (↑s : Type u)), #(↑p : Type u) = c) ↔
    ∃ (s_1 : Set (↑s : Type u)), #(↑(Subtype.val (p := fun (x : α) ↦ x ∈ s) '' s_1) : Type u) = c
⊢ c ≤ #(↑s : Type u) ↔ ∃ p ⊆ s, #(↑p : Type u) = c

Tactic:
rw [le_mk_iff_exists_set, ← Subtype.exists_set_subtype]

Premises used: Cardinal.le_mk_iff_exists_set, Subtype.exists_set_subtype
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u}
α : Type u
s : Set α
h : ∀ (a : Set (↑s : Type u)), #(↑a : Type u) = c ↔ #(↑(Subtype.val (p := fun (x : α) ↦ x ∈ s) '' a) : Type u) = c
⊢ (∃ (p : Set (↑s : Type u)), #(↑p : Type u) = c) ↔
    ∃ (s_1 : Set (↑s : Type u)), #(↑(Subtype.val (p := fun (x : α) ↦ x ∈ s) '' s_1) : Type u) = c

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u}
α : Type u
s : Set α
t : Set (↑s : Type u)
h : Injective.{u + 1, u + 1} (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
⊢ #(↑t : Type u) = c ↔ #(↑(Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) : Type u) = c

Tactic:
rw [mk_image_eq]

Premises used: Cardinal.mk_image_eq
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u}
α : Type u
s : Set α
t : Set (↑s : Type u)
⊢ Injective.{u + 1, u + 1} (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
apply Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
rw : lift.{u, max u v} #(↑(range Sum.inl) : Type (max u v)) = lift.{v, u} #α
rw₁ : lift.{max u v, u} #α = lift.{v, u} #α
rw₂ rw₃ : lift.{v, u} #α = lift.{v, u} #α
⊢ #(↑(range Sum.inl) : Type (max u v)) = lift.{v, u} #α

Tactic:
rw [← lift_id'.{u, v} #_, (Equiv.Set.rangeInl α β).lift_cardinal_eq, lift_umax.{u, v}]

Premises used: Equiv.lift_cardinal_eq, Equiv.Set.rangeInl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
rw : lift.{v, max v u} #(↑(range Sum.inr) : Type (max u v)) = lift.{u, v} #β
rw₁ : lift.{max u v, v} #β = lift.{u, v} #β
rw₂ rw₃ : lift.{u, v} #β = lift.{u, v} #β
⊢ #(↑(range Sum.inr) : Type (max u v)) = lift.{u, v} #β

Tactic:
rw [← lift_id'.{v, u} #_, (Equiv.Set.rangeInr α β).lift_cardinal_eq, lift_umax.{v, u}]

Premises used: Equiv.lift_cardinal_eq, Equiv.Set.rangeInr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
rw : 1 < #α ↔ ∃ (x : α) (y : α), x ≠ y
rw₁ : Nontrivial α ↔ ∃ (x : α) (y : α), x ≠ y
rw₂ rw₃ : (∃ (x : α) (y : α), x ≠ y) ↔ ∃ (x : α) (y : α), x ≠ y
⊢ 2 ≤ #α ↔ ∃ (x : α) (y : α), x ≠ y

Tactic:
rw [two_le_iff_one_lt, one_lt_iff_nontrivial, nontrivial_iff]

Premises used: Cardinal.two_le_iff_one_lt, nontrivial_iff, Cardinal.one_lt_iff_nontrivial
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x : α
rw : (∃ (x : α) (y : α), x ≠ y) ↔ ∃ (y : α), y ≠ x
rw₁ : Nontrivial α ↔ ∃ (y : α), y ≠ x
rw₂ rw₃ : (∃ (y : α), y ≠ x) ↔ ∃ (y : α), y ≠ x
⊢ 2 ≤ #α ↔ ∃ (y : α), y ≠ x

Tactic:
rw [two_le_iff, ← nontrivial_iff, nontrivial_iff_exists_ne x]

Premises used: nontrivial_iff_exists_ne, nontrivial_iff, Cardinal.two_le_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
simp :
  (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) ↔
    ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
⊢ #α = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ

Tactic:
simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]

Premises used: Finset.card_eq_two, Cardinal.mk_eq_nat_iff_finset, Nat.cast_two
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
mp :
  (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) →
    ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
mpr :
  (∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ) →
    ∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}
⊢ (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) ↔
    ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x y : α
hne : x ≠ y
ht : (↑{x, y} : Set α) = univ
⊢ Eq (α := Set α) {x, y} univ

Tactic:
simpa using ht
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x y : α
hne : x ≠ y
ht : (↑{x, y} : Set α) = univ
⊢ ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ

Tactic:
exact ⟨x, y, hne, by simpa using ht⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x y : α
hne : x ≠ y
h : Eq (α := Set α) {x, y} univ
⊢ (↑{x, y} : Set α) = univ

Tactic:
simpa using h
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x y : α
hne : x ≠ y
h : Eq (α := Set α) {x, y} univ
⊢ ∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}

Tactic:
exact ⟨{x, y}, by simpa using h, x, y, hne, rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
simp :
  (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) ↔
    ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
mp :
  (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) →
    ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
mpr mpr₁ :
  (∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ) →
    ∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}
⊢ #α = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ

Tactic:
classical
  simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]
  constructor
  · rintro ⟨t, ht, x, y, hne, rfl⟩
    exact ⟨x, y, hne, by simpa using ht⟩
  · rintro ⟨x, y, hne, h⟩
    exact ⟨{x, y}, by simpa using h, x, y, hne, rfl⟩

Premises used: Finset.card_eq_two, Cardinal.mk_eq_nat_iff_finset, Nat.cast_two, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x : α
rw : (∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ) ↔ ∃! y : α, y ≠ x
⊢ #α = 2 ↔ ∃! y : α, y ≠ x

Tactic:
rw [mk_eq_two_iff]

Premises used: Cardinal.mk_eq_two_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x : α
mp : (∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ) → ∃! y : α, y ≠ x
mpr : (∃! y : α, y ≠ x) → ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
⊢ (∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ) ↔ ∃! y : α, y ≠ x

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x a b : α
hne : a ≠ b
h : Eq (α := Set α) {a, b} univ
⊢ ∀ (x : α), x = a ∨ x = b

Tactic:
simp only [eq_univ_iff_forall, mem_insert_iff, mem_singleton_iff] at h

Premises used: Set.eq_univ_iff_forall, Set.mem_singleton_iff, Set.mem_insert_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x a b : α
hne : a ≠ b
h : ∀ (x : α), x = a ∨ x = b
mp : ∀ (hne : x ≠ b) (h : ∀ (x_1 : α), x_1 = x ∨ x_1 = b), ∃! y : α, y ≠ x
mp₁ : ∀ (hne : a ≠ x) (h : ∀ (x_1 : α), x_1 = a ∨ x_1 = x), ∃! y : α, y ≠ x
⊢ ∃! y : α, y ≠ x

Tactic:
rcases h x with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x b : α
hne : x ≠ b
h : ∀ (x_1 : α), x_1 = x ∨ x_1 = b
⊢ ∃! y : α, y ≠ x

Tactic:
⟨b, hne.symm, fun z => (h z).resolve_left⟩

Premises used: Or.resolve_left, Ne.symm, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x a : α
hne : a ≠ x
h : ∀ (x_1 : α), x_1 = a ∨ x_1 = x
⊢ ∃! y : α, y ≠ x

Tactic:
⟨a, hne, fun z => (h z).resolve_right⟩

Premises used: ExistsUnique, And.intro, Exists.intro, Or.resolve_right
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x b : α
hne : x ≠ b
h : ∀ (x_1 : α), x_1 = x ∨ x_1 = b
⊢ ∃! y : α, y ≠ x

Tactic:
exacts [⟨b, hne.symm, fun z => (h z).resolve_left⟩, ⟨a, hne, fun z => (h z).resolve_right⟩]
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x y : α
hne : y ≠ x
hy : ∀ (y_1 : α), (fun (y : α) ↦ y ≠ x) y_1 → y_1 = y
⊢ ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ

Tactic:
⟨x, y, hne.symm, eq_univ_of_forall fun z => or_iff_not_imp_left.2 (hy z)⟩

Premises used: Iff.mpr, Ne.symm, Set.eq_univ_of_forall, Classical.or_iff_not_imp_left, And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x y : α
hne : y ≠ x
hy : ∀ (y_1 : α), (fun (y : α) ↦ y ≠ x) y_1 → y_1 = y
⊢ ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ

Tactic:
exact ⟨x, y, hne.symm, eq_univ_of_forall fun z => or_iff_not_imp_left.2 (hy z)⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
l : List α
h : (↑l.length : Cardinal.{u_1}) < #α
contrapose! : ∀ (h : ∀ (z : α), z ∈ l), #α ≤ (↑l.length : Cardinal.{u_1})
⊢ ∃ (z : α), z ∉ l

Tactic:
contrapose! h
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
l : List α
h : ∀ (z : α), z ∈ l
⊢ #α = #(↑univ : Type u_1)

Tactic:
mk_univ.symm

Premises used: Cardinal.mk_univ, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
l : List α
h : ∀ (z : α), z ∈ l
⊢ #(↑univ : Type u_1) ≤ #↥l.toFinset

Tactic:
mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x)

Premises used: List.mem_toFinset, Iff.mpr, Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
l : List α
h : ∀ (z : α), z ∈ l
⊢ #↥l.toFinset = (↑l.toFinset.card : Cardinal.{u_1})

Tactic:
Cardinal.mk_coe_finset

Premises used: Cardinal.mk_coe_finset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
l : List α
h : ∀ (z : α), z ∈ l
⊢ LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑l.toFinset.card : Cardinal.{u_1}) (↑l.length : Cardinal.{u_1})

Tactic:
Nat.cast_le.mpr (List.toFinset_card_le l)

Premises used: Iff.mpr, List.toFinset_card_le, Nat.cast_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
l : List α
h : ∀ (z : α), z ∈ l
⊢ #α ≤ (↑l.length : Cardinal.{u_1})

Tactic:
calc
    #α = #(Set.univ : Set α) := mk_univ.symm
    _ ≤ #l.toFinset := mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x)
    _ = l.toFinset.card := Cardinal.mk_coe_finset
    _ ≤ l.length := Nat.cast_le.mpr (List.toFinset_card_le l)

Premises used: List.mem_toFinset, Iff.mpr, Cardinal.mk_univ, Set.univ, Cardinal.mk_coe_finset, List.toFinset, List.toFinset_card_le, Cardinal.mk_le_mk_of_subset, Finset.card, Nat.cast_le, Eq.symm, List.length
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
l : List α
h : (↑l.length : Cardinal.{u_1}) < #α
contrapose! contrapose!₁ : ∀ (h : (↑l.length : Cardinal.{u_1}) < #α), ∃ (z : α), z ∉ l
contrapose!₂ contrapose!₃ contrapose!₄ : ∀ (h : ∀ (z : α), z ∈ l), #α ≤ (↑l.length : Cardinal.{u_1})
⊢ ∃ (z : α), z ∉ l

Tactic:
classical
  contrapose! h
  calc
    #α = #(Set.univ : Set α) := mk_univ.symm
    _ ≤ #l.toFinset := mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x)
    _ = l.toFinset.card := Cardinal.mk_coe_finset
    _ ≤ l.length := Nat.cast_le.mpr (List.toFinset_card_le l)

Premises used: Cardinal.mk_univ, Set.univ, Cardinal.mk_coe_finset, Eq.symm, List.length
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
h : 3 ≤ #α
x y : α
⊢ (↑3 : Cardinal.{u_1}) ≤ #α

Tactic:
simpa using h
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
h : 3 ≤ #α
x y : α
⊢ (↑3 : Cardinal.{u_1}) ≤ #α

Tactic:
have : ↑(3 : ℕ) ≤ #α := by simpa using h
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
h : 3 ≤ #α
x y : α
this : (↑3 : Cardinal.{u_1}) ≤ #α
rwa : HAdd.hAdd (α := Cardinal.{u_1}) (↑2 : Cardinal.{u_1}) 1 ≤ #α
rwa₁ rwa₂ rwa₃ rwa₄ : (↑(HAdd.hAdd (α := ℕ) 2 1) : Cardinal.{u_1}) ≤ #α
⊢ (↑2 : Cardinal.{u_1}) < #α

Tactic:
rwa [← natCast_add_one_le_iff, ← Nat.cast_add_one]

Premises used: Cardinal.natCast_add_one_le_iff, Nat.cast_add_one