awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
i : Fin n
⊢ Iio i.castSucc = map castSuccEmb (Iio i)

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n m : ℕ
⊢ Finset.card (α := Fin n) {i : Fin n | (↑i : ℕ) < m} = min n m

Tactic:
simp [← card_map valEmbedding, ← filter_filter, exists_iff, map_filter']

Premises used: Finset.map_filter', Fin.valEmbedding, Finset.filter_filter, Finset.card_map, Fin.exists_iff
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
rw :
  (if p 0 then
      Finset.card (α := Fin n)
          (filter
            ((fun (x : Fin (n + 1)) ↦ p x) ∘
              (⇑{ toFun := succ, inj' := ⋯ : 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' := ⋯ : 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}
⊢ 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}

Tactic:
rw [Fin.univ_succ, filter_cons, apply_ite Finset.card, card_cons, filter_map, card_map]

Premises used: Finset.card_map, apply_ite, Fin.univ_succ, Finset.filter_cons, Finset.card_cons, Finset.card, Finset.filter_map
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
⊢ (if p 0 then
      Finset.card (α := Fin n)
          (filter
            ((fun (x : Fin (n + 1)) ↦ p x) ∘
              (⇑{ toFun := succ, inj' := ⋯ : 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' := ⋯ : 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:
rfl
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
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}
⊢ 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}

Tactic:
rw [card_filter_univ_succ]

Premises used: Fin.card_filter_univ_succ
-- Module: Mathlib.Data.Fintype.Fin
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}
neg : ¬p 0 → Finset.card (α := Fin n) {x : Fin n | p x.succ} = 0 + 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}

Tactic:
split_ifs
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
h : 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:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
p : Fin (n + 1) → Prop
inst : DecidablePred p
h : ¬p 0
⊢ Finset.card (α := Fin n) {x : Fin n | p x.succ} = 0 + Finset.card (α := Fin n) {x : Fin n | p x.succ}

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Fintype.Fin
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
⊢ Finset.card (α := Fin 0) {i : Fin 0 | List.Vector.get Vector.nil i = a} = List.count a (List.Vector.toList Vector.nil)

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Fin
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
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
⊢ Finset.card (α := Fin n.succ) {i : Fin n.succ | (x ::ᵥ xs).get i = 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]

Premises used: List.Vector.get_cons_zero, beq_iff_eq, List.count_cons, List.Vector.toList_cons, add_comm, Fin.card_filter_univ_succ', List.Vector.get_cons_succ, OfNat.ofNat, Eq, ite
-- Module: Mathlib.Data.Fintype.Fin
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)
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
⊢ Finset.card (α := Fin n) {i : Fin n | v.get i = a} = List.count a v.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]

Premises used: List.Vector.get_cons_zero, beq_iff_eq, Fin.cons, List.count_cons, List.Vector.toList_cons, Fin.card_filter_univ_succ', List.Vector.get_cons_succ
-- Module: Mathlib.Data.Fintype.Fin
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
rw : Finset.card (α := Fin n) {i : Fin n | p i} ≤ #(Iio k)
⊢ Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑k : ℕ)

Tactic:
rw [← Fin.card_Iio]

Premises used: Fin.card_Iio
-- Module: Mathlib.Data.Fintype.Fin
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
⊢ {i : Fin n | p i} ⊆ Iio k

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Fin
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} ≤ #(Iio k)

Tactic:
exact card_le_card (by grind)

Premises used: Finset.card_le_card
-- Module: Mathlib.Data.Fintype.Fin
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 : ℕ)

Tactic:
have h1 (k : Fin n) (hk : ¬ p k) : #{i | p i} ≤ k := by
    rw [← Fin.card_Iio]
    exact card_le_card (by grind)
-- Module: Mathlib.Data.Fintype.Fin
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

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Fin
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 : ℕ)
refine : ∀ (h : p j), (↑j : ℕ) < Finset.card (α := Fin n) {i : Fin n | p i}
⊢ (↑j : ℕ) < Finset.card (α := Fin n) {i : Fin n | p i} ↔ p j

Tactic:
refine ⟨by grind, fun h ↦ ?_⟩
-- Module: Mathlib.Data.Fintype.Fin
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
by_contra! : ∀ (hc : Finset.card (α := Fin n) {i : Fin n | p i} ≤ (↑j : ℕ)), False
⊢ (↑j : ℕ) < Finset.card (α := Fin n) {i : Fin n | p i}

