awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ (((LT.lt (α := Fin n.succ) 0 0 → Eq (α := α 0) (cons (α := α) x₀ x 0) (cons (α := α) y₀ y 0)) ∧
          ∀ (i : Fin n), i.succ < 0 → Eq (α := α i.succ) (cons (α := α) x₀ x i.succ) (cons (α := α) y₀ y i.succ)) ∧
        s x₀ y₀ ∨
      ∃ (i : Fin n),
        ((0 < i.succ → Eq (α := α 0) (cons (α := α) x₀ x 0) (cons (α := α) y₀ y 0)) ∧
            ∀ (i_1 : Fin n),
              i_1.succ < i.succ → Eq (α := α i_1.succ) (cons (α := α) x₀ x i_1.succ) (cons (α := α) y₀ y i_1.succ)) ∧
          s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ (i : Fin n), (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)

Tactic:
simp [and_assoc, exists_and_left]

Premises used: exists_and_left, and_assoc
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
inst : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q₁ q₂ : (j : Fin (n + 1)) → α j
⊢ i.insertNth (α := α) x p ∈ Icc q₁ q₂ ↔
    x ∈ Icc (q₁ i) (q₂ i) ∧
      Membership.mem (γ := Set ((j : Fin n) → α (i.succAbove j)))
        (Icc (fun (j : Fin n) ↦ q₁ (i.succAbove j)) fun (j : Fin n) ↦ q₂ (i.succAbove j)) p

Tactic:
simp only [mem_Icc, insertNth_le_iff, le_insertNth_iff, and_assoc, @and_left_comm (x ≤ q₂ i)]

Premises used: Fin.insertNth_le_iff, and_left_comm, and_assoc, Set.mem_Icc, Fin.le_insertNth_iff
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
inst : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
q₁ q₂ : (j : Fin (n + 1)) → α j
hx : x ∈ Icc (q₁ i) (q₂ i)
p : (j : Fin n) → α (i.succAbove j)
⊢ p ∈ i.insertNth (α := α) x ⁻¹' Icc q₁ q₂ ↔
    Membership.mem (γ := Set ((j : Fin n) → α (i.succAbove j)))
      (Icc (fun (j : Fin n) ↦ q₁ (i.succAbove j)) fun (j : Fin n) ↦ q₂ (i.succAbove j)) p

Tactic:
simp only [mem_preimage, insertNth_mem_Icc, hx, true_and]

Premises used: Fin.insertNth_mem_Icc, Set.mem_preimage, true_and
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
inst : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
q₁ q₂ : (j : Fin (n + 1)) → α j
hx : ¬x ∈ Icc (q₁ i) (q₂ i)
p : (j : Fin n) → α (i.succAbove j)
⊢ p ∈ i.insertNth (α := α) x ⁻¹' Icc q₁ q₂ ↔ Membership.mem (γ := Set ((j : Fin n) → α (i.succAbove j))) ∅ p

Tactic:
simp only [mem_preimage, insertNth_mem_Icc, hx, false_and, mem_empty_iff_false]

Premises used: false_and, Fin.insertNth_mem_Icc, Set.mem_empty_iff_false, Set.mem_preimage
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
r : α → α → Prop
inst : IsTrans α r
f : Fin (n + 1) → α
a : α
⊢ ((fun (x1 x2 : Fin (n + 1).succ) ↦ x1 < x2) ⇒ r) (vecCons a f) (vecCons a f) ↔
    r a (f 0) ∧ ((fun (x1 x2 : Fin (n + 1)) ↦ x1 < x2) ⇒ r) f f

Tactic:
simp only [liftFun_iff_succ r, forall_iff_succ, cons_val_succ, cons_val_zero, ← succ_castSucc,
    castSucc_zero]

Premises used: Fin.liftFun_iff_succ, Matrix.cons_val_zero, Matrix.cons_val_succ, Fin.forall_iff_succ, Fin.castSucc_zero, Fin.succ_castSucc
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
⊢ StrictMono (vecCons a f) ↔ a < f 0 ∧ StrictMono f

Tactic:
liftFun_vecCons (· < ·)

Premises used: StrictMono, liftFun_vecCons, LT.lt
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
⊢ Monotone (vecCons a f) ↔ a ≤ f 0 ∧ Monotone f

Tactic:
simpa only [monotone_iff_forall_lt] using @liftFun_vecCons α n (· ≤ ·) _ f a

Premises used: LE.le, liftFun_vecCons, monotone_iff_forall_lt
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
⊢ StrictAnti (vecCons a f) ↔ f 0 < a ∧ StrictAnti f

Tactic:
liftFun_vecCons (· > ·)

Premises used: liftFun_vecCons, GT.gt, StrictAnti
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
⊢ Antitone (vecCons a f) ↔ f 0 ≤ a ∧ Antitone f

Tactic:
monotone_vecCons (α := αᵒᵈ)

Premises used: Antitone, OrderDual, monotone_vecCons
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
hf : StrictMono f
ha : a < f 0
⊢ StrictMono (Matrix.vecCons a f)

Tactic:
strictMono_vecCons.2 ⟨ha, hf⟩

Premises used: Iff.mpr, And.intro, strictMono_vecCons
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
hf : StrictAnti f
ha : f 0 < a
⊢ StrictAnti (Matrix.vecCons a f)

Tactic:
strictAnti_vecCons.2 ⟨ha, hf⟩

Premises used: Iff.mpr, And.intro, strictAnti_vecCons
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
hf : Monotone f
ha : a ≤ f 0
⊢ Monotone (Matrix.vecCons a f)

Tactic:
monotone_vecCons.2 ⟨ha, hf⟩

Premises used: Iff.mpr, And.intro, monotone_vecCons
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
hf : Antitone f
ha : f 0 ≤ a
⊢ Antitone (Matrix.vecCons a f)

Tactic:
antitone_vecCons.2 ⟨ha, hf⟩

Premises used: Iff.mpr, antitone_vecCons, And.intro
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
⊢ Monotone (β := ℕ) ![1, 2, 2, 3]

Tactic:
decide
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α_1 : Type u_1
inst : Preorder α_1
n_1 : ℕ
f : Fin (n_1 + 1) → α_1
a : α_1
n : ℕ
α : Fin (n + 1) → Type u_2
inst_1 : (i : Fin (n + 1)) → LE (α i)
⊢ ∀ {a b : α (last n) × ((i : Fin n) → α i.castSucc)},
    LE.le (α := (i : Fin (n + 1)) → α i)
        ((snocEquiv α : (a : α (last n) × ((i : Fin n) → α i.castSucc)) → (i : Fin (n + 1)) → α i) a :
          (i : Fin (n + 1)) → α i)
        ((snocEquiv α : (a : α (last n) × ((i : Fin n) → α i.castSucc)) → (i : Fin (n + 1)) → α i) b :
          (i : Fin (n + 1)) → α i) ↔
      a ≤ b

Tactic:
simp [Pi.le_def, Prod.le_def, forall_iff_castSucc]

Premises used: Fin.forall_iff_castSucc, Pi.le_def, Prod.le_def
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α_1 : Type u_1
inst : Preorder α_1
n_1 : ℕ
f : Fin (n_1 + 1) → α_1
a : α_1
n : ℕ
α : Fin (n + 1) → Type u_2
inst_1 : (i : Fin (n + 1)) → LE (α i)
p : Fin (n + 1)
⊢ ∀ {a b : α p × ((i : Fin n) → α (p.succAbove i))},
    LE.le (α := (i : Fin (n + 1)) → α i)
        ((insertNthEquiv α p : (a : α p × ((i : Fin n) → α (p.succAbove i))) → (i : Fin (n + 1)) → α i) a :
          (i : Fin (n + 1)) → α i)
        ((insertNthEquiv α p : (a : α p × ((i : Fin n) → α (p.succAbove i))) → (i : Fin (n + 1)) → α i) b :
          (i : Fin (n + 1)) → α i) ↔
      a ≤ b

Tactic:
simp [Pi.le_def, Prod.le_def, p.forall_iff_succAbove]

Premises used: Pi.le_def, Fin.forall_iff_succAbove, Prod.le_def
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
α : Fin (n + 1) → Type u_2
inst : (i : Fin (n + 1)) → LE (α i)
h :
  ∀ (x : α 0 × ((i : Fin n) → α (succAbove 0 i))) (x_1 : Fin (n + 1)),
    Eq (α := α x_1)
      ((insertNthOrderIso α 0 : (a : α 0 × ((i : Fin n) → α (succAbove 0 i))) → (i : Fin (n + 1)) → α i) x x_1 : α x_1)
      ((consOrderIso α : (a : α 0 × ((i : Fin n) → α (succAbove 0 i))) → (i : Fin (n + 1)) → α i) x x_1 : α x_1)
⊢ Eq (α := α 0 × ((i : Fin n) → α (succAbove 0 i)) ≃o ((i : Fin (n + 1)) → α i)) (insertNthOrderIso α 0)
    (consOrderIso α)

Tactic:
ext
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
α : Fin (n + 1) → Type u_2
inst : (i : Fin (n + 1)) → LE (α i)
x : α 0 × ((i : Fin n) → α (succAbove 0 i))
x_1 : Fin (n + 1)
⊢ Eq (α := α x_1)
    ((insertNthOrderIso α 0 : (a : α 0 × ((i : Fin n) → α (succAbove 0 i))) → (i : Fin (n + 1)) → α i) x x_1 : α x_1)
    ((consOrderIso α : (a : α 0 × ((i : Fin n) → α (succAbove 0 i))) → (i : Fin (n + 1)) → α i) x x_1 : α x_1)

Tactic:
simp [insertNthOrderIso]

Premises used: Fin.insertNthOrderIso
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
α : Type u_2
inst : LE α
h :
  ∀ (x : α × ((i : Fin n) → α)) (x_1 : Fin (n + 1)),
    Eq (α := α)
      (((insertNthOrderIso.{u_2} (fun (x : Fin (n + 1)) ↦ α) (last n) :
              α × ((i : Fin n) → α) ≃o ((i : Fin (n + 1)) → α)) :
            (a : α × ((i : Fin n) → α)) → (i : Fin (n + 1)) → α)
          x x_1 :
        α)
      (((snocOrderIso.{u_2} (n := n) fun (x : Fin (n + 1)) ↦ α : α × ((i : Fin n) → α) ≃o ((i : Fin (n + 1)) → α)) :
            (a : α × ((i : Fin n) → α)) → (i : Fin (n + 1)) → α)
          x x_1 :
        α)
⊢ Eq.{u_2 + 1} (α := α × ((i : Fin n) → α) ≃o ((i : Fin (n + 1)) → α))
    (insertNthOrderIso.{u_2} (fun (x : Fin (n + 1)) ↦ α) (last n) : α × ((i : Fin n) → α) ≃o ((i : Fin (n + 1)) → α))
    (snocOrderIso.{u_2} (n := n) fun (x : Fin (n + 1)) ↦ α : α × ((i : Fin n) → α) ≃o ((i : Fin (n + 1)) → α))

Tactic:
ext
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
α : Type u_2
inst : LE α
x : α × ((i : Fin n) → α)
x_1 : Fin (n + 1)
⊢ Eq (α := α)
    (((insertNthOrderIso.{u_2} (fun (x : Fin (n + 1)) ↦ α) (last n) :
            α × ((i : Fin n) → α) ≃o ((i : Fin (n + 1)) → α)) :
          (a : α × ((i : Fin n) → α)) → (i : Fin (n + 1)) → α)
        x x_1 :
      α)
    (((snocOrderIso.{u_2} (n := n) fun (x : Fin (n + 1)) ↦ α : α × ((i : Fin n) → α) ≃o ((i : Fin (n + 1)) → α)) :
          (a : α × ((i : Fin n) → α)) → (i : Fin (n + 1)) → α)
        x x_1 :
      α)

Tactic:
simp
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ Eq (α := { x : Fin (n + 1) // x ≠ p })
    ((finSuccAboveOrderIso p : (a : Fin n) → { x : Fin (n + 1) // x ≠ p }) i : { x : Fin (n + 1) // x ≠ p })
    (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ≠ p) (p.succAbove i) ⋯ : { x : Fin (n + 1) // x ≠ p })

Tactic:
rfl

Premises used: Fin.succAbove, Option.casesOn', rfl, ite
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
x : { x : Fin (n + 1) // x ≠ last n }
rw :
  some (((finSuccAboveOrderIso (last n)).symm : (a : { x : Fin (n + 1) // x ≠ last n }) → Fin n) x) =
    some ((↑x : Fin (n + 1)).castLT ⋯)
⊢ ((finSuccAboveOrderIso (last n)).symm : (a : { x : Fin (n + 1) // x ≠ last n }) → Fin n) x =
    (↑x : Fin (n + 1)).castLT ⋯

Tactic:
rw [← Option.some_inj]

Premises used: Option.some_inj
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
x : { x : Fin (n + 1) // x ≠ last n }
⊢ some (((finSuccAboveOrderIso (last n)).symm : (a : { x : Fin (n + 1) // x ≠ last n }) → Fin n) x) =
    some ((↑x : Fin (n + 1)).castLT ⋯)

Tactic:
simp [finSuccAboveOrderIso, finSuccAboveEquiv, OrderIso.symm]

Premises used: OrderIso.symm, finSuccAboveEquiv, finSuccAboveOrderIso
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
p : Fin (n + 1)
h : p ≠ last n
x : { x : Fin (n + 1) // x ≠ p }
rw :
  some (((finSuccAboveEquiv p).symm : (a : { x : Fin (n + 1) // x ≠ p }) → Fin n) x) =
    some ((p.castLT ⋯).predAbove (↑x : Fin (n + 1)))
⊢ ((finSuccAboveEquiv p).symm : (a : { x : Fin (n + 1) // x ≠ p }) → Fin n) x =
    (p.castLT ⋯).predAbove (↑x : Fin (n + 1))

Tactic:
rw [← Option.some_inj]

Premises used: Option.some_inj
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
p : Fin (n + 1)
h : p ≠ last n
x : { x : Fin (n + 1) // x ≠ p }
⊢ some (((finSuccAboveEquiv p).symm : (a : { x : Fin (n + 1) // x ≠ p }) → Fin n) x) =
    some ((p.castLT ⋯).predAbove (↑x : Fin (n + 1)))

Tactic:
simpa [finSuccAboveEquiv, OrderIso.symm] using finSuccEquiv'_ne_last_apply h x.property

Premises used: finSuccEquiv'_ne_last_apply, OrderIso.symm, finSuccAboveEquiv, Subtype.property
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n_1 : ℕ
f : Fin (n_1 + 1) → α
a : α
n_2 n m : ℕ
h : n ≤ m
i : Fin n
⊢ (↑(castLE h i) : ℕ) < n

Tactic:
simp
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n_1 : ℕ
f : Fin (n_1 + 1) → α
a : α
n_2 n m : ℕ
h : n ≤ m
x : Fin n
⊢ (fun (i : { i : Fin m // (↑i : ℕ) < n }) ↦ (⟨(↑(↑i : Fin m) : ℕ), ⋯⟩ : Fin n))
      ((fun (i : Fin n) ↦
          (Subtype.mk (p := fun (i : Fin m) ↦ (↑i : ℕ) < n) (castLE h i) ⋯ : { i : Fin m // (↑i : ℕ) < n }))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n_1 : ℕ
f : Fin (n_1 + 1) → α
a : α
n_2 n m : ℕ
h : n ≤ m
x : { i : Fin m // (↑i : ℕ) < n }
⊢ (fun (i : Fin n) ↦ (Subtype.mk (p := fun (i : Fin m) ↦ (↑i : ℕ) < n) (castLE h i) ⋯ : { i : Fin m // (↑i : ℕ) < n }))
      ((fun (i : { i : Fin m // (↑i : ℕ) < n }) ↦ (⟨(↑(↑i : Fin m) : ℕ), ⋯⟩ : Fin n)) x) =
    x

Tactic:
simp
-- Module: Mathlib.Order.Fin.Tuple
Goal:
α : Type u_1
inst : Preorder α
n_1 : ℕ
f : Fin (n_1 + 1) → α
a : α
n_2 n m : ℕ
h : n ≤ m
⊢ ∀ {a b : Fin n},
    LE.le (α := { i : Fin m // (↑i : ℕ) < n })
        (({ toFun := fun (i : Fin n) ↦ Subtype.mk (p := fun (i : Fin m) ↦ (↑i : ℕ) < n) (castLE h i) ⋯,
                invFun := fun (i : { i : Fin m // (↑i : ℕ) < n }) ↦ ⟨(↑(↑i : Fin m) : ℕ), ⋯⟩, left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Fin n) → { i : Fin m // (↑i : ℕ) < n })
            a :
          { i : Fin m // (↑i : ℕ) < n })
        (({ toFun := fun (i : Fin n) ↦ Subtype.mk (p := fun (i : Fin m) ↦ (↑i : ℕ) < n) (castLE h i) ⋯,
                invFun := fun (i : { i : Fin m // (↑i : ℕ) < n }) ↦ ⟨(↑(↑i : Fin m) : ℕ), ⋯⟩, left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Fin n) → { i : Fin m // (↑i : ℕ) < n })
            b :
          { i : Fin m // (↑i : ℕ) < n }) ↔
      a ≤ b

Tactic:
simp [(strictMono_castLE h).le_iff_le]

Premises used: Fin.strictMono_castLE, StrictMono.le_iff_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
a : α
h : (f : (a : α) → α) a ≤ a
⊢ (lfp : (a : α →o α) → α) f ≤ a

Tactic:
sInf_le h

Premises used: sInf_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
a : α
h : (f : (a : α) → α) a = a
⊢ (lfp : (a : α →o α) → α) f ≤ a

Tactic:
f.lfp_le h.le

Premises used: Eq.le, OrderHom.lfp_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
a : α
h : ∀ (b : α), (f : (a : α) → α) b ≤ b → a ≤ b
⊢ a ≤ (lfp : (a : α →o α) → α) f

Tactic:
le_sInf h

Premises used: le_sInf
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
a : α
ha : a ≤ (lfp : (a : α →o α) → α) f
⊢ LE.le (α := α) ((f : (a : α) → α) a : α) ((lfp : (a : α →o α) → α) f : α)

Tactic:
f.le_lfp fun _ hb => (f.mono <| le_sInf_iff.1 ha _ hb).trans hb

Premises used: le_sInf_iff, OrderHom.le_lfp, OrderHom.mono, Iff.mp, LE.le.trans
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ Eq (α := α) ((f : (a : α) → α) ((lfp : (a : α →o α) → α) f : α) : α) ((lfp : (a : α →o α) → α) f : α)

Tactic:
have h : f f.lfp ≤ f.lfp := f.map_le_lfp le_rfl
  h.antisymm <| f.lfp_le <| f.mono h

Premises used: le_rfl, LE.le.antisymm, OrderHom.map_le_lfp, OrderHom.mono, OrderHom.lfp_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ IsFixedPt (α := α) ((⇑f : (a : α) → α) : (a : α) → α) ((lfp : (a : α →o α) → α) f : α)

Tactic:
f.map_lfp

Premises used: OrderHom.map_lfp, Function.IsFixedPt
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
a : α
ha : (lfp : (a : α →o α) → α) f ≤ a
⊢ LE.le (α := α) ((lfp : (a : α →o α) → α) f : α) ((f : (a : α) → α) a : α)

Tactic:
calc
    f.lfp = f f.lfp := f.map_lfp.symm
    _ ≤ f a := f.mono ha

Premises used: Trans.trans, OrderHom.map_lfp, OrderHom.mono, Eq.symm
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ IsLeast (α := α) ({a : α | (f : (a : α) → α) a ≤ a} : Set α) ((lfp : (a : α →o α) → α) f : α)

Tactic:
⟨f.map_lfp.le, fun _ => f.lfp_le⟩

Premises used: OrderHom.map_lfp, Eq.le, IsLeast, And.intro, OrderHom.lfp_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ IsLeast (α := α) (fixedPoints (⇑f : (a : α) → α) : Set α) ((lfp : (a : α →o α) → α) f : α)

Tactic:
⟨f.isFixedPt_lfp, fun _ => f.lfp_le_fixed⟩

Premises used: OrderHom.isFixedPt_lfp, IsLeast, And.intro, OrderHom.lfp_le_fixed
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ (lfp : (a : α →o α) → α) f → p ((f : (a : α) → α) a)
hSup : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sSup s)
s : Set α := {a : α | a ≤ (lfp : (a : α →o α) → α) f ∧ p a}
⊢ p (sSup s)

Tactic:
specialize hSup s fun a => And.right

Premises used: And.right
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ (lfp : (a : α →o α) → α) f → p ((f : (a : α) → α) a)
s : Set α := {a : α | a ≤ (lfp : (a : α →o α) → α) f ∧ p a}
hSup : p (sSup s)
suffices : sSup s = (lfp : (a : α →o α) → α) f
⊢ p ((lfp : (a : α →o α) → α) f)

Tactic:
suffices sSup s = f.lfp from this ▸ hSup
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ (lfp : (a : α →o α) → α) f → p ((f : (a : α) → α) a)
s : Set α := {a : α | a ≤ (lfp : (a : α →o α) → α) f ∧ p a}
hSup : p (sSup s)
⊢ sSup s ≤ (lfp : (a : α →o α) → α) f

Tactic:
have h : sSup s ≤ f.lfp := sSup_le fun b => And.left
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ (lfp : (a : α →o α) → α) f → p ((f : (a : α) → α) a)
s : Set α := {a : α | a ≤ (lfp : (a : α →o α) → α) f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ (lfp : (a : α →o α) → α) f
⊢ Membership.mem (α := α) s ((f : (a : α) → α) (sSup s) : α)

Tactic:
have hmem : f (sSup s) ∈ s := ⟨f.map_le_lfp h, step _ hSup h⟩
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ (lfp : (a : α →o α) → α) f → p ((f : (a : α) → α) a)
s : Set α := {a : α | a ≤ (lfp : (a : α →o α) → α) f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ (lfp : (a : α →o α) → α) f
hmem : Membership.mem (α := α) s ((f : (a : α) → α) (sSup s) : α)
⊢ sSup s = (lfp : (a : α →o α) → α) f

Tactic:
h.antisymm (f.lfp_le <| le_sSup hmem)

Premises used: LE.le.antisymm, le_sSup, OrderHom.lfp_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ (lfp : (a : α →o α) → α) f → p ((f : (a : α) → α) a)
s : Set α := {a : α | a ≤ (lfp : (a : α →o α) → α) f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ (lfp : (a : α →o α) → α) f
hmem : Membership.mem (α := α) s ((f : (a : α) → α) (sSup s) : α)
⊢ sSup s = (lfp : (a : α →o α) → α) f

Tactic:
exact h.antisymm (f.lfp_le <| le_sSup hmem)

Premises used: LE.le.antisymm, le_sSup, OrderHom.lfp_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
a : α
h : a ≤ (f : (a : α) → α) a
⊢ a ≤ (gfp : (a : α →o α) → α) f

Tactic:
le_sSup h

Premises used: le_sSup
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
a : α
h : ∀ b ≤ (f : (a : α) → α) b, b ≤ a
⊢ (gfp : (a : α →o α) → α) f ≤ a

Tactic:
sSup_le h

Premises used: sSup_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ IsFixedPt (α := α) ((⇑f : (a : α) → α) : (a : α) → α) ((gfp : (a : α →o α) → α) f : α)

Tactic:
f.dual.isFixedPt_lfp

Premises used: setOf, OrderHom.isFixedPt_lfp, OrderDual, OrderHom.dual, DFunLike.coe
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ Eq (α := α) ((f : (a : α) → α) ((gfp : (a : α →o α) → α) f : α) : α) ((gfp : (a : α →o α) → α) f : α)

Tactic:
f.dual.map_lfp

Premises used: OrderHom.map_lfp, setOf, OrderDual, OrderHom.dual, DFunLike.coe
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
a : α
ha : a ≤ (gfp : (a : α →o α) → α) f
⊢ LE.le (α := α) ((f : (a : α) → α) a : α) ((gfp : (a : α →o α) → α) f : α)

Tactic:
f.dual.lfp_le_map ha

Premises used: setOf, OrderDual, OrderHom.dual, DFunLike.coe, OrderHom.lfp_le_map
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
a : α
ha : (gfp : (a : α →o α) → α) f ≤ a
⊢ LE.le (α := α) ((gfp : (a : α →o α) → α) f : α) ((f : (a : α) → α) a : α)

Tactic:
f.dual.map_le_lfp ha

Premises used: setOf, OrderHom.map_le_lfp, OrderDual, OrderHom.dual, DFunLike.coe
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ IsGreatest (α := α) ({a : α | a ≤ (f : (a : α) → α) a} : Set α) ((gfp : (a : α →o α) → α) f : α)

Tactic:
f.dual.isLeast_lfp_le

Premises used: Set.Mem, setOf, upperBounds, IsGreatest, OrderDual, OrderHom.dual, DFunLike.coe, OrderHom.isLeast_lfp_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ IsGreatest (α := α) (fixedPoints (⇑f : (a : α) → α) : Set α) ((gfp : (a : α →o α) → α) f : α)

Tactic:
f.dual.isLeast_lfp

Premises used: Set.Mem, setOf, OrderHom.isLeast_lfp, upperBounds, IsGreatest, OrderDual, OrderHom.dual, DFunLike.coe
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → (gfp : (a : α →o α) → α) f ≤ a → p ((f : (a : α) → α) a)
hInf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)
⊢ p ((gfp : (a : α →o α) → α) f)

Tactic:
f.dual.lfp_induction step hInf

Premises used: OrderHom.lfp_induction, setOf, OrderDual, OrderHom.dual, DFunLike.coe
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ LE.le (α := α) ((lfp : (a : α →o α) → α) f : α) ((gfp : (a : α →o α) → α) f : α)

Tactic:
f.lfp_le_fixed f.isFixedPt_gfp

Premises used: OrderHom.isFixedPt_gfp, OrderHom.lfp_le_fixed
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
β : Type v
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : β →o α
g : α →o β
⊢ Eq.{u + 1} (α := α) ((f : (a : β) → α) ((lfp : (a : β →o β) → β) (g.comp f) : β) : α)
    ((lfp : (a : α →o α) → α) (f.comp g) : α)

Tactic:
le_antisymm ((f.comp g).map_lfp ▸ f.mono (lfp_le_fixed _ <| congr_arg g (f.comp g).map_lfp)) <|
    lfp_le _ (congr_arg f (g.comp f).map_lfp).le

Premises used: OrderHom.map_lfp, OrderHom.comp, Eq.le, congr_arg, le_antisymm, OrderHom.lfp_le, DFunLike.coe
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
β : Type v
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : β →o α
g : α →o β
⊢ Eq.{u + 1} (α := α) ((f : (a : β) → α) ((gfp : (a : β →o β) → β) (g.comp f) : β) : α)
    ((gfp : (a : α →o α) → α) (f.comp g) : α)

Tactic:
f.dual.map_lfp_comp g.dual

Premises used: setOf, OrderDual, OrderHom.dual, DFunLike.coe, OrderHom.map_lfp_comp
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
a : α := (lfp : (a : α →o α) → α) (comp lfp h)
⊢ Eq (α := α) ((lfp : (a : α →o α) → α) (comp lfp h) : α) ((lfp : (a : α →o α) → α) h.onDiag : α)

Tactic:
(lfp_le _ ?_).antisymm (lfp_le _ (Eq.le ?_))

Premises used: LE.le.antisymm, Eq.le, OrderHom.lfp_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
a : α := (lfp : (a : α →o α) → α) (comp lfp h)
refine_1 :
  LE.le (α := α) ((comp lfp h : (a : α) → α) ((lfp : (a : α →o α) → α) h.onDiag : α) : α)
    ((lfp : (a : α →o α) → α) h.onDiag : α)
refine_2 :
  Eq (α := α) ((h.onDiag : (a : α) → α) ((lfp : (a : α →o α) → α) (comp lfp h) : α) : α)
    ((lfp : (a : α →o α) → α) (comp lfp h) : α)
⊢ Eq (α := α) ((lfp : (a : α →o α) → α) (comp lfp h) : α) ((lfp : (a : α →o α) → α) h.onDiag : α)

Tactic:
refine (lfp_le _ ?_).antisymm (lfp_le _ (Eq.le ?_))

Premises used: LE.le.antisymm, Eq.le, OrderHom.lfp_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
a : α := (lfp : (a : α →o α) → α) (comp lfp h)
⊢ LE.le (α := α) ((comp lfp h : (a : α) → α) ((lfp : (a : α →o α) → α) h.onDiag : α) : α)
    ((lfp : (a : α →o α) → α) h.onDiag : α)

Tactic:
lfp_le _ h.onDiag.map_lfp.le

Premises used: OrderHom.onDiag, OrderHom.map_lfp, Eq.le, OrderHom.lfp_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
a : α := (lfp : (a : α →o α) → α) (comp lfp h)
⊢ LE.le (α := α) ((comp lfp h : (a : α) → α) ((lfp : (a : α →o α) → α) h.onDiag : α) : α)
    ((lfp : (a : α →o α) → α) h.onDiag : α)

Tactic:
exact lfp_le _ h.onDiag.map_lfp.le

Premises used: OrderHom.onDiag, OrderHom.map_lfp, Eq.le, OrderHom.lfp_le