awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
ι : Sort u_3
inst_1 : CompleteLattice β
f : ι → α →o β
x : α
⊢ Eq.{u_2 + 1} (α := β) ((⨆ (i : ι), f i : (a : α) → β) x : β) ((⨆ (i : ι), (⇑(f i) : (a : α) → β)) x : β)

Tactic:
simp [iSup_apply]

Premises used: OrderHom.iSup_apply
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : CompleteLattice β
x : Set (α →o β)
⊢ IsLUB (α := (a : α) → β) (DFunLike.coe (β := fun (x : α) ↦ β) '' x) (⇑(sSup x) : (a : α) → β)

Tactic:
simp [isLUB_pi, Set.image_image, isLUB_biSup]

Premises used: Set.image_image, isLUB_biSup, isLUB_pi
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : CompleteLattice β
x : Set (α →o β)
⊢ IsGLB (α := (a : α) → β) (DFunLike.coe (β := fun (x : α) ↦ β) '' x) (⇑(sInf x) : (a : α) → β)

Tactic:
simp [isGLB_pi, Set.image_image, isGLB_biInf]

Premises used: Set.image_image, isGLB_biInf, isGLB_pi
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
mp :
  (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α),
      (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂) →
    ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
mpr :
  (∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)) →
    ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α),
      (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂
⊢ (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α),
      (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂) ↔
    ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)

Tactic:
constructor
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h :
  ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α),
    (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂
⊢ ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)

Tactic:
h 1 0

Premises used: Nat.iterate, OfNat.ofNat
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h :
  ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α),
    (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂
⊢ ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)

Tactic:
exact h 1 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁_1 a₂_1 a₁ a₂ : α
⊢ (⇑f : (a : α) → α)^[0] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[0] (a₁ ⊔ a₂)

Tactic:
rfl
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁_1 a₂_1 : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ (⇑f : (a : α) → α)^[n + 1] (a₁ ⊔ a₂) = (⇑f : (a : α) → α)^[n] ((f : (a : α) → α) (a₁ ⊔ a₂))

Tactic:
Function.iterate_succ_apply f n _

Premises used: Function.iterate_succ_apply, DFunLike.coe
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁_1 a₂_1 : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ LE.le (α := α) ((⇑f : (a : α) → α)^[n] ((f : (a : α) → α) (a₁ ⊔ a₂)) : α)
    ((⇑f : (a : α) → α)^[n] ((f : (a : α) → α) a₁ ⊔ a₂) : α)

Tactic:
f.mono.iterate n (h a₁ a₂)

Premises used: Monotone.iterate, OrderHom.mono
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁_1 a₂_1 : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ LE.le (α := α) ((⇑f : (a : α) → α)^[n] ((f : (a : α) → α) a₁ ⊔ a₂) : α)
    ((⇑f : (a : α) → α)^[n] ((f : (a : α) → α) a₁) ⊔ a₂ : α)

Tactic:
ih _ _
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁_1 a₂_1 : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
a₁ a₂ : α
rw rw₁ : (⇑f : (a : α) → α)^[n.succ] a₁ ⊔ a₂ = (⇑f : (a : α) → α)^[n + 1] a₁ ⊔ a₂
⊢ (⇑f : (a : α) → α)^[n] ((f : (a : α) → α) a₁) ⊔ a₂ = (⇑f : (a : α) → α)^[n + 1] a₁ ⊔ a₂

Tactic:
rw [← Function.iterate_succ_apply]

Premises used: Function.iterate_succ_apply
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁_1 a₂_1 : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
a₁ a₂ : α
f₁ : (⇑f : (a : α) → α)^[n] ((f : (a : α) → α) a₁) ⊔ a₂ = (⇑f : (a : α) → α)^[n + 1] a₁ ⊔ a₂
⊢ (⇑f : (a : α) → α)^[n + 1] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n + 1] a₁ ⊔ a₂

