awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓
          s.attach.inf
            ((fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (b (↑i_1 : ι) ⋯)) ∘ fun (x : ↥s) ↦
              Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) ⋯) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), (↑j : ι) ≠ i
this :
  f i ((fun (j : ι) (hj : j ∈ insert i s) ↦ (if hji : j = i then cast ⋯ a else g j ⋯ : κ j)) i ⋯) ⊓
      s.attach.inf
        ((fun (i_1 : ↥(insert i s)) ↦
            f (↑i_1 : ι)
              ((fun (j : ι) (hj : j ∈ insert i s) ↦ (if hji : j = i then cast ⋯ a else g j ⋯ : κ j)) (↑i_1 : ι) ⋯)) ∘
          fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) ⋯) ≤
    c
⊢ (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯)) ≤ c

Tactic:
simpa only [cast_eq, dif_pos, Function.comp_def, Subtype.coe_mk, dif_neg, aux] using this

Premises used: Subtype.coe_mk, dif_pos, dif_neg, Function.comp_def, cast_eq
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓
          s.attach.inf
            ((fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (b (↑i_1 : ι) ⋯)) ∘ fun (x : ↥s) ↦
              Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) ⋯) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), (↑j : ι) ≠ i
j : ι
hj : j ∈ insert i s
⊢ j = i ∨ j ∈ s

Tactic:
rw [mem_insert] at hj

Premises used: Finset.mem_insert
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
c : α
h :
  ∀ (b : (a : ι) → a ∈ Insert.insert i s → κ a),
    (∀ (a : ι) (h : a ∈ Insert.insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓
          s.attach.inf
            ((fun (i_1 : ↥(Insert.insert i s)) ↦ f (↑i_1 : ι) (b (↑i_1 : ι) ⋯)) ∘ fun (x : ↥s) ↦
              Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) (↑x : ι) ⋯) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), (↑j : ι) ≠ i
j : ι
hj_1 : j ∈ Insert.insert i s
hj : j = i ∨ j ∈ s
insert :
  ∀ (hi : j ∉ s)
    (h :
      ∀ (b : (a : ι) → a ∈ Insert.insert j s → κ a),
        (∀ (a : ι) (h : a ∈ Insert.insert j s), b a h ∈ t a) →
          f j (b j ⋯) ⊓
              s.attach.inf
                ((fun (i : ↥(Insert.insert j s)) ↦ f (↑i : ι) (b (↑i : ι) ⋯)) ∘ fun (x : ↥s) ↦
                  Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert j s) (↑x : ι) ⋯) ≤
            c)
    (a : κ j) (ha : a ∈ t j) (aux : ∀ (j_1 : ↥s), (↑j_1 : ι) ≠ j) (hj : j ∈ Insert.insert j s),
    (fun (j_1 : ι) (hj : j_1 ∈ Insert.insert j s) ↦ (if hji : j_1 = j then cast ⋯ a else g j_1 ⋯ : κ j_1)) j hj ∈ t j
insert₁ :
  ∀ (hj : j ∈ s),
    (fun (j : ι) (hj : j ∈ Insert.insert i s) ↦ (if hji : j = i then cast ⋯ a else g j ⋯ : κ j)) j hj_1 ∈ t j
⊢ (fun (j : ι) (hj : j ∈ Insert.insert i s) ↦ (if hji : j = i then cast ⋯ a else g j ⋯ : κ j)) j hj_1 ∈ t j

Tactic:
obtain (rfl | hj) := hj

Premises used: rfl
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
s : Finset ι
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
c : α
g : (a : ι) → a ∈ s → κ a
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
j : ι
hi : j ∉ s
h :
  ∀ (b : (a : ι) → a ∈ insert j s → κ a),
    (∀ (a : ι) (h : a ∈ insert j s), b a h ∈ t a) →
      f j (b j ⋯) ⊓
          s.attach.inf
            ((fun (i : ↥(insert j s)) ↦ f (↑i : ι) (b (↑i : ι) ⋯)) ∘ fun (x : ↥s) ↦
              Subtype.mk (p := fun (x : ι) ↦ x ∈ insert j s) (↑x : ι) ⋯) ≤
        c
