awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
b : Y
hb_1 : Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) b
hb : ∃ a ∈ s.finset, (f : (a : X) → Y) a = b
a : X
ha' : a ∈ s.finset
ha :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) a : Y)
obtain :
  ∀ (b : X) (hb' : b ∈ s.finset)
    (hb :
      Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
        ((f : (a : X) → Y) b : Y)),
    LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
        (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
            ((f : (a : X) → Y) a) ha :
          ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
        (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
            ((f : (a : X) → Y) b) hb :
          ↥(Finset.image (⇑f : (a : X) → Y) s.finset)) ∨
      LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
        (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
            ((f : (a : X) → Y) b) hb :
          ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
        (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
            ((f : (a : X) → Y) a) ha :
          ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
⊢ Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
        ((f : (a : X) → Y) a) ha ≤
      Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) b
        hb_1 ∨
    Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x) b hb_1 ≤
      Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
        ((f : (a : X) → Y) a) ha

Tactic:
obtain ⟨b, hb', rfl⟩ := hb

Premises used: rfl
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : X
ha' : a ∈ s.finset
ha :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) a : Y)
b : X
hb' : b ∈ s.finset
hb :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) b : Y)
h : Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) a ha' ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) b hb'
⊢ LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset)) ∨
    LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))

Tactic:
Or.inl (f.monotone h)

Premises used: OrderHom.monotone, Or.inl
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : X
ha' : a ∈ s.finset
ha :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) a : Y)
b : X
hb' : b ∈ s.finset
hb :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) b : Y)
h : Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) a ha' ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) b hb'
⊢ LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset)) ∨
    LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))

Tactic:
exact Or.inl (f.monotone h)

Premises used: OrderHom.monotone, Or.inl
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : X
ha' : a ∈ s.finset
ha :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) a : Y)
b : X
hb' : b ∈ s.finset
hb :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) b : Y)
h : Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) b hb' ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) a ha'
⊢ LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset)) ∨
    LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))

Tactic:
Or.inr (f.monotone h)

Premises used: OrderHom.monotone, Or.inr
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
a : X
ha' : a ∈ s.finset
ha :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) a : Y)
b : X
hb' : b ∈ s.finset
hb :
  Membership.mem.{u_2, u_2} (α := Y) (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset)
    ((f : (a : X) → Y) b : Y)
h : Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) b hb' ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s.finset) a ha'
⊢ LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset)) ∨
    LE.le.{u_2} (α := ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) b) hb :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))
      (Subtype.mk (p := fun (x : Y) ↦ Membership.mem (γ := Finset Y) (Finset.image (⇑f : (a : X) → Y) s.finset) x)
          ((f : (a : X) → Y) a) ha :
        ↥(Finset.image (⇑f : (a : X) → Y) s.finset))

Tactic:
exact Or.inr (f.monotone h)

Premises used: OrderHom.monotone, Or.inr
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
y : Y
⊢ y ∈ (s.map f).finset ↔ ∃ x ∈ s.finset, (f : (a : X) → Y) x = y

Tactic:
simp [map]

Premises used: PartialOrder.NonemptyFiniteChains.map
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
f : X →o Y
a b : NonemptyFiniteChains X
h : a ≤ b
x : Y
hx : Membership.mem (γ := Finset Y) (finset ((fun (s : NonemptyFiniteChains X) ↦ s.map f) a)) x
simp : ∀ (hx : ∃ x_1 ∈ a.finset, (f : (a : X) → Y) x_1 = x), ∃ x_1 ∈ b.finset, (f : (a : X) → Y) x_1 = x
⊢ Membership.mem (γ := Finset Y) (finset ((fun (s : NonemptyFiniteChains X) ↦ s.map f) b)) x

Tactic:
simp only [mem_map_iff] at hx ⊢

Premises used: PartialOrder.NonemptyFiniteChains.mem_map_iff
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
f : X →o Y
a b : NonemptyFiniteChains X
h : a ≤ b
x : Y
hx : ∃ x_1 ∈ a.finset, (f : (a : X) → Y) x_1 = x
obtain :
  ∀ (x : X) (hx : x ∈ a.finset),
    ∃ x_1 ∈ b.finset, Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x_1 : Y) ((f : (a : X) → Y) x : Y)
⊢ ∃ x_1 ∈ b.finset, (f : (a : X) → Y) x_1 = x