Tactic:
calc
          f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
          _ ≤ f^[n] (f a₁ ⊔ a₂) := f.mono.iterate n (h a₁ a₂)
          _ ≤ f^[n] (f a₁) ⊔ a₂ := ih _ _
          _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]

Premises used: Monotone.iterate, Nat.iterate, OrderHom.mono, HAdd.hAdd, Max.max, Function.iterate_succ_apply, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
n : ℕ
zero : ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[0] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[0] a₁ ⊔ a₂
succ :
  ∀ (n : ℕ) (ih : ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂) (a₁ a₂ : α),
    (⇑f : (a : α) → α)^[n + 1] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n + 1] a₁ ⊔ a₂
⊢ ∀ (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂

Tactic:
induction n with
      | zero => intro a₁ a₂; rfl
      | succ n ih =>
        intro a₁ a₂
        calc
          f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
          _ ≤ f^[n] (f a₁ ⊔ a₂) := f.mono.iterate n (h a₁ a₂)
          _ ≤ f^[n] (f a₁) ⊔ a₂ := ih _ _
          _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]

Premises used: Monotone.iterate, Nat.iterate, OrderHom.mono, HAdd.hAdd, Max.max, Function.iterate_succ_apply, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
⊢ ∀ (n : ℕ) (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂

Tactic:
have h' : ∀ n a₁ a₂, f^[n] (a₁ ⊔ a₂) ≤ f^[n] a₁ ⊔ a₂ := by
      intro n
      induction n with
      | zero => intro a₁ a₂; rfl
      | succ n ih =>
        intro a₁ a₂
        calc
          f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
          _ ≤ f^[n] (f a₁ ⊔ a₂) := f.mono.iterate n (h a₁ a₂)
          _ ≤ f^[n] (f a₁) ⊔ a₂ := ih _ _
          _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
⊢ (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) = (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₁ ⊔ a₂))

Tactic:
Function.iterate_add_apply f n₁ n₂ _

Premises used: Function.iterate_add_apply, DFunLike.coe
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
rw rw₁ :
  (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₂ ⊔ a₁)) =
    (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₂ ⊔ a₁))
⊢ (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₁ ⊔ a₂)) =
    (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₂ ⊔ a₁))

Tactic:
rw [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
⊢ (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₂ ⊔ a₁)) ≤
    (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] a₂ ⊔ a₁)

Tactic:
f.mono.iterate n₁ (h' n₂ _ _)

Premises used: Monotone.iterate, OrderHom.mono
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
rw rw₁ :
  (⇑f : (a : α) → α)^[n₁] (a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂) = (⇑f : (a : α) → α)^[n₁] (a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂)
⊢ (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] a₂ ⊔ a₁) = (⇑f : (a : α) → α)^[n₁] (a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂)

Tactic:
rw [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
⊢ (⇑f : (a : α) → α)^[n₁] (a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂

Tactic:
h' n₁ a₁ _
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_3
inst : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), LE.le (α := α) ((f : (a : α) → α) (a₁ ⊔ a₂) : α) ((f : (a : α) → α) a₁ ⊔ a₂ : α)
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f : (a : α) → α)^[n] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n] a₁ ⊔ a₂
f₁ :
  (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₁ ⊔ a₂)) =
    (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] (a₂ ⊔ a₁))
f₂ :
  (⇑f : (a : α) → α)^[n₁] ((⇑f : (a : α) → α)^[n₂] a₂ ⊔ a₁) = (⇑f : (a : α) → α)^[n₁] (a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂)
⊢ (⇑f : (a : α) → α)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f : (a : α) → α)^[n₁] a₁ ⊔ (⇑f : (a : α) → α)^[n₂] a₂