a : κ j
ha : a ∈ t j
aux : ∀ (j_1 : ↥s), (↑j_1 : ι) ≠ j
hj : j ∈ insert j s
⊢ (fun (j_1 : ι) (hj : j_1 ∈ insert j s) ↦ (if hji : j_1 = j then cast ⋯ a else g j_1 ⋯ : κ j_1)) j hj ∈ t j

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓
          s.attach.inf
            ((fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (b (↑i_1 : ι) ⋯)) ∘ fun (x : ↥s) ↦
              Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) ⋯) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), (↑j : ι) ≠ i
j : ι
hj_1 : j ∈ insert i s
hj : j ∈ s
⊢ (fun (j : ι) (hj : j ∈ insert i s) ↦ (if hji : j = i then cast ⋯ a else g j ⋯ : κ j)) j hj_1 ∈ t j

Tactic:
simpa [ne_of_mem_of_not_mem hj hi] using hg _ _

Premises used: ne_of_mem_of_not_mem
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
⊢ Eq.{u_1 + 1} (α := α) (s.sup fun (i : ι) ↦ (t i).inf (f i))
    ((s.pi (β := κ) t).inf fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.sup fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))

Tactic:
@inf_sup αᵒᵈ _ _ _ _ _ _ _ _

Premises used: Finset.inf_sup, Finset.sup, OrderDual, Finset.inf
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
t : Finset γ
f : β × γ → α
a : α
⊢ (s ×ˢ t).sup f ≤ a ↔ (s.sup fun (i : β) ↦ t.sup fun (i' : γ) ↦ f (i, i')) ≤ a

Tactic:
simp [@forall_comm _ γ]

Premises used: forall_comm
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
t : Finset γ
f : β × γ → α
rw :
  Eq.{u_2 + 1} (α := α) (s.sup fun (i : β) ↦ t.sup fun (i' : γ) ↦ f (i, i'))
    (t.sup fun (i' : γ) ↦ s.sup fun (i : β) ↦ f (i, i'))
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := α) (t.sup fun (c : γ) ↦ s.sup fun (b : β) ↦ f (b, c))
    (t.sup fun (i' : γ) ↦ s.sup fun (i : β) ↦ f (i, i'))
⊢ (s ×ˢ t).sup f = t.sup fun (i' : γ) ↦ s.sup fun (i : β) ↦ f (i, i')

Tactic:
rw [sup_product_left, Finset.sup_comm]

Premises used: Finset.sup_product_left, Finset.sup_comm
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : OrderBot α
inst_3 : OrderBot β
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
obtain : ∀ (a : ι) (ha : a ∈ s), (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i
⊢ (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i

Tactic:
obtain ⟨a, ha⟩ := hs
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : OrderBot α
inst_3 : OrderBot β
s : Finset ι
t : Finset κ
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
obtain : ∀ (b : κ) (hb : b ∈ t), (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i
⊢ (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i

Tactic:
obtain ⟨b, hb⟩ := ht
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : OrderBot α
inst_3 : OrderBot β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
simp : (∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2) ↔ (∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2
⊢ (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i

Tactic:
simp only [Prod.map, Finset.sup_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]

Premises used: and_imp, Prod.map, Prod.forall, Finset.sup_le_iff, Finset.mem_product, Prod.le_def
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : OrderBot α
inst_3 : OrderBot β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) → ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : OrderBot α
inst_3 : OrderBot β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ (∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2) ↔ (∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2

Tactic:
exact ⟨fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩, by simp_all⟩
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
α : Type u_2
ι : Type u_5
κ : Type u_6
inst : DistribLattice α
inst_1 : OrderBot α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
simp_rw : Eq.{u_2 + 1} (α := α) (s.sup fun (i : ι) ↦ f i ⊓ t.sup g) ((s ×ˢ t).sup fun (i : ι × κ) ↦ f i.1 ⊓ g i.2)
simp_rw₁ :
  Eq.{u_2 + 1} (α := α) (s.sup fun (i : ι) ↦ t.sup fun (i_1 : κ) ↦ f i ⊓ g i_1)
    ((s ×ˢ t).sup fun (i : ι × κ) ↦ f i.1 ⊓ g i.2)
⊢ s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun (i : ι × κ) ↦ f i.1 ⊓ g i.2

Tactic:
simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left, sup_product_left]

Premises used: Finset.sup_inf_distrib_left, Finset.sup_product_left, Finset.sup_inf_distrib_right
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
s : Finset β
t : Finset γ
h : (s ×ˢ t).Nonempty
f : β × γ → α
a : α
⊢ (s ×ˢ t).sup' h f ≤ a ↔ (s.sup' ⋯ fun (i : β) ↦ t.sup' ⋯ fun (i' : γ) ↦ f (i, i')) ≤ a

Tactic:
simp [@forall_comm _ γ]

Premises used: forall_comm
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
s : Finset β
t : Finset γ
h : (s ×ˢ t).Nonempty
f : β × γ → α
rw :
  Eq.{u_2 + 1} (α := α) (s.sup' ⋯ fun (i : β) ↦ t.sup' ⋯ fun (i' : γ) ↦ f (i, i'))
    (t.sup' ⋯ fun (i' : γ) ↦ s.sup' ⋯ fun (i : β) ↦ f (i, i'))
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := α) (t.sup' ⋯ fun (c : γ) ↦ s.sup' ⋯ fun (b : β) ↦ f (b, c))
    (t.sup' ⋯ fun (i' : γ) ↦ s.sup' ⋯ fun (i : β) ↦ f (i, i'))
