awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
rw : insert a s₂ ∩ s₁ = insert a (s₁ ∩ s₂)
rw₁ : insert a (s₂ ∩ s₁) = insert a (s₁ ∩ s₂)
⊢ s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)
have rw₂ : insert a (s₁ ∩ s₂) = insert a (s₁ ∩ s₂)
Tactic: rw [inter_comm, insert_inter_of_mem h, inter_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₂
x : α
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂
have this : ¬(x = a ∧ x ∈ s₂)
Tactic: have : ¬(x = a ∧ x ∈ s₂) := by rintro ⟨rfl, H⟩; exact h H
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₁
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂
have rw : insert a s₂ ∩ s₁ = s₁ ∩ s₂
Tactic: rw [inter_comm, insert_inter_of_notMem h, inter_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₁
rw : insert a s₂ ∩ s₁ = s₁ ∩ s₂
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂
have rw₁ : s₂ ∩ s₁ = s₁ ∩ s₂
Tactic: rw [inter_comm, insert_inter_of_notMem h, inter_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₁
rw : insert a s₂ ∩ s₁ = s₁ ∩ s₂
rw₁ : s₂ ∩ s₁ = s₁ ∩ s₂
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂
have rw₂ : s₁ ∩ s₂ = s₁ ∩ s₂
Tactic: rw [inter_comm, insert_inter_of_notMem h, inter_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
⊢ insert a s₁ ∩ s₂ = if a ∈ s₂ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂
have pos : a ∈ s₂ → insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
pos : a ∈ s₂ → insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂)
⊢ insert a s₁ ∩ s₂ = if a ∈ s₂ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂
have neg : a ∉ s₂ → insert a s₁ ∩ s₂ = s₁ ∩ s₂
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
⊢ s₁ ∩ insert a s₂ = if a ∈ s₁ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂
have pos : a ∈ s₁ → s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
pos : a ∈ s₁ → s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)
⊢ s₁ ∩ insert a s₂ = if a ∈ s₁ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂
have neg : a ∉ s₁ → s₁ ∩ insert a s₂ = s₁ ∩ s₂
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
H : a ∈ s
⊢ insert a ∅ ∩ s = insert a ∅
have rw : insert a (∅ ∩ s) = insert a ∅
Tactic: rw [insert_inter_of_mem H, empty_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
H : a ∈ s
rw : insert a (∅ ∩ s) = insert a ∅
⊢ insert a ∅ ∩ s = insert a ∅
have rw₁ : Eq (α := Finset α) (insert a ∅) (insert a ∅)
Tactic: rw [insert_inter_of_mem H, empty_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
H : a ∉ s
⊢ ∀ (x : α), x ∉ {a} ∩ s
have simp : ∀ (x : α), ¬(x = a ∧ x ∈ s)
Tactic: simp only [mem_inter, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ {a} ∩ s = if a ∈ s then {a} else ∅
have pos : ∀ (h : a ∈ s), {a} ∩ s = {a}
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
pos : ∀ (h : a ∈ s), {a} ∩ s = {a}
⊢ {a} ∩ s = if a ∈ s then {a} else ∅
have neg : ∀ (h : a ∉ s), {a} ∩ s = ∅
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s ∩ {a} = {a}
have rw : {a} ∩ s = {a}
Tactic: rw [inter_comm, singleton_inter_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∈ s
rw : {a} ∩ s = {a}
⊢ s ∩ {a} = {a}
have rw₁ : Eq (α := Finset α) {a} {a}
Tactic: rw [inter_comm, singleton_inter_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ s ∩ {a} = ∅
have rw : {a} ∩ s = ∅
Tactic: rw [inter_comm, singleton_inter_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∉ s
rw : {a} ∩ s = ∅
⊢ s ∩ {a} = ∅
have rw₁ : Eq.{u_1 + 1} (α := Finset α) ∅ ∅
Tactic: rw [inter_comm, singleton_inter_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
⊢ s ∩ {a} = if a ∈ s then {a} else ∅
have pos : ∀ (h : a ∈ s), s ∩ {a} = {a}
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
pos : ∀ (h : a ∈ s), s ∩ {a} = {a}
⊢ s ∩ {a} = if a ∈ s then {a} else ∅
have neg : ∀ (h : a ∉ s), s ∩ {a} = ∅
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
⊢ insert a s ∪ t = s ∪ insert a t
have rw : insert a (s ∪ t) = s ∪ insert a t
Tactic: rw [insert_union, union_insert]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
rw : insert a (s ∪ t) = s ∪ insert a t
⊢ insert a s ∪ t = s ∪ insert a t
have rw₁ : insert a (s ∪ t) = insert a (s ∪ t)
Tactic: rw [insert_union, union_insert]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
⊢ (l ++ l').toFinset = l.toFinset ∪ l'.toFinset
have nil : ([] ++ l').toFinset = toFinset [] ∪ l'.toFinset
Tactic: induction l with
  | nil => simp
  | cons hd tl hl => simp [hl]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Lemmas (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
nil : ([] ++ l').toFinset = toFinset [] ∪ l'.toFinset
⊢ (l ++ l').toFinset = l.toFinset ∪ l'.toFinset
have cons : ∀ (hd : α) (tl : List α) (hl : (tl ++ l').toFinset = tl.toFinset ∪ l'.toFinset),
  (hd :: tl ++ l').toFinset = (hd :: tl).toFinset ∪ l'.toFinset
Tactic: induction l with
  | nil => simp
  | cons hd tl hl => simp [hl]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Pi (goal)
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.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 : ι) ⋯))
have insert : ∀ (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 : ι) sorry))),
  Eq.{u_1 + 1} (α := α) ((insert i s).inf fun (i : ι) ↦ (t i).sup (f i))
    (((insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ insert i s → κ a) ↦
      (insert i s).attach.inf fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) sorry))
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih => ?_
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Pi (goal)
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 : ι) ⋯))
⊢ Eq.{u_1 + 1} (α := α) ((insert i s).inf fun (i : ι) ↦ (t i).sup (f i))
    (((insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ insert i s → κ a) ↦
      (insert i s).attach.inf fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) ⋯))
have insert : Eq.{u_1 + 1} (α := α)
  ((t i ×ˢ s.pi (β := κ) t).sup fun (i_1 : κ i × ((a : ι) → a ∈ s → κ a)) ↦
    f i i_1.1 ⊓ s.attach.inf fun (i_2 : ↥s) ↦ f (↑i_2 : ι) (i_1.2 (↑i_2 : ι) sorry))
  (((insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ insert i s → κ a) ↦
    inf
      (insert (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) i sorry)
        (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) sorry) s.attach))
      fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) sorry))
Tactic: rw [inf_insert, ih, attach_insert, sup_inf_sup]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Pi (goal)
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 : ι) ⋯))
⊢ Eq.{u_1 + 1} (α := α)
    ((t i ×ˢ s.pi (β := κ) t).sup fun (i_1 : κ i × ((a : ι) → a ∈ s → κ a)) ↦
      f i i_1.1 ⊓ s.attach.inf fun (i_2 : ↥s) ↦ f (↑i_2 : ι) (i_1.2 (↑i_2 : ι) ⋯))
    (((insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ insert i s → κ a) ↦
      inf
        (insert (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) i ⋯)
          (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) ⋯) s.attach))
        fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) ⋯))