Tactic:
obtain ⟨x, hx, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
f : X →o Y
a b : NonemptyFiniteChains X
h : a ≤ b
x : X
hx : x ∈ a.finset
⊢ ∃ x_1 ∈ b.finset, Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x_1 : Y) ((f : (a : X) → Y) x : Y)

Tactic:
⟨x, h hx, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.NonemptyFiniteChains
Goal:
X : Type u_1
Y : Type u_2
inst : PartialOrder X
inst_1 : PartialOrder Y
f : X →o Y
a b : NonemptyFiniteChains X
h : a ≤ b
x : X
hx : x ∈ a.finset
⊢ ∃ x_1 ∈ b.finset, Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x_1 : Y) ((f : (a : X) → Y) x : Y)

Tactic:
exact ⟨x, h hx, rfl⟩
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : NoMaxOrder β
simp_rw :
  (∀ (b : β), Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}) ↔ ∀ (b : β), Set.Finite.{u_1} (α := α) {x : α | h x < b}
⊢ Northcott h ↔ Tendsto h cofinite atTop

Tactic:
simp_rw [northcott_iff, tendsto_atTop, eventually_cofinite, not_le]

Premises used: not_le, Filter.eventually_cofinite, Filter.tendsto_atTop, northcott_iff
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : NoMaxOrder β
⊢ (∀ (b : β), Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}) ↔ ∀ (b : β), Set.Finite.{u_1} (α := α) {x : α | h x < b}

Tactic:
⟨fun H b ↦ (H b).subset fun x ↦ le_of_lt, fun H b ↦ ?_⟩

Premises used: le_of_lt, Set.Finite.subset, Iff.intro
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : NoMaxOrder β
refine :
  ∀ (H : ∀ (b : β), Set.Finite.{u_1} (α := α) {x : α | h x < b}) (b : β), Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}
⊢ (∀ (b : β), Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}) ↔ ∀ (b : β), Set.Finite.{u_1} (α := α) {x : α | h x < b}

Tactic:
refine ⟨fun H b ↦ (H b).subset fun x ↦ le_of_lt, fun H b ↦ ?_⟩
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : NoMaxOrder β
H : ∀ (b : β), Set.Finite.{u_1} (α := α) {x : α | h x < b}
b : β
obtain : ∀ (b' : β) (hc : b < b'), Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}
⊢ Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}

Tactic:
obtain ⟨b', hc⟩ := exists_gt b

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : NoMaxOrder β
H : ∀ (b : β), Set.Finite.{u_1} (α := α) {x : α | h x < b}
b b' : β
hc : b < b'
⊢ Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}

