awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
ι : Sort u_4
κ : Sort u_5
inst_1 : Nonempty ι
inst_2 : Finite κ
f : ι → α
hf : Directed r f
g : κ → ι
⊢ ∃ (z : ι), ∀ (i : κ), r (f (g i)) (f z)

Tactic:
simpa using
    (hf.comp_of_surjective PLift.down_surjective).finite_set_le (Set.finite_range (PLift.up ∘ g))

Premises used: Function.comp, Set.finite_range, Directed.finite_set_le, Directed.comp_of_surjective, PLift.up, PLift.down_surjective
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
ι : Sort u_4
κ : Sort u_5
inst_1 : Nonempty ι
inst_2 : Finite κ
f : ι → α
hf : Directed r f
g : κ → ι
⊢ ∃ (z : ι), ∀ (i : κ), r (f (g i)) (f z)

Tactic:
classical
  simpa using
    (hf.comp_of_surjective PLift.down_surjective).finite_set_le (Set.finite_range (PLift.up ∘ g))

Premises used: Function.comp, Set.finite_range, Directed.finite_set_le, Directed.comp_of_surjective, PLift.up, PLift.down_surjective
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsDirectedOrder α
f : β → α
⊢ ∃ (M : α), ∀ (i : β), f i ≤ M

Tactic:
directed_id.finite_le _

Premises used: Directed.finite_le, directed_id
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
f : β → α
⊢ ∃ (M : α), ∀ (i : β), M ≤ f i

Tactic:
directed_id.finite_le (r := (· ≥ ·)) _

Premises used: Directed.finite_le, directed_id
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
s : Set α
hs : s.Finite
⊢ ∃ (M : α), ∀ i ∈ s, i ≤ M

Tactic:
directed_id.finite_set_le hs

Premises used: Directed.finite_set_le, directed_id
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
s : Set α
hs : s.Finite
⊢ ∃ (M : α), ∀ i ∈ s, M ≤ i

Tactic:
directed_id.finite_set_le (r := (· ≥ ·)) hs

Premises used: Directed.finite_set_le, directed_id
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsDirectedOrder α
f : β → α
obtain : ∀ (M : α) (hM : ∀ (i : β), f i ≤ M), BddAbove (Set.range f)
⊢ BddAbove (Set.range f)

Tactic:
obtain ⟨M, hM⟩ := Finite.exists_le f

Premises used: Finite.exists_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsDirectedOrder α
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
⊢ BddAbove (Set.range f)

Tactic:
⟨M, fun a ha => ?_⟩

Premises used: BddAbove, Set.Nonempty, Exists.intro
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsDirectedOrder α
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
refine : ∀ (a : α) (ha : a ∈ Set.range f), a ≤ M
⊢ BddAbove (Set.range f)

Tactic:
refine ⟨M, fun a ha => ?_⟩
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsDirectedOrder α
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
a : α
ha : a ∈ Set.range f
obtain : ∀ (b : β), f b ≤ M
⊢ a ≤ M

Tactic:
obtain ⟨b, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsDirectedOrder α
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
b : β
⊢ f b ≤ M

Tactic:
hM b
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsDirectedOrder α
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
b : β
⊢ f b ≤ M

Tactic:
exact hM b
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
f : β → α
obtain : ∀ (M : α) (hM : ∀ (i : β), M ≤ f i), BddBelow (Set.range f)
⊢ BddBelow (Set.range f)

Tactic:
obtain ⟨M, hM⟩ := Finite.exists_ge f

Premises used: Finite.exists_ge
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
⊢ BddBelow (Set.range f)

Tactic:
⟨M, fun a ha => ?_⟩

Premises used: Set.Nonempty, BddBelow, Exists.intro
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
refine : ∀ (a : α) (ha : a ∈ Set.range f), M ≤ a
⊢ BddBelow (Set.range f)

Tactic:
refine ⟨M, fun a ha => ?_⟩
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
a : α
ha : a ∈ Set.range f
obtain : ∀ (b : β), M ≤ f b
⊢ M ≤ a