Tactic:
calc
      f^[n₁ + n₂] (a₁ ⊔ a₂) = f^[n₁] (f^[n₂] (a₁ ⊔ a₂)) :=
        Function.iterate_add_apply f n₁ n₂ _
      _ = f^[n₁] (f^[n₂] (a₂ ⊔ a₁)) := by rw [sup_comm]
      _ ≤ f^[n₁] (f^[n₂] a₂ ⊔ a₁) := f.mono.iterate n₁ (h' n₂ _ _)
      _ = f^[n₁] (a₁ ⊔ f^[n₂] a₂) := by rw [sup_comm]
      _ ≤ f^[n₁] a₁ ⊔ f^[n₂] a₂ := h' n₁ a₁ _

Premises used: Function.iterate_add_apply, Monotone.iterate, Nat.iterate, OrderHom.mono, HAdd.hAdd, Max.max, DFunLike.coe
-- Module: Mathlib.Order.Hom.PowersetCard
Goal:
n : ℕ
I : Type u_1
inst : LinearOrder I
f : Fin n ↪o I
symm :
  f =
    (fun (s : (↑(powersetCard I n) : Type u_1)) ↦ ((↑s : Finset I).orderEmbOfFin ⋯ : Fin n ↪o I))
      ((fun (f : Fin n ↪o I) ↦
          ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
        f)
⊢ (fun (s : (↑(powersetCard I n) : Type u_1)) ↦ ((↑s : Finset I).orderEmbOfFin ⋯ : Fin n ↪o I))
      ((fun (f : Fin n ↪o I) ↦
          ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
        f) =
    f

Tactic:
symm
-- Module: Mathlib.Order.Hom.PowersetCard
Goal:
n : ℕ
I : Type u_1
inst : LinearOrder I
f : Fin n ↪o I
hfs :
  ∀ (x : Fin n),
    Membership.mem (α := I) (γ := Finset I)
      (↑((fun (f : Fin n ↪o I) ↦
              ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
            f) :
        Finset I)
      ((f : (a : Fin n) → I) x : I)
⊢ f =
    (fun (s : (↑(powersetCard I n) : Type u_1)) ↦ ((↑s : Finset I).orderEmbOfFin ⋯ : Fin n ↪o I))
      ((fun (f : Fin n ↪o I) ↦
          ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
        f)

Tactic:
apply Finset.orderEmbOfFin_unique'

Premises used: Finset.orderEmbOfFin_unique'
-- Module: Mathlib.Order.Hom.PowersetCard
Goal:
n : ℕ
I : Type u_1
inst : LinearOrder I
f : Fin n ↪o I
⊢ ∀ (x : Fin n),
    Membership.mem (α := I) (γ := Finset I)
      (↑((fun (f : Fin n ↪o I) ↦
              ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
            f) :
        Finset I)
      ((f : (a : Fin n) → I) x : I)

Tactic:
simp
-- Module: Mathlib.Order.Hom.PowersetCard
Goal:
n : ℕ
I : Type u_1
inst : LinearOrder I
s : (↑(powersetCard I n) : Type u_1)
a :
  ∀ (a : I),
    Membership.mem (γ := Finset I)
        (↑((fun (f : Fin n ↪o I) ↦
                ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
              ((fun (s : (↑(powersetCard I n) : Type u_1)) ↦ ((↑s : Finset I).orderEmbOfFin ⋯ : Fin n ↪o I)) s)) :
          Finset I)
        a ↔
      a ∈ (↑s : Finset I)
⊢ (fun (f : Fin n ↪o I) ↦
        ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
      ((fun (s : (↑(powersetCard I n) : Type u_1)) ↦ ((↑s : Finset I).orderEmbOfFin ⋯ : Fin n ↪o I)) s) =
    s

Tactic:
ext
-- Module: Mathlib.Order.Hom.PowersetCard
Goal:
n : ℕ
I : Type u_1
inst : LinearOrder I
s : (↑(powersetCard I n) : Type u_1)
a : I
⊢ Membership.mem (γ := Finset I)
      (↑((fun (f : Fin n ↪o I) ↦
              ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2)))
            ((fun (s : (↑(powersetCard I n) : Type u_1)) ↦ ((↑s : Finset I).orderEmbOfFin ⋯ : Fin n ↪o I)) s)) :
        Finset I)
      a ↔
    a ∈ (↑s : Finset I)

Tactic:
simp
-- Module: Mathlib.Order.Hom.PowersetCard
Goal:
n : ℕ
I : Type u_1
inst : LinearOrder I
f : Fin n ↪o I
⊢ (ofFinEmbEquiv : (a : Fin n ↪o I) → (↑(powersetCard I n) : Type u_1)) f =
    ofFinEmb n I (f.toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : I) ↦ x1 ≤ x2))

Tactic:
rfl

Premises used: Set.powersetCard.ofFinEmb, Set.powersetCard.map, rfl
-- Module: Mathlib.Order.Hom.PowersetCard
Goal:
n : ℕ
I : Type u_1
inst : LinearOrder I
s : (↑(powersetCard I n) : Type u_1)
⊢ Eq (α := Fin n ↪o I) ((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) s : Fin n ↪o I)
    ((↑s : Finset I).orderEmbOfFin ⋯ : Fin n ↪o I)

Tactic:
rfl

Premises used: Finset.orderEmbOfFin, RelEmbedding.trans, rfl
-- Module: Mathlib.Order.Hom.PowersetCard
Goal:
n : ℕ
I : Type u_1
inst : LinearOrder I
f : Fin n ↪o I
i : I
⊢ Membership.mem (γ := (↑(powersetCard I n) : Type u_1))
      ((ofFinEmbEquiv : (a : Fin n ↪o I) → (↑(powersetCard I n) : Type u_1)) f : (↑(powersetCard I n) : Type u_1)) i ↔
    Membership.mem (γ := Set I) (range (ι := Fin n) (⇑f : (a : Fin n) → I)) i

Tactic:
simp [ofFinEmbEquiv_apply]

Premises used: Set.powersetCard.ofFinEmbEquiv_apply
-- Module: Mathlib.Order.Hom.PowersetCard
Goal:
n : ℕ
I : Type u_1
inst : LinearOrder I
s : (↑(powersetCard I n) : Type u_1)
i : I
⊢ Membership.mem (γ := Set I)
      (range (ι := Fin n)
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) s : Fin n ↪o I) :
          (a : Fin n) → I))
      i ↔
    i ∈ s

Tactic:
simp [ofFinEmbEquiv_symm_apply]

Premises used: Set.powersetCard.ofFinEmbEquiv_symm_apply
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Prod.{u_1, u_2} (Set α) (Set β)
⊢ (fun (s : Set (α ⊕ β)) ↦ (Sum.inl ⁻¹' s, Sum.inr ⁻¹' s))
      ((fun (s : Prod.{u_1, u_2} (Set α) (Set β)) ↦ Sum.inl '' s.1 ∪ Sum.inr '' s.2) s) =
    s

Tactic:
simp [preimage_image_eq _ Sum.inl_injective, preimage_image_eq _ Sum.inr_injective]

Premises used: Sum.inr_injective, Sum.inl_injective, Set.preimage_image_eq
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ {a b : Set (α ⊕ β)},
    LE.le (α := Prod.{u_1, u_2} (Set α) (Set β))
        (({ toFun := fun (s : Set (α ⊕ β)) ↦ (Sum.inl ⁻¹' s, Sum.inr ⁻¹' s),
                invFun := fun (s : Prod.{u_1, u_2} (Set α) (Set β)) ↦ Sum.inl '' s.1 ∪ Sum.inr '' s.2, left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Set (α ⊕ β)) → Set α × Set β)
            a :
          Prod.{u_1, u_2} (Set α) (Set β))
        (({ toFun := fun (s : Set (α ⊕ β)) ↦ (Sum.inl ⁻¹' s, Sum.inr ⁻¹' s),
                invFun := fun (s : Prod.{u_1, u_2} (Set α) (Set β)) ↦ Sum.inl '' s.1 ∪ Sum.inr '' s.2, left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Set (α ⊕ β)) → Set α × Set β)
            b :
          Prod.{u_1, u_2} (Set α) (Set β)) ↔
      a ≤ b

Tactic:
simp [subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
s : Prod.{u_1, u_2} (Set α) (Set β)
⊢ (OrderIso.symm sumEquiv : (a : Set α × Set β) → Set (α ⊕ β)) s = Sum.inl '' s.1 ∪ Sum.inr '' s.2

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, rfl
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Prod.{u_1, u_2} (Set α) (Set β)
t : Set γ
hf : MapsTo f s.1 t
hg : MapsTo g s.2 t
a : α
⊢ Membership.mem (γ := Set (α ⊕ β)) ((OrderIso.symm sumEquiv : (a : Set α × Set β) → Set (α ⊕ β)) s : Set (α ⊕ β))
      (Sum.inl a) →
    Sum.elim f g (Sum.inl a) ∈ t

Tactic:
aesop
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Prod.{u_1, u_2} (Set α) (Set β)
t : Set γ
hf : MapsTo f s.1 t
hg : MapsTo g s.2 t
b : β
⊢ Membership.mem (γ := Set (α ⊕ β)) ((OrderIso.symm sumEquiv : (a : Set α × Set β) → Set (α ⊕ β)) s : Set (α ⊕ β))
      (Sum.inr b) →
    Sum.elim f g (Sum.inr b) ∈ t

Tactic:
aesop
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Prod.{u_1, u_2} (Set α) (Set β)
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
a₁ : α
h₁ :
  Membership.mem (γ := Set (α ⊕ β)) ((OrderIso.symm sumEquiv : (a : Set α × Set β) → Set (α ⊕ β)) s : Set (α ⊕ β))
    (Sum.inl a₁)
a₂ : α
h₂ :
  Membership.mem (γ := Set (α ⊕ β)) ((OrderIso.symm sumEquiv : (a : Set α × Set β) → Set (α ⊕ β)) s : Set (α ⊕ β))
    (Sum.inl a₂)
heq : Sum.elim f g (Sum.inl a₁) = Sum.elim f g (Sum.inl a₂)
⊢ Eq (α := α ⊕ β) (Sum.inl a₁) (Sum.inl a₂)

Tactic:
aesop
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Prod.{u_1, u_2} (Set α) (Set β)
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
a₁ : α
h₁ :
  Membership.mem (γ := Set (α ⊕ β)) ((OrderIso.symm sumEquiv : (a : Set α × Set β) → Set (α ⊕ β)) s : Set (α ⊕ β))
    (Sum.inl a₁)
b₂ : β
h₂ :
  Membership.mem (γ := Set (α ⊕ β)) ((OrderIso.symm sumEquiv : (a : Set α × Set β) → Set (α ⊕ β)) s : Set (α ⊕ β))
    (Sum.inr b₂)
heq : Sum.elim f g (Sum.inl a₁) = Sum.elim f g (Sum.inr b₂)
⊢ Sum.inl a₁ = Sum.inr b₂

Tactic:
aesop
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Prod.{u_1, u_2} (Set α) (Set β)
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
b₁ : β
h₁ :
  Membership.mem (γ := Set (α ⊕ β)) ((OrderIso.symm sumEquiv : (a : Set α × Set β) → Set (α ⊕ β)) s : Set (α ⊕ β))
    (Sum.inr b₁)
a₂ : α
h₂ :
  Membership.mem (γ := Set (α ⊕ β)) ((OrderIso.symm sumEquiv : (a : Set α × Set β) → Set (α ⊕ β)) s : Set (α ⊕ β))
    (Sum.inl a₂)
heq : Sum.elim f g (Sum.inr b₁) = Sum.elim f g (Sum.inl a₂)
⊢ Sum.inr b₁ = Sum.inl a₂

Tactic:
aesop
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Prod.{u_1, u_2} (Set α) (Set β)
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
b₁ : β
h₁ :
  Membership.mem (γ := Set (α ⊕ β)) ((OrderIso.symm sumEquiv : (a : Set α × Set β) → Set (α ⊕ β)) s : Set (α ⊕ β))
    (Sum.inr b₁)
b₂ : β
h₂ :
  Membership.mem (γ := Set (α ⊕ β)) ((OrderIso.symm sumEquiv : (a : Set α × Set β) → Set (α ⊕ β)) s : Set (α ⊕ β))
    (Sum.inr b₂)
heq : Sum.elim f g (Sum.inr b₁) = Sum.elim f g (Sum.inr b₂)
⊢ Eq (α := α ⊕ β) (Sum.inr b₁) (Sum.inr b₂)

Tactic:
aesop
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
e : α ≃o β
⊢ Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β)) univ