have insert : ∀ (c : α),
  ((t i ×ˢ s.pi (β := κ) t).sup fun (i_1 : κ i × ((a : ι) → a ∈ s → κ a)) ↦
        f i i_1.1 ⊓ s.attach.inf fun (i_2 : ↥s) ↦ f (↑i_2 : ι) (i_1.2 (↑i_2 : ι) sorry)) ≤
      c ↔
    (((insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ insert i s → κ a) ↦
        inf
          (insert (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) i sorry)
            (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) sorry) s.attach))
          fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) sorry)) ≤
      c
Tactic: refine eq_of_forall_ge_iff fun c => ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Pi (goal)
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 : α
⊢ ((t i ×ˢ s.pi (β := κ) t).sup fun (i_1 : κ i × ((a : ι) → a ∈ s → κ a)) ↦
        f i i_1.1 ⊓ s.attach.inf fun (i_2 : ↥s) ↦ f (↑i_2 : ι) (i_1.2 (↑i_2 : ι) ⋯)) ≤
      c ↔
    (((insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ insert i s → κ a) ↦
        inf
          (insert (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) i ⋯)
            (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) ⋯) s.attach))
          fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) ⋯)) ≤
      c
have insert : (∀ (a : κ i) (b : (a : ι) → a ∈ s → κ a),
    a ∈ t i →
      (∀ (a : ι) (h : a ∈ s), b a h ∈ t a) → (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (b (↑i : ι) sorry)) ≤ c) ↔
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i sorry) ⊓
          s.attach.inf
            ((fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (b (↑i_1 : ι) sorry)) ∘ fun (x : ↥s) ↦
              Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) sorry) ≤
        c
