awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ)
allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists
l : List (Finset α)
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄,
      x ≤ (↑m.toList.permutations : Multiset (List α)) → x ≤ (↑n.toList.permutations : Multiset (List α)) → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a b : List α
ha : b ~ m.toList
hb : b ~ n.toList
hab : a = b
⊢ m = n

Tactic:
exact Finset.perm_toList.mp <| Perm.trans ha.symm hb

Premises used: List.Perm.trans, Finset.perm_toList, Iff.mp, List.Perm.symm
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
l : List α
refine_2 : (∃ (a : Finset α), a.val = (↑l : Multiset α)) ↔ l.Nodup
⊢ Membership.mem (γ := Finset (List α))
      (let univSubsets : Multiset (Finset α) := Finset.val (Finset.powerset Finset.univ);
      let allPerms : Multiset (List α) := univSubsets.bind fun (s : Finset α) ↦ s.val.lists;
      { val := allPerms, nodup := ⋯ })
      l ↔
    l.Nodup

Tactic:
simp only [Finset.mem_mk, Multiset.mem_bind, Finset.mem_val, Finset.mem_powerset,
      Finset.subset_univ, Multiset.mem_lists_iff, Multiset.quot_mk_to_coe, true_and]

Premises used: Finset.mem_mk, Multiset.quot_mk_to_coe, Finset.mem_powerset, Multiset.mem_lists_iff, Multiset.mem_bind, true_and, Finset.subset_univ, Finset.mem_val
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
l : List α
refine_2 : (∃ (a : Finset α), a.val = (↑l : Multiset α)) → l.Nodup
refine_2₁ : l.Nodup → ∃ (a : Finset α), a.val = (↑l : Multiset α)
⊢ (∃ (a : Finset α), a.val = (↑l : Multiset α)) ↔ l.Nodup

Tactic:
constructor
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
l : List α
h : ∃ (a : Finset α), a.val = (↑l : Multiset α)
refine_2 : ∀ (f : Finset α) (hf : f.val = (↑l : Multiset α)), l.Nodup
⊢ l.Nodup

Tactic:
rcases h with ⟨f, hf⟩
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
l : List α
f : Finset α
hf : f.val = (↑l : Multiset α)
⊢ f.val.Nodup

Tactic:
f.nodup

Premises used: Finset.nodup
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
l : List α
f : Finset α
hf : f.val = (↑l : Multiset α)
a : l.Nodup ↔ f.val.Nodup
⊢ l.Nodup

Tactic:
convert! f.nodup

Premises used: Finset.nodup
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
l : List α
f : Finset α
hf : f.val = (↑l : Multiset α)
a : l.Nodup ↔ (↑l : Multiset α).Nodup
⊢ l.Nodup ↔ f.val.Nodup

Tactic:
rw [hf]
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
l : List α
f : Finset α
hf : f.val = (↑l : Multiset α)
⊢ l.Nodup ↔ (↑l : Multiset α).Nodup

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
l : List α
h : l.Nodup
⊢ ∃ (a : Finset α), a.val = (↑l : Multiset α)

Tactic:
CanLift.prf _ h

Premises used: CanLift.prf
-- Module: Mathlib.Data.Fintype.List
Goal:
α : Type u_1
inst : Fintype α
l : List α
h : l.Nodup
⊢ ∃ (a : Finset α), a.val = (↑l : Multiset α)

Tactic:
exact CanLift.prf _ h

Premises used: CanLift.prf
-- Module: Mathlib.Data.Fintype.OfMap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α
s : Multiset α
H : ∀ (x : α), x ∈ s
⊢ ∀ (x : α), x ∈ s.toFinset

Tactic:
simpa using H
-- Module: Mathlib.Data.Fintype.OfMap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α
l : List α
H : ∀ (x : α), x ∈ l
⊢ ∀ (x : α), x ∈ l.toFinset