Tactic:
e.surjective.range_eq

Premises used: OrderIso.surjective, Function.Surjective.range_eq
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
e : α ≃o β
s : Set α
⊢ image.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) ((⇑e : (a : α) → β) '' s) = s

Tactic:
e.toEquiv.symm_image_image s

Premises used: RelIso.toEquiv, Equiv.symm_image_image
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
e : α ≃o β
s : Set β
⊢ image.{u_1, u_2} (α := α) (⇑e : (a : α) → β) ((⇑e.symm : (a : β) → α) '' s) = s

Tactic:
e.toEquiv.image_symm_image s

Premises used: Equiv.image_symm_image, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
e : α ≃o β
s : Set α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' s) ((⇑e.symm : (a : β) → α) ⁻¹' s)

Tactic:
e.toEquiv.image_eq_preimage_symm s

Premises used: Equiv.image_eq_preimage_symm, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
e : α ≃o β
s : Set α
⊢ preimage.{u_1, u_2} (β := β) (⇑e : (a : α) → β) ((⇑e.symm : (a : β) → α) ⁻¹' s) = s

Tactic:
e.toEquiv.preimage_symm_preimage s

Premises used: Equiv.preimage_symm_preimage, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
e : α ≃o β
s : Set β
⊢ preimage.{u_2, u_1} (β := α) (⇑e.symm : (a : β) → α) ((⇑e : (a : α) → β) ⁻¹' s) = s

Tactic:
e.toEquiv.symm_preimage_preimage s

Premises used: Equiv.symm_preimage_preimage, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
e : α ≃o β
s : Set β
⊢ image.{u_1, u_2} (α := α) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) ⁻¹' s) = s

Tactic:
e.toEquiv.image_preimage s

Premises used: RelIso.toEquiv, Equiv.image_preimage
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
e : α ≃o β
s : Set α
⊢ preimage.{u_1, u_2} (β := β) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) '' s) = s

Tactic:
e.toEquiv.preimage_image s

Premises used: Equiv.preimage_image, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
h_mono : StrictMono f
h_surj : Function.Surjective f
⊢ (⇑(orderIsoOfSurjective f h_mono h_surj) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
h_mono : StrictMono f
h_surj : Function.Surjective f
a : α
⊢ ((orderIsoOfSurjective f h_mono h_surj).symm : (a : β) → α) (f a) = a

Tactic:
(orderIsoOfSurjective f h_mono h_surj).symm_apply_apply _

Premises used: OrderIso.symm_apply_apply, StrictMono.orderIsoOfSurjective
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
h_mono : StrictMono f
h_surj : Function.Surjective f
b : β
⊢ f (((orderIsoOfSurjective f h_mono h_surj).symm : (a : β) → α) b) = b

Tactic:
(orderIsoOfSurjective f h_mono h_surj).apply_symm_apply _

Premises used: OrderIso.apply_symm_apply, StrictMono.orderIsoOfSurjective