awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
toSemilatticeSup : SemilatticeSup α
inf : α → α → α
inf_le_left : ∀ (a b : α), inf a b ≤ a
inf_le_right : ∀ (a b : α), inf a b ≤ b
le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf b c
inf_1 : α → α → α
inf_le_left_1 : ∀ (a b : α), inf_1 a b ≤ a
inf_le_right_1 : ∀ (a b : α), inf_1 a b ≤ b
le_inf_1 : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf_1 b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
mk :
  ∀ (inf_le_left_2 : ∀ (a b : α), inf a b ≤ a) (inf_le_right_2 : ∀ (a b : α), inf a b ≤ b)
    (le_inf_2 : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf b c) (H : ∀ (x y : α), x ≤ y ↔ x ≤ y),
    { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
        le_inf := le_inf : Lattice α } =
      {
        toSemilatticeSup :=
          { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
              le_inf := le_inf }.toSemilatticeSup,
        inf := inf, inf_le_left := inf_le_left_2, inf_le_right := inf_le_right_2, le_inf := le_inf_2 }
⊢ { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
      le_inf := le_inf : Lattice α } =
    {
      toSemilatticeSup :=
        { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
            le_inf := le_inf }.toSemilatticeSup,
      inf := inf_1, inf_le_left := inf_le_left_1, inf_le_right := inf_le_right_1, le_inf := le_inf_1 }

Tactic:
cases SemilatticeInf.ext H

Premises used: SemilatticeInf.ext
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
toSemilatticeSup : SemilatticeSup α
inf : α → α → α
inf_le_left : ∀ (a b : α), inf a b ≤ a
inf_le_right : ∀ (a b : α), inf a b ≤ b
le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf b c
inf_le_left_1 : ∀ (a b : α), inf a b ≤ a
inf_le_right_1 : ∀ (a b : α), inf a b ≤ b
le_inf_1 : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
      le_inf := le_inf : Lattice α } =
    {
      toSemilatticeSup :=
        { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
            le_inf := le_inf }.toSemilatticeSup,
      inf := inf, inf_le_left := inf_le_left_1, inf_le_right := inf_le_right_1, le_inf := le_inf_1 }

Tactic:
congr
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
DistribLattice.le_sup_inf x y z

Premises used: DistribLattice.le_sup_inf
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
a b c : α
⊢ a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)

Tactic:
le_antisymm sup_inf_le le_sup_inf

Premises used: le_sup_inf, le_antisymm, sup_inf_le
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
a b c : α
⊢ a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)

Tactic:
simp only [sup_inf_left, sup_comm _ c]

Premises used: sup_inf_left, sup_comm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
a b c : α
rw rw₁ : a ⊓ (b ⊔ c) = a ⊓ (b ⊔ c)
⊢ a ⊓ (b ⊔ c) = a ⊓ (a ⊔ c) ⊓ (b ⊔ c)

Tactic:
rw [inf_sup_self]

Premises used: inf_sup_self
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
a b c : α
⊢ a ⊓ (a ⊔ c) ⊓ (b ⊔ c) = a ⊓ (a ⊓ b ⊔ c)

Tactic:
simp only [inf_assoc, sup_inf_right]

Premises used: sup_inf_right, inf_assoc
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
a b c : α
rw rw₁ : a ⊓ (a ⊓ b ⊔ c) = a ⊓ (a ⊓ b ⊔ c)
⊢ a ⊓ (a ⊓ b ⊔ c) = (a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c)

Tactic:
rw [sup_inf_self]

Premises used: sup_inf_self
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
a b c : α
rw rw₁ : (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c)
⊢ (a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c) = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c)