Tactic:
simpa using H
-- Module: Mathlib.Data.Fintype.OfMap
Goal:
α : Type u_1
a : α
inst : Subsingleton α
⊢ Eq (α := Finset α) univ {a}

Tactic:
rfl

Premises used: Finset.univ, rfl
-- Module: Mathlib.Data.Fintype.OfMap
Goal:
α : Type u_1
inst : IsEmpty α
⊢ Eq.{u_1 + 1} (α := Finset α) univ ∅

Tactic:
rfl

Premises used: Finset.univ, rfl
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Fintype α
a : Option α
⊢ Membership.mem (γ := Finset (Option α)) ((insertNone : (a : Finset α) → Finset (Option α)) univ : Finset (Option α)) a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Finite α
⊢ Finite.{u_3 + 1} (Option α)

Tactic:
have := Fintype.ofFinite α
  Finite.of_fintype _

Premises used: Fintype.ofFinite, Finite.of_fintype, Option
-- Module: Mathlib.Data.Fintype.Option
Goal:
α : Type u_3
inst : Fintype α
⊢ Eq.{u_3 + 1} (α := Finset (Option α)) univ ((insertNone : (a : Finset α) → Finset (Option α)) univ)

Tactic:
rfl

Premises used: Finset.univ, rfl
-- Module: Mathlib.Data.Fintype.Option
Goal:
α : Type u_3
inst : Fintype α
⊢ none ∉ map Embedding.some univ

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
apply : P (ULift.{u, 0} (Fin (card α))) → Trunc (P α)
⊢ Trunc (P α)

Tactic:
apply Trunc.bind (this (Fintype.card α))

Premises used: Trunc.bind, Fintype.card
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
h : P (ULift.{u, 0} (Fin (card α)))
apply : α ≃ Fin (card α) → P α
⊢ Trunc (P α)

Tactic:
apply Trunc.map _ (Fintype.truncEquivFin α)

Premises used: Trunc.map, Fintype.truncEquivFin
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
h : P (ULift.{u, 0} (Fin (card α)))
e : α ≃ Fin (card α)
⊢ P α

Tactic:
exact of_equiv (Equiv.ulift.trans e.symm) h

Premises used: Equiv.trans, Equiv.ulift, Equiv.symm
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
suffices : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
⊢ Trunc (P α)

Tactic:
suffices ∀ n : ℕ, Trunc (P (ULift <| Fin n)) by
    apply Trunc.bind (this (Fintype.card α))
    intro h
    apply Trunc.map _ (Fintype.truncEquivFin α)
    intro e
    exact of_equiv (Equiv.ulift.trans e.symm) h
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
⊢ card PEmpty.{u + 1} = card.{u} (ULift.{u, 0} (Fin 0))

Tactic:
simp only [card_fin, card_pempty, card_ulift]

Premises used: Fintype.card_fin, Fintype.card_pempty, Fintype.card_ulift
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
⊢ card PEmpty.{u + 1} = card.{u} (ULift.{u, 0} (Fin 0))

Tactic:
have : card PEmpty = card (ULift (Fin 0)) := by
      simp only [card_fin, card_pempty, card_ulift]
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
this : card PEmpty.{u + 1} = card.{u} (ULift.{u, 0} (Fin 0))
zero : PEmpty.{u + 1} ≃ ULift.{u, 0} (Fin 0) → Trunc (P (ULift.{u, 0} (Fin 0)))
⊢ Trunc (P (ULift.{u, 0} (Fin 0)))

Tactic:
apply Trunc.bind (truncEquivOfCardEq this)

Premises used: Trunc.bind, Fintype.truncEquivOfCardEq
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
this : card PEmpty.{u + 1} = card.{u} (ULift.{u, 0} (Fin 0))
e : PEmpty.{u + 1} ≃ ULift.{u, 0} (Fin 0)
zero : P (ULift.{u, 0} (Fin 0))
⊢ Trunc (P (ULift.{u, 0} (Fin 0)))

