awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
s t : Finset α
a : α
inst_1 : DecidableEq α
rw :
  Membership.mem (γ := UpperSet α) (upperClosure ((↑s : Set α) ∪ (↑t : Set α))) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∨
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
rw₁ :
  Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α) ⊓ upperClosure (↑t : Set α)) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∨
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
⊢ Membership.mem (γ := UpperSet α) (upperClosure (↑(s ∪ t) : Set α)) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∨
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
have rw₂ : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∨
    Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a ↔
  Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∨
    Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
Tactic: rw [coe_union, upperClosure_union, UpperSet.mem_inf_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
⊢ s.truncatedInf a ≤ a
have unfold : (if h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a then {b ∈ s | b ≤ a}.inf' sorry id else ⊥) ≤ a
Tactic: unfold truncatedInf
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
⊢ (if h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a then {b ∈ s | b ≤ a}.inf' ⋯ id else ⊥) ≤ a
have pos : ∀ (h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a), {b ∈ s | b ≤ a}.inf' sorry id ≤ a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
pos : ∀ (h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a), {b ∈ s | b ≤ a}.inf' ⋯ id ≤ a
⊢ (if h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a then {b ∈ s | b ≤ a}.inf' ⋯ id else ⊥) ≤ a
have neg : ∀ (h : a ∉ upperClosure (↑s : Set α)), ⊥ ≤ a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
⊢ {b ∈ s | b ≤ a}.inf' ⋯ id ≤ a
have pos : ∀ (b : α) (hb : b ∈ (↑s : Set α)) (hba : b ≤ a), {b ∈ s | b ≤ a}.inf' sorry id ≤ a
Tactic: obtain ⟨b, hb, hba⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
b a : α
⊢ truncatedInf {b} a = if b ≤ a then b else ⊥
have simp : (if h : b ≤ a then inf' ({b ∈ {b} | b ≤ a}) sorry fun (x : α) ↦ x else ⊥) = if b ≤ a then b else ⊥
Tactic: simp only [truncatedInf, coe_singleton, upperClosure_singleton, UpperSet.mem_Ici_iff,
    id_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
b a : α
⊢ (if h : b ≤ a then inf' ({b ∈ {b} | b ≤ a}) ⋯ fun (x : α) ↦ x else ⊥) = if b ≤ a then b else ⊥
have pos : b ≤ a → (inf' ({b ∈ {b} | b ≤ a}) sorry fun (x : α) ↦ x) = b
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
b a : α
pos : b ≤ a → (inf' ({b ∈ {b} | b ≤ a}) ⋯ fun (x : α) ↦ x) = b
⊢ (if h : b ≤ a then inf' ({b ∈ {b} | b ≤ a}) ⋯ fun (x : α) ↦ x else ⊥) = if b ≤ a then b else ⊥
have neg : ¬b ≤ a → Eq.{u_1 + 1} (α := α) ⊥ ⊥
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
inst_2 : BoundedOrder β
inst_3 : DecidableLE β
inst_4 : DecidableLE α
inst_5 : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
⊢ (e : (a : α) → β) (s.truncatedInf a) =
    (map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s).truncatedInf
      ((e : (a : α) → β) a)
have this : Membership.mem (α := β) (γ := UpperSet β)
    (upperClosure
      (↑(map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s) : Set β))
    ((e : (a : α) → β) a : β) ↔
  Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
Tactic: have : e a ∈ upperClosure (s.map e.toEquiv.toEmbedding) ↔ a ∈ upperClosure s := by simp
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
inst_2 : BoundedOrder β
inst_3 : DecidableLE β
inst_4 : DecidableLE α
inst_5 : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
this :
  Membership.mem (α := β) (γ := UpperSet β)
      (upperClosure
        (↑(map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s) : Set β))
      ((e : (a : α) → β) a : β) ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
⊢ (e : (a : α) → β) (s.truncatedInf a) =
    (map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s).truncatedInf
      ((e : (a : α) → β) a)
have simp_rw : Eq.{u_2 + 1} (α := β)
  (if h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a then
    {b ∈ s | b ≤ a}.inf' sorry ((⇑e : (a : α) → β) ∘ id)
  else ⊥)
  (if h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a then
    {b ∈ map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s |
          b ≤ (e : (a : α) → β) a}.inf'
      sorry id
  else ⊥)
Tactic: simp_rw [truncatedInf, apply_dite e, map_finset_inf', map_bot, this]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
inst_2 : BoundedOrder β
inst_3 : DecidableLE β
inst_4 : DecidableLE α
inst_5 : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
this :
  Membership.mem (α := β) (γ := UpperSet β)
      (upperClosure
        (↑(map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s) : Set β))
      ((e : (a : α) → β) a : β) ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
⊢ Eq.{u_2 + 1} (α := β)
    (if h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a then
      {b ∈ s | b ≤ a}.inf' ⋯ ((⇑e : (a : α) → β) ∘ id)
    else ⊥)
    (if h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a then
      {b ∈ map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s |
            b ≤ (e : (a : α) → β) a}.inf'
        ⋯ id
    else ⊥)
have e_t : ∀ (h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a),
  {b ∈ s | b ≤ a}.inf' sorry ((⇑e : (a : α) → β) ∘ id) =
    {b ∈ map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s |
          b ≤ (e : (a : α) → β) a}.inf'
      sorry id
Tactic: congr with h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑s : Set α)
ha : a ∈ s
⊢ s.truncatedInf a = a
have refine : a ≤ s.truncatedInf a
Tactic: refine le_antisymm truncatedInf_le ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑s : Set α)
ha : a ∈ s
⊢ a ≤ s.truncatedInf a
have simp_rw : ∀ (b : α), b ∈ s ∧ b ≤ a → a ≤ id b
Tactic: simp_rw [truncatedInf_of_mem (subset_upperClosure ha), le_inf'_iff, mem_filter]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
Goal:
α : Type u_1
inst : SemilatticeInf α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
inst_3 : DecidableEq α
hs : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
ht : a ∉ upperClosure (↑t : Set α)
⊢ (s ∪ t).truncatedInf a = s.truncatedInf a
have ht₁ : ∀ x ∈ t, ¬x ≤ a
Tactic: simp only [mem_upperClosure, mem_coe, not_exists, not_and] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
inst_3 : DecidableEq α
hs : a ∉ upperClosure (↑s : Set α)
ht : Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
⊢ (s ∪ t).truncatedInf a = t.truncatedInf a
have rw : (t ∪ s).truncatedInf a = t.truncatedInf a
Tactic: rw [union_comm, truncatedInf_union_left ht hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
inst_3 : DecidableEq α
hs : a ∉ upperClosure (↑s : Set α)
ht : Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
rw : (t ∪ s).truncatedInf a = t.truncatedInf a
⊢ (s ∪ t).truncatedInf a = t.truncatedInf a
have rw₁ : t.truncatedInf a = t.truncatedInf a
Tactic: rw [union_comm, truncatedInf_union_left ht hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
inst_3 : DecidableEq α
hs : a ∉ upperClosure (↑s : Set α)
ht : a ∉ upperClosure (↑t : Set α)
⊢ a ∉ upperClosure (↑(s ∪ t) : Set α)
have rw : a ∉ upperClosure (↑s : Set α) ⊓ upperClosure (↑t : Set α)
Tactic: rw [coe_union, upperClosure_union]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
⊢ Membership.mem (γ := LowerSet α) (lowerClosure (↑(s ⊼ t) : Set α)) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∧
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
have rw : Membership.mem (γ := LowerSet α) (lowerClosure ((↑s : Set α) ⊼ (↑t : Set α))) a ↔
  Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∧
    Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
Tactic: rw [coe_infs, lowerClosure_infs, LowerSet.mem_inf_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
rw :
  Membership.mem (γ := LowerSet α) (lowerClosure ((↑s : Set α) ⊼ (↑t : Set α))) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∧
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
⊢ Membership.mem (γ := LowerSet α) (lowerClosure (↑(s ⊼ t) : Set α)) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∧
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
have rw₁ : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α) ⊓ lowerClosure (↑t : Set α)) a ↔
  Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∧
    Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
Tactic: rw [coe_infs, lowerClosure_infs, LowerSet.mem_inf_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
rw :
  Membership.mem (γ := LowerSet α) (lowerClosure ((↑s : Set α) ⊼ (↑t : Set α))) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∧
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
rw₁ :
  Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α) ⊓ lowerClosure (↑t : Set α)) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∧
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
⊢ Membership.mem (γ := LowerSet α) (lowerClosure (↑(s ⊼ t) : Set α)) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∧
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
have rw₂ : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∧
    Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a ↔
  Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∧
    Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
Tactic: rw [coe_infs, lowerClosure_infs, LowerSet.mem_inf_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
⊢ Membership.mem (γ := UpperSet α) (upperClosure (↑(s ⊻ t) : Set α)) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∧
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
have rw : Membership.mem (γ := UpperSet α) (upperClosure ((↑s : Set α) ⊻ (↑t : Set α))) a ↔
  Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∧
    Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
Tactic: rw [coe_sups, upperClosure_sups, UpperSet.mem_sup_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
rw :
  Membership.mem (γ := UpperSet α) (upperClosure ((↑s : Set α) ⊻ (↑t : Set α))) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∧
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
⊢ Membership.mem (γ := UpperSet α) (upperClosure (↑(s ⊻ t) : Set α)) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∧
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
have rw₁ : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α) ⊔ upperClosure (↑t : Set α)) a ↔
  Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∧
    Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
Tactic: rw [coe_sups, upperClosure_sups, UpperSet.mem_sup_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
rw :
  Membership.mem (γ := UpperSet α) (upperClosure ((↑s : Set α) ⊻ (↑t : Set α))) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∧
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
rw₁ :
  Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α) ⊔ upperClosure (↑t : Set α)) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∧
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
⊢ Membership.mem (γ := UpperSet α) (upperClosure (↑(s ⊻ t) : Set α)) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∧
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
have rw₂ : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∧
    Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a ↔
  Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∧
    Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
Tactic: rw [coe_sups, upperClosure_sups, UpperSet.mem_sup_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
hs : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
ht : Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
⊢ (s ⊼ t).truncatedSup a = s.truncatedSup a ⊓ t.truncatedSup a
have simp : Eq (α := α) (({b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b}).sup' sorry fun (x : α) ↦ id x)
  (({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' sorry fun (i : α × α) ↦ id i.1 ⊓ id i.2)
Tactic: simp only [truncatedSup_of_mem, hs, ht, infs_aux.2 ⟨hs, ht⟩, sup'_inf_sup', filter_infs_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
hs : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
ht : Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
⊢ Eq (α := α)
    (sup' (image (Function.uncurry fun (x1 x2 : α) ↦ x1 ⊓ x2) ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b})) ⋯ fun (x : α) ↦
      id x)
    (({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ fun (i : α × α) ↦ id i.1 ⊓ id i.2)
have rw : Eq (α := α)
  (({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' sorry ((fun (x : α) ↦ id x) ∘ Function.uncurry fun (x1 x2 : α) ↦ x1 ⊓ x2))
  (({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' sorry fun (i : α × α) ↦ id i.1 ⊓ id i.2)
Tactic: rw [sup'_image]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
hs : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
ht : Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
⊢ (s ⊻ t).truncatedInf a = s.truncatedInf a ⊔ t.truncatedInf a
have simp : Eq (α := α) (({b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a}).inf' sorry fun (x : α) ↦ id x)
  (({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' sorry fun (i : α × α) ↦ id i.1 ⊔ id i.2)
Tactic: simp only [truncatedInf_of_mem, hs, ht, sups_aux.2 ⟨hs, ht⟩, inf'_sup_inf', filter_sups_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
hs : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
ht : Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
⊢ Eq (α := α)
    (inf' (image (Function.uncurry fun (x1 x2 : α) ↦ x1 ⊔ x2) ({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a})) ⋯ fun (x : α) ↦
      id x)
    (({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' ⋯ fun (i : α × α) ↦ id i.1 ⊔ id i.2)
have rw : Eq (α := α)
  (({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' sorry ((fun (x : α) ↦ id x) ∘ Function.uncurry fun (x1 x2 : α) ↦ x1 ⊔ x2))
  (({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' sorry fun (i : α × α) ↦ id i.1 ⊔ id i.2)
Tactic: rw [inf'_image]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
ha : a ∉ lowerClosure (↑s : Set α) ⊓ lowerClosure (↑t : Set α)
⊢ a ∉ lowerClosure (↑(s ⊼ t) : Set α)
have rwa : a ∉ lowerClosure ((↑s : Set α) ⊼ (↑t : Set α))
Tactic: rwa [coe_infs, lowerClosure_infs]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
ha : a ∉ upperClosure (↑s : Set α) ⊔ upperClosure (↑t : Set α)
⊢ a ∉ upperClosure (↑(s ⊻ t) : Set α)
have rwa : a ∉ upperClosure ((↑s : Set α) ⊻ (↑t : Set α))
Tactic: rwa [coe_sups, upperClosure_sups]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have pos : ∀ (h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s),
  #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Tactic: by_cases h𝒜 : s ∈ lowerClosure (𝒜 : Set <| Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
pos :
  ∀ (h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s),
    #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have neg : ∀ (h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))),
  #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Tactic: by_cases h𝒜 : s ∈ lowerClosure (𝒜 : Set <| Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have pos : ∀ (hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s),
  #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Tactic: by_cases hℬ : s ∈ lowerClosure (ℬ : Set <| Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s
pos :
  ∀ (hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s),
    #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have neg : ∀ (hℬ : s ∉ lowerClosure (↑ℬ : Set (Finset α))),
  #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Tactic: by_cases hℬ : s ∈ lowerClosure (ℬ : Set <| Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have pos : ∀ (hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s),
  #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Tactic: by_cases hℬ : s ∈ lowerClosure (ℬ : Set <| Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))
pos :
  ∀ (hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s),
    #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have neg : ∀ (hℬ : s ∉ lowerClosure (↑ℬ : Set (Finset α))),
  #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Tactic: by_cases hℬ : s ∈ lowerClosure (ℬ : Set <| Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s
hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have pos : #(𝒜.truncatedSup s ⊔ ℬ.truncatedSup s) + #(𝒜.truncatedSup s ⊓ ℬ.truncatedSup s) =
  #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Tactic: rw [truncatedSup_union h𝒜 hℬ, truncatedSup_infs h𝒜 hℬ]