mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
⊢ (cons (inr b) u hb).toRight = cons b u.toRight ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (image Sum.swap u).toLeft = u.toRight

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (image Sum.swap u).toRight = u.toLeft

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inl a) u).toLeft = insert a u.toLeft

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inr b) u).toLeft = u.toLeft

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inl a) u).toRight = u.toRight

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inr b) u).toRight = insert b u.toRight

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
m : ↑s
hmax : t.maximum = ↑m
⊢ ↑m < x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∩ v).toLeft = u.toLeft ∩ v.toLeft

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∩ v).toRight = u.toRight ∩ v.toRight

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∪ v).toLeft = u.toLeft ∪ v.toLeft

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∪ v).toRight = u.toRight ∪ v.toRight

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u \ v).toLeft = u.toLeft \ v.toLeft

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u \ v).toRight = u.toRight \ v.toRight

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
s✝ : Finset α✝
t : Finset β✝
s₁ s₂ : Finset α✝
t₁ t₂ : Finset β✝
a✝ : α✝
b✝ : β✝
x : α✝ ⊕ β✝
u v : Finset (α✝ ⊕ β✝)
a : α✝
b : β✝
α : Type u_4
β : Type u_5
s : Finset α × Finset β
⊢ (fun s ↦ (s.toLeft, s.toRight)) ((fun s ↦ s.1.disjSum s.2) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
s : Finset α✝
t : Finset β✝
s₁ s₂ : Finset α✝
t₁ t₂ : Finset β✝
a✝ : α✝
b✝ : β✝
x : α✝ ⊕ β✝
u v : Finset (α✝ ⊕ β✝)
a : α✝
b : β✝
α : Type u_4
β : Type u_5
⊢ ∀ {a b : Finset (α ⊕ β)},
    { toFun := fun s ↦ (s.toLeft, s.toRight), invFun := fun s ↦ s.1.disjSum s.2, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun s ↦ (s.toLeft, s.toRight), invFun := fun s ↦ s.1.disjSum s.2, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ⊆ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a✝ : α
b✝ : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
f : α ⊕ β ↪ γ
⊢ Disjoint (map (Embedding.inl.trans f) s) (map (Embedding.inr.trans f) t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = max (↑a) tl.maximum
⊢ (a :: (tl ++ [hd])).maximum = max (↑a) (tl ++ [hd]).maximum

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst✝¹ : Std.Commutative op
inst✝ : Std.Associative op
⊢ fold op (op b₁ b₂) f (s.disjSum t) = op (fold op b₁ (fun x ↦ f (inl x)) s) (fold op b₂ (fun x ↦ f (inr x)) t)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Set.range (Subtype.val ∘ ofNat s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑s
⊢ toFunAux x = #({y ∈ range ↑x | y ∈ s})

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ toFunAux (ofNat s 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
⊢ ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithBot α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ↑a ≤ b) → l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → ↑a_1 ≤ b
⊢ a ∈ a :: l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
b : WithBot α
h : ∀ (a : α), a ∈ l → ↑a ≤ b
⊢ l.maximum ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
m : ℕ
h : m < ↑(succ (ofNat s n)) ∧ m ∈ s
⊢ m = ↑(ofNat s n) ∨ m < ↑(ofNat s n) ∧ m ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
⊢ {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ l.maximum = ↑m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
⊢ ↑a ≤ l.maximum ↔ ∃ b, b ∈ l ∧ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
h : l ≠ []
head✝ : α
tail✝ : List α
x✝ : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝).maximum ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
h : 0 < l.length
head✝ : α
tail✝ : List α
x✝ : 0 < (head✝ :: tail✝).length
⊢ (head✝ :: tail✝).maximum ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
h : 0 < l.length
⊢ maximum_of_length_pos h ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ a ≤ maximum_of_length_pos w

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : 0 < l.length
⊢ l[i] ≤ maximum_of_length_pos h

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l l' : List α
h : l ~ l'
⊢ l.maximum = l'.maximum

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
⊢ toFunAux (ofNat s (n + 1)) = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
⊢ Denumerable α

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Countable α
inst✝² : Infinite α
inst✝¹ : Countable β
inst✝ : Infinite β
⊢ Nonempty (α ≃ β)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
d : α
⊢ l.max?.getD d = WithBot.unbotD d l.maximum

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : EquivLike F α β
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
⊢ f a = ⊤ ↔ a = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f g : TopHom α β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f : TopHom β γ
g : TopHom α β
⊢ (⇑f ∘ ⇑g) ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Top α
inst✝¹ : Top β
inst✝ : Top γ
g : TopHom β γ
f₁ f₂ : TopHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeInf β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ (⇑f ⊓ ⇑g) ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ (⇑f ⊔ ⇑g) ⊤ = ⊤

Tactic:
rw [Pi.sup_apply, map_top, map_top, sup_top_eq]

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ (⇑f ⊔ ⇑g) ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h : l ≠ []
⊢ ↑(foldr max ⊥ l) = l.maximum

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedOrderHom α β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_top'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊤ = ⊤
map_bot'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊥ = ⊥
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
map_top'✝¹ : { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun ⊤ = ⊤
map_bot'✝¹ : { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun ⊥ = ⊥
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_top'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊤ = ⊤
map_bot'✝ : { toFun := toFun✝, monotone' := monotone'✝ }.toFun ⊥ = ⊥
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, monotone' := monotone'✝¹, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ }
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    { toFun := toFun✝, monotone' := monotone'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ }
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
a : α
h : ∀ (x : α), x ∈ l → x ≤ a
⊢ foldr max ⊥ l ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
f g : BoundedOrderHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ x ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
a x : α
hx : x ∈ l
h : a ≤ x
⊢ a ≤ foldr max ⊥ l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
a x b : α
hx : x ∈ l
h : a ≤ x
⊢ a ≤ foldr max b l

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : SupHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f a ≤ f b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : EquivLike F α β
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ f (a ⊔ b) ≤ c ↔ f a ⊔ f b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
⊢ f x ≤ f y ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f g : SupHom α β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a ⊔ b) = (⇑f ∘ ⇑g) a ⊔ (⇑f ∘ ⇑g) b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Max α
inst✝¹ : Max β
inst✝ : Max γ
g : SupHom β γ
f₁ f₂ : SupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : Max α
inst✝ : SemilatticeSup β
f g : SupHom α β
a b : α
⊢ (⇑f ⊔ ⇑g) (a ⊔ b) = (⇑f ⊔ ⇑g) a ⊔ (⇑f ⊔ ⇑g) b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : Max α
inst✝ : SemilatticeSup β
P : β → Prop
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ ∀ (a b : { x // P x }), ↑(a ⊔ b) = ↑a ⊔ ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
g : LatticeHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
h : (fun f ↦ f.toFun) { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ } = (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun (a ⊓ b) =
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun a ⊓ { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ } =
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
f g : LatticeHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
P : β → Prop
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
this : Lattice { x // P x } := Subtype.lattice Psup Pinf
⊢ ∀ (a b : { x // P x }),
    (SupHom.subtypeVal Psup).toFun (a ⊓ b) = (SupHom.subtypeVal Psup).toFun a ⊓ (SupHom.subtypeVal Psup).toFun b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f a = f a ⊔ f b

Tactic:
sup_eq_left.2 (OrderHomClass.mono f h : f b ≤ f a)

Goal state after:
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f a = f a
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
⊢ f (max a b) = f a ⊔ f b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
⊢ f (min a b) = f a ⊓ f b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Union

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
f : β → α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq β
s : Finset γ
t : γ → Finset β
c : α
⊢ (s.biUnion t).sup f ≤ c ↔ (s.sup fun x ↦ (t x).sup f) ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Union

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
f : β → α
inst✝ : DecidableEq β
s : Finset γ
Hs : s.Nonempty
t : γ → Finset β
Ht : ∀ (b : γ), (t b).Nonempty
c : α
⊢ (s.biUnion t).sup' ⋯ f ≤ c ↔ (s.sup' Hs fun b ↦ (t b).sup' ⋯ f) ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Lattice α
inst✝⁵ : Lattice β
inst✝⁴ : FunLike F α β
inst✝³ : OrderBot α
inst✝² : OrderBot β
inst✝¹ : BotHomClass F α β
inst✝ : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
⊢ Disjoint (f a) (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b) = f a \ f b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Union

Goal state before:
pp: α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
⊢ s.sup t = s.biUnion t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a ∆ b) = f a ∆ f b

Tactic:
by

Goal state after: