awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : Fin (HPow.hPow (α := ℕ) (β := ℕ) 2 32)
⊢ (BitVec.toFin ∘ Int32.toBitVec) ((Int32.ofBitVec ∘ BitVec.ofFin) x) = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : Int64
⊢ (Int64.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int64.toBitVec) x) = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : Fin (HPow.hPow (α := ℕ) (β := ℕ) 2 64)
⊢ (BitVec.toFin ∘ Int64.toBitVec) ((Int64.ofBitVec ∘ BitVec.ofFin) x) = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
n : ℕ
x : BitVec n
⊢ { toFin := x.toFin : BitVec n } = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
n : ℕ
x : Fin (HPow.hPow (α := ℕ) 2 n)
⊢ { toFin := x : BitVec n }.toFin = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
⊢ card UInt8 = HPow.hPow (α := ℕ) (β := ℕ) 2 8

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
⊢ card UInt16 = HPow.hPow (α := ℕ) (β := ℕ) 2 16

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
⊢ card UInt32 = HPow.hPow (α := ℕ) (β := ℕ) 2 32

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
⊢ card UInt64 = HPow.hPow (α := ℕ) (β := ℕ) 2 64

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
⊢ card Int8 = HPow.hPow (α := ℕ) (β := ℕ) 2 8

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
⊢ card Int16 = HPow.hPow (α := ℕ) (β := ℕ) 2 16

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
⊢ card Int32 = HPow.hPow (α := ℕ) (β := ℕ) 2 32

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
⊢ card Int64 = HPow.hPow (α := ℕ) (β := ℕ) 2 64

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
n : ℕ
⊢ card (BitVec n) = HPow.hPow (α := ℕ) 2 n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u_1
inst : FinEnum α
β : α → Type u_2
inst_1 : (a : α) → FinEnum (β a)
xs : List α
f : (a : α) → a ∈ xs → β a
⊢ Membership.mem (γ := List ((i : α) → i ∈ xs → β i)) (xs.pi (α := β) fun (x : α) ↦ FinEnum.toList (β x)) f

Tactic:
(mem_pi _ _).mpr fun _ _ ↦ mem_toList _

Premises used: Iff.mpr, List.mem_pi, FinEnum.mem_toList
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u_1
inst : FinEnum α
β : α → Type u_2
inst_1 : (a : α) → FinEnum (β a)
f : (a : α) → β a
⊢ f ∈ enum β

Tactic:
simpa [Pi.enum] using ⟨fun a _ => f a, mem_pi_toList _ _, rfl⟩

Premises used: List.Pi.enum
-- Module: Mathlib.Data.FinEnum
Goal:
α_1 : Type u_1
inst : FinEnum α_1
β : α_1 → Type u_2
inst_1 : (a : α_1) → FinEnum (β a)
p : Prop
inst_2 : Decidable p
α : p → Type
inst_3 : (hp : p) → FinEnum (α hp)
hp : p
x : (hp : p) → α hp
⊢ Membership.mem (γ := List ((hp : p) → α hp)) (map (fun (x : α hp) (x_1 : p) ↦ x) (FinEnum.toList (α hp))) x

