awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
simp_rw : 2 < Finset.card.{u_1} (α := α) univ ↔ ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
simp_rw₁ :
  (∃ (a : α) (b : α) (c : α),
      Membership.mem (γ := Finset α) univ a ∧
        Membership.mem (γ := Finset α) univ b ∧ Membership.mem (γ := Finset α) univ c ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔
    ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ 2 < card α ↔ ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
have simp_rw₂ : (∃ (a : α) (b : α) (c : α), True ∧ True ∧ True ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔
  ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic: simp_rw [← Finset.card_univ, two_lt_card_iff, mem_univ, true_and]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Finite α
f : α → α
hinj : Injective f
x : α
⊢ ∃ (a : α), f a = x
have have : ∀ (this : (a : Prop) → Decidable a), ∃ (a : α), f a = x
Tactic: have := Classical.propDecidable
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
⊢ ∃ (a : α), f a = x
have intro : ∀ (val : Fintype α), ∃ (a : α), f a = x
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (hypothesis)
Goal:
α : Type u_1
inst : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val : Fintype α
⊢ ∃ (a : α), f a = x
have h₁ : image f univ = univ
Tactic: have h₁ : image f univ = univ :=
    eq_of_subset_of_card_le (subset_univ _)
      ((card_image_of_injective univ hinj).symm ▸ le_rfl)
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (hypothesis)
Goal:
α : Type u_1
inst : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val : Fintype α
h₁ : image f univ = univ
⊢ ∃ (a : α), f a = x
have h₂ : x ∈ image f univ
Tactic: have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ x
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
⊢ ∃ (a : α), f a = x
have intro : ∀ (y : α) (h : Membership.mem (γ := Finset α) univ y ∧ f y = x), ∃ (a : α), f a = x
Tactic: obtain ⟨y, h⟩ := mem_image.1 h₂
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
⊢ Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card α ↔ s = Set.univ
have rw : #s.toFinset = Fintype.card α ↔ s = Set.univ
Tactic: rw [← Set.toFinset_card, Finset.card_eq_iff_eq_univ, ← Set.toFinset_univ, Set.toFinset_inj]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
rw : #s.toFinset = Fintype.card α ↔ s = Set.univ
⊢ Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card α ↔ s = Set.univ
have rw₁ : s.toFinset = univ ↔ s = Set.univ
Tactic: rw [← Set.toFinset_card, Finset.card_eq_iff_eq_univ, ← Set.toFinset_univ, Set.toFinset_inj]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
rw : #s.toFinset = Fintype.card α ↔ s = Set.univ
rw₁ : s.toFinset = univ ↔ s = Set.univ
⊢ Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card α ↔ s = Set.univ
have rw₂ : s.toFinset = Set.toFinset Set.univ ↔ s = Set.univ
Tactic: rw [← Set.toFinset_card, Finset.card_eq_iff_eq_univ, ← Set.toFinset_univ, Set.toFinset_inj]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
rw : #s.toFinset = Fintype.card α ↔ s = Set.univ
rw₁ : s.toFinset = univ ↔ s = Set.univ
rw₂ : s.toFinset = Set.toFinset Set.univ ↔ s = Set.univ
⊢ Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card α ↔ s = Set.univ
have rw₃ : s = Set.univ ↔ s = Set.univ
Tactic: rw [← Set.toFinset_card, Finset.card_eq_iff_eq_univ, ← Set.toFinset_univ, Set.toFinset_inj]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { a : α // p a }
x : α
hx : ¬p x
⊢ x ∉ Set.range (ι := { x : α // p x }) (Subtype.val (p := fun (x : α) ↦ p x))
have rwa : x ∉ {x : α | p x}
Tactic: rwa [Subtype.range_coe_subtype]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { a : α // p a }
inst_2 : DecidablePred p
⊢ card.{u_1} { x : α // p x } = Finset.card.{u_1} (α := α) {x : α | p x}
have refine : ∀ (x : α), Membership.mem (γ := Finset α) {x : α | p x} x ↔ p x
Tactic: refine Fintype.card_of_subtype _ ?_
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
⊢ card.{u_1} { x : α // ¬p x } = card α - card.{u_1} { x : α // p x }
have H : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}) x ↔ p x
Tactic: rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
H : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}) x ↔ p x
⊢ card.{u_1} { x : α // ¬p x } = card α - card.{u_1} { x : α // p x }
have H₁ : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
Tactic: rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
⊢ card.{u_1} { x : α // ¬p x } = card α - card.{u_1} { x : α // p x }
have rw : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}ᶜ) = card α - card.{u_1} { x : α // p x }
Tactic: classical
    rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
rw : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}ᶜ) = card α - card.{u_1} { x : α // p x }
⊢ card.{u_1} { x : α // ¬p x } = card α - card.{u_1} { x : α // p x }
have H : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
Tactic: classical
    rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
rw : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}ᶜ) = card α - card.{u_1} { x : α // p x }
H : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
⊢ card.{u_1} { x : α // ¬p x } = card α - card.{u_1} { x : α // p x }
have rw₁ : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x})ᶜ = card α - card.{u_1} { x : α // p x }
Tactic: classical
    rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
rw : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}ᶜ) = card α - card.{u_1} { x : α // p x }
H : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
rw₁ : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x})ᶜ = card α - card.{u_1} { x : α // p x }
H₁ : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
⊢ card.{u_1} { x : α // ¬p x } = card α - card.{u_1} { x : α // p x }
have rw₂ : card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}) = card α - card.{u_1} { x : α // p x }
Tactic: classical
    rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
rw : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}ᶜ) = card α - card.{u_1} { x : α // p x }
H : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
rw₁ : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x})ᶜ = card α - card.{u_1} { x : α // p x }
H₁ : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
rw₂ : card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}) = card α - card.{u_1} { x : α // p x }
H₂ : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
⊢ card.{u_1} { x : α // ¬p x } = card α - card.{u_1} { x : α // p x }
have rw₃ : card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}) =
  card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x})