Tactic:
rw [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
a b c : α
rw rw₁ : (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c)
⊢ (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) = a ⊓ b ⊔ a ⊓ c

Tactic:
rw [sup_inf_left]

Premises used: sup_inf_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
x y z : α
rw rw₁ : x ⊓ y ⊔ x ⊓ z ≤ x ⊓ y ⊔ x ⊓ z
⊢ x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ x ⊓ z

Tactic:
rw [inf_sup_left]

Premises used: inf_sup_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
a b c : α
⊢ (a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c

Tactic:
simp only [inf_sup_left, inf_comm _ c]

Premises used: inf_comm, inf_sup_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
rw : (y ⊔ x) ⊓ (z ⊔ x) = (y ⊔ x) ⊓ (x ⊔ z)
rw₁ rw₂ : (y ⊔ x) ⊓ (z ⊔ x) = (y ⊔ x) ⊓ (z ⊔ x)
⊢ y ⊓ z ⊔ x = (y ⊔ x) ⊓ (x ⊔ z)

Tactic:
rw [sup_inf_right, sup_comm x]

Premises used: sup_inf_right, sup_comm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
rw rw₁ : y ⊔ x ⊓ z = y ⊔ x ⊓ z
⊢ (y ⊔ x) ⊓ (y ⊔ z) = y ⊔ x ⊓ z

Tactic:
rw [← sup_inf_left]

Premises used: sup_inf_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : DistribLattice α
a b c : α
h₁ : b ⊓ a = c ⊓ a
h₂ : b ⊔ a = c ⊔ a
⊢ b = c

Tactic:
le_antisymm (le_of_inf_le_sup_le (le_of_eq h₁) (le_of_eq h₂))
    (le_of_inf_le_sup_le (le_of_eq h₁.symm) (le_of_eq h₂.symm))

Premises used: le_of_inf_le_sup_le, le_antisymm, le_of_eq, Eq.symm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : LinearOrder α
a b : α
p : α → Prop
ha : p a
hb : p b
h : a ≤ b
rwa rwa₁ rwa₂ rwa₃ : p b
⊢ p (max a b)

Tactic:
rwa [sup_eq_right.2 h]

Premises used: Iff.mpr, sup_eq_right
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : LinearOrder α
a b : α
p : α → Prop
ha : p a
hb : p b
h : b ≤ a
rwa rwa₁ rwa₂ rwa₃ : p a
⊢ p (max a b)

Tactic:
rwa [sup_eq_left.2 h]

Premises used: Iff.mpr, sup_eq_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ a ≤ max b c ↔ a ≤ b ∨ a ≤ c

Tactic:
grind
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ a < max b c ↔ a < b ∨ a < c

Tactic:
grind
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ max b c < a ↔ b < a ∧ c < a

Tactic:
⟨fun h => ⟨le_sup_left.trans_lt h, le_sup_right.trans_lt h⟩,
   fun h => sup_ind (p := (· < a)) b c h.1 h.2⟩

Premises used: le_sup_left, le_sup_right, And.right, And.left, And.intro, Iff.intro, sup_ind, LE.le.trans_lt
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : LinearOrder α
a b c d : α
⊢ max (max a b) (max c d) = max (max a c) (max b d)

Tactic:
sup_sup_sup_comm _ _ _ _

Premises used: sup_sup_sup_comm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
h : ∀ (x y : α), x ⊔ y = maxDefault x y
⊢ Eq.{u + 1} (α := α → α → α) (fun (x1 x2 : α) ↦ x1 ⊔ x2) maxDefault

Tactic:
ext x y
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
pos : ∀ (h' : x ≤ y), x ⊔ y = y
neg : ∀ (h' : ¬x ≤ y), x ⊔ y = x
⊢ x ⊔ y = if x ≤ y then y else x

Tactic:
split_ifs with h'
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
h' : x ≤ y
⊢ x ⊔ y = y

Tactic:
sup_of_le_right h'

Premises used: sup_of_le_right
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
h' : ¬x ≤ y
⊢ x ⊔ y = x

Tactic:
sup_of_le_left <| (total_of (· ≤ ·) x y).resolve_left h'

Premises used: Or.resolve_left, LE.le, total_of, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
h' : x ≤ y
⊢ x ⊔ y = y

Tactic:
exacts [sup_of_le_right h', sup_of_le_left <| (total_of (· ≤ ·) x y).resolve_left h']

Premises used: sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
h : ∀ (x y : α), x ⊓ y = minDefault x y
⊢ Eq.{u + 1} (α := α → α → α) (fun (x1 x2 : α) ↦ x1 ⊓ x2) minDefault

Tactic:
ext x y
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
pos : ∀ (h' : x ≤ y), x ⊓ y = x
neg : ∀ (h' : ¬x ≤ y), x ⊓ y = y
⊢ x ⊓ y = if x ≤ y then x else y

Tactic:
split_ifs with h'
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
h' : x ≤ y
⊢ x ⊓ y = x

Tactic:
inf_of_le_left h'

Premises used: inf_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
h' : ¬x ≤ y
⊢ x ⊓ y = y

Tactic:
inf_of_le_right <| (total_of (· ≤ ·) x y).resolve_left h'

Premises used: inf_of_le_right, Or.resolve_left, LE.le, total_of
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
h' : x ≤ y
⊢ x ⊓ y = x

Tactic:
exacts [inf_of_le_left h', inf_of_le_right <| (total_of (· ≤ ·) x y).resolve_left h']

Premises used: inf_of_le_left, inf_of_le_right
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u
inst : Lattice α
inst_1 : DecidableEq α
inst_2 : DecidableLE α
inst_3 : DecidableLT α
inst_4 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ ∀ (a b : α), a ⊓ b = if a ≤ b then a else b

Tactic:
congr_fun₂ inf_eq_minDefault

Premises used: congr_fun₂, inf_eq_minDefault
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u
inst : Lattice α
inst_1 : DecidableEq α
inst_2 : DecidableLE α
inst_3 : DecidableLT α
inst_4 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ ∀ (a b : α), a ⊓ b = if a ≤ b then a else b

Tactic:
exact congr_fun₂ inf_eq_minDefault

Premises used: congr_fun₂, inf_eq_minDefault
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u
inst : Lattice α
inst_1 : DecidableEq α
inst_2 : DecidableLE α
inst_3 : DecidableLT α
inst_4 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ ∀ (a b : α), a ⊔ b = if a ≤ b then b else a

Tactic:
congr_fun₂ sup_eq_maxDefault

Premises used: congr_fun₂, sup_eq_maxDefault
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u
inst : Lattice α
inst_1 : DecidableEq α
inst_2 : DecidableLE α
inst_3 : DecidableLT α
inst_4 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ ∀ (a b : α), a ⊔ b = if a ≤ b then b else a

Tactic:
exact congr_fun₂ sup_eq_maxDefault

Premises used: congr_fun₂, sup_eq_maxDefault
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Min α
a b : αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) (a ⊔ b) : α) ((ofDual : (a : αᵒᵈ) → α) a ⊓ (ofDual : (a : αᵒᵈ) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Max α
a b : α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) (a ⊔ b) : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a ⊓ (toDual : (a : α) → αᵒᵈ) b : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : LinearOrder α
a b : αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) (max a b) : α)
    (min ((ofDual : (a : αᵒᵈ) → α) a) ((ofDual : (a : αᵒᵈ) → α) b) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : LinearOrder α
a b : α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) (max a b) : αᵒᵈ)
    (min ((toDual : (a : α) → αᵒᵈ) a) ((toDual : (a : α) → αᵒᵈ) b) : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lattice
Goal:
ι : Type u_1
α' : ι → Type u_2
inst : (i : ι) → Max (α' i)
f g : (i : ι) → α' i
i : ι
⊢ (f ⊔ g) i = f i ⊔ g i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lattice
Goal:
ι : Type u_1
α' : ι → Type u_2
inst : (i : ι) → Max (α' i)
f g : (i : ι) → α' i
⊢ f ⊔ g = fun (i : ι) ↦ f i ⊔ g i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Lattice
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
inl : ∀ (a b : π j), update (β := π) f j (a ⊔ b) j = (update (β := π) f j a ⊔ update (β := π) f j b) j
inr : ∀ (hji : j ≠ i), update (β := π) f i (a ⊔ b) j = (update (β := π) f i a ⊔ update (β := π) f i b) j
⊢ update (β := π) f i (a ⊔ b) j = (update (β := π) f i a ⊔ update (β := π) f i b) j

Tactic:
obtain rfl | hji := eq_or_ne j i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Order.Lattice
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
j : ι
a b : π j
⊢ update (β := π) f j (a ⊔ b) j = (update (β := π) f j a ⊔ update (β := π) f j b) j

Tactic:
simp [update_of_ne, *]

Premises used: Function.update_of_ne
-- Module: Mathlib.Order.Lattice
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
hji : j ≠ i
⊢ update (β := π) f i (a ⊔ b) j = (update (β := π) f i a ⊔ update (β := π) f i b) j

Tactic:
simp [update_of_ne, *]

Premises used: Function.update_of_ne
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : SemilatticeSup β
f g : α → β
hf : Monotone f
hg : Monotone g
⊢ Monotone (f ⊔ g)

Tactic:
fun _ _ h => sup_le_sup (hf h) (hg h)

Premises used: sup_le_sup, Monotone
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : LinearOrder β
f g : α → β
hf : Monotone f
hg : Monotone g
⊢ Monotone.{u, v} (β := β) fun (x : α) ↦ max (f x) (g x)

Tactic:
hf.sup hg

Premises used: Monotone.sup
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
f : α → β
h : Monotone f
x y : α
⊢ f x ⊔ f y ≤ f (x ⊔ y)

Tactic:
sup_le (h le_sup_left) (h le_sup_right)

Premises used: le_sup_left, le_sup_right, sup_le
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
inst_1 : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
x y : α
hxy : x ≤ y
rw : f x ≤ f (x ⊔ y)
⊢ f x ≤ f y

Tactic:
rw [← sup_eq_right.2 hxy]

Premises used: Iff.mpr, sup_eq_right
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
inst_1 : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
x y : α
hxy : x ≤ y
⊢ f x ≤ f (x ⊔ y)

Tactic:
apply h
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
f : α → β
h : ∀ (x y : α), f x ⊔ f y ≤ f (x ⊔ y)
⊢ Monotone f

Tactic:
of_left_le_map_sup fun x y ↦ le_sup_left.trans (h x y)

Premises used: le_sup_left, LE.le.trans, Monotone.of_left_le_map_sup
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
f : α → β
h : ∀ (x y : α), f (x ⊔ y) = f x ⊔ f y
⊢ Monotone f

Tactic:
of_le_map_sup fun x y ↦ (h x y).ge

Premises used: Eq.ge, Monotone.of_le_map_sup
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : SemilatticeSup β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ f (max x y) = f x ⊔ f y

Tactic:
simp only [h, hf h, sup_of_le_right]

Premises used: sup_of_le_right
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : SemilatticeSup β
f : α → β
hf : Monotone f
x y : α
h : y ≤ x
⊢ f (max x y) = f x ⊔ f y

Tactic:
simp only [h, hf h, sup_of_le_left]

Premises used: sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
P : α → Prop
x₀ : α
hP : Monotone P
⊢ (∃ (x : α), x₀ ≤ x ∧ P x) ↔ ∃ (x : α), P x

Tactic:
⟨fun h => h.imp fun _ h => h.2, fun ⟨x, hx⟩ => ⟨x ⊔ x₀, le_sup_right, hP le_sup_left hx⟩⟩

Premises used: _private.0.exists_ge_and_iff_exists.match_1, le_sup_left, Exists, le_sup_right, Exists.imp, LE.le, And, Max.max, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
P Q : α → Prop
hP : Monotone P
hQ : Monotone Q
⊢ ((∃ (x : α), P x) ∧ ∃ (x : α), Q x) ↔ ∃ (x : α), P x ∧ Q x

Tactic:
⟨fun ⟨⟨x, hPx⟩, ⟨y, hQx⟩⟩ ↦ ⟨x ⊔ y, ⟨hP le_sup_left hPx, hQ le_sup_right hQx⟩⟩,
    fun ⟨x, hPx, hQx⟩ ↦ ⟨⟨x, hPx⟩, ⟨x, hQx⟩⟩⟩

Premises used: _private.0.exists_and_iff_of_monotone.match_2, le_sup_left, Exists, le_sup_right, And, Max.max, And.intro, Iff.intro, Exists.intro, _private.0.exists_and_iff_of_monotone.match_1
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : SemilatticeSup β
f g : α → β
s : Set α
hf : MonotoneOn f s
hg : MonotoneOn g s
⊢ MonotoneOn (f ⊔ g) s

Tactic:
fun _ hx _ hy h => sup_le_sup (hf hx hy h) (hg hx hy h)

Premises used: sup_le_sup, MonotoneOn
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : LinearOrder β
f g : α → β
s : Set α
hf : MonotoneOn f s
hg : MonotoneOn g s
⊢ MonotoneOn.{u, v} (β := β) (fun (x : α) ↦ max (f x) (g x)) s

Tactic:
hf.sup hg

Premises used: MonotoneOn.sup
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊔ y) = f x ⊔ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
rw : f (x ⊔ y) = f y
rw₁ rw₂ : f y = f y
⊢ f x ⊔ f y = f y

Tactic:
rw [← h _ hx _ hy, sup_eq_right.2 hxy]

Premises used: Iff.mpr, sup_eq_right
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
inl : x ≤ y → f (max x y) = f x ⊔ f y
inr : y ≤ x → f (max x y) = f x ⊔ f y
⊢ f (max x y) = f x ⊔ f y

Tactic:
cases le_total x y

Premises used: le_total
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
inl : ∀ (this : f x ≤ f y), f (max x y) = f x ⊔ f y
inl₁ : x ∈ s
inl₂ : y ∈ s
⊢ f (max x y) = f x ⊔ f y

Tactic:
have := hf ?_ ?_ ‹_›
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
inr : ∀ (this : f y ≤ f x), f (max x y) = f x ⊔ f y
inr₁ : y ∈ s
inr₂ : x ∈ s
⊢ f (max x y) = f x ⊔ f y

Tactic:
have := hf ?_ ?_ ‹_›
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
this : f x ≤ f y
⊢ f (max x y) = f x ⊔ f y

Tactic:
simp only [*, sup_of_le_left, sup_of_le_right]

Premises used: sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
this : f x ≤ f y
⊢ f (max x y) = f x ⊔ f y

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Premises used: sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
⊢ x ∈ s

Tactic:
assumption
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
⊢ x ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Premises used: sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
⊢ y ∈ s

Tactic:
assumption
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : x ≤ y
⊢ y ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Premises used: sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
this : f y ≤ f x
⊢ f (max x y) = f x ⊔ f y

Tactic:
simp only [*, sup_of_le_left, sup_of_le_right]

Premises used: sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
this : f y ≤ f x
⊢ f (max x y) = f x ⊔ f y

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Premises used: sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
⊢ y ∈ s

Tactic:
assumption
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
⊢ y ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Premises used: sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
⊢ x ∈ s

Tactic:
assumption
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst : LinearOrder α
inst_1 : SemilatticeSup β
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
h : y ≤ x
⊢ x ∈ s

Tactic:
first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Premises used: sup_of_le_right, sup_of_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : SemilatticeSup β
f g : α → β
hf : Antitone f
hg : Antitone g
⊢ Antitone (f ⊔ g)

Tactic:
fun _ _ h => sup_le_sup (hf h) (hg h)

Premises used: sup_le_sup, Antitone
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : LinearOrder β
f g : α → β
hf : Antitone f
hg : Antitone g
⊢ Antitone.{u, v} (β := β) fun (x : α) ↦ max (f x) (g x)

Tactic:
hf.sup hg

Premises used: Antitone.sup
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
inst_1 : SemilatticeInf β
f : α → β
h : Antitone f
x y : α
⊢ f (x ⊔ y) ≤ f x ⊓ f y

Tactic:
h.dual_right.le_map_sup x y

Premises used: Antitone.dual_right, Monotone.le_map_sup
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : SemilatticeInf β
f : α → β
hf : Antitone f
x y : α
⊢ f (max x y) = f x ⊓ f y

Tactic:
hf.dual_right.map_sup x y

Premises used: Antitone.dual_right, Monotone.map_sup, OrderDual
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
P : α → Prop
x₀ : α
hP : Antitone P
⊢ (∃ (x : α), x ≤ x₀ ∧ P x) ↔ ∃ (x : α), P x

Tactic:
exists_ge_and_iff_exists <| hP.dual_left

Premises used: Antitone.dual_left, OrderDual, exists_ge_and_iff_exists
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
P Q : α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ (x : α), P x) ∧ ∃ (x : α), Q x) ↔ ∃ (x : α), P x ∧ Q x

Tactic:
⟨fun ⟨⟨x, hPx⟩, ⟨y, hQx⟩⟩ ↦ ⟨x ⊓ y, ⟨hP inf_le_left hPx, hQ inf_le_right hQx⟩⟩,
    fun ⟨x, hPx, hQx⟩ ↦ ⟨⟨x, hPx⟩, ⟨x, hQx⟩⟩⟩

Premises used: _private.0.exists_and_iff_of_monotone.match_2, Exists, inf_le_right, And, And.intro, Iff.intro, Exists.intro, inf_le_left, _private.0.exists_and_iff_of_monotone.match_1, Min.min
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : SemilatticeSup β
f g : α → β
s : Set α
hf : AntitoneOn f s
hg : AntitoneOn g s
⊢ AntitoneOn (f ⊔ g) s

Tactic:
fun _ hx _ hy h => sup_le_sup (hf hx hy h) (hg hx hy h)

Premises used: sup_le_sup, AntitoneOn