awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
h : a ∉ lowerClosure (↑s : Set α)
⊢ a ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : BoundedOrder β
inst_3 : DecidableLE α
inst_4 : OrderTop α
inst_5 : DecidableLE β
e : α ≃o β
s : Finset α
a : α
⊢ Membership.mem (α := β) (γ := LowerSet β)
      (lowerClosure
        (↑(map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s) : Set β))
      ((e : (a : α) → β) a : β) ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : BoundedOrder β
inst_3 : DecidableLE α
inst_4 : OrderTop α
inst_5 : DecidableLE β
e : α ≃o β
s : Finset α
a : α
⊢ Membership.mem (α := β) (γ := LowerSet β)
      (lowerClosure
        (↑(map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s) : Set β))
      ((e : (a : α) → β) a : β) ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a

Tactic:
have : e a ∈ lowerClosure (s.map e.toEquiv.toEmbedding : Set β) ↔ a ∈ lowerClosure s := by simp
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : BoundedOrder β
inst_3 : DecidableLE α
inst_4 : OrderTop α
inst_5 : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this :
  Membership.mem (α := β) (γ := LowerSet β)
      (lowerClosure
        (↑(map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s) : Set β))
      ((e : (a : α) → β) a : β) ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
simp_rw :
  Eq.{u_2 + 1} (α := β)
    (if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then
      {b ∈ s | a ≤ b}.sup' ⋯ ((⇑e : (a : α) → β) ∘ id)
    else ⊤)
    (if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then
      {b ∈ map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s |
            (e : (a : α) → β) a ≤ b}.sup'
        ⋯ id
    else ⊤)
⊢ (e : (a : α) → β) (s.truncatedSup a) =
    (map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s).truncatedSup
      ((e : (a : α) → β) a)

Tactic:
simp_rw [truncatedSup, apply_dite e, map_finset_sup', map_top, this]

Premises used: apply_dite, map_finset_sup', Finset.truncatedSup, TopHomClass.map_top, DFunLike.coe
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : BoundedOrder β
inst_3 : DecidableLE α
inst_4 : OrderTop α
inst_5 : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this :
  Membership.mem (α := β) (γ := LowerSet β)
      (lowerClosure
        (↑(map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s) : Set β))
      ((e : (a : α) → β) a : β) ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
e_t :
  ∀ (h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a),
    {b ∈ s | a ≤ b}.sup' ⋯ ((⇑e : (a : α) → β) ∘ id) =
      {b ∈ map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s |
            (e : (a : α) → β) a ≤ b}.sup'
        ⋯ id
⊢ Eq.{u_2 + 1} (α := β)
    (if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then
      {b ∈ s | a ≤ b}.sup' ⋯ ((⇑e : (a : α) → β) ∘ id)
    else ⊤)
    (if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then
      {b ∈ map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s |
            (e : (a : α) → β) a ≤ b}.sup'
        ⋯ id
    else ⊤)

Tactic:
congr with h
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : BoundedOrder β
inst_3 : DecidableLE α
inst_4 : OrderTop α
inst_5 : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this :
  Membership.mem (α := β) (γ := LowerSet β)
      (lowerClosure
        (↑(map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s) : Set β))
      ((e : (a : α) → β) a : β) ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
⊢ {b ∈ s | a ≤ b}.sup' ⋯ ((⇑e : (a : α) → β) ∘ id) =
    {b ∈ map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s |
          (e : (a : α) → β) a ≤ b}.sup'
      ⋯ id

Tactic:
simp only [filter_map, Function.comp_def, Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv,
    OrderIso.le_iff_le, id, sup'_map]

Premises used: Equiv.coe_toEmbedding, id, OrderIso.le_iff_le, Function.comp_def, Finset.sup'_map, RelIso.coe_fn_toEquiv, Finset.filter_map
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑s : Set α)
ha : a ∈ s
⊢ s.truncatedSup a = a

Tactic:
le_antisymm ?_ le_truncatedSup

Premises used: Finset.le_truncatedSup, le_antisymm
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑s : Set α)
ha : a ∈ s
refine : s.truncatedSup a ≤ a
⊢ s.truncatedSup a = a

Tactic:
refine le_antisymm ?_ le_truncatedSup

Premises used: Finset.le_truncatedSup, le_antisymm
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑s : Set α)
ha : a ∈ s
simp_rw : ∀ (b : α), b ∈ s ∧ a ≤ b → id b ≤ a
⊢ s.truncatedSup a ≤ a

Tactic:
simp_rw [truncatedSup_of_mem (subset_lowerClosure ha), sup'_le_iff, mem_filter]

Premises used: subset_lowerClosure, Finset.truncatedSup_of_mem, Finset.sup'_le_iff, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑s : Set α)
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ id b ≤ a

Tactic:
(hs.eq ha hb hab).ge

Premises used: Eq.ge, IsAntichain.eq
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑s : Set α)
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ id b ≤ a