Tactic:
(H b').subset fun x hx ↦ lt_of_le_of_lt hx hc

Premises used: lt_of_le_of_lt, Set.Finite.subset
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : NoMaxOrder β
H : ∀ (b : β), Set.Finite.{u_1} (α := α) {x : α | h x < b}
b b' : β
hc : b < b'
⊢ Set.Finite.{u_1} (α := α) {a : α | h a ≤ b}

Tactic:
exact (H b').subset fun x hx ↦ lt_of_le_of_lt hx hc

Premises used: lt_of_le_of_lt, Set.Finite.subset
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : Northcott h
s : Set α
hs : s.Nonempty
obtain : ∀ (a₁ : α) (h₁ : a₁ ∈ s), ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'
⊢ ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'

Tactic:
obtain ⟨a₁, h₁⟩ := hs
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : Northcott h
s : Set α
a₁ : α
h₁ : a₁ ∈ s
obtain :
  ∀ (a₂ : α) (h₂ : a₂ ∈ {a : α | h a ≤ h a₁} ∩ s) (h₃ : ∀ b ∈ {a : α | h a ≤ h a₁} ∩ s, h a₂ ≤ h b),
    ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'
⊢ ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'

Tactic:
obtain ⟨a₂, h₂, h₃⟩ := Set.exists_min_image ({a | h a ≤ h a₁} ∩ s) h
    ((finite_le (h a₁)).inter_of_left s) ⟨a₁, le_rfl, h₁⟩

Premises used: le_rfl, Set.Finite.inter_of_left, Northcott.finite_le, setOf, Set.exists_min_image, LE.le, Inter.inter, And.intro, Exists.intro
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
h : α → β
inst : LinearOrder β
inst_1 : Northcott h
s : Set α
a₁ : α
h₁ : a₁ ∈ s
a₂ : α
h₂ : a₂ ∈ {a : α | h a ≤ h a₁} ∩ s
h₃ : ∀ b ∈ {a : α | h a ≤ h a₁} ∩ s, h a₂ ≤ h b
⊢ ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'

Tactic:
grind
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst : Preorder β
inst_1 : LE γ
inst_2 : Northcott h
H : ∀ (c : γ), BddAbove (h' ⁻¹' {x : γ | x ≤ c})
c : γ
obtain : ∀ (b : β) (hb : ∀ y ∈ h' ⁻¹' {x : γ | x ≤ c}, y ≤ b), Set.Finite.{u_1} (α := α) {a : α | (h' ∘ h) a ≤ c}
⊢ Set.Finite.{u_1} (α := α) {a : α | (h' ∘ h) a ≤ c}

Tactic:
obtain ⟨b, hb⟩ := bddAbove_def.mp (H c)

Premises used: Iff.mp, bddAbove_def
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst : Preorder β
inst_1 : LE γ
inst_2 : Northcott h
H : ∀ (c : γ), BddAbove (h' ⁻¹' {x : γ | x ≤ c})
c : γ
b : β
hb : ∀ y ∈ h' ⁻¹' {x : γ | x ≤ c}, y ≤ b
⊢ Subset.{u_1} (α := Set α) {a : α | (h' ∘ h) a ≤ c} {a : α | h a ≤ b}

Tactic:
grind
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst : Preorder β
inst_1 : LE γ
inst_2 : Northcott h
H : ∀ (c : γ), BddAbove (h' ⁻¹' {x : γ | x ≤ c})
c : γ
b : β
hb : ∀ y ∈ h' ⁻¹' {x : γ | x ≤ c}, y ≤ b
⊢ Set.Finite.{u_1} (α := α) {a : α | (h' ∘ h) a ≤ c}

Tactic:
exact (finite_le (h := h) b).subset <| by grind

Premises used: Northcott.finite_le, Set.Finite.subset
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst : LE γ
inst_1 : Northcott h'
H : ∀ (b : β), (h ⁻¹' {b}).Finite
c : γ
⊢ Set.Finite.{u_1} (α := α) {a : α | (h' ∘ h) a ≤ c}

Tactic:
Set.Finite.of_finite_fibers h ?_ fun x _ ↦ (H x).inter_of_right _

Premises used: setOf, Function.comp, Set.Finite.of_finite_fibers, LE.le, Set.Finite.inter_of_right
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst : LE γ
inst_1 : Northcott h'
H : ∀ (b : β), (h ⁻¹' {b}).Finite
c : γ
refine : (h '' {a : α | (h' ∘ h) a ≤ c}).Finite
⊢ Set.Finite.{u_1} (α := α) {a : α | (h' ∘ h) a ≤ c}

Tactic:
refine Set.Finite.of_finite_fibers h ?_ fun x _ ↦ (H x).inter_of_right _

Premises used: Set.Finite.of_finite_fibers, Set.Finite.inter_of_right
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst : LE γ
inst_1 : Northcott h'
H : ∀ (b : β), (h ⁻¹' {b}).Finite
c : γ
⊢ h '' {a : α | (h' ∘ h) a ≤ c} ⊆ {a : β | h' a ≤ c}

Tactic:
grind
-- Module: Mathlib.Order.Northcott
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst : LE γ
inst_1 : Northcott h'
H : ∀ (b : β), (h ⁻¹' {b}).Finite
c : γ
⊢ (h '' {a : α | (h' ∘ h) a ≤ c}).Finite

Tactic:
exact (finite_le (h := h') c).subset <| by grind

Premises used: Northcott.finite_le, Set.Finite.subset
-- Module: Mathlib.Order.Notation
Goal:
α : Type u_1
inst : Top α
⊢ Nonempty α

Tactic:
⟨⊤⟩

Premises used: Nonempty.intro, Top.top
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n m : Nucleus X
x y : X
f g : Nucleus X
h : Eq.{u_1 + 1} (α := (a : X) → X) ((fun (x : Nucleus X) ↦ x.toFun) f) ((fun (x : Nucleus X) ↦ x.toFun) g)
obtain :
  ∀ (toFun : X → X) (map_inf' : ∀ (a b : X), toFun (a ⊓ b) = toFun a ⊓ toFun b)
    (idempotent' :
      ∀ (x : X),
        { toFun := toFun, map_inf' := map_inf' : InfHom X X }.toFun
            ({ toFun := toFun, map_inf' := map_inf' : InfHom X X }.toFun x) ≤
          { toFun := toFun, map_inf' := map_inf' : InfHom X X }.toFun x)
    (le_apply' : ∀ (x : X), x ≤ { toFun := toFun, map_inf' := map_inf' : InfHom X X }.toFun x)
    (h :
      Eq.{u_1 + 1} (α := (a : X) → X)
        ((fun (x : Nucleus X) ↦ x.toFun)
          { toFun := toFun, map_inf' := map_inf', idempotent' := idempotent', le_apply' := le_apply' })
        ((fun (x : Nucleus X) ↦ x.toFun) g)),
    { toFun := toFun, map_inf' := map_inf', idempotent' := idempotent', le_apply' := le_apply' : Nucleus X } = g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n m : Nucleus X
x y : X
g : Nucleus X
toFun : X → X
map_inf' : ∀ (a b : X), toFun (a ⊓ b) = toFun a ⊓ toFun b
idempotent' :
  ∀ (x : X),
    { toFun := toFun, map_inf' := map_inf' : InfHom X X }.toFun
        ({ toFun := toFun, map_inf' := map_inf' : InfHom X X }.toFun x) ≤
      { toFun := toFun, map_inf' := map_inf' : InfHom X X }.toFun x
le_apply' : ∀ (x : X), x ≤ { toFun := toFun, map_inf' := map_inf' : InfHom X X }.toFun x
h :
  Eq.{u_1 + 1} (α := (a : X) → X)
    ((fun (x : Nucleus X) ↦ x.toFun)
      { toFun := toFun, map_inf' := map_inf', idempotent' := idempotent', le_apply' := le_apply' })
    ((fun (x : Nucleus X) ↦ x.toFun) g)
⊢ { toFun := toFun, map_inf' := map_inf', idempotent' := idempotent', le_apply' := le_apply' : Nucleus X } = g

Tactic:
congr!
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n : Nucleus X
⊢ n.toFun = (⇑n : (a : X) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n : Nucleus X
⊢ Eq (α := (a : X) → X) (⇑n.toInfHom : (a : X) → X) (⇑n : (a : X) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
f : InfHom X X
h1 : ∀ (x : X), f.toFun (f.toFun x) ≤ f.toFun x
h2 : ∀ (x : X), x ≤ f.toFun x
⊢ Eq (α := (a : X) → X) (⇑{ toInfHom := f, idempotent' := h1, le_apply' := h2 : Nucleus X } : (a : X) → X)
    (⇑f : (a : X) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n : Nucleus X
x : X
⊢ Eq (α := X) ((n : (a : X) → X) ((n : (a : X) → X) x : X) : X) ((n : (a : X) → X) x : X)

Tactic:
n.toClosureOperator.idempotent x

Premises used: Nucleus.toClosureOperator, ClosureOperator.idempotent
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n : Nucleus X
x : X
⊢ x ≤ (n : (a : X) → X) x

Tactic:
n.toClosureOperator.le_closure x

Premises used: ClosureOperator.le_closure, Nucleus.toClosureOperator
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n : Nucleus X
⊢ Monotone (α := X) (β := X) (⇑n : (a : X) → X)

Tactic:
n.toClosureOperator.monotone

Premises used: Nucleus.toClosureOperator, ClosureOperator.monotone
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n : Nucleus X
x y : X
⊢ Eq (α := X) ((n : (a : X) → X) (x ⊓ y) : X) ((n : (a : X) → X) x ⊓ (n : (a : X) → X) y : X)

Tactic:
InfHomClass.map_inf n x y

Premises used: InfHomClass.map_inf
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
m n : Nucleus X
h : ∀ (a : X), Eq (α := X) ((m : (a : X) → X) a : X) ((n : (a : X) → X) a : X)
⊢ m = n

Tactic:
DFunLike.ext m n h

Premises used: DFunLike.ext
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n m : Nucleus X
⊢ LE.le (α := (a : X) → X) (⇑m : (a : X) → X) (⇑n : (a : X) → X) ↔ m ≤ n

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n m : Nucleus X
⊢ LT.lt (α := (a : X) → X) (⇑m : (a : X) → X) (⇑n : (a : X) → X) ↔ m < n

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
toInfHom₁ toInfHom₂ : InfHom X X
le_apply₁ : ∀ (x : X), toInfHom₁.toFun (toInfHom₁.toFun x) ≤ toInfHom₁.toFun x
le_apply₂ : ∀ (x : X), toInfHom₂.toFun (toInfHom₂.toFun x) ≤ toInfHom₂.toFun x
idempotent₁ : ∀ (x : X), x ≤ toInfHom₁.toFun x
idempotent₂ : ∀ (x : X), x ≤ toInfHom₂.toFun x
⊢ { toInfHom := toInfHom₁, idempotent' := le_apply₁, le_apply' := idempotent₁ : Nucleus X } ≤
      { toInfHom := toInfHom₂, idempotent' := le_apply₂, le_apply' := idempotent₂ } ↔
    toInfHom₁ ≤ toInfHom₂

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n_1 m_1 : Nucleus X
x_1 y_1 : X
m n : Nucleus X
x y : X
⊢ Eq (α := X) (((⇑m : (a : X) → X) ⊓ (⇑n : (a : X) → X)) (x ⊓ y) : X)
    (((⇑m : (a : X) → X) ⊓ (⇑n : (a : X) → X)) x ⊓ ((⇑m : (a : X) → X) ⊓ (⇑n : (a : X) → X)) y : X)

Tactic:
simp [inf_inf_inf_comm]

Premises used: inf_inf_inf_comm
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n_1 m_1 : Nucleus X
x_1 y : X
m n : Nucleus X
x : X
simp :
  LE.le (α := X)
    ((m : (a : X) → X) x ⊓ (m : (a : X) → X) ((n : (a : X) → X) x : X) ⊓
        ((n : (a : X) → X) ((m : (a : X) → X) x : X) ⊓ (n : (a : X) → X) x) :
      X)
    ((m : (a : X) → X) x ⊓ (n : (a : X) → X) x : X)
⊢ LE.le (α := X) (((⇑m : (a : X) → X) ⊓ (⇑n : (a : X) → X)) (((⇑m : (a : X) → X) ⊓ (⇑n : (a : X) → X)) x) : X)
    (((⇑m : (a : X) → X) ⊓ (⇑n : (a : X) → X)) x : X)

Tactic:
simp only [Pi.inf_apply, map_inf, idempotent]

Premises used: Nucleus.idempotent, Nucleus.map_inf, Pi.inf_apply
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n_1 m_1 : Nucleus X
x_1 y : X
m n : Nucleus X
x : X
⊢ LE.le (α := X)
    ((m : (a : X) → X) x ⊓ (m : (a : X) → X) ((n : (a : X) → X) x : X) ⊓
        ((n : (a : X) → X) ((m : (a : X) → X) x : X) ⊓ (n : (a : X) → X) x) :
      X)
    ((m : (a : X) → X) x ⊓ (n : (a : X) → X) x : X)

Tactic:
inf_le_inf inf_le_left inf_le_right

Premises used: inf_le_inf, inf_le_right, inf_le_left
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n_1 m_1 : Nucleus X
x_1 y : X
m n : Nucleus X
x : X
⊢ LE.le (α := X)
    ((m : (a : X) → X) x ⊓ (m : (a : X) → X) ((n : (a : X) → X) x : X) ⊓
        ((n : (a : X) → X) ((m : (a : X) → X) x : X) ⊓ (n : (a : X) → X) x) :
      X)
    ((m : (a : X) → X) x ⊓ (n : (a : X) → X) x : X)

Tactic:
exact inf_le_inf inf_le_left inf_le_right

Premises used: inf_le_inf, inf_le_right, inf_le_left
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
m n : Nucleus X
⊢ Eq (α := (a : X) → X) (⇑(m ⊓ n) : (a : X) → X) ((⇑m : (a : X) → X) ⊓ (⇑n : (a : X) → X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
m n : Nucleus X
x : X
⊢ Eq (α := X) ((m ⊓ n : (a : X) → X) x : X) ((m : (a : X) → X) x ⊓ (n : (a : X) → X) x : X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Nucleus
Goal:
X : Type u_1
inst : SemilatticeInf X
n m : Nucleus X
x y : X
⊢ ∀ (a b : X), a ⊓ b = a ⊓ b

Tactic:
simp