Tactic:
simpa using ⟨x hp, rfl⟩
-- Module: Mathlib.Data.FinEnum
Goal:
α_1 : Type u_1
inst : FinEnum α_1
β : α_1 → Type u_2
inst_1 : (a : α_1) → FinEnum (β a)
p : Prop
inst_2 : Decidable p
α : p → Type
inst_3 : (hp : p) → FinEnum (α hp)
hp : ¬p
⊢ ∀ (x : (hp : p) → α hp), Membership.mem (γ := List ((hp : p) → α hp)) [fun (hp' : p) ↦ ⋯.elim] x

Tactic:
simp [funext_iff, hp]

Premises used: funext_iff
-- Module: Mathlib.Data.Finite.Card
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst : Finite α
have : (this : α ≃ Fin (⋯.choose (p := fun (n : ℕ) ↦ Nonempty.{max 1 (u_4 + 1)} (α ≃ Fin n)))) → α ≃ Fin (Nat.card α)
⊢ α ≃ Fin (Nat.card α)

Tactic:
have := (Finite.exists_equiv_fin α).choose_spec.some
-- Module: Mathlib.Data.Finite.Card
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst : Finite α
this : α ≃ Fin (⋯.choose (p := fun (n : ℕ) ↦ Nonempty.{max 1 (u_4 + 1)} (α ≃ Fin n)))
rwa rwa₁ rwa₂ rwa₃ : α ≃ Fin (⋯.choose (p := fun (n : ℕ) ↦ Nonempty.{max 1 (u_4 + 1)} (α ≃ Fin n)))
⊢ α ≃ Fin (Nat.card α)

Tactic:
rwa [Nat.card_eq_of_equiv_fin this]

Premises used: Nat.card_eq_of_equiv_fin
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Finite α
n : ℕ
h : Nat.card α = n
subst : α ≃ Fin (Nat.card α)
⊢ α ≃ Fin n

Tactic:
subst h
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Finite α
⊢ α ≃ Fin (Nat.card α)

Tactic:
apply Finite.equivFin

Premises used: Finite.equivFin
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_4
inl : Finite α → Nat.card α = if x : Finite α then Fintype.card α else 0
inr : Infinite α → Nat.card α = if x : Finite α then Fintype.card α else 0
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Tactic:
cases finite_or_infinite α

Premises used: finite_or_infinite
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_4
h : Finite α
this : Fintype α := Fintype.ofFinite α
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Tactic:
simp only [this, *, Nat.card_eq_fintype_card, dif_pos]

Premises used: dif_pos, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_4
h : Infinite α
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Tactic:
simp only [*, card_eq_zero_of_infinite, not_finite_iff_infinite.mpr, dite_false]

Premises used: Iff.mpr, dite_false, not_finite_iff_infinite, Nat.card_eq_zero_of_infinite
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
haveI : ∀ (this : Fintype α), 0 < Nat.card α ↔ Nonempty α
⊢ 0 < Nat.card α ↔ Nonempty α

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
this : Fintype α
rw : 0 < Fintype.card α ↔ Nonempty α
rw₁ rw₂ : Nonempty α ↔ Nonempty α
⊢ 0 < Nat.card α ↔ Nonempty α

Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]

Premises used: Fintype.card_pos_iff, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
h : Nonempty α
⊢ 0 < Nat.card α

Tactic:
Finite.card_pos_iff.mpr h

Premises used: Iff.mpr, Finite.card_pos_iff
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
haveI : ∀ (this : Fintype α), Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this : Fintype α
haveI : ∀ (this : Fintype β), Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)

Tactic:
haveI := Fintype.ofFinite β
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this_1 : Fintype α
this : Fintype β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_eq]

Premises used: Fintype.card_eq, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
haveI : ∀ (this : Fintype α), Nat.card α ≤ 1 ↔ Subsingleton α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
this : Fintype α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_le_one_iff_subsingleton]

Premises used: Nat.card_eq_fintype_card, Fintype.card_le_one_iff_subsingleton
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
haveI : ∀ (this : Fintype α), 1 < Nat.card α ↔ Nontrivial α
⊢ 1 < Nat.card α ↔ Nontrivial α

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
this : Fintype α
⊢ 1 < Nat.card α ↔ Nontrivial α

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.one_lt_card_iff_nontrivial]

Premises used: Fintype.one_lt_card_iff_nontrivial, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
h : Nontrivial α
⊢ 1 < Nat.card α

Tactic:
one_lt_card_iff_nontrivial.mpr h

Premises used: Iff.mpr, Finite.one_lt_card_iff_nontrivial
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
haveI : ∀ (this : Fintype α), Nat.card.{u_1} (Option α) = Nat.card α + 1
⊢ Nat.card.{u_1} (Option α) = Nat.card α + 1

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
this : Fintype α
⊢ Nat.card.{u_1} (Option α) = Nat.card α + 1

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_option]

Premises used: Fintype.card_option, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α ↪ β
⊢ Nat.card α ≤ Nat.card β

Tactic:
Nat.card_le_card_of_injective _ f.injective

Premises used: Nat.card_le_card_of_injective, Function.Embedding.injective
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
haveI : ∀ (this : Fintype α), Nat.card α = 0 ↔ IsEmpty α
⊢ Nat.card α = 0 ↔ IsEmpty α

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
this : Fintype α
⊢ Nat.card α = 0 ↔ IsEmpty α

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_eq_zero_iff]

Premises used: Fintype.card_eq_zero_iff, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
h : Nat.card β = 0 → Nat.card α = 0
⊢ Nat.card α ≤ Nat.card β

Tactic:
(or_not_of_imp h).casesOn (fun h => le_of_eq_of_le h (Nat.zero_le _)) fun h =>
    @Nat.card_le_card_of_injective α β (Nat.finite_of_card_ne_zero h) f hf

Premises used: or_not_of_imp, Or.casesOn
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
h : Nat.card β = 0 → Nat.card α = 0
⊢ Nat.card α ≤ Nat.card β

Tactic:
card_le_of_injective' f.2 h