Tactic:
exact (hs.eq ha hb hab).ge

Premises used: Eq.ge, IsAntichain.eq
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
inst_3 : DecidableEq α
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

Tactic:
simpa only [truncatedSup_of_mem, hs, ht, lower_aux.2 (Or.inl hs), filter_union] using
    sup'_union _ _ _

Premises used: Iff.mpr, _private.0.Finset.lower_aux, Finset.truncatedSup_of_mem, Finset.sup'_union, Or.inl, Finset.filter_union
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
inst_3 : DecidableEq α
hs : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
ht : a ∉ lowerClosure (↑t : Set α)
⊢ ∀ x ∈ t, ¬a ≤ x

Tactic:
simp only [mem_lowerClosure, mem_coe, not_exists, not_and] at ht

Premises used: not_exists, mem_lowerClosure, not_and, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
inst_3 : DecidableEq α
hs : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
ht : ∀ x ∈ t, ¬a ≤ x
⊢ (s ∪ t).truncatedSup a = s.truncatedSup a

Tactic:
simp only [truncatedSup_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty,
    lower_aux.2 (Or.inl hs)]

Premises used: Iff.mpr, _private.0.Finset.lower_aux, Finset.truncatedSup_of_mem, Finset.filter_false_of_mem, Finset.union_empty, Or.inl, Finset.filter_union
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
inst_3 : DecidableEq α
hs : a ∉ lowerClosure (↑s : Set α)
ht : Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
rw : (t ∪ s).truncatedSup a = t.truncatedSup a
rw₁ rw₂ : t.truncatedSup a = t.truncatedSup a
⊢ (s ∪ t).truncatedSup a = t.truncatedSup a

Tactic:
rw [union_comm, truncatedSup_union_left ht hs]

Premises used: Finset.union_comm, Finset.truncatedSup_union_left
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
inst_3 : DecidableEq α
hs : a ∉ lowerClosure (↑s : Set α)
ht : a ∉ lowerClosure (↑t : Set α)
⊢ (s ∪ t).truncatedSup a = ⊤

Tactic:
truncatedSup_of_notMem fun h ↦ (lower_aux.1 h).elim hs ht

Premises used: _private.0.Finset.lower_aux, Iff.mp, Or.elim, Finset.truncatedSup_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
⊢ Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a → {b ∈ s | b ≤ a}.Nonempty

Tactic:
fun ⟨b, hb, hab⟩ ↦ ⟨b, mem_filter.2 ⟨hb, hab⟩⟩