Tactic: classical
    rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
rw : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}ᶜ) = card α - card.{u_1} { x : α // p x }
H : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
rw₁ : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x})ᶜ = card α - card.{u_1} { x : α // p x }
H₁ : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
rw₂ : card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}) = card α - card.{u_1} { x : α // p x }
H₂ : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
rw₃ :
  card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}) =
    card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x})
⊢ card.{u_1} { x : α // ¬p x } = card α - card.{u_1} { x : α // p x }
have s : Finset α
Tactic: classical
    rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
rw : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}ᶜ) = card α - card.{u_1} { x : α // p x }
H : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
rw₁ : Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x})ᶜ = card α - card.{u_1} { x : α // p x }
H₁ : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
rw₂ : card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}) = card α - card.{u_1} { x : α // p x }
H₂ : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}ᶜ) x ↔ ¬p x
rw₃ :
  card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x}) =
    card α - Finset.card.{u_1} (α := α) (Set.toFinset {x : α | p x})
s : Finset α
⊢ card.{u_1} { x : α // ¬p x } = card α - card.{u_1} { x : α // p x }
have H₃ : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}) x ↔ p x
Tactic: classical
    rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Finite α
p q : α → Prop
inst_1 : Fintype { x : α // p x }
inst_2 : Fintype { x : α // ¬p x }
inst_3 : Fintype { x : α // q x }
inst_4 : Fintype { x : α // ¬q x }
h : card.{u_1} { x : α // p x } = card.{u_1} { x : α // q x }
⊢ card.{u_1} { x : α // ¬p x } = card.{u_1} { x : α // ¬q x }
have intro : ∀ (val : Fintype α), card.{u_1} { x : α // ¬p x } = card.{u_1} { x : α // ¬q x }
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_4
inst : Fintype α
x : α
h : Fintype.card α = 1
⊢ Eq (α := Finset α) univ {x}
have symm : Eq (α := Finset α) {x} univ
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_4
inst : Fintype α
x : α
h : Fintype.card α = 1
⊢ Eq (α := Finset α) {x} univ
have apply : card.{u_4} (α := α) univ ≤ card (α := α) {x}
Tactic: apply eq_of_subset_of_card_le (subset_univ {x})
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
⊢ WellFounded r
have intro : ∀ (val : Fintype α), WellFounded r
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
val : Fintype α
x y : α
hxy : r x y
⊢ SSubset.{u_1} (α := Finset α) {z : α | r z x} {z : α | r z y}
have simp_rw : (∀ ⦃x_1 : α⦄, r x_1 x → r x_1 y) ∧ ¬∀ ⦃x_1 : α⦄, r x_1 y → r x_1 x
Tactic: simp_rw [Finset.lt_iff_ssubset.symm, lt_iff_le_not_ge, Finset.le_iff_subset,
        Finset.subset_iff, mem_filter_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (hypothesis)
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
val : Fintype α
⊢ WellFounded r
have this : ∀ (x y : α) (hxy : r x y), card.{u_1} (α := α) {z : α | r z x} < card.{u_1} (α := α) {z : α | r z y}
Tactic: have (x y) (hxy : r x y) : #{z | r z x} < #{z | r z y} :=
    Finset.card_lt_card <| by
      simp_rw [Finset.lt_iff_ssubset.symm, lt_iff_le_not_ge, Finset.le_iff_subset,
        Finset.subset_iff, mem_filter_univ]
      exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
⊢ WellFounded r
have intro : ∀ (val : Fintype α), WellFounded r
Tactic: classical
  cases nonempty_fintype α
  have (x y) (hxy : r x y) : #{z | r z x} < #{z | r z y} :=
    Finset.card_lt_card <| by
      simp_rw [Finset.lt_iff_ssubset.symm, lt_iff_le_not_ge, Finset.le_iff_subset,
        Finset.subset_iff, mem_filter_univ]
      exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
  exact Subrelation.wf (this _ _) (measure _).wf
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Finite α
r : α → α → Prop
inst_1 : IsTrans α r
inst_2 : Std.Irrefl r
intro : ∀ (val : Fintype α), WellFounded r
⊢ WellFounded r
have intro₁ : ∀ (val : Fintype α)
  (this : ∀ (x y : α) (hxy : r x y), card.{u_1} (α := α) {z : α | r z x} < card.{u_1} (α := α) {z : α | r z y}),
  WellFounded r
Tactic: classical
  cases nonempty_fintype α
  have (x y) (hxy : r x y) : #{z | r z x} < #{z | r z y} :=
    Finset.card_lt_card <| by
      simp_rw [Finset.lt_iff_ssubset.symm, lt_iff_le_not_ge, Finset.le_iff_subset,
        Finset.subset_iff, mem_filter_univ]
      exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
  exact Subrelation.wf (this _ _) (measure _).wf
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
α : Type u_4
inst : Fintype α
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
⊢ P α
have obtain : ∀ (n : ℕ) (hn : card α = n), P α
Tactic: obtain ⟨n, hn⟩ : ∃ n, Fintype.card α = n := ⟨Fintype.card α, rfl⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
α : Type u_4
inst : Fintype α
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
hn : card α = n
⊢ P α
have h : ∀ (n : ℕ) (ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α) (α : Type u_4) [inst : Fintype α]
  (hn : card α = n), P α
Tactic: induction n using Nat.strong_induction_on generalizing α with | _ n ih
Cleared hypotheses: α, inst, n, hn
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α
α : Type u_4
inst : Fintype α
hn : card α = n
⊢ P α
have h : ∀ (hsing : Subsingleton α), P α
Tactic: rcases subsingleton_or_nontrivial α with hsing | hnontriv
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α
α : Type u_4
inst : Fintype α
hn : card α = n
h : ∀ (hsing : Subsingleton α), P α
⊢ P α
have h₁ : ∀ (hnontriv : Nontrivial α), P α
Tactic: rcases subsingleton_or_nontrivial α with hsing | hnontriv
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α
α : Type u_4
inst : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ P α
have h : ∀ (β : Type u_4) [inst_1 : Fintype β], card β < card α → P β
Tactic: apply hstep
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (hypothesis)
Goal:
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_3 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α] (hn : card α = m), P α
α : Type u_4
inst : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_4
inst_1 : Fintype β
hlt : card β < card α
⊢ P β
have hlt₁ : card β < n
Tactic: rw [hn] at hlt
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
m n : ℕ
h : m ≤ n
| m
have rw : card (Fin m)
Tactic: rw [← Fintype.card_fin m]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
m n : ℕ
h : m ≤ n
⊢ card { i : Fin n // (↑i : ℕ) < m } = m
have conv_rhs : card { i : Fin n // (↑i : ℕ) < m } = card (Fin m)
Tactic: conv_rhs => rw [← Fintype.card_fin m]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
m n : ℕ
h : m ≤ n
⊢ card { i : Fin n // (↑i : ℕ) < m } = card (Fin m)
have f : { i : Fin n // (↑i : ℕ) < m } ≃ Fin m
Tactic: apply Fintype.card_congr
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
n m : ℕ
h : Fin n = Fin m
⊢ cast h = Fin.cast ⋯
have refl : ∀ (h : Fin n = Fin n), cast h = Fin.cast sorry
Tactic: cases fin_injective h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖
have rw : ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖
Tactic: rw [Subsingleton.elim emb Embedding.fintype]
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖
have refine_1 : ∀ (α₁ α₂ : Type u_1) (h₂ : Fintype α₂) (e : α₁ ≃ α₂)
  (ih : (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) α₁),
  (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) α₂
Tactic: refine Fintype.induction_empty_option (P := fun t ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖)
        (fun α₁ α₂ h₂ e ih ↦ ?_) (?_) (fun γ h ih ↦ ?_) α
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
emb : Fintype (α ↪ β)
refine_1 :
  ∀ (α₁ α₂ : Type u_1) (h₂ : Fintype α₂) (e : α₁ ≃ α₂)
    (ih : (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) α₁),
    (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) α₂
⊢ ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖
have refine_2 : (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) PEmpty.{u_1 + 1}
Tactic: refine Fintype.induction_empty_option (P := fun t ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖)
        (fun α₁ α₂ h₂ e ih ↦ ?_) (?_) (fun γ h ih ↦ ?_) α
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
emb : Fintype (α ↪ β)
refine_1 :
  ∀ (α₁ α₂ : Type u_1) (h₂ : Fintype α₂) (e : α₁ ≃ α₂)
    (ih : (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) α₁),
    (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) α₂
refine_2 : ‖PEmpty.{u_1 + 1} ↪ β‖ = ‖β‖.descFactorial ‖PEmpty.{u_1 + 1}‖
⊢ ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖
have refine_3 : ∀ (γ : Type u_1) (h : Fintype γ) (ih : (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) γ),
  (fun (t : Type u_1) [Fintype t] ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) (Option γ)
Tactic: refine Fintype.induction_empty_option (P := fun t ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖)
        (fun α₁ α₂ h₂ e ih ↦ ?_) (?_) (fun γ h ih ↦ ?_) α
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
β : Type u_2
inst : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₁‖
this : Fintype α₁ := ofEquiv α₂ e.symm
⊢ ‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖
have refine_1 : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖
Tactic: rw [← card_congr (Equiv.embeddingCongr e (Equiv.refl β)), ih, card_congr e]
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
β : Type u_2
inst : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₁‖
this : Fintype α₁ := ofEquiv α₂ e.symm
refine_1 : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖
⊢ ‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖
have refine_1₁ : ‖β‖.descFactorial ‖α₁‖ = ‖β‖.descFactorial ‖α₂‖
Tactic: rw [← card_congr (Equiv.embeddingCongr e (Equiv.refl β)), ih, card_congr e]
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
β : Type u_2
inst : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₁‖
this : Fintype α₁ := ofEquiv α₂ e.symm
refine_1 : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖
refine_1₁ : ‖β‖.descFactorial ‖α₁‖ = ‖β‖.descFactorial ‖α₂‖
⊢ ‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖
have refine_1₂ : ‖β‖.descFactorial ‖α₂‖ = ‖β‖.descFactorial ‖α₂‖
Tactic: rw [← card_congr (Equiv.embeddingCongr e (Equiv.refl β)), ih, card_congr e]