Premises used: Function.Embedding.inj', Finite.card_le_of_injective'
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card α = 0 → Nat.card β = 0
⊢ Nat.card β ≤ Nat.card α

Tactic:
(or_not_of_imp h).casesOn (fun h => le_of_eq_of_le h (Nat.zero_le _)) fun h =>
    @Nat.card_le_card_of_surjective α β (Nat.finite_of_card_ne_zero h) f hf

Premises used: or_not_of_imp, Or.casesOn
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
inl : Finite β → Nat.card α = 0
inr : Infinite β → Nat.card α = 0
⊢ Nat.card α = 0

Tactic:
cases finite_or_infinite β

Premises used: finite_or_infinite
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h_1 : Finite β
⊢ IsEmpty β

Tactic:
haveI := card_eq_zero_iff.mp h
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h_1 : Finite β
this : IsEmpty β
⊢ IsEmpty α

Tactic:
haveI := Function.isEmpty f
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h_1 : Finite β
this_1 : IsEmpty β
this : IsEmpty α
⊢ Nat.card α = 0

Tactic:
Nat.card_of_isEmpty

Premises used: Nat.card_of_isEmpty
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h_1 : Finite β
this_1 : IsEmpty β
this : IsEmpty α
⊢ Nat.card α = 0

Tactic:
exact Nat.card_of_isEmpty

Premises used: Nat.card_of_isEmpty
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h_1 : Infinite β
⊢ Infinite α

Tactic:
haveI := Infinite.of_surjective f hf
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h_1 : Infinite β
this : Infinite α
⊢ Nat.card α = 0

Tactic:
Nat.card_eq_zero_of_infinite

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h_1 : Infinite β
this : Infinite α
⊢ Nat.card α = 0

Tactic:
exact Nat.card_eq_zero_of_infinite

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
f : α → β
hf : Function.Injective f
h : Nat.card α = 0
⊢ Nat.card β = 0

Tactic:
card_eq_zero_of_surjective (Function.invFun_surjective hf) h

Premises used: Finite.card_eq_zero_of_surjective, Function.invFun_surjective
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
f : α ↪ β
h : Nat.card α = 0
⊢ Nat.card β = 0

Tactic:
card_eq_zero_of_injective f.2 h

Premises used: Finite.card_eq_zero_of_injective, Function.Embedding.inj'
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
f : α → β
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) ≤ Nat.card.{u_1} (↑s : Type u_1)

Tactic:
Nat.card_le_card_of_surjective _ Set.imageFactorization_surjective

Premises used: Nat.card_le_card_of_surjective, Set.imageFactorization_surjective
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
⊢ Nat.card.{u_2} (↑(Set.range f) : Type u_2) ≤ Nat.card α

Tactic:
Nat.card_le_card_of_surjective _ Set.rangeFactorization_surjective

Premises used: Nat.card_le_card_of_surjective, Set.rangeFactorization_surjective
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
p : α → Prop
haveI : ∀ (this : Fintype α), Nat.card.{u_1} { x : α // p x } ≤ Nat.card α
⊢ Nat.card.{u_1} { x : α // p x } ≤ Nat.card α

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
p : α → Prop
this : Fintype α
⊢ Nat.card.{u_1} { x : α // p x } ≤ Nat.card α

Tactic:
simpa only [Nat.card_eq_fintype_card] using Fintype.card_subtype_le p

Premises used: Fintype.card_subtype_le, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
p : α → Prop
haveI haveI₁ haveI₂ : ∀ (this : Fintype α), Nat.card.{u_1} { x : α // p x } ≤ Nat.card α
⊢ Nat.card.{u_1} { x : α // p x } ≤ Nat.card α

Tactic:
classical
  haveI := Fintype.ofFinite α
  simpa only [Nat.card_eq_fintype_card] using Fintype.card_subtype_le p

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
p : α → Prop
x : α
hx : ¬p x
haveI : ∀ (this : Fintype α), Nat.card.{u_1} { x : α // p x } < Nat.card α
⊢ Nat.card.{u_1} { x : α // p x } < Nat.card α

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
p : α → Prop
x : α
hx : ¬p x
this : Fintype α
⊢ Nat.card.{u_1} { x : α // p x } < Nat.card α

Tactic:
simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx

Premises used: Fintype.card_subtype_lt, gt_iff_lt, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
inst : Finite α
p : α → Prop
x : α
hx : ¬p x
haveI haveI₁ haveI₂ : ∀ (this : Fintype α), Nat.card.{u_1} { x : α // p x } < Nat.card α
⊢ Nat.card.{u_1} { x : α // p x } < Nat.card α

Tactic:
classical
  haveI := Fintype.ofFinite α
  simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx

Premises used: gt_iff_lt, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_4
inst : Finite α
a : Eq (α := ℕ∞) ((↑(Nat.card α) : ℕ∞) : ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_4}) → ℕ∞) (Cardinal.mk α) : ℕ∞)
⊢ Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_4}) → ℕ∞) (Cardinal.mk α) : ℕ∞) ((↑(Nat.card α) : ℕ∞) : ℕ∞)

Tactic:
apply symm

Premises used: symm
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_4
inst : Finite α
a : (↑(Nat.card α) : Cardinal.{u_4}) = Cardinal.mk α
⊢ Eq (α := ℕ∞) ((↑(Nat.card α) : ℕ∞) : ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_4}) → ℕ∞) (Cardinal.mk α) : ℕ∞)