Tactic: simp only [Finset.sup_le_iff, mem_product, mem_pi, and_imp, Prod.forall,
    inf_insert, inf_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Pi (goal)
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 : α
⊢ (∀ (a : κ i) (b : (a : ι) → a ∈ s → κ a),
      a ∈ t i →
        (∀ (a : ι) (h : a ∈ s), b a h ∈ t a) → (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (b (↑i : ι) ⋯)) ≤ c) ↔
    ∀ (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
have insert : ∀
  (h :
    ∀ (b : (a : ι) → a ∈ insert i s → κ a),
      (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
        f i (b i sorry) ⊓
            s.attach.inf
              ((fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (b (↑i_1 : ι) sorry)) ∘ fun (x : ↥s) ↦
                Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) sorry) ≤
          c)
  (a : κ i) (g : (a : ι) → a ∈ s → κ a) (ha : a ∈ t i) (hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a),
  (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) sorry)) ≤ c
Tactic: refine
    ⟨fun h g hg =>
      h (g i <| mem_insert_self _ _) (fun j hj => g j <| mem_insert_of_mem hj)
        (hg _ <| mem_insert_self _ _) fun j hj => hg _ <| mem_insert_of_mem hj,
      fun h a g ha hg => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Pi (hypothesis)
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
⊢ (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯)) ≤ c
have aux : ∀ (j : ↥s), (↑j : ι) ≠ i
Tactic: have aux : ∀ j : { x // x ∈ s }, ↑j ≠ i := fun j : s => ne_of_mem_of_not_mem j.2 hi
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Pi (goal)
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
⊢ (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯)) ≤ c
have insert : ∀
  (this :
    f i ((fun (j : ι) (hj : j ∈ insert i s) ↦ (if hji : j = i then cast sorry a else g j sorry : κ j)) i sorry) ⊓
        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 sorry a else g j sorry : κ j)) (↑i_1 : ι) sorry)) ∘
            fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) sorry) ≤
      c),
  (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) sorry)) ≤ c
Tactic: have := h (fun j hj => if hji : j = i then cast (congr_arg κ hji.symm) a
      else g _ <| mem_of_mem_insert_of_ne hj hji) (fun j hj => ?_)
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Pi (goal)
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
insert :
  ∀
    (this :
      f i ((fun (j : ι) (hj : j ∈ Insert.insert i s) ↦ (if hji : j = i then cast ⋯ a else g j ⋯ : κ j)) i ⋯) ⊓
          s.attach.inf
            ((fun (i_1 : ↥(Insert.insert i s)) ↦
                f (↑i_1 : ι)
                  ((fun (j : ι) (hj : j ∈ Insert.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.insert i s) (↑x : ι) ⋯) ≤
        c),
    (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯)) ≤ c
⊢ (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯)) ≤ c
have insert₁ : ∀ (j : ι) (hj : j ∈ Insert.insert i s),
  (fun (j : ι) (hj : j ∈ Insert.insert i s) ↦ (if hji : j = i then cast sorry a else g j sorry : κ j)) j hj ∈ t j
Tactic: have := h (fun j hj => if hji : j = i then cast (congr_arg κ hji.symm) a
      else g _ <| mem_of_mem_insert_of_ne hj hji) (fun j hj => ?_)
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Pi (hypothesis)
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
⊢ (fun (j : ι) (hj : j ∈ insert i s) ↦ (if hji : j = i then cast ⋯ a else g j ⋯ : κ j)) j hj ∈ t j
have hj₁ : j = i ∨ j ∈ s
Tactic: rw [mem_insert] at hj
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Pi (goal)
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 = i ∨ 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
have insert : ∀ (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 sorry) ⊓
            s.attach.inf
              ((fun (i : ↥(insert j s)) ↦ f (↑i : ι) (b (↑i : ι) sorry)) ∘ fun (x : ↥s) ↦
                Subtype.mk (p := fun (x : ι) ↦ x ∈ insert j s) (↑x : ι) sorry) ≤
          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 sorry a else g j_1 sorry : κ j_1)) j hj ∈ t j
Tactic: obtain (rfl | hj) := hj
Cleared hypotheses: i, hi, h, a, ha, aux, hj_1, hj
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Pi (goal)
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
⊢ (fun (j : ι) (hj : j ∈ Insert.insert i s) ↦ (if hji : j = i then cast ⋯ a else g j ⋯ : κ j)) j hj_1 ∈ t j
have insert₁ : ∀ (hj : j ∈ s),
  (fun (j : ι) (hj : j ∈ Insert.insert i s) ↦ (if hji : j = i then cast sorry a else g j sorry : κ j)) j hj_1 ∈ t j
Tactic: obtain (rfl | hj) := hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
inst_1 : OrderBot α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ (s ×ˢ t).sup f = t.sup fun (i' : γ) ↦ s.sup fun (i : β) ↦ f (i, i')
have 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'))
Tactic: rw [sup_product_left, Finset.sup_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
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'))
⊢ (s ×ˢ t).sup f = t.sup fun (i' : γ) ↦ s.sup fun (i : β) ↦ f (i, i')
have 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'))
Tactic: rw [sup_product_left, Finset.sup_comm]