Tactic:
by_contra! hc
-- Module: Mathlib.Data.Fintype.Fin
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 q univ ⊆ filter p univ

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Fin
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}
rw : #(filter p univ) ≤ min n (Finset.card (α := Fin n) {i : Fin n | p i})
⊢ #(filter p univ) ≤ #(filter q univ)

Tactic:
rw [card_filter_val_lt]

Premises used: Fin.card_filter_val_lt
-- Module: Mathlib.Data.Fintype.Fin
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) ≤ min n (Finset.card (α := Fin n) {i : Fin n | p i})

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Fin
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 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)
-- Module: Mathlib.Data.Fintype.Fin
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
⊢ j ∈ filter p univ

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Fin
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
⊢ j ∈ filter p univ

Tactic:
have : j ∈ univ.filter p := by grind
-- Module: Mathlib.Data.Fintype.Fin
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_1 : filter q univ = filter p univ
this : j ∈ filter p univ
⊢ False

Tactic:
grind
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
h : ∀ (a : ℕ), a ∈ image (α := Fin n) val univ ↔ a ∈ range n
⊢ image (α := Fin n) val univ = range n

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n a : ℕ
⊢ a ∈ image (α := Fin n) val univ ↔ a ∈ range n

Tactic:
simp [Fin.exists_iff]

Premises used: Fin.exists_iff
-- Module: Mathlib.Data.Fintype.Fin
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)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (sup univ fun (n_1 : Fin n) ↦ f (↑n_1 : ℕ)) (sup univ fun (x : Fin n) ↦ f (↑x : ℕ))
⊢ (sup univ fun (n_1 : Fin n) ↦ f (↑n_1 : ℕ)) = (range n).sup f

Tactic:
rw [← image_fin_univ, sup_image, Function.comp_def]

Premises used: Finset.image_fin_univ, Function.comp_def, Finset.sup_image
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
b : (↑(Set.range f) : Type u_2)
⊢ ∀ (a : α), f a = (↑b : β) ↔ Membership.mem (γ := Finset α) Finset.univ a ∧ (fun (a : α) ↦ f a = (↑b : β)) a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
b : (↑(Set.range f) : Type u_2)
⊢ f (hf.invOfMemRange b) = (↑b : β)

Tactic:
(Finset.choose_spec (fun a => f a = b) _ _).right

Premises used: Function.Injective.invOfMemRange, And.right, Finset.choose_spec, Subtype.val, Eq
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
a : α
⊢ hf.invOfMemRange (Subtype.mk (p := fun (x : β) ↦ x ∈ Set.range f) (f a) ⋯) = a

Tactic:
hf (Finset.choose_spec (fun a' => f a' = f a) _ _).right

Premises used: And.right, Finset.choose_spec, Eq
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
inst_2 : Nonempty α
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)
⊢ (Set.range f).restrict (π := fun (a : β) ↦ α) (invFun f) = hf.invOfMemRange

Tactic:
ext ⟨b, h⟩
-- Module: Mathlib.Data.Fintype.Inv
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
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))
⊢ (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:
apply hf
-- Module: Mathlib.Data.Fintype.Inv
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
⊢ 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:
simp [hf.left_inv_of_invOfMemRange, @invFun_eq _ _ _ f b (Set.mem_range.mp h)]

Premises used: Set.mem_range, Function.Injective.left_inv_of_invOfMemRange, Iff.mp, Function.invFun_eq
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
a : α
⊢ hf.invOfMemRange (Subtype.mk (p := fun (x : β) ↦ x ∈ Set.range f) (f a) ⋯) = a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α ↪ β
b : (↑(Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_2)
⊢ (f : (a : α) → β) (f.invOfMemRange b) = (↑b : β)

Tactic:
f.injective.left_inv_of_invOfMemRange b

Premises used: Function.Embedding.invOfMemRange, Function.Injective.left_inv_of_invOfMemRange, Function.Embedding.injective
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α ↪ β
a : α
⊢ f.invOfMemRange
      (Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) ((f : (a : α) → β) a) ⋯) =
    a

Tactic:
f.injective.right_inv_of_invOfMemRange a

Premises used: Function.Embedding.invOfMemRange, Function.Injective.right_inv_of_invOfMemRange, Set.Mem, Function.Embedding.injective
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α ↪ β
inst_2 : Nonempty α
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)
⊢ Set.restrict (π := fun (a : β) ↦ α) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      (invFun (⇑f : (a : α) → β)) =
    f.invOfMemRange

Tactic:
ext ⟨b, h⟩
-- Module: Mathlib.Data.Fintype.Inv
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
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)) :
      β)
⊢ 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:
apply f.injective