Tactic:
rw [Cardinal.natCast_eq_toENat]

Premises used: Cardinal.natCast_eq_toENat
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_4
inst : Finite α
⊢ (↑(Nat.card α) : Cardinal.{u_4}) = Cardinal.mk α

Tactic:
Nat.cast_card

Premises used: Nat.cast_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_4
inst : Finite α
⊢ (↑(Nat.card α) : Cardinal.{u_4}) = Cardinal.mk α

Tactic:
exact Nat.cast_card

Premises used: Nat.cast_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
inl :
  ∀ (h : Finite.{u_1 + 1} (↑(s ∪ t) : Type u_1)),
    Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)
inr :
  ∀ (h : Infinite.{u_1 + 1} (↑(s ∪ t) : Type u_1)),
    Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)
⊢ Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)

Tactic:
rcases _root_.finite_or_infinite (↥(s ∪ t)) with h | h

Premises used: finite_or_infinite, Set.Elem, Union.union
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
h : Finite.{u_1 + 1} (↑(s ∪ t) : Type u_1)
⊢ Finite.{u_1 + 1} (↑s : Type u_1) ∧ Finite.{u_1 + 1} (↑t : Type u_1)

Tactic:
rw [finite_coe_iff, finite_union, ← finite_coe_iff, ← finite_coe_iff] at h

Premises used: Set.finite_union, Set.finite_coe_iff
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
h : Finite.{u_1 + 1} (↑s : Type u_1) ∧ Finite.{u_1 + 1} (↑t : Type u_1)
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
cases h
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
h : Finite.{u_1 + 1} (↑s : Type u_1) ∧ Finite.{u_1 + 1} (↑t : Type u_1)
left : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ Finite.{u_1 + 1} (↑t : Type u_1)

Tactic:
cases h
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
left : Finite.{u_1 + 1} (↑s : Type u_1)
right : Finite.{u_1 + 1} (↑t : Type u_1)
inl : Cardinal.mk (↑(s ∪ t) : Type u_1) ≤ Cardinal.mk (↑s : Type u_1) + Cardinal.mk (↑t : Type u_1)
⊢ Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)

Tactic:
rw [← @Nat.cast_le Cardinal, Nat.cast_add, Nat.cast_card, Nat.cast_card, Nat.cast_card]

Premises used: Nat.cast_add, Nat.cast_card, Nat.cast_le
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
left : Finite.{u_1 + 1} (↑s : Type u_1)
right : Finite.{u_1 + 1} (↑t : Type u_1)
⊢ Cardinal.mk (↑(s ∪ t) : Type u_1) ≤ Cardinal.mk (↑s : Type u_1) + Cardinal.mk (↑t : Type u_1)

Tactic:
Cardinal.mk_union_le s t

Premises used: Cardinal.mk_union_le
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
left : Finite.{u_1 + 1} (↑s : Type u_1)
right : Finite.{u_1 + 1} (↑t : Type u_1)
⊢ Cardinal.mk (↑(s ∪ t) : Type u_1) ≤ Cardinal.mk (↑s : Type u_1) + Cardinal.mk (↑t : Type u_1)

Tactic:
exact Cardinal.mk_union_le s t

Premises used: Cardinal.mk_union_le
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
h : Infinite.{u_1 + 1} (↑(s ∪ t) : Type u_1)
⊢ Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)

Tactic:
simp
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
have : ∀ (this : Fintype (↑t : Type u_1)), Nat.card.{u_1} (↑s : Type u_1) < Nat.card.{u_1} (↑t : Type u_1)
⊢ Nat.card.{u_1} (↑s : Type u_1) < Nat.card.{u_1} (↑t : Type u_1)