Tactic:
obtain ⟨b, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
b : β
⊢ M ≤ f b

Tactic:
hM b
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
b : β
⊢ M ≤ f b

Tactic:
exact hM b
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → α
inst_1 : Nonempty ι
inst_2 : Finite ι
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
ha : a ≤ ⨆ (i : ι), f i
obtain : ∀ (i : ι) (hi : ∀ (i_1 : ι), f (id i_1) ≤ f i), ∃ (i : ι), a ≤ f i
⊢ ∃ (i : ι), a ≤ f i

Tactic:
obtain ⟨i, hi⟩ := hf.finite_le id

Premises used: id, Directed.finite_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → α
inst_1 : Nonempty ι
inst_2 : Finite ι
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
ha : a ≤ ⨆ (i : ι), f i
i : ι
hi : ∀ (i_1 : ι), f (id i_1) ≤ f i
⊢ ∃ (i : ι), a ≤ f i

Tactic:
⟨i, ha.trans <| iSup_le hi⟩

Premises used: Exists.intro, iSup_le, LE.le.trans
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → α
inst_1 : Nonempty ι
inst_2 : Finite ι
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
ha : a ≤ ⨆ (i : ι), f i
i : ι
hi : ∀ (i_1 : ι), f (id i_1) ≤ f i
⊢ ∃ (i : ι), a ≤ f i

Tactic:
exact ⟨i, ha.trans <| iSup_le hi⟩
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → α
inst_1 : Nonempty ι
inst_2 : Finite ι
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
i : ι
hai : a ≤ f i
⊢ a ≤ ⨆ (i : ι), f i

Tactic:
le_iSup_of_le i hai

Premises used: le_iSup_of_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → α
inst_1 : Nonempty ι
inst_2 : Finite ι
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
i : ι
hai : a ≤ f i
⊢ a ≤ ⨆ (i : ι), f i

Tactic:
exact le_iSup_of_le i hai

Premises used: le_iSup_of_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
a : α
hs : s.Nonempty
hs' : s.Finite
hs'' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Nonempty.{u_2 + 1} (↑s : Type u_2)

Tactic:
have := hs.to_subtype
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
a : α
hs : s.Nonempty
hs' : s.Finite
hs'' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
⊢ Finite.{u_2 + 1} (↑s : Type u_2)

Tactic:
have := hs'.to_subtype
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
a : α
hs : s.Nonempty
hs' : s.Finite
hs'' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
this_1 : Nonempty.{u_2 + 1} (↑s : Type u_2)
this : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b

Tactic:
simp [sSup_eq_iSup', le_iSup_iff_of_directed hs''.directed_val]

Premises used: DirectedOn.directed_val, le_iSup_iff_of_directed, sSup_eq_iSup'
-- Module: Mathlib.Data.Fintype.Order
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
f : ι → Set α
inst : Nonempty ι
inst_1 : Finite ι
hf : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) f
⊢ s ⊆ ⋃ (i : ι), f i ↔ ∃ (i : ι), s ⊆ f i

Tactic:
le_iSup_iff_of_directed hf

Premises used: le_iSup_iff_of_directed, Set.iUnion
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_2
S : Set (Set α)
s : Set α
hS : S.Nonempty
hS' : S.Finite
hS'' : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
⊢ s ⊆ sSup S ↔ ∃ t ∈ S, s ⊆ t

Tactic:
le_sSup_iff_of_directedOn hS hS' hS''

Premises used: le_sSup_iff_of_directedOn
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
a : α
f : ι → α
c : ι
h : a ≤ f c
⊢ a ≤ iSup f

Tactic:
_root_.le_ciSup_of_le (bddAbove_range f) c h

Premises used: le_ciSup_of_le, Finite.bddAbove_range
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
a : α
f : ι → α
c : ι
h : f c ≤ a
⊢ iInf f ≤ a

Tactic:
_root_.ciInf_le_of_le (bddBelow_range f) c h

