awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α β : Type u
s : Set α
t : Set β
rw : #(↑(s ×ˢ t) : Type u) = #((↑s : Type u) × (↑t : Type u))
⊢ #(↑(s ×ˢ t) : Type u) = #(↑s : Type u) * #(↑t : Type u)
have rw₁ : #((↑s : Type u) × (↑t : Type u)) = #((↑s : Type u) × (↑t : Type u))
Tactic: rw [mul_def, mk_congr (Equiv.Set.prod ..)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ #(↑(image2 f s t) : Type u) ≤ #(↑s : Type u) * #(↑t : Type u)
have rw : #(↑(uncurry f '' s ×ˢ t) : Type u) ≤ #(↑(s ×ˢ t) : Type u)
Tactic: rw [← image_uncurry_prod, ← mk_setProd]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift.{v, u} #α ≤ lift.{u, v} #β
have rw : lift.{u, v} #(↑(range f) : Type v) ≤ lift.{u, v} #β
Tactic: rw [← Cardinal.mk_range_eq_of_injective hf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
ι : Type v
f : ι → Set α
⊢ lift.{v, u} #(↑(⋃ (i : ι), f i) : Type u) ≤ lift.{u, v} #ι * ⨆ (i : ι), lift.{v, u} #(↑(f i) : Type u)
have refine : (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)) = sum fun (i : ι) ↦ lift.{v, u} #(↑(f i) : Type u)
Tactic: refine mk_iUnion_le_sum_mk_lift.trans <| Eq.trans_le ?_ (sum_le_lift_mk_mul_iSup _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
ι : Type v
f : ι → Set α
⊢ (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)) = sum fun (i : ι) ↦ lift.{v, u} #(↑(f i) : Type u)
have rw : (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)) = lift.{v, max u v} (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u))
Tactic: rw [← lift_sum, lift_id'.{_, u}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
ι : Type v
f : ι → Set α
rw : (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)) = lift.{v, max u v} (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u))
⊢ (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)) = sum fun (i : ι) ↦ lift.{v, u} #(↑(f i) : Type u)
have rw₁ : (sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)) = sum.{v, u} fun (i : ι) ↦ #(↑(f i) : Type u)
Tactic: rw [← lift_sum, lift_id'.{_, u}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
A : Set (Set α)
⊢ #(↑(⋃₀ A) : Type u) ≤ #(↑A : Type u) * ⨆ (s : (↑A : Type u)), #(↑(↑s : Set α) : Type u)
have rw : #(↑(⋃ (i : (↑A : Type u)), (↑i : Set α)) : Type u) ≤ #(↑A : Type u) * ⨆ (s : (↑A : Type u)), #(↑(↑s : Set α) : Type u)
Tactic: rw [sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι α : Type u
A : ι → Set α
s : Set ι
⊢ #(↑(⋃ x ∈ s, A x) : Type u) ≤ #(↑s : Type u) * ⨆ (x : (↑s : Type u)), #(↑(A (↑x : ι)) : Type u)
have rw : #(↑(⋃ (x : (↑s : Type u)), A (↑x : ι)) : Type u) ≤ #(↑s : Type u) * ⨆ (x : (↑s : Type u)), #(↑(A (↑x : ι)) : Type u)
Tactic: rw [biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
ι : Type v
A : ι → Set α
s : Set ι
⊢ lift.{v, u} #(↑(⋃ x ∈ s, A x) : Type u) ≤
    lift.{u, v} #(↑s : Type v) * ⨆ (x : (↑s : Type v)), lift.{v, u} #(↑(A (↑x : ι)) : Type u)
have rw : lift.{v, u} #(↑(⋃ (x : (↑s : Type v)), A (↑x : ι)) : Type u) ≤
  lift.{u, v} #(↑s : Type v) * ⨆ (x : (↑s : Type v)), lift.{v, u} #(↑(A (↑x : ι)) : Type u)
Tactic: rw [biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u_1
s : Set α
n : ℕ
⊢ #(↑s : Type u_1) = (↑n : Cardinal.{u_1}) ↔ ∃ (t : Finset α), (↑t : Set α) = s ∧ t.card = n
have mp : #(↑s : Type u_1) = (↑n : Cardinal.{u_1}) → ∃ (t : Finset α), (↑t : Set α) = s ∧ t.card = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u_1
s : Set α
n : ℕ
mp : #(↑s : Type u_1) = (↑n : Cardinal.{u_1}) → ∃ (t : Finset α), (↑t : Set α) = s ∧ t.card = n
⊢ #(↑s : Type u_1) = (↑n : Cardinal.{u_1}) ↔ ∃ (t : Finset α), (↑t : Set α) = s ∧ t.card = n
have mpr : (∃ (t : Finset α), (↑t : Set α) = s ∧ t.card = n) → #(↑s : Type u_1) = (↑n : Cardinal.{u_1})
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u_1
s : Set α
n : ℕ
h : #(↑s : Type u_1) = (↑n : Cardinal.{u_1})
⊢ ∃ (t : Finset α), (↑t : Set α) = s ∧ t.card = n
have mp : ∀ (s : Finset α) (h : #(↑(↑s : Set α) : Type u_1) = (↑n : Cardinal.{u_1})),
  ∃ (t : Finset α), (↑t : Set α) = (↑s : Set α) ∧ t.card = n
Tactic: lift s to Finset α using lt_aleph0_iff_set_finite.1 (h.symm ▸ natCast_lt_aleph0)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
⊢ #α = (↑n : Cardinal.{u}) ↔ ∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n
have rw : #(↑univ : Type u) = (↑n : Cardinal.{u}) ↔ ∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n
Tactic: rw [← mk_univ, mk_set_eq_nat_iff_finset]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
rw : #(↑univ : Type u) = (↑n : Cardinal.{u}) ↔ ∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n
⊢ #α = (↑n : Cardinal.{u}) ↔ ∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n
have rw₁ : (∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n) ↔ ∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n
Tactic: rw [← mk_univ, mk_set_eq_nat_iff_finset]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
⊢ #α = (↑n : Cardinal.{u}) ↔ ∃ (h : Fintype α), Fintype.card α = n
have rw : (∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n) ↔ ∃ (h : Fintype α), Fintype.card α = n
Tactic: rw [mk_eq_nat_iff_finset]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
⊢ (∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n) ↔ ∃ (h : Fintype α), Fintype.card α = n
have mp : (∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n) → ∃ (h : Fintype α), Fintype.card α = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
mp : (∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n) → ∃ (h : Fintype α), Fintype.card α = n
⊢ (∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n) ↔ ∃ (h : Fintype α), Fintype.card α = n
have mpr : (∃ (h : Fintype α), Fintype.card α = n) → ∃ (t : Finset α), (↑t : Set α) = univ ∧ t.card = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
⊢ #(↑s : Type u) = 1 ↔ ∃ (x : α), s = {x}
have rw : Subsingleton.{u + 1} (↑s : Type u) ∧ Nonempty.{u + 1} (↑s : Type u) ↔ ∃ (x : α), s = {x}
Tactic: rw [eq_one_iff_unique, Set.exists_eq_singleton_iff_nonempty_subsingleton,
    Set.nonempty_coe_sort, Set.subsingleton_coe, and_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
rw : Subsingleton.{u + 1} (↑s : Type u) ∧ Nonempty.{u + 1} (↑s : Type u) ↔ ∃ (x : α), s = {x}
⊢ #(↑s : Type u) = 1 ↔ ∃ (x : α), s = {x}
have rw₁ : Subsingleton.{u + 1} (↑s : Type u) ∧ Nonempty.{u + 1} (↑s : Type u) ↔ s.Nonempty ∧ s.Subsingleton
Tactic: rw [eq_one_iff_unique, Set.exists_eq_singleton_iff_nonempty_subsingleton,
    Set.nonempty_coe_sort, Set.subsingleton_coe, and_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
rw : Subsingleton.{u + 1} (↑s : Type u) ∧ Nonempty.{u + 1} (↑s : Type u) ↔ ∃ (x : α), s = {x}
rw₁ : Subsingleton.{u + 1} (↑s : Type u) ∧ Nonempty.{u + 1} (↑s : Type u) ↔ s.Nonempty ∧ s.Subsingleton
⊢ #(↑s : Type u) = 1 ↔ ∃ (x : α), s = {x}
have rw₂ : Subsingleton.{u + 1} (↑s : Type u) ∧ s.Nonempty ↔ s.Nonempty ∧ s.Subsingleton
Tactic: rw [eq_one_iff_unique, Set.exists_eq_singleton_iff_nonempty_subsingleton,
    Set.nonempty_coe_sort, Set.subsingleton_coe, and_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
rw : Subsingleton.{u + 1} (↑s : Type u) ∧ Nonempty.{u + 1} (↑s : Type u) ↔ ∃ (x : α), s = {x}
rw₁ : Subsingleton.{u + 1} (↑s : Type u) ∧ Nonempty.{u + 1} (↑s : Type u) ↔ s.Nonempty ∧ s.Subsingleton
rw₂ : Subsingleton.{u + 1} (↑s : Type u) ∧ s.Nonempty ↔ s.Nonempty ∧ s.Subsingleton
⊢ #(↑s : Type u) = 1 ↔ ∃ (x : α), s = {x}
have rw₃ : s.Subsingleton ∧ s.Nonempty ↔ s.Nonempty ∧ s.Subsingleton
Tactic: rw [eq_one_iff_unique, Set.exists_eq_singleton_iff_nonempty_subsingleton,
    Set.nonempty_coe_sort, Set.subsingleton_coe, and_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
rw : Subsingleton.{u + 1} (↑s : Type u) ∧ Nonempty.{u + 1} (↑s : Type u) ↔ ∃ (x : α), s = {x}
rw₁ : Subsingleton.{u + 1} (↑s : Type u) ∧ Nonempty.{u + 1} (↑s : Type u) ↔ s.Nonempty ∧ s.Subsingleton
rw₂ : Subsingleton.{u + 1} (↑s : Type u) ∧ s.Nonempty ↔ s.Nonempty ∧ s.Subsingleton
rw₃ : s.Subsingleton ∧ s.Nonempty ↔ s.Nonempty ∧ s.Subsingleton
⊢ #(↑s : Type u) = 1 ↔ ∃ (x : α), s = {x}
have rw₄ : s.Nonempty ∧ s.Subsingleton ↔ s.Nonempty ∧ s.Subsingleton
Tactic: rw [eq_one_iff_unique, Set.exists_eq_singleton_iff_nonempty_subsingleton,
    Set.nonempty_coe_sort, Set.subsingleton_coe, and_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #(↑(insert a s) : Type u) = #(↑s : Type u) + 1
have rw : Disjoint s {a}
Tactic: rw [← union_singleton, mk_union_of_disjoint, mk_singleton]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
a : α
⊢ #(↑(insert a s) : Type u) ≤ #(↑s : Type u) + 1
have pos : ∀ (h : a ∈ s), #(↑(insert a s) : Type u) ≤ #(↑s : Type u) + 1
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
a : α
pos : ∀ (h : a ∈ s), #(↑(insert a s) : Type u) ≤ #(↑s : Type u) + 1
⊢ #(↑(insert a s) : Type u) ≤ #(↑s : Type u) + 1
have neg : ∀ (h : a ∉ s), #(↑(insert a s) : Type u) ≤ #(↑s : Type u) + 1
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #(↑(insert a s) : Type u) ≤ #(↑s : Type u) + 1
have neg : #(↑s : Type u) + 1 ≤ #(↑s : Type u) + 1
Tactic: rw [mk_insert h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
t : Set α
⊢ #(↑t : Type u) ≤ (↑n : Cardinal.{u}) ↔ ∀ (s : Finset α), (↑s : Set α) ⊆ t → s.card ≤ n
have refine : ∀ (H : ∀ (s : Finset α), (↑s : Set α) ⊆ t → s.card ≤ n), #(↑t : Type u) ≤ (↑n : Cardinal.{u})
Tactic: refine ⟨fun H s hs ↦ by simpa using (mk_le_mk_of_subset hs).trans H, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), (↑s : Set α) ⊆ t → s.card ≤ n
⊢ #(↑t : Type u) ≤ (↑n : Cardinal.{u})
have apply : ∀ (s : Finset (↑t : Type u)), s.card ≤ n
Tactic: apply card_le_of (fun s ↦ ?_)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), (↑s : Set α) ⊆ t → s.card ≤ n
s : Finset (↑t : Type u)
u : Finset α := Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ t)) s
⊢ s.card ≤ n
have this : u.card = s.card
Tactic: have : u.card = s.card := Finset.card_image_of_injOn Subtype.coe_injective.injOn
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), (↑s : Set α) ⊆ t → s.card ≤ n
s : Finset (↑t : Type u)
let let₁ let₂ : s.card ≤ n
⊢ s.card ≤ n
have let₃ : let u := Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ t)) s;
∀ (this : u.card = s.card), s.card ≤ n
Tactic: classical
  let u : Finset α := s.image Subtype.val
  have : u.card = s.card := Finset.card_image_of_injOn Subtype.coe_injective.injOn
  grind
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
⊢ #(↑A : Type u) < #(↑B : Type u)
have have : ∀ (this : Fintype (↑A : Type u)), #(↑A : Type u) < #(↑B : Type u)
Tactic: have : Fintype A := (hfin.subset hlt.subset).fintype
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
this : Fintype (↑A : Type u)
⊢ #(↑A : Type u) < #(↑B : Type u)
have have : ∀ (this : Fintype (↑B : Type u)), #(↑A : Type u) < #(↑B : Type u)
Tactic: have : Fintype B := hfin.fintype
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
A B : Set α
hfin : A.Finite
hlt : A ⊂ B
⊢ #(↑A : Type u) < #(↑B : Type u)
have inl : ∀ (hfin : Finite.{u + 1} (↑B : Type u)), #(↑A : Type u) < #(↑B : Type u)
Tactic: rcases finite_or_infinite B with hfin | hinf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
A B : Set α
hfin : A.Finite
hlt : A ⊂ B
inl : ∀ (hfin : Finite.{u + 1} (↑B : Type u)), #(↑A : Type u) < #(↑B : Type u)
⊢ #(↑A : Type u) < #(↑B : Type u)
have inr : ∀ (hinf : Infinite.{u + 1} (↑B : Type u)), #(↑A : Type u) < #(↑B : Type u)
Tactic: rcases finite_or_infinite B with hfin | hinf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
S T : Set α
h : T ⊆ S
⊢ #(↑(S \ T ∪ T) : Type u) = #(↑S : Type u)
have rw : #(↑S : Type u) = #(↑S : Type u)
Tactic: rw [diff_union_of_subset h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
S T : Set α
h : T ⊆ S
⊢ #(↑(S \ T) : Type u) + #(↑T : Type u) = #(↑S : Type u)
have refine : Disjoint (S \ T) T
Tactic: refine (mk_union_of_disjoint <| ?_).symm.trans <| by rw [diff_union_of_subset h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
S T : Set α
h : #(↑S : Type u) < #(↑T : Type u)
⊢ (T \ S).Nonempty
have rw : #(↑(T \ S) : Type u) ≠ 0
Tactic: rw [← mk_set_ne_zero_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
α : Type u
S : Set α
h : #(↑S : Type u) < #α
⊢ Sᶜ.Nonempty
have h₁ : #(↑S : Type u) < #(↑univ : Type u)
Tactic: rw [← mk_univ (α := α)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ lift.{v, u} #(↑(f ⁻¹' s) : Type u) ≤ lift.{u, v} #(↑s : Type v)
have rw : Nonempty (Embedding.{u + 1, v + 1} (↑(f ⁻¹' s) : Type u) (↑s : Type v))
Tactic: rw [lift_mk_le.{0}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Nonempty (Embedding.{u + 1, v + 1} (↑(f ⁻¹' s) : Type u) (↑s : Type v))
have 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) sorry)
Tactic: use Subtype.coind (fun x => f x.1) fun x => mem_preimage.mp x.2
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ 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) ⋯)
have inj' : Injective.{u + 1, v + 1} (β := β) fun (x : (↑(f ⁻¹' s) : Type u)) ↦ f (↑x : α)
Tactic: apply Subtype.coind_injective
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift.{u, v} #(↑s : Type v) ≤ lift.{v, u} #(↑(f ⁻¹' s) : Type u)
have h₁ : f '' f ⁻¹' s = s
Tactic: rw [← image_preimage_eq_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
h : f '' f ⁻¹' s = s
⊢ lift.{u, v} #(↑s : Type v) ≤ lift.{v, u} #(↑(f ⁻¹' s) : Type u)
have nth_rewrite : lift.{u, v} #(↑(f '' f ⁻¹' s) : Type v) ≤ lift.{v, u} #(↑(f ⁻¹' s) : Type u)
Tactic: nth_rewrite 1 [← h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #(↑(f ⁻¹' s) : Type u) = #(↑s : Type u)
have h₁ : #(↑(f ⁻¹' s) : Type u) = lift.{u, u} #(↑(f ⁻¹' s) : Type u)
Tactic: convert! mk_preimage_of_injective_of_subset_range_lift.{u, u} f s h h2 using 1
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
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)
⊢ #(↑(f ⁻¹' s) : Type u) = #(↑s : Type u)
have h₂ : #(↑s : Type u) = lift.{u, u} #(↑s : Type u)
Tactic: convert! mk_preimage_of_injective_of_subset_range_lift.{u, u} f s h h2 using 1
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #(↑(f ⁻¹' s) : Type u) = lift.{u, u} #(↑(f ⁻¹' s) : Type u)
have h₁ : #(↑(f ⁻¹' s) : Type u) = #(↑(f ⁻¹' s) : Type u)
Tactic: rw [lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #(↑s : Type u) = lift.{u, u} #(↑s : Type u)
have h₁ : #(↑s : Type u) = #(↑s : Type u)
Tactic: rw [lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ lift.{v, u} #(↑((⇑f : (a : α) → β) ⁻¹' s) : Type u) = lift.{u, v} #(↑s : Type v)
have apply : s ⊆ range.{v, u + 1} (ι := α) (⇑f : (a : α) → β)
Tactic: apply mk_preimage_of_injective_of_subset_range_lift _ _ f.injective
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ s ⊆ range.{v, u + 1} (ι := α) (⇑f : (a : α) → β)
have rw : s ⊆ univ
Tactic: rw [f.range_eq_univ]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ #(↑(f ⁻¹' s) : Type u) ≤ #(↑s : Type u)
have rw : lift.{u, u} #(↑(f ⁻¹' s) : Type u) ≤ lift.{u, u} #(↑s : Type u)
Tactic: rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ #(↑s : Type u) ≤ #(↑(f ⁻¹' s) : Type u)
have rw : lift.{u, u} #(↑s : Type u) ≤ lift.{u, u} #(↑(f ⁻¹' s) : Type u)
Tactic: rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ lift.{u, v} #(↑t : Type v) ≤ lift.{v, u} #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u)
have h₁ : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
Tactic: rw [image_eq_range] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
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} #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u)
have 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)
Tactic: convert! mk_preimage_of_subset_range_lift _ _ h using 1
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
⊢ lift.{v, u} #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u) =
    lift.{v, u} #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)
have 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)
Tactic: rw [mk_sep]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ #(↑t : Type u) ≤ #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u)
have h₁ : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
Tactic: rw [image_eq_range] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
⊢ #(↑t : Type u) ≤ #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u)
have h₁ : #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u) = #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)
Tactic: convert! mk_preimage_of_subset_range _ _ h using 1
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun (x : (↑s : Type u)) ↦ f (↑x : α)
⊢ #(↑{x : α | x ∈ s ∧ f x ∈ t} : Type u) = #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)
have h₁ : #(↑{x : (↑s : Type u) | f (↑x : α) ∈ t} : Type u) = #(↑((fun (x : (↑s : Type u)) ↦ f (↑x : α)) ⁻¹' t) : Type u)
Tactic: rw [mk_sep]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u}
α : Type u
s : Set α
⊢ c ≤ #(↑s : Type u) ↔ ∃ p ⊆ s, #(↑p : Type u) = c
have 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
Tactic: rw [le_mk_iff_exists_set, ← Subtype.exists_set_subtype]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u}
α : Type u
s : Set α
⊢ (∃ (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
have h : ∀ (a : Set (↑s : Type u)), #(↑a : Type u) = c ↔ #(↑(Subtype.val (p := fun (x : α) ↦ x ∈ s) '' a) : Type u) = c
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u}
α : Type u
s : Set α
t : Set (↑s : Type u)
⊢ #(↑t : Type u) = c ↔ #(↑(Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) : Type u) = c
have h : Injective.{u + 1, u + 1} (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
Tactic: rw [mk_image_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
β : Type v
⊢ #(↑(range Sum.inl) : Type (max u v)) = lift.{v, u} #α
have rw : lift.{u, max u v} #(↑(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}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
β : Type v
rw : lift.{u, max u v} #(↑(range Sum.inl) : Type (max u v)) = lift.{v, u} #α
⊢ #(↑(range Sum.inl) : Type (max u v)) = lift.{v, u} #α
have rw₁ : lift.{max u v, u} #α = lift.{v, u} #α
Tactic: rw [← lift_id'.{u, v} #_, (Equiv.Set.rangeInl α β).lift_cardinal_eq, lift_umax.{u, v}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
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} #α
⊢ #(↑(range Sum.inl) : Type (max u v)) = lift.{v, u} #α
have rw₂ : lift.{v, u} #α = lift.{v, u} #α
Tactic: rw [← lift_id'.{u, v} #_, (Equiv.Set.rangeInl α β).lift_cardinal_eq, lift_umax.{u, v}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
β : Type v
⊢ #(↑(range Sum.inr) : Type (max u v)) = lift.{u, v} #β
have rw : lift.{v, max v u} #(↑(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}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
β : Type v
rw : lift.{v, max v u} #(↑(range Sum.inr) : Type (max u v)) = lift.{u, v} #β
⊢ #(↑(range Sum.inr) : Type (max u v)) = lift.{u, v} #β
have rw₁ : lift.{max u v, v} #β = lift.{u, v} #β
Tactic: rw [← lift_id'.{v, u} #_, (Equiv.Set.rangeInr α β).lift_cardinal_eq, lift_umax.{v, u}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
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} #β
⊢ #(↑(range Sum.inr) : Type (max u v)) = lift.{u, v} #β
have rw₂ : lift.{u, v} #β = lift.{u, v} #β
Tactic: rw [← lift_id'.{v, u} #_, (Equiv.Set.rangeInr α β).lift_cardinal_eq, lift_umax.{v, u}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
⊢ 2 ≤ #α ↔ ∃ (x : α) (y : α), x ≠ y
have rw : 1 < #α ↔ ∃ (x : α) (y : α), x ≠ y
Tactic: rw [two_le_iff_one_lt, one_lt_iff_nontrivial, nontrivial_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : 1 < #α ↔ ∃ (x : α) (y : α), x ≠ y
⊢ 2 ≤ #α ↔ ∃ (x : α) (y : α), x ≠ y
have rw₁ : Nontrivial α ↔ ∃ (x : α) (y : α), x ≠ y
Tactic: rw [two_le_iff_one_lt, one_lt_iff_nontrivial, nontrivial_iff]