Tactic:
apply Trunc.mk

Premises used: Trunc.mk
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
this : card PEmpty.{u + 1} = card.{u} (ULift.{u, 0} (Fin 0))
e : PEmpty.{u + 1} ≃ ULift.{u, 0} (Fin 0)
⊢ P (ULift.{u, 0} (Fin 0))

Tactic:
exact of_equiv e h_empty
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
⊢ card.{u} (Option (ULift.{u, 0} (Fin n))) = card.{u} (ULift.{u, 0} (Fin n.succ))

Tactic:
simp only [card_fin, card_option, card_ulift]

Premises used: Fintype.card_fin, Fintype.card_option, Fintype.card_ulift
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
⊢ card.{u} (Option (ULift.{u, 0} (Fin n))) = card.{u} (ULift.{u, 0} (Fin n.succ))

Tactic:
have : card (Option (ULift (Fin n))) = card (ULift (Fin n.succ)) := by
      simp only [card_fin, card_option, card_ulift]
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
this : card.{u} (Option (ULift.{u, 0} (Fin n))) = card.{u} (ULift.{u, 0} (Fin n.succ))
succ : Option (ULift.{u, 0} (Fin n)) ≃ ULift.{u, 0} (Fin n.succ) → Trunc (P (ULift.{u, 0} (Fin (n + 1))))
⊢ Trunc (P (ULift.{u, 0} (Fin (n + 1))))

Tactic:
apply Trunc.bind (truncEquivOfCardEq this)

Premises used: Trunc.bind, Fintype.truncEquivOfCardEq
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
this : card.{u} (Option (ULift.{u, 0} (Fin n))) = card.{u} (ULift.{u, 0} (Fin n.succ))
e : Option (ULift.{u, 0} (Fin n)) ≃ ULift.{u, 0} (Fin n.succ)
apply : P (ULift.{u, 0} (Fin n)) → P (ULift.{u, 0} (Fin (n + 1)))
⊢ Trunc (P (ULift.{u, 0} (Fin (n + 1))))

Tactic:
apply Trunc.map _ ih

Premises used: Trunc.map
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
ih_1 : Trunc (P (ULift.{u, 0} (Fin n)))
this : card.{u} (Option (ULift.{u, 0} (Fin n))) = card.{u} (ULift.{u, 0} (Fin n.succ))
e : Option (ULift.{u, 0} (Fin n)) ≃ ULift.{u, 0} (Fin n.succ)
ih : P (ULift.{u, 0} (Fin n))
⊢ P (ULift.{u, 0} (Fin (n + 1)))

Tactic:
exact of_equiv e (h_option ih)
-- Module: Mathlib.Data.Fintype.Option
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
zero : Trunc (P (ULift.{u, 0} (Fin 0)))
succ : (n : ℕ) → (ih : Trunc (P (ULift.{u, 0} (Fin n)))) → Trunc (P (ULift.{u, 0} (Fin (n + 1))))
⊢ Trunc (P (ULift.{u, 0} (Fin n)))

