awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Infinite α
s : Finset α
n : ℕ
hn : #s ≤ n
zero : ∀ (s : Finset α) (hn : #s ≤ 0), ∃ (t : Finset α), s ⊆ t ∧ #t = 0
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n
have succ : ∀ (n : ℕ) (IH : ∀ (s : Finset α) (hn : #s ≤ n), ∃ (t : Finset α), s ⊆ t ∧ #t = n) (s : Finset α) (hn : #s ≤ n + 1),
  ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
Tactic: induction n generalizing s with
  | zero => exact ⟨s, subset_rfl, Nat.eq_zero_of_le_zero hn⟩
  | succ n IH =>
    rcases hn.eq_or_lt with hn' | hn'
    · exact ⟨s, subset_rfl, hn'⟩
    obtain ⟨t, hs, ht⟩ := IH _ (Nat.le_of_lt_succ hn')
    obtain ⟨x, hx⟩ := exists_notMem_finset t
    refine ⟨Finset.cons x t hx, hs.trans (Finset.subset_cons _), ?_⟩
    simp [ht]
Cleared hypotheses: s, n, hn
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
⊢ Fintype ι
have h : ¬Infinite ι
Tactic: apply fintypeOfNotInfinite
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
i : Infinite ι
⊢ False
have h : ∀ (s : Finset ι) (c : #s = n + 1), False
Tactic: obtain ⟨s, c⟩ := Infinite.exists_subset_card_eq ι (n + 1)
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
i : Infinite ι
s : Finset ι
c : #s = n + 1
⊢ False
have w₁ : #s ≤ n
Tactic: specialize w s
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
i : Infinite ι
s : Finset ι
c : #s = n + 1
w : #s ≤ n
⊢ False
have w₁ : n + 1 ≤ n
Tactic: rw [c] at w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
n : ℕ
⊢ map (α := Fin n) valEmbedding univ = Iio n
have h : ∀ (a : ℕ), a ∈ map (α := Fin n) valEmbedding univ ↔ a ∈ Iio n
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
n : ℕ
⊢ (↑(Ioi 0) : Set (Fin n.succ)) = (↑(map (succEmb n) univ) : Set (Fin n.succ))
have h : ∀ (x : Fin n.succ), x ∈ (↑(Ioi 0) : Set (Fin n.succ)) ↔ x ∈ (↑(map (succEmb n) univ) : Set (Fin n.succ))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
n : ℕ
⊢ (↑(Iio (last n)) : Set (Fin (n + 1))) = (↑(map castSuccEmb univ) : Set (Fin (n + 1)))
have h : ∀ (x : Fin (n + 1)), x ∈ (↑(Iio (last n)) : Set (Fin (n + 1))) ↔ x ∈ (↑(map castSuccEmb univ) : Set (Fin (n + 1)))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
⊢ Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | p x} =
    if p 0 then Finset.card (α := Fin n) {x : Fin n | p x.succ} + 1 else Finset.card (α := Fin n) {x : Fin n | p x.succ}
have rw : (if p 0 then
    Finset.card (α := Fin n)
        (filter
          ((fun (x : Fin (n + 1)) ↦ p x) ∘
            (⇑{ toFun := succ, inj' := sorry : Fin n ↪ Fin (n + 1) } : (a : Fin n) → Fin (n + 1)))
          univ) +
      1
  else
    Finset.card (α := Fin n)
      (filter
        ((fun (x : Fin (n + 1)) ↦ p x) ∘
          (⇑{ toFun := succ, inj' := sorry : Fin n ↪ Fin (n + 1) } : (a : Fin n) → Fin (n + 1)))
        univ)) =
  if p 0 then Finset.card (α := Fin n) {x : Fin n | p x.succ} + 1 else Finset.card (α := Fin n) {x : Fin n | p x.succ}
Tactic: rw [Fin.univ_succ, filter_cons, apply_ite Finset.card, card_cons, filter_map, card_map]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
⊢ Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | p x} =
    (if p 0 then 1 else 0) + Finset.card (α := Fin n) {x : Fin n | p x.succ}
have rw : (if p 0 then Finset.card (α := Fin n) {x : Fin n | p x.succ} + 1 else Finset.card (α := Fin n) {x : Fin n | p x.succ}) =
  (if p 0 then 1 else 0) + Finset.card (α := Fin n) {x : Fin n | p x.succ}
Tactic: rw [card_filter_univ_succ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
⊢ (if p 0 then Finset.card (α := Fin n) {x : Fin n | p x.succ} + 1
    else Finset.card (α := Fin n) {x : Fin n | p x.succ}) =
    (if p 0 then 1 else 0) + Finset.card (α := Fin n) {x : Fin n | p x.succ}
have pos : p 0 → Finset.card (α := Fin n) {x : Fin n | p x.succ} + 1 = 1 + Finset.card (α := Fin n) {x : Fin n | p x.succ}
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
pos : p 0 → Finset.card (α := Fin n) {x : Fin n | p x.succ} + 1 = 1 + Finset.card (α := Fin n) {x : Fin n | p x.succ}
⊢ (if p 0 then Finset.card (α := Fin n) {x : Fin n | p x.succ} + 1
    else Finset.card (α := Fin n) {x : Fin n | p x.succ}) =
    (if p 0 then 1 else 0) + Finset.card (α := Fin n) {x : Fin n | p x.succ}
have neg : ¬p 0 → Finset.card (α := Fin n) {x : Fin n | p x.succ} = 0 + Finset.card (α := Fin n) {x : Fin n | p x.succ}
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
α : Type u_1
n_1 : ℕ
inst : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : Finset.card (α := Fin n) {i : Fin n | xs.get i = a} = List.count a xs.toList
⊢ Finset.card (α := Fin n.succ) {i : Fin n.succ | (x ::ᵥ xs).get i = a} = List.count a (x ::ᵥ xs).toList
have cons : (if (x ::ᵥ xs).get 0 = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
  List.count a (x ::ᵥ xs).toList
Tactic: simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
      hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
α : Type u_1
n_1 : ℕ
inst : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : Finset.card (α := Fin n) {i : Fin n | xs.get i = a} = List.count a xs.toList
cons :
  (if (x ::ᵥ xs).get 0 = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x ::ᵥ xs).toList
⊢ Finset.card (α := Fin n.succ) {i : Fin n.succ | (x ::ᵥ xs).get i = a} = List.count a (x ::ᵥ xs).toList
have cons₁ : (if x = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
  List.count a (x ::ᵥ xs).toList
Tactic: simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
      hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
α : Type u_1
n_1 : ℕ
inst : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : Finset.card (α := Fin n) {i : Fin n | xs.get i = a} = List.count a xs.toList
cons :
  (if (x ::ᵥ xs).get 0 = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x ::ᵥ xs).toList
cons₁ :
  (if x = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x ::ᵥ xs).toList
⊢ Finset.card (α := Fin n.succ) {i : Fin n.succ | (x ::ᵥ xs).get i = a} = List.count a (x ::ᵥ xs).toList
have cons₂ : (if x = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
  List.count a (x :: xs.toList)
Tactic: simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
      hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
α : Type u_1
n_1 : ℕ
inst : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : Finset.card (α := Fin n) {i : Fin n | xs.get i = a} = List.count a xs.toList
cons :
  (if (x ::ᵥ xs).get 0 = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x ::ᵥ xs).toList
cons₁ :
  (if x = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x ::ᵥ xs).toList
cons₂ :
  (if x = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x :: xs.toList)
⊢ Finset.card (α := Fin n.succ) {i : Fin n.succ | (x ::ᵥ xs).get i = a} = List.count a (x ::ᵥ xs).toList
have cons₃ : (if x = a then 1 else 0) + Finset.card (α := Fin n) {x : Fin n | xs.get x = a} = List.count a (x :: xs.toList)
Tactic: simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
      hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
α : Type u_1
n_1 : ℕ
inst : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : Finset.card (α := Fin n) {i : Fin n | xs.get i = a} = List.count a xs.toList
cons :
  (if (x ::ᵥ xs).get 0 = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x ::ᵥ xs).toList
cons₁ :
  (if x = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x ::ᵥ xs).toList
cons₂ :
  (if x = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x :: xs.toList)
cons₃ : (if x = a then 1 else 0) + Finset.card (α := Fin n) {x : Fin n | xs.get x = a} = List.count a (x :: xs.toList)
⊢ Finset.card (α := Fin n.succ) {i : Fin n.succ | (x ::ᵥ xs).get i = a} = List.count a (x ::ᵥ xs).toList
have cons₄ : (if x = a then 1 else 0) + List.count a xs.toList = List.count a (x :: xs.toList)
Tactic: simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
      hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
α : Type u_1
n_1 : ℕ
inst : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : Finset.card (α := Fin n) {i : Fin n | xs.get i = a} = List.count a xs.toList
cons :
  (if (x ::ᵥ xs).get 0 = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x ::ᵥ xs).toList
cons₁ :
  (if x = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x ::ᵥ xs).toList
cons₂ :
  (if x = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x :: xs.toList)
cons₃ : (if x = a then 1 else 0) + Finset.card (α := Fin n) {x : Fin n | xs.get x = a} = List.count a (x :: xs.toList)
cons₄ : (if x = a then 1 else 0) + List.count a xs.toList = List.count a (x :: xs.toList)
⊢ Finset.card (α := Fin n.succ) {i : Fin n.succ | (x ::ᵥ xs).get i = a} = List.count a (x ::ᵥ xs).toList
have cons₅ : (if x = a then 1 else 0) + List.count a xs.toList = List.count a xs.toList + if (x == a) = true then 1 else 0
Tactic: simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
      hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
α : Type u_1
n_1 : ℕ
inst : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : Finset.card (α := Fin n) {i : Fin n | xs.get i = a} = List.count a xs.toList
cons :
  (if (x ::ᵥ xs).get 0 = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x ::ᵥ xs).toList
cons₁ :
  (if x = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x ::ᵥ xs).toList
cons₂ :
  (if x = a then 1 else 0) + Finset.card (α := Fin n) {x_1 : Fin n | (x ::ᵥ xs).get x_1.succ = a} =
    List.count a (x :: xs.toList)
cons₃ : (if x = a then 1 else 0) + Finset.card (α := Fin n) {x : Fin n | xs.get x = a} = List.count a (x :: xs.toList)
cons₄ : (if x = a then 1 else 0) + List.count a xs.toList = List.count a (x :: xs.toList)
cons₅ : (if x = a then 1 else 0) + List.count a xs.toList = List.count a xs.toList + if (x == a) = true then 1 else 0
⊢ Finset.card (α := Fin n.succ) {i : Fin n.succ | (x ::ᵥ xs).get i = a} = List.count a (x ::ᵥ xs).toList
have cons₆ : (List.count a xs.toList + if x = a then 1 else 0) = List.count a xs.toList + if (x == a) = true then 1 else 0
Tactic: simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
      hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
v : List.Vector α n
⊢ Finset.card (α := Fin n) {i : Fin n | v.get i = a} = List.count a v.toList
have nil : Finset.card (α := Fin 0) {i : Fin 0 | List.Vector.get Vector.nil i = a} = List.count a (List.Vector.toList Vector.nil)
Tactic: induction v with
  | nil => simp
  | @cons n x xs hxs =>
    simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
      hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
v : List.Vector α n
nil :
  Finset.card (α := Fin 0) {i : Fin 0 | List.Vector.get Vector.nil i = a} = List.count a (List.Vector.toList Vector.nil)
⊢ Finset.card (α := Fin n) {i : Fin n | v.get i = a} = List.count a v.toList
have cons : ∀ {n : ℕ} {x : α} {xs : List.Vector α n}
  (hxs : Finset.card (α := Fin n) {i : Fin n | xs.get i = a} = List.count a xs.toList),
  Finset.card (α := Fin n.succ) {i : Fin n.succ | (x ::ᵥ xs).get i = a} = List.count a (x ::ᵥ xs).toList
Tactic: induction v with
  | nil => simp
  | @cons n x xs hxs =>
    simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
      hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
n : ℕ
j : Fin n
p : Fin n → Prop
inst : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
k : Fin n
hk : ¬p k
⊢ Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑k : ℕ)
have rw : Finset.card (α := Fin n) {i : Fin n | p i} ≤ #(Iio k)
Tactic: rw [← Fin.card_Iio]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (hypothesis)
Goal:
n : ℕ
j : Fin n
p : Fin n → Prop
inst : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
⊢ (↑j : ℕ) < Finset.card (α := Fin n) {i : Fin n | p i} ↔ p j
have h1 : ∀ (k : Fin n) (hk : ¬p k), Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑k : ℕ)
Tactic: have h1 (k : Fin n) (hk : ¬ p k) : #{i | p i} ≤ k := by
    rw [← Fin.card_Iio]
    exact card_le_card (by grind)
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
n : ℕ
j : Fin n
p : Fin n → Prop
inst : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n) (hk : ¬p k), Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑k : ℕ)
⊢ (↑j : ℕ) < Finset.card (α := Fin n) {i : Fin n | p i} ↔ p j
have refine : ∀ (h : p j), (↑j : ℕ) < Finset.card (α := Fin n) {i : Fin n | p i}
Tactic: refine ⟨by grind, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
n : ℕ
j : Fin n
p : Fin n → Prop
inst : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n) (hk : ¬p k), Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑k : ℕ)
h : p j
⊢ (↑j : ℕ) < Finset.card (α := Fin n) {i : Fin n | p i}
have by_contra! : ∀ (hc : Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑j : ℕ)), False
Tactic: by_contra! hc
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
n : ℕ
j : Fin n
p : Fin n → Prop
inst : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n) (hk : ¬p k), Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑k : ℕ)
h : p j
hc : Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑j : ℕ)
q : Fin n → Prop := fun (x : Fin n) ↦ (↑x : ℕ) < Finset.card (α := Fin n) {i : Fin n | p i}
⊢ #(filter p univ) ≤ #(filter q univ)
have rw : #(filter p univ) ≤ min n (Finset.card (α := Fin n) {i : Fin n | p i})
Tactic: rw [card_filter_val_lt]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (hypothesis)
Goal:
n : ℕ
j : Fin n
p : Fin n → Prop
inst : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n) (hk : ¬p k), Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑k : ℕ)
h : p j
hc : Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑j : ℕ)
q : Fin n → Prop := fun (x : Fin n) ↦ (↑x : ℕ) < Finset.card (α := Fin n) {i : Fin n | p i}
⊢ False
have this : filter q univ = filter p univ
Tactic: have : univ.filter q = univ.filter p :=
    eq_of_subset_of_card_le (by grind) (by rw [card_filter_val_lt]; grind)
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (hypothesis)
Goal:
n : ℕ
j : Fin n
p : Fin n → Prop
inst : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n) (hk : ¬p k), Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑k : ℕ)
h : p j
hc : Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑j : ℕ)
q : Fin n → Prop := fun (x : Fin n) ↦ (↑x : ℕ) < Finset.card (α := Fin n) {i : Fin n | p i}
this : filter q univ = filter p univ
⊢ False
have this₁ : j ∈ filter p univ
Tactic: have : j ∈ univ.filter p := by grind
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
n : ℕ
⊢ image (α := Fin n) val univ = range n
have h : ∀ (a : ℕ), a ∈ image (α := Fin n) val univ ↔ a ∈ range n
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
n : ℕ
f : ℕ → α
⊢ (sup univ fun (n_1 : Fin n) ↦ f (↑n_1 : ℕ)) = (range n).sup f
have rw : (sup univ fun (n_1 : Fin n) ↦ f (↑n_1 : ℕ)) = (image (α := Fin n) val univ).sup f
Tactic: rw [← image_fin_univ, sup_image, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
n : ℕ
f : ℕ → α
rw : (sup univ fun (n_1 : Fin n) ↦ f (↑n_1 : ℕ)) = (image (α := Fin n) val univ).sup f
⊢ (sup univ fun (n_1 : Fin n) ↦ f (↑n_1 : ℕ)) = (range n).sup f
have rw₁ : (sup univ fun (n_1 : Fin n) ↦ f (↑n_1 : ℕ)) = sup (β := Fin n) univ (f ∘ val)
Tactic: rw [← image_fin_univ, sup_image, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.Fintype.Fin (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
n : ℕ
f : ℕ → α
rw : (sup univ fun (n_1 : Fin n) ↦ f (↑n_1 : ℕ)) = (image (α := Fin n) val univ).sup f
rw₁ : (sup univ fun (n_1 : Fin n) ↦ f (↑n_1 : ℕ)) = sup (β := Fin n) univ (f ∘ val)
⊢ (sup univ fun (n_1 : Fin n) ↦ f (↑n_1 : ℕ)) = (range n).sup f
have rw₂ : Eq.{u_1 + 1} (α := α) (sup univ fun (n_1 : Fin n) ↦ f (↑n_1 : ℕ)) (sup univ fun (x : Fin n) ↦ f (↑x : ℕ))
Tactic: rw [← image_fin_univ, sup_image, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.Fintype.Inv (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
inst_2 : Nonempty α
⊢ (Set.range f).restrict (π := fun (a : β) ↦ α) (invFun f) = hf.invOfMemRange
have h : ∀ (b : β) (h : b ∈ Set.range f),
  (Set.range f).restrict (π := fun (a : β) ↦ α) (invFun f) (Subtype.mk (p := fun (x : β) ↦ x ∈ Set.range f) b h) =
    hf.invOfMemRange (Subtype.mk (p := fun (x : β) ↦ x ∈ Set.range f) b h)
Tactic: ext ⟨b, h⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Inv (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
inst_2 : Nonempty α
b : β
h : b ∈ Set.range f
⊢ (Set.range f).restrict (π := fun (a : β) ↦ α) (invFun f) (Subtype.mk (p := fun (x : β) ↦ x ∈ Set.range f) b h) =
    hf.invOfMemRange (Subtype.mk (p := fun (x : β) ↦ x ∈ Set.range f) b h)
have h₁ : f ((Set.range f).restrict (π := fun (a : β) ↦ α) (invFun f) (Subtype.mk (p := fun (x : β) ↦ x ∈ Set.range f) b h)) =
  f (hf.invOfMemRange (Subtype.mk (p := fun (x : β) ↦ x ∈ Set.range f) b h))
Tactic: apply hf
-- Lean 4 proof step from Mathlib.Data.Fintype.Inv (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α ↪ β
inst_2 : Nonempty α
⊢ Set.restrict (π := fun (a : β) ↦ α) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      (invFun (⇑f : (a : α) → β)) =
    f.invOfMemRange
have h : ∀ (b : β) (h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
  Set.restrict (π := fun (a : β) ↦ α) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) (invFun (⇑f : (a : α) → β))
      (Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h) =
    f.invOfMemRange
      (Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h)
Tactic: ext ⟨b, h⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Inv (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α ↪ β
inst_2 : Nonempty α
b : β
h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
⊢ Set.restrict (π := fun (a : β) ↦ α) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) (invFun (⇑f : (a : α) → β))
      (Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h) =
    f.invOfMemRange
      (Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h)
have h₁ : Eq.{u_2 + 1} (α := β)
  ((f : (a : α) → β)
      (Set.restrict (π := fun (a : β) ↦ α) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
        (invFun (⇑f : (a : α) → β))
        (Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h)) :
    β)
  ((f : (a : α) → β)
      (f.invOfMemRange
        (Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h)) :
    β)
Tactic: apply f.injective
-- Lean 4 proof step from Mathlib.Data.Fintype.Inv (goal)
Goal:
α : Type u_4
p : α → Prop
inst : Fintype { a : α // p a }
inst_1 : DecidableEq α
x : { a : α // p a }
h : ∃! a : { a : α // p a }, (↑a : α) = (↑x : α)
⊢ choose (fun (y : { a : α // p a }) ↦ (↑y : α) = (↑x : α)) h = x
have rw : (↑(choose (fun (y : { a : α // p a }) ↦ (↑y : α) = (↑x : α)) h) : α) = (↑x : α)
Tactic: rw [Subtype.ext_iff, Fintype.choose_spec (fun y : { a : α // p a } => (y : α) = x) _]
-- Lean 4 proof step from Mathlib.Data.Fintype.Inv (goal)
Goal:
α : Type u_4
p : α → Prop
inst : Fintype { a : α // p a }
inst_1 : DecidableEq α
x : { a : α // p a }
h : ∃! a : { a : α // p a }, (↑a : α) = (↑x : α)
rw : (↑(choose (fun (y : { a : α // p a }) ↦ (↑y : α) = (↑x : α)) h) : α) = (↑x : α)
⊢ choose (fun (y : { a : α // p a }) ↦ (↑y : α) = (↑x : α)) h = x
have rw₁ : (↑x : α) = (↑x : α)
Tactic: rw [Subtype.ext_iff, Fintype.choose_spec (fun y : { a : α // p a } => (y : α) = x) _]
-- Lean 4 proof step from Mathlib.Data.Fintype.Lattice (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i
have empty : a ∈ inf ∅ f ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → a ∈ f i
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Fintype.Lattice (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
empty : a ∈ inf ∅ f ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → a ∈ f i
⊢ a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i
have cons : ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s),
  (a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i) → (a ∈ (cons a_1 s h).inf f ↔ ∀ i ∈ cons a_1 s h, a ∈ f i)
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Fintype.Lattice (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Nonempty α
inst_2 : LinearOrder β
f : α → β
⊢ ∃ (x₀ : α), ∀ (x : α), f x ≤ f x₀
have intro : ∀ (val : Fintype α), ∃ (x₀ : α), ∀ (x : α), f x ≤ f x₀
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Data.Fintype.Lattice (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Nonempty α
inst_2 : LinearOrder β
f : α → β
⊢ ∃ (x₀ : α), ∀ (x : α), f x₀ ≤ f x
have intro : ∀ (val : Fintype α), ∃ (x₀ : α), ∀ (x : α), f x₀ ≤ f x
Tactic: cases nonempty_fintype α