Tactic:
have : Fintype t := Finite.fintype ht
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this : Fintype (↑t : Type u_1)
have : ∀ (this : Fintype (↑s : Type u_1)), Nat.card.{u_1} (↑s : Type u_1) < Nat.card.{u_1} (↑t : Type u_1)
⊢ Nat.card.{u_1} (↑s : Type u_1) < Nat.card.{u_1} (↑t : Type u_1)

Tactic:
have : Fintype s := Finite.fintype (subset ht (subset_of_ssubset hsub))
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this_1 : Fintype (↑t : Type u_1)
this : Fintype (↑s : Type u_1)
simp : Fintype.card.{u_1} (↑s : Type u_1) < Fintype.card.{u_1} (↑t : Type u_1)
⊢ Nat.card.{u_1} (↑s : Type u_1) < Nat.card.{u_1} (↑t : Type u_1)

Tactic:
simp only [Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this_1 : Fintype (↑t : Type u_1)
this : Fintype (↑s : Type u_1)
⊢ Fintype.card.{u_1} (↑s : Type u_1) < Fintype.card.{u_1} (↑t : Type u_1)

Tactic:
Set.card_lt_card hsub

Premises used: Set.card_lt_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this_1 : Fintype (↑t : Type u_1)
this : Fintype (↑s : Type u_1)
⊢ Fintype.card.{u_1} (↑s : Type u_1) < Fintype.card.{u_1} (↑t : Type u_1)

Tactic:
exact Set.card_lt_card hsub

Premises used: Set.card_lt_card
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
hsub : s ⊆ t
⊢ ENat.card.{u_1} (↑s : Type u_1) ≤ ENat.card.{u_1} (↑t : Type u_1)

Tactic:
ENat.card_le_card_of_injective <| inclusion_injective hsub

Premises used: ENat.card_le_card_of_injective, Set.inclusion_injective
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
suffices : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1) → t ⊆ s
⊢ ENat.card.{u_1} (↑s : Type u_1) < ENat.card.{u_1} (↑t : Type u_1)

Tactic:
suffices ENat.card t ≤ ENat.card s → t ⊆ s from
    lt_of_le_not_ge (ecard_le_ecard hsub.subset) fun hle ↦ not_subset_of_ssubset hsub <| this hle
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
this : ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0
rwa : t \ s = ∅
rwa₁ : IsEmpty.{u_1 + 1} (↑(t \ s) : Type u_1)
rwa₂ : ENat.card.{u_1} (↑(t \ s) : Type u_1) = 0
rwa₃ rwa₄ rwa₅ rwa₆ : ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0
⊢ t ⊆ s

Tactic:
rwa [← diff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]

Premises used: ENat.card_eq_zero_iff_empty, Set.isEmpty_coe_sort, Set.diff_eq_empty, nonpos_iff_eq_zero
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
suffices : ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0
⊢ t ⊆ s

Tactic:
suffices ENat.card ↑(t \ s) ≤ 0 by
    rwa [← diff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
suffices : ENat.card.{u_1} (↑(t \ s) : Type u_1) + ENat.card.{u_1} (↑s : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
⊢ ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0

Tactic:
suffices ENat.card ↑(t \ s) + ENat.card ↑s ≤ 0 + ENat.card ↑s from
    WithTop.le_of_add_le_add_right (ENat.card_lt_top.mpr hs).ne this
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
this : ENat.card.{u_1} (↑t : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
rwa : ENat.card.{u_1} ((↑(t \ s) : Type u_1) ⊕ (↑s : Type u_1)) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
rwa₁ : ENat.card.{u_1} (↑(t \ s ∪ s) : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
rwa₂ rwa₃ rwa₄ rwa₅ : ENat.card.{u_1} (↑t : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
⊢ ENat.card.{u_1} (↑(t \ s) : Type u_1) + ENat.card.{u_1} (↑s : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)

Tactic:
rwa [← ENat.card_sum, ← ENat.card_congr <| Equiv.Set.union disjoint_sdiff_left,
      diff_union_of_subset hsub.subset]

Premises used: ENat.card_congr, Equiv.Set.union, HasSSubset.SSubset.subset, ENat.card_sum, Set.disjoint_sdiff_left, Set.diff_union_of_subset
-- Module: Mathlib.Data.Finite.Card
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
suffices : ENat.card.{u_1} (↑t : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
⊢ ENat.card.{u_1} (↑(t \ s) : Type u_1) + ENat.card.{u_1} (↑s : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)

Tactic:
suffices ENat.card ↑t ≤ 0 + ENat.card ↑s by
    rwa [← ENat.card_sum, ← ENat.card_congr <| Equiv.Set.union disjoint_sdiff_left,
      diff_union_of_subset hsub.subset]