Premises used: ciInf_le_of_le, Finite.bddBelow_range
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
f g : ι → α
H : ∀ (x : ι), f x ≤ g x
⊢ iSup f ≤ iSup g

Tactic:
_root_.ciSup_mono (bddAbove_range g) H

Premises used: Finite.bddAbove_range, ciSup_mono
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
f g : ι → α
H : ∀ (x : ι), f x ≤ g x
⊢ iInf f ≤ iInf g

Tactic:
_root_.ciInf_mono (bddBelow_range f) H

Premises used: Finite.bddBelow_range, ciInf_mono
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ f i ≤ ⨆ (j : ι), f j

Tactic:
le_ciSup_of_le i le_rfl

Premises used: le_rfl, Finite.le_ciSup_of_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ ⨅ (j : ι), f j ≤ f i

Tactic:
le_ciSup (α := αᵒᵈ) f i

Premises used: iInf, Finite.le_ciSup, OrderDual
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Nonempty ι
f : ι → α
a : α
⊢ (⨆ (i : ι), f i) ⊔ a = ⨆ (i : ι), f i ⊔ a

Tactic:
le_antisymm (sup_le ?_ ?_) <| ciSup_le fun i ↦ sup_le_sup_right (le_ciSup f i) a

Premises used: sup_le_sup_right, Finite.le_ciSup, le_antisymm, sup_le, ciSup_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Nonempty ι
f : ι → α
a : α
refine_1 : LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), f i ⊔ a)
refine_2 : a ≤ ⨆ (i : ι), f i ⊔ a
⊢ (⨆ (i : ι), f i) ⊔ a = ⨆ (i : ι), f i ⊔ a

Tactic:
refine le_antisymm (sup_le ?_ ?_) <| ciSup_le fun i ↦ sup_le_sup_right (le_ciSup f i) a

Premises used: sup_le_sup_right, Finite.le_ciSup, le_antisymm, sup_le, ciSup_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Nonempty ι
f : ι → α
a : α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), f i ⊔ a)

Tactic:
ciSup_le fun i ↦ le_ciSup_of_le i le_sup_left

Premises used: le_sup_left, Finite.le_ciSup_of_le, ciSup_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Nonempty ι
f : ι → α
a : α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), f i ⊔ a)

Tactic:
exact ciSup_le fun i ↦ le_ciSup_of_le i le_sup_left

Premises used: le_sup_left, Finite.le_ciSup_of_le, ciSup_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Nonempty ι
f : ι → α
a : α
⊢ a ≤ ⨆ (i : ι), f i ⊔ a

Tactic:
le_ciSup_of_le (Classical.arbitrary ι) le_sup_right

Premises used: le_sup_right, Finite.le_ciSup_of_le, Classical.arbitrary
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Nonempty ι
f : ι → α
a : α
⊢ a ≤ ⨆ (i : ι), f i ⊔ a

Tactic:
exact le_ciSup_of_le (Classical.arbitrary ι) le_sup_right
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Nonempty ι
f : ι → α
a : α
⊢ (⨅ (i : ι), f i) ⊓ a = ⨅ (i : ι), f i ⊓ a

Tactic:
ciSup_sup (α := αᵒᵈ) ..