⊢ (s ×ˢ t).sup' h f = t.sup' ⋯ fun (i' : γ) ↦ s.sup' ⋯ fun (i : β) ↦ f (i, i')

Tactic:
rw [sup'_product_left, Finset.sup'_comm]

Premises used: Finset.sup'_product_left, Finset.sup'_comm
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
obtain : ∀ (a : ι) (ha : a ∈ s), (s.sup' ⋯ f, t.sup' ht g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i
⊢ (s.sup' hs f, t.sup' ht g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i

Tactic:
obtain ⟨a, ha⟩ := hs
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Finset ι
t : Finset κ
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
obtain : ∀ (b : κ) (hb : b ∈ t), (s.sup' ⋯ f, t.sup' ⋯ g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i
⊢ (s.sup' ⋯ f, t.sup' ht g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i

Tactic:
obtain ⟨b, hb⟩ := ht
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
simp : ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) ↔ ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2
⊢ (s.sup' ⋯ f, t.sup' ⋯ g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i

Tactic:
simp only [Prod.map, sup'_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]

Premises used: and_imp, Prod.map, Finset.sup'_le_iff, Prod.forall, Finset.mem_product, Prod.le_def
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) → ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) ↔ ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2

Tactic:
exact ⟨by simp_all, fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩⟩
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Finset ι
t : Finset κ
hst : (s ×ˢ t).Nonempty
f : ι → α
g : κ → β
⊢ (s ×ˢ t).sup' hst (Prod.map f g) = (s.sup' ⋯ f, t.sup' ⋯ g)

Tactic:
(prodMk_sup'_sup' _ _ _ _).symm

Premises used: Finset.prodMk_sup'_sup', Eq.symm
-- Module: Mathlib.Data.Finset.Lattice.Prod
Goal:
α : Type u_2
ι : Type u_5
κ : Type u_6
inst : DistribLattice α
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → α
simp_rw :
  Eq.{u_2 + 1} (α := α) (s.sup' hs fun (i : ι) ↦ f i ⊓ t.sup' ht g) ((s ×ˢ t).sup' ⋯ fun (i : ι × κ) ↦ f i.1 ⊓ g i.2)
simp_rw₁ :
  Eq.{u_2 + 1} (α := α) (s.sup' ⋯ fun (x : ι) ↦ t.sup' ht fun (i : κ) ↦ f x ⊓ g i)
    ((s ×ˢ t).sup' ⋯ fun (i : ι × κ) ↦ f i.1 ⊓ g i.2)
⊢ s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' ⋯ fun (i : ι × κ) ↦ f i.1 ⊓ g i.2

Tactic:
simp_rw [Finset.sup'_inf_distrib_right, Finset.sup'_inf_distrib_left, sup'_product_left]

Premises used: Finset.sup'_product_left, Finset.sup'_inf_distrib_right, Finset.sup'_inf_distrib_left
-- Module: Mathlib.Data.Finset.Lattice.Union
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : β → α
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : DecidableEq β
s : Finset γ
t : γ → Finset β
c : α
⊢ (s.biUnion t).sup f ≤ c ↔ (s.sup fun (x : γ) ↦ (t x).sup f) ≤ c

Tactic:
simp [@forall_comm _ β]

Premises used: forall_comm
-- Module: Mathlib.Data.Finset.Lattice.Union
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : β → α
inst : SemilatticeInf α
inst_1 : OrderTop α
inst_2 : DecidableEq β
s : Finset γ
t : γ → Finset β
⊢ (s.biUnion t).inf f = s.inf fun (x : γ) ↦ (t x).inf f

Tactic:
@sup_biUnion αᵒᵈ _ _ _ _ _ _ _ _

Premises used: OrderDual, Finset.sup_biUnion, Finset.inf
-- Module: Mathlib.Data.Finset.Lattice.Union
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
f : β → α
inst_1 : 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:
simp [@forall_comm _ β]

Premises used: forall_comm
-- Module: Mathlib.Data.Finset.Lattice.Union
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeInf α
f : β → α
inst_1 : DecidableEq β
s : Finset γ
Hs : s.Nonempty
t : γ → Finset β
Ht : ∀ (b : γ), (t b).Nonempty
⊢ (s.biUnion t).inf' ⋯ f = s.inf' Hs fun (b : γ) ↦ (t b).inf' ⋯ f

Tactic:
sup'_biUnion (α := αᵒᵈ) _ Hs Ht

Premises used: Finset.inf', WithTop.some, WithTop.untop, OrderDual, Finset.inf, Finset.sup'_biUnion, WithTop
-- Module: Mathlib.Data.Finset.Lattice.Union
Goal:
α : Type u_7
β : Type u_8
inst : DecidableEq β
s : Finset α
t : α → Finset β
h : ∀ (a : β), a ∈ s.sup t ↔ a ∈ s.biUnion t
⊢ s.sup t = s.biUnion t

Tactic:
ext
-- Module: Mathlib.Data.Finset.Lattice.Union
Goal:
α : Type u_7
β : Type u_8
inst : DecidableEq β
s : Finset α
t : α → Finset β
a : β
h : (∃ i ∈ s, a ∈ t i) ↔ a ∈ s.biUnion t
h₁ h₂ : (∃ i ∈ s, a ∈ t i) ↔ ∃ a_1 ∈ s, a ∈ t a_1
⊢ a ∈ s.sup t ↔ a ∈ s.biUnion t

Tactic:
rw [mem_sup, mem_biUnion]

Premises used: Finset.mem_sup, Finset.mem_biUnion
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ s.max = s.sup WithBot.some

Tactic:
rfl

Premises used: Finset.max, rfl
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
⊢ Eq.{u_2 + 1} (α := WithBot α) (Finset.max ∅) ⊥

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.max, Finset.sup, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
⊢ (insert a s).max = max (↑a : WithBot α) s.max

Tactic:
fold_insert_idem

Premises used: Finset.fold_insert_idem, Finset.max, Finset.sup
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
⊢ Finset.max (insert a ∅) = (↑a : WithBot α)

Tactic:
max_insert

Premises used: Finset.max_insert
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
⊢ Finset.max (insert a ∅) = (↑a : WithBot α)

Tactic:
exact max_insert

Premises used: Finset.max_insert
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ Finset.max {a, b} = max (↑a : WithBot α) (↑b : WithBot α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
a : α
h : a ∈ s
⊢ ∃ (b : α), s.max = (↑b : WithBot α)

Tactic:
let ⟨b, h, _⟩ := WithBot.le_iff_forall.1 (le_sup (α := WithBot α) h) _ rfl; ⟨b, h⟩

Premises used: WithBot.some, _private.0.Finset.max_of_mem.match_1, WithBot.le_iff_forall, Exists, Exists.intro, Finset.max, Iff.mp, Eq, rfl, Finset.le_sup
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ ∃ (a : α), s.max = (↑a : WithBot α)

Tactic:
let ⟨_, h⟩ := h
  max_of_mem h

Premises used: WithBot.some, Exists, Finset.max, _private.0.Finset.max_of_nonempty.match_1, Eq, Finset.max_of_mem
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
obtain : ∀ (a : α) (ha : s.max = (↑a : WithBot α)), s = ∅
⊢ s = ∅

Tactic:
obtain ⟨a, ha⟩ := max_of_nonempty H

Premises used: Finset.max_of_nonempty
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
a : α
ha : s.max = (↑a : WithBot α)
⊢ ⊥ = (↑a : WithBot α)

Tactic:
rw [h] at ha
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
a : α
ha : ⊥ = (↑a : WithBot α)
⊢ s = ∅

Tactic:
cases ha
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
H : Finset.max ∅ = (↑a : WithBot α)
⊢ Membership.mem (γ := Finset α) ∅ a

Tactic:
cases H
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
h : a ∉ s
h_1 : ∀ {a : α}, s.max = (↑a : WithBot α) → a ∈ s
⊢ ∀ {a_1 : α}, (insert a s).max = (↑a_1 : WithBot α) → a_1 ∈ insert a s

Tactic:
grind [WithBot.coe_eq_coe]

Premises used: WithBot.coe_eq_coe
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
empty : ∀ {a : α}, Finset.max ∅ = (↑a : WithBot α) → Membership.mem (γ := Finset α) ∅ a
insert :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      (∀ {a : α}, s.max = (↑a : WithBot α) → a ∈ s) →
        ∀ {a_3 : α}, (Insert.insert a s).max = (↑a_3 : WithBot α) → a_3 ∈ Insert.insert a s
⊢ ∀ {a : α}, s.max = (↑a : WithBot α) → a ∈ s

Tactic:
induction s using Finset.induction_on with
  | empty => intro _ H; cases H
  | _ => grind [WithBot.coe_eq_coe]

Premises used: WithBot.coe_eq_coe
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
as : a ∈ s
⊢ (↑a : WithBot α) ≤ s.max

Tactic:
le_sup as

Premises used: Finset.max, Finset.le_sup
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
h : s.max < (↑a : WithBot α)
⊢ a ∉ s

Tactic:
mt le_max h.not_ge

Premises used: mt, LT.lt.not_ge, Finset.le_max
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
a b : α
h₁ : a ∈ s
h₂ : s.max = (↑b : WithBot α)
⊢ a ≤ b

Tactic:
WithBot.coe_le_coe.mp <| (le_max h₁).trans h₂.le

Premises used: Eq.le, WithBot.coe_le_coe, Iff.mp, LE.le.trans, Finset.le_max
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
a b : α
h₁ : b < a
h₂ : s.max = (↑b : WithBot α)
⊢ a ∉ s

Tactic:
Finset.notMem_of_max_lt_coe <| h₂.trans_lt <| WithBot.coe_lt_coe.mpr h₁

Premises used: Iff.mpr, Finset.notMem_of_max_lt_coe, WithBot.coe_lt_coe, Eq.trans_lt
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
⊢ (s ∪ t).max = max s.max t.max

Tactic:
sup_union

Premises used: Finset.sup_union, Finset.max
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
st : s ⊆ t
⊢ s.max ≤ t.max

Tactic:
sup_mono st

Premises used: Finset.sup_mono, Finset.max
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
M : WithBot α
s : Finset α
st : ∀ a ∈ s, (↑a : WithBot α) ≤ M
⊢ s.max ≤ M

Tactic:
Finset.sup_le st

Premises used: Finset.sup_le, Finset.max
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
m : WithBot α
s : Finset α
⊢ s.max ≤ m ↔ ∀ a ∈ s, (↑a : WithBot α) ≤ m

Tactic:
Finset.sup_le_iff

Premises used: Finset.max, Finset.sup_le_iff
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : OrderTop α
s : Finset α
⊢ (∃ b ∈ s, (↑b : WithBot α) = ⊤) ↔ ⊤ ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ s.min = s.inf WithTop.some

Tactic:
rfl

Premises used: Finset.min, rfl
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
⊢ Eq.{u_2 + 1} (α := WithTop α) (Finset.min ∅) ⊤

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.min, Finset.inf, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
⊢ (insert a s).min = min (↑a : WithTop α) s.min

Tactic:
fold_insert_idem

Premises used: Finset.min, Finset.fold_insert_idem, Finset.inf
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
⊢ Finset.min (insert a ∅) = (↑a : WithTop α)

Tactic:
min_insert

Premises used: Finset.min_insert
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a : α
⊢ Finset.min (insert a ∅) = (↑a : WithTop α)

Tactic:
exact min_insert

Premises used: Finset.min_insert
-- Module: Mathlib.Data.Finset.Max
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ Finset.min {a, b} = min (↑a : WithTop α) (↑b : WithTop α)

Tactic:
simp