Premises used: Function.Embedding.injective
-- Module: Mathlib.Data.Fintype.Inv
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
⊢ 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:
simp [f.left_inv_of_invOfMemRange, @invFun_eq _ _ _ f b (Set.mem_range.mp h)]

Premises used: Set.mem_range, Iff.mp, Function.invFun_eq, Function.Embedding.left_inv_of_invOfMemRange
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α ↪ β
a : α
⊢ f.invOfMemRange
      (Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) ((f : (a : α) → β) a) ⋯) =
    a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
hp : ∃! a : α, p a
⊢ ∃! a : α, Membership.mem (γ := Finset α) univ a ∧ p a

Tactic:
simpa
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
hp : ∃! a : α, p a
⊢ p (choose p hp)

Tactic:
(chooseX p hp).property

Premises used: Fintype.choose, Fintype.chooseX, Subtype.property
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α_1
p_1 : α_1 → Prop
inst_1 : DecidablePred p_1
α : Type u_4
p : α → Prop
inst_2 : Fintype { a : α // p a }
inst_3 : DecidableEq α
x y : { a : α // p a }
hy : (fun (a : { a : α // p a }) ↦ (↑a : α) = (↑x : α)) y
⊢ y = x

Tactic:
simpa [Subtype.ext_iff] using hy

Premises used: Subtype.ext_iff
-- Module: Mathlib.Data.Fintype.Inv
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 : α)
rw₁ rw₂ : (↑x : α) = (↑x : α)
⊢ 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) _]

Premises used: Fintype.choose_spec, Subtype.ext_iff, Subtype.val, Eq
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α → β
f_bij : Bijective f
⊢ LeftInverse (bijInv f_bij) f

Tactic:
fun a =>
  f_bij.left (choose_spec (fun a' => f a' = f a) _)

Premises used: Function.LeftInverse, Fintype.choose_spec, Function.Bijective.existsUnique, And.left, Eq
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α → β
f_bij : Bijective f
⊢ RightInverse (bijInv f_bij) f

Tactic:
fun b =>
  choose_spec (fun a' => f a' = b) _

Premises used: Function.LeftInverse, Fintype.choose_spec, Function.Bijective.existsUnique, Function.RightInverse, Eq, Fintype.bijInv
-- Module: Mathlib.Data.Fintype.Inv
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α → β
f_bij : Bijective f
⊢ Bijective (bijInv f_bij)

Tactic:
⟨(rightInverse_bijInv _).injective, (leftInverse_bijInv _).surjective⟩

Premises used: And.intro, Function.Bijective, Function.LeftInverse.surjective, Fintype.leftInverse_bijInv, Function.RightInverse.injective, Fintype.rightInverse_bijInv
-- Module: Mathlib.Data.Fintype.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : CompleteLattice β
f : α → β
⊢ sup univ f = iSup f

Tactic:
(sup_eq_iSup _ f).trans <| congr_arg _ <| funext fun _ => iSup_pos (mem_univ _)

Premises used: Finset.mem_univ, iSup_pos, congr_arg, funext, Finset.sup_eq_iSup, Eq.trans
-- Module: Mathlib.Data.Fintype.Lattice
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : CompleteLattice β
f : α → β
⊢ inf univ f = iInf f

Tactic:
@sup_univ_eq_iSup _ βᵒᵈ _ _ (f : α → βᵒᵈ)

Premises used: iInf, OrderDual, Finset.sup_univ_eq_iSup, Finset.inf
-- Module: Mathlib.Data.Fintype.Lattice
Goal:
α : Type u_2
inst : Fintype α
inst_1 : SemilatticeInf α
inst_2 : OrderBot α
a : α
⊢ fold min a (fun (x : α) ↦ x) univ = ⊥

Tactic:
eq_bot_iff.2 <|
    ((Finset.fold_op_rel_iff_and <| @le_inf_iff α _).1 le_rfl).2 ⊥ <| Finset.mem_univ _

Premises used: Iff.mpr, Finset.mem_univ, le_rfl, Bot.bot, le_inf_iff, And.right, Finset.fold_op_rel_iff_and, Iff.mp, eq_bot_iff
-- Module: Mathlib.Data.Fintype.Lattice
Goal:
α : Type u_2
inst : Fintype α
inst_1 : SemilatticeSup α
inst_2 : OrderTop α
a : α
⊢ fold max a (fun (x : α) ↦ x) univ = ⊤

Tactic:
@fold_inf_univ αᵒᵈ _ _ _ _

Premises used: OrderDual, Finset.fold_inf_univ