Premises used: iInf, Finite.ciSup_sup, OrderDual
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Finite ι
inst_1 : Finite ι'
inst_2 : ConditionallyCompleteLattice α
f : ι × ι' → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (a : ι × ι'), f a) (⨆ (i : ι), ⨆ (i' : ι'), f (i, i'))

Tactic:
_root_.ciSup_prod (bddAbove_range f)

Premises used: ciSup_prod, Finite.bddAbove_range
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Finite ι
inst_1 : Finite ι'
inst_2 : ConditionallyCompleteLattice α
f : ι × ι' → α
⊢ Eq.{u_1 + 1} (α := α) (⨅ (a : ι × ι'), f a) (⨅ (i : ι), ⨅ (i' : ι'), f (i, i'))

Tactic:
ciSup_prod (α := αᵒᵈ) f

Premises used: Finite.ciSup_prod, iInf, OrderDual
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
⊢ ∃ (j : ι), f j = ⨆ (i : ι), f i

Tactic:
exists_eq_ciSup_of_finite

Premises used: exists_eq_ciSup_of_finite
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
obtain : ∀ (j : ι) (hj : f j = ⨆ (i : ι), f i), g (⨆ (i : ι), f i) = ⨆ (i : ι), g (f i)
⊢ g (⨆ (i : ι), f i) = ⨆ (i : ι), g (f i)

Tactic:
obtain ⟨j, hj⟩ : ∃ j, f j = ⨆ i, f i := exists_eq_ciSup_of_finite

Premises used: exists_eq_ciSup_of_finite
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
j : ι
hj : f j = ⨆ (i : ι), f i
rw : g (f j) = ⨆ (i : ι), g (f i)
⊢ g (⨆ (i : ι), f i) = ⨆ (i : ι), g (f i)

Tactic:
rw [← hj]
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
j : ι
hj : f j = ⨆ (i : ι), f i
⊢ g (f j) = ⨆ (i : ι), g (f i)

Tactic:
le_antisymm (le_ciSup_of_le j le_rfl) <|
    ciSup_le fun i ↦ hg (hs i) (hs j) (hj ▸ le_ciSup f i)

Premises used: le_rfl, Eq.rec, Finite.le_ciSup, le_antisymm, Finite.le_ciSup_of_le, Eq.symm, ciSup_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
j : ι
hj : f j = ⨆ (i : ι), f i
⊢ g (f j) = ⨆ (i : ι), g (f i)

Tactic:
exact le_antisymm (le_ciSup_of_le j le_rfl) <|
    ciSup_le fun i ↦ hg (hs i) (hs j) (hj ▸ le_ciSup f i)

Premises used: le_rfl, Eq.rec, Finite.le_ciSup, le_antisymm, Finite.le_ciSup_of_le, Eq.symm, ciSup_le
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
⊢ g (⨅ (i : ι), f i) = ⨅ (i : ι), g (f i)

Tactic:
map_iSup_of_monotoneOn (α := αᵒᵈ) (β := βᵒᵈ) (fun _ hi _ hj h ↦ hg hj hi h) hs

Premises used: iInf, Finite.map_iSup_of_monotoneOn, OrderDual
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : AntitoneOn g s
hs : ∀ (i : ι), f i ∈ s
⊢ g (⨆ (i : ι), f i) = ⨅ (i : ι), g (f i)

Tactic:
map_iSup_of_monotoneOn (β := βᵒᵈ) hg hs

Premises used: iInf, Finite.map_iSup_of_monotoneOn, OrderDual
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : AntitoneOn g s
hs : ∀ (i : ι), f i ∈ s
⊢ g (⨅ (i : ι), f i) = ⨆ (i : ι), g (f i)

Tactic:
map_iInf_of_monotoneOn (β := βᵒᵈ) hg hs

Premises used: iSup, Finite.map_iInf_of_monotoneOn, OrderDual
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
f : ι → α
g : α → β
hg : Monotone g
⊢ g (⨆ (i : ι), f i) = ⨆ (i : ι), g (f i)

Tactic:
map_iSup_of_monotoneOn (monotoneOn_univ.mpr hg) (fun i ↦ Set.mem_univ (f i))

Premises used: Iff.mpr, Finite.map_iSup_of_monotoneOn, Set.mem_univ, monotoneOn_univ
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
f : ι → α
g : α → β
hg : Monotone g
⊢ g (⨅ (i : ι), f i) = ⨅ (i : ι), g (f i)

Tactic:
map_iSup_of_monotone (α := αᵒᵈ) (β := βᵒᵈ) f fun _ _ h ↦ hg h

Premises used: iInf, Finite.map_iSup_of_monotone, OrderDual
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
f : ι → α
g : α → β
hg : Antitone g
⊢ g (⨆ (i : ι), f i) = ⨅ (i : ι), g (f i)

Tactic:
map_iSup_of_monotone (β := βᵒᵈ) f hg

Premises used: iInf, Finite.map_iSup_of_monotone, OrderDual
-- Module: Mathlib.Data.Fintype.Order
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
f : ι → α
g : α → β
hg : Antitone g
⊢ g (⨅ (i : ι), f i) = ⨆ (i : ι), g (f i)

Tactic:
map_iInf_of_monotone (β := βᵒᵈ) f hg

Premises used: iSup, Finite.map_iInf_of_monotone, OrderDual
-- Module: Mathlib.Data.Fintype.Parity
Goal:
α : Type u_1
⊢ Fact (Even (card (Fin 2)))

Tactic:
⟨⟨1, rfl⟩⟩

Premises used: Fact.mk, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ (permsOfList (a :: l)).length = (a :: l).length !

Tactic:
simp [Nat.factorial_succ, permsOfList, length_permsOfList, succ_mul, add_comm]

Premises used: Nat.factorial_succ, add_comm, Nat.succ_mul, permsOfList
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
⊢ ∀ (x : α), (f : (a : α) → α) x ≠ x → False

Tactic:
simp only [not_mem_nil] at h

Premises used: List.not_mem_nil
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → False
⊢ Membership.mem (γ := List (Equiv.Perm α)) (permsOfList []) f

Tactic:
List.mem_singleton.2 (Equiv.ext fun x => Decidable.byContradiction <| h x)

Premises used: Iff.mpr, Equiv.ext, List.mem_singleton, Decidable.byContradiction, permsOfList
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → False
⊢ Membership.mem (γ := List (Equiv.Perm α)) (permsOfList []) f

Tactic:
exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.byContradiction <| h x)

Premises used: Iff.mpr, Equiv.ext, List.mem_singleton, Decidable.byContradiction
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
pos : ∀ (hfa : (f : (a : α) → α) a = a), f ∈ permsOfList (a :: l)
neg : ∀ (hfa : ¬(f : (a : α) → α) a = a), f ∈ permsOfList (a :: l)
⊢ f ∈ permsOfList (a :: l)

Tactic:
by_cases hfa : f a = a

Premises used: DFunLike.coe
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : (f : (a : α) → α) a = a
⊢ f ∈ permsOfList (a :: l)

Tactic:
mem_append_left _ (IH fun x hx => mem_of_ne_of_mem ?_ (h x hx))

Premises used: List.mem_of_ne_of_mem, List.mem_append_left, permsOfList
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : (f : (a : α) → α) a = a
pos : ∀ (x : α) (hx : (f : (a : α) → α) x ≠ x), x ≠ a
⊢ f ∈ permsOfList (a :: l)

Tactic:
refine mem_append_left _ (IH fun x hx => mem_of_ne_of_mem ?_ (h x hx))

Premises used: List.mem_of_ne_of_mem, List.mem_append_left
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
x : α
hx : (f : (a : α) → α) x ≠ x
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : (f : (a : α) → α) x = x
⊢ False

Tactic:
hx hfa
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
x : α
hx : (f : (a : α) → α) x ≠ x
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : (f : (a : α) → α) x = x
⊢ False

Tactic:
exact hx hfa
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
⊢ Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)

Tactic:
have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
x : α
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : ¬(f : (a : α) → α) x = x
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
hx : (Equiv.swap x ((f : (a : α) → α) x) * f : (a : α) → α) x ≠ x
apply : (Equiv.swap x ((f : (a : α) → α) x) * f : (a : α) → α) x = x
⊢ False

Tactic:
apply hx
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
x : α
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : ¬(f : (a : α) → α) x = x
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
hx : (Equiv.swap x ((f : (a : α) → α) x) * f : (a : α) → α) x ≠ x
⊢ (Equiv.swap x ((f : (a : α) → α) x) * f : (a : α) → α) x = x

Tactic:
simp only [mul_apply, swap_apply_right]

Premises used: Equiv.Perm.mul_apply, Equiv.swap_apply_right