Premises used: Iff.mpr, LE.le, And.intro, Exists.intro, Finset.Nonempty, Finset.mem_filter, _private.0.Finset.inf_aux.match_1, Finset.filter
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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
rw₂ 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
⊢ Membership.mem (γ := UpperSet α) (upperClosure (↑(s ∪ 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]

Premises used: UpperSet.mem_inf_iff, upperClosure_union, Finset.coe_union
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
⊢ s.truncatedInf a = {b ∈ s | b ≤ a}.inf' ⋯ id

Tactic:
dif_pos h

Premises used: Finset.truncatedInf, dif_pos
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
h : a ∉ upperClosure (↑s : Set α)
⊢ s.truncatedInf a = ⊥

Tactic:
dif_neg h

Premises used: Finset.truncatedInf, dif_neg
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
unfold :
  (if h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a then {b ∈ s | b ≤ a}.inf' ⋯ id else ⊥) ≤ a
⊢ s.truncatedInf a ≤ a

Tactic:
unfold truncatedInf

Premises used: Finset.truncatedInf
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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
neg : ∀ (h : a ∉ upperClosure (↑s : Set α)), ⊥ ≤ a
⊢ (if h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a then {b ∈ s | b ≤ a}.inf' ⋯ id else ⊥) ≤ a

Tactic:
split_ifs with h
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
pos : ∀ (b : α) (hb : b ∈ (↑s : Set α)) (hba : b ≤ a), {b ∈ s | b ≤ a}.inf' ⋯ id ≤ a
⊢ {b ∈ s | b ≤ a}.inf' ⋯ id ≤ a

Tactic:
obtain ⟨b, hb, hba⟩ := h
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
b : α
hb : b ∈ (↑s : Set α)
hba : b ≤ a
⊢ {b ∈ s | b ≤ a}.inf' ⋯ id ≤ a

Tactic:
hba.trans' <| inf'_le id <| mem_filter.2 ⟨hb, ‹_›⟩

Premises used: Iff.mpr, id, And.intro, Finset.mem_filter, LE.le.trans', Finset.inf'_le
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
b : α
hb : b ∈ (↑s : Set α)
hba : b ≤ a
⊢ {b ∈ s | b ≤ a}.inf' ⋯ id ≤ a

Tactic:
exact hba.trans' <| inf'_le id <| mem_filter.2 ⟨hb, ‹_›⟩

Premises used: Iff.mpr, id, And.intro, Finset.mem_filter, LE.le.trans', Finset.inf'_le
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
h : a ∉ upperClosure (↑s : Set α)
⊢ ⊥ ≤ a

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
h : a ∉ upperClosure (↑s : Set α)
⊢ ⊥ ≤ a

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
a : α
⊢ a ∉ upperClosure (↑∅ : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
b a : α
simp : (if h : b ≤ a then inf' ({b ∈ {b} | b ≤ a}) ⋯ fun (x : α) ↦ x else ⊥) = if b ≤ a then b else ⊥
⊢ truncatedInf {b} a = if b ≤ a then b else ⊥

Tactic:
simp only [truncatedInf, coe_singleton, upperClosure_singleton, UpperSet.mem_Ici_iff,
    id_eq]

Premises used: Finset.coe_singleton, Finset.truncatedInf, upperClosure_singleton, UpperSet.mem_Ici_iff, id_eq
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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
neg : ¬b ≤ a → Eq.{u_1 + 1} (α := α) ⊥ ⊥
⊢ (if h : b ≤ a then inf' ({b ∈ {b} | b ≤ a}) ⋯ fun (x : α) ↦ x else ⊥) = if b ≤ a then b else ⊥

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
b a : α
h : b ≤ a
⊢ (inf' ({b ∈ {b} | b ≤ a}) ⋯ fun (x : α) ↦ x) = b

Tactic:
simp [Finset.filter_true_of_mem, *]

Premises used: Finset.filter_true_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
b a : α
h : ¬b ≤ a
⊢ Eq.{u_1 + 1} (α := α) ⊥ ⊥

Tactic:
simp [Finset.filter_true_of_mem, *]

Premises used: Finset.filter_true_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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 : α
⊢ 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:
simp
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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 : α
⊢ 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
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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
simp_rw :
  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 ⊥)
⊢ (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)

Tactic:
simp_rw [truncatedInf, apply_dite e, map_finset_inf', map_bot, this]

Premises used: apply_dite, Finset.truncatedInf, map_finset_inf', BotHomClass.map_bot, DFunLike.coe
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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_t :
  ∀ (h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a),
    {b ∈ s | b ≤ a}.inf' ⋯ ((⇑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'
        ⋯ id
⊢ 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 ⊥)

Tactic:
congr with h
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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
h : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
⊢ {b ∈ s | b ≤ a}.inf' ⋯ ((⇑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'
      ⋯ id

Tactic:
simp only [filter_map, Function.comp_def, Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv,
    OrderIso.le_iff_le, id, inf'_map]

Premises used: Equiv.coe_toEmbedding, Finset.inf'_map, id, OrderIso.le_iff_le, Function.comp_def, RelIso.coe_fn_toEquiv, Finset.filter_map
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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

Tactic:
le_antisymm truncatedInf_le ?_

Premises used: Finset.truncatedInf_le, le_antisymm
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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
refine : a ≤ s.truncatedInf a
⊢ s.truncatedInf a = a

Tactic:
refine le_antisymm truncatedInf_le ?_

Premises used: Finset.truncatedInf_le, le_antisymm
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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
simp_rw : ∀ (b : α), b ∈ s ∧ b ≤ a → a ≤ id b
⊢ a ≤ s.truncatedInf a

Tactic:
simp_rw [truncatedInf_of_mem (subset_upperClosure ha), le_inf'_iff, mem_filter]

Premises used: Finset.le_inf'_iff, subset_upperClosure, Finset.mem_filter, Finset.truncatedInf_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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
b : α
hb : b ∈ s
hba : b ≤ a
⊢ a ≤ id b

Tactic:
(hs.eq hb ha hba).ge

Premises used: Eq.ge, IsAntichain.eq
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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
b : α
hb : b ∈ s
hba : b ≤ a
⊢ a ≤ id b

Tactic:
exact (hs.eq hb ha hba).ge

Premises used: Eq.ge, IsAntichain.eq
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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 : Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
⊢ (s ∪ t).truncatedInf a = s.truncatedInf a ⊓ t.truncatedInf a

Tactic:
simpa only [truncatedInf_of_mem, hs, ht, upper_aux.2 (Or.inl hs), filter_union] using
    inf'_union _ _ _

Premises used: Iff.mpr, _private.0.Finset.upper_aux, Or.inl, Finset.filter_union, Finset.inf'_union, Finset.truncatedInf_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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 α)
⊢ ∀ x ∈ t, ¬x ≤ a

Tactic:
simp only [mem_upperClosure, mem_coe, not_exists, not_and] at ht

Premises used: not_exists, not_and, Finset.mem_coe, mem_upperClosure