Tactic:
induction n with
  | zero =>
    have : card PEmpty = card (ULift (Fin 0)) := by
      simp only [card_fin, card_pempty, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.mk
    exact of_equiv e h_empty
  | succ n ih =>
    have : card (Option (ULift (Fin n))) = card (ULift (Fin n.succ)) := by
      simp only [card_fin, card_option, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.map _ ih
    intro ih
    exact of_equiv e (h_option ih)

Premises used: Trunc.mk, Nat.zero, Nat.succ
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
i : Fintype PEmpty.{u + 1}
⊢ P PEmpty.{u + 1}

Tactic:
h_empty
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
i : Fintype PEmpty.{u + 1}
⊢ P PEmpty.{u + 1}

Tactic:
convert! h_empty
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α_1 : Type u
h_fintype : Fintype α_1
f_empty : ∀ (i : Fintype PEmpty.{u + 1}), P PEmpty.{u + 1} := ⋯
α : Type u
hα : Fintype α
Pα : ∀ (h : Fintype α), P α
hα' : Fintype (Option α)
⊢ P (Option α)

Tactic:
h_option α (Pα _)
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α_1 : Type u
h_fintype : Fintype α_1
f_empty : ∀ (i : Fintype PEmpty.{u + 1}), P PEmpty.{u + 1} := ⋯
α : Type u
hα : Fintype α
Pα : ∀ (h : Fintype α), P α
hα' : Fintype (Option α)
⊢ P (Option α)

Tactic:
convert! h_option α (Pα _)
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
⊢ Trunc (∀ (h : Fintype α), P α)

Tactic:
obtain ⟨p⟩ :=
    let f_empty := fun i => by convert! h_empty
    let h_option : ∀ {α : Type u} [Fintype α] [DecidableEq α],
          (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α) := by
      rintro α hα - Pα hα'
      convert! h_option α (Pα _)
    @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
      f_empty h_option α _ (Classical.decEq α)
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
x : Trunc (∀ (h : Fintype α), P α)
⊢ ∀ (h : Fintype α), P α

Tactic:
obtain ⟨p⟩ :=
    let f_empty := fun i => by convert! h_empty
    let h_option : ∀ {α : Type u} [Fintype α] [DecidableEq α],
          (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α) := by
      rintro α hα - Pα hα'
      convert! h_option α (Pα _)
    @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
      f_empty h_option α _ (Classical.decEq α)
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
h : Trunc (∀ (h : Fintype α), P α)
p : ∀ (h : Fintype α), P α
⊢ P α

Tactic:
p _
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
h : Trunc (∀ (h : Fintype α), P α)
p : ∀ (h : Fintype α), P α
⊢ P α

Tactic:
exact p _
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst : Finite α
intro : ∀ (val : Fintype α), P α
⊢ P α

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst : Finite α
val : Fintype α
⊢ P α

Tactic:
Fintype.induction_empty_option ?_ ?_ ?_ α

Premises used: Fintype.induction_empty_option
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst : Finite α
val : Fintype α
intro : ∀ (α β : Type u) [Fintype β] (e : α ≃ β), P α → P β
intro₁ : P PEmpty.{u + 1}
intro₂ : ∀ (α : Type u) [Fintype α], P α → P (Option α)
⊢ P α

Tactic:
refine Fintype.induction_empty_option ?_ ?_ ?_ α
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst : Finite α
val : Fintype α
⊢ ∀ (α β : Type u) [Fintype β] (e : α ≃ β), P α → P β

Tactic:
fun α β _ => of_equiv
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst : Finite α
val : Fintype α
⊢ P PEmpty.{u + 1}

Tactic:
h_empty
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst : Finite α
val : Fintype α
⊢ ∀ (α : Type u) [Fintype α], P α → P (Option α)

Tactic:
@h_option
-- Module: Mathlib.Data.Fintype.Option
Goal:
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst : Finite α
val : Fintype α
⊢ ∀ (α β : Type u) [Fintype β] (e : α ≃ β), P α → P β

Tactic:
exacts [fun α β _ => of_equiv, h_empty, @h_option]
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
⊢ a ⊓ s.toFinset.sup id ≤ s.toFinset.sup fun (i : α) ↦ a ⊓ id i

Tactic:
(Finset.sup_inf_distrib_left s.toFinset id a).le

Premises used: Finset.sup_inf_distrib_left, id, Eq.le, Set.toFinset
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
h : Eq (α := α) (⨆ b ∈ s, a ⊓ b) (s.toFinset.sup fun (i : α) ↦ a ⊓ id i)
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
convert! (Finset.sup_inf_distrib_left s.toFinset id a).le using 1
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
h : Eq.{u_2 + 1} (α := α) (⨆ b ∈ s, a ⊓ b) (⨆ a_1 ∈ s.toFinset, a ⊓ id a_1)
⊢ Eq (α := α) (⨆ b ∈ s, a ⊓ b) (s.toFinset.sup fun (i : α) ↦ a ⊓ id i)

Tactic:
rw [Finset.sup_eq_iSup]

Premises used: Finset.sup_eq_iSup
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
h : Eq.{u_2 + 1} (α := α) (⨆ b ∈ s, a ⊓ b) (⨆ a_1 ∈ s, a ⊓ id a_1)
⊢ Eq.{u_2 + 1} (α := α) (⨆ b ∈ s, a ⊓ b) (⨆ a_1 ∈ s.toFinset, a ⊓ id a_1)

Tactic:
simp_rw [Set.mem_toFinset]

Premises used: Set.mem_toFinset
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
⊢ Eq.{u_2 + 1} (α := α) (⨆ b ∈ s, a ⊓ b) (⨆ a_1 ∈ s, a ⊓ id a_1)

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
⊢ (s.toFinset.inf fun (i : α) ↦ a ⊔ id i) ≤ a ⊔ s.toFinset.inf id

Tactic:
(Finset.inf_sup_distrib_left s.toFinset id a).ge

Premises used: Eq.ge, Finset.inf_sup_distrib_left, id, Set.toFinset
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
h : Eq (α := α) (⨅ b ∈ s, a ⊔ b) (s.toFinset.inf fun (i : α) ↦ a ⊔ id i)
⊢ ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

Tactic:
convert! (Finset.inf_sup_distrib_left s.toFinset id a).ge using 1
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
h : Eq.{u_2 + 1} (α := α) (⨅ b ∈ s, a ⊔ b) (⨅ a_1 ∈ s.toFinset, a ⊔ id a_1)
⊢ Eq (α := α) (⨅ b ∈ s, a ⊔ b) (s.toFinset.inf fun (i : α) ↦ a ⊔ id i)

Tactic:
rw [Finset.inf_eq_iInf]

Premises used: Finset.inf_eq_iInf
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
h : Eq.{u_2 + 1} (α := α) (⨅ b ∈ s, a ⊔ b) (⨅ a_1 ∈ s, a ⊔ id a_1)
⊢ Eq.{u_2 + 1} (α := α) (⨅ b ∈ s, a ⊔ b) (⨅ a_1 ∈ s.toFinset, a ⊔ id a_1)

Tactic:
simp_rw [Set.mem_toFinset]

Premises used: Set.mem_toFinset
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
⊢ Eq.{u_2 + 1} (α := α) (⨅ b ∈ s, a ⊔ b) (⨅ a_1 ∈ s, a ⊔ id a_1)

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
γ : Type u_3
inst_1 : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
⊢ ∃ (z : γ), ∀ i ∈ hs.toFinset (s := s), r (f i) (f z)

Tactic:
D.finset_le hs.toFinset

Premises used: Set.Finite.toFinset, Directed.finset_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
γ : Type u_3
inst_1 : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
h : ∀ (x a : γ), a ∈ s → r (f a) (f x) ↔ a ∈ hs.toFinset (s := s) → r (f a) (f x)
⊢ ∃ (z : γ), ∀ i ∈ s, r (f i) (f z)

Tactic:
convert! D.finset_le hs.toFinset using 3

Premises used: Set.Finite.toFinset, Directed.finset_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
γ : Type u_3
inst_1 : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
x a : γ
h h₁ : a ∈ s → r (f a) (f x) ↔ a ∈ s → r (f a) (f x)
⊢ a ∈ s → r (f a) (f x) ↔ a ∈ hs.toFinset (s := s) → r (f a) (f x)

Tactic:
rw [Set.Finite.mem_toFinset]

Premises used: Set.Finite.mem_toFinset