awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
β : Type u_2
inst : CommSemiring β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : 0 < c₀ * d₁
calc : (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁) = a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀)
calc₁ : a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁) = a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁)
calc₂ : a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁) ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁)
⊢ (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁) ≤ (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁)
have calc₃ : c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁) = (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁)
Tactic: calc (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁)
      = a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀) := by ring
    _ ≤ a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁) := mul_add_mul_le_mul_add_mul h₀₁ h₁₀
    _ = a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁) := by ring
    _ ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁) := by gcongr
    _ = (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁) := by ring
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
⊢ {t ∈ 𝒜 | t.erase a = s} =
    if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅
have h : ∀ (t : Finset α),
  t ∈ {t ∈ 𝒜 | t.erase a = s} ↔
    Membership.mem (γ := Finset (Finset α))
      (if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔
    Membership.mem (γ := Finset (Finset α))
      (if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅) t
have pos : s ∈ 𝒜 → insert a s ∈ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s, insert a s} t)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
pos : s ∈ 𝒜 → insert a s ∈ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s, insert a s} t)
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔
    Membership.mem (γ := Finset (Finset α))
      (if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅) t
have neg : s ∈ 𝒜 → insert a s ∉ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s} t)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
pos : s ∈ 𝒜 → insert a s ∈ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s, insert a s} t)
neg : s ∈ 𝒜 → insert a s ∉ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s} t)
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔
    Membership.mem (γ := Finset (Finset α))
      (if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅) t
have pos₁ : s ∉ 𝒜 → insert a s ∈ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {insert a s} t)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
pos : s ∈ 𝒜 → insert a s ∈ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s, insert a s} t)
neg : s ∈ 𝒜 → insert a s ∉ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s} t)
pos₁ : s ∉ 𝒜 → insert a s ∈ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {insert a s} t)
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔
    Membership.mem (γ := Finset (Finset α))
      (if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅) t
have neg₁ : s ∉ 𝒜 → insert a s ∉ 𝒜 → (t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) ∅ t)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h : s ∈ 𝒜
h_1 : insert a s ∈ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s, insert a s} t
have pos : t = s ∨ t = insert a s → t ∈ 𝒜
Tactic: simp [erase_eq_iff ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h : s ∈ 𝒜
h_1 : insert a s ∉ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {s} t
have neg : t ∈ 𝒜 ∧ (t = s ∨ t = insert a s) ↔ t = s
Tactic: simp [erase_eq_iff ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h : s ∉ 𝒜
h_1 : insert a s ∈ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) {insert a s} t
have pos : t ∈ 𝒜 ∧ (t = s ∨ t = insert a s) ↔ t = insert a s
Tactic: simp [erase_eq_iff ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h : s ∉ 𝒜
h_1 : insert a s ∉ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ Membership.mem (γ := Finset (Finset α)) ∅ t
have neg : t ∈ 𝒜 → ¬t = s ∧ ¬t = insert a s
Tactic: simp [erase_eq_iff ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
⊢ collapse 𝒜 a f s = (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
have rw : ∑ t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅,
    f t =
  (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
Tactic: rw [collapse, filter_collapse_eq ha]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
⊢ ∑ t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅,
      f t =
    (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
have pos : s ∈ 𝒜 → insert a s ∈ 𝒜 → ∑ x ∈ {s, insert a s}, f x = f s + f (insert a s)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
pos : s ∈ 𝒜 → insert a s ∈ 𝒜 → ∑ x ∈ {s, insert a s}, f x = f s + f (insert a s)
⊢ ∑ t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅,
      f t =
    (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
have neg : s ∈ 𝒜 → insert a s ∉ 𝒜 → ∑ x ∈ {s}, f x = f s + 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
pos : s ∈ 𝒜 → insert a s ∈ 𝒜 → ∑ x ∈ {s, insert a s}, f x = f s + f (insert a s)
neg : s ∈ 𝒜 → insert a s ∉ 𝒜 → ∑ x ∈ {s}, f x = f s + 0
⊢ ∑ t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅,
      f t =
    (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
have pos₁ : s ∉ 𝒜 → insert a s ∈ 𝒜 → ∑ x ∈ {insert a s}, f x = 0 + f (insert a s)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
pos : s ∈ 𝒜 → insert a s ∈ 𝒜 → ∑ x ∈ {s, insert a s}, f x = f s + f (insert a s)
neg : s ∈ 𝒜 → insert a s ∉ 𝒜 → ∑ x ∈ {s}, f x = f s + 0
pos₁ : s ∉ 𝒜 → insert a s ∈ 𝒜 → ∑ x ∈ {insert a s}, f x = 0 + f (insert a s)
⊢ ∑ t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅,
      f t =
    (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
have neg₁ : s ∉ 𝒜 → insert a s ∉ 𝒜 → ∑ x ∈ ∅, f x = HAdd.hAdd (α := β) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t u : Finset α
ha : a ∉ s
ht : t ∈ 𝒜
hu : u ∈ 𝒜
hts : t = s
hus : u = insert a s
⊢ collapse 𝒜 a f s = f t + f u
have subst : ∀ (ha : a ∉ t) (hus : u = insert a t), collapse 𝒜 a f t = f t + f u
Tactic: subst hts
Cleared hypotheses: s, ha, hts, hus
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t u : Finset α
ht : t ∈ 𝒜
hu : u ∈ 𝒜
ha : a ∉ t
hus : u = insert a t
⊢ collapse 𝒜 a f t = f t + f u
have subst : ∀ (hu : insert a t ∈ 𝒜), collapse 𝒜 a f t = f t + f (insert a t)
Tactic: subst hus
Cleared hypotheses: u, hu, hus
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
ht : t ∈ 𝒜
ha : a ∉ t
hu : insert a t ∈ 𝒜
⊢ collapse 𝒜 a f t = f t + f (insert a t)
have simp_rw : ((if t ∈ 𝒜 then f t else 0) + if insert a t ∈ 𝒜 then f (insert a t) else 0) = f t + f (insert a t)
Tactic: simp_rw [collapse_eq ha, if_pos ht, if_pos hu]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
ht : t ∈ 𝒜
ha : a ∉ t
hu : insert a t ∈ 𝒜
simp_rw : ((if t ∈ 𝒜 then f t else 0) + if insert a t ∈ 𝒜 then f (insert a t) else 0) = f t + f (insert a t)
⊢ collapse 𝒜 a f t = f t + f (insert a t)
have simp_rw₁ : (f t + if insert a t ∈ 𝒜 then f (insert a t) else 0) = f t + f (insert a t)
Tactic: simp_rw [collapse_eq ha, if_pos ht, if_pos hu]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = s
ht : t ∈ 𝒜
⊢ f t ≤ collapse 𝒜 a f s
have subst : ∀ (ha : a ∉ t), f t ≤ collapse 𝒜 a f t
Tactic: subst hts
Cleared hypotheses: s, ha, hts
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
⊢ f t ≤ collapse 𝒜 a f t
have rw : f t ≤ f t + if insert a t ∈ 𝒜 then f (insert a t) else 0
Tactic: rw [collapse_eq ha, if_pos ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
⊢ f t ≤ f t + if insert a t ∈ 𝒜 then f (insert a t) else 0
have pos : insert a t ∈ 𝒜 → f t ≤ f t + f (insert a t)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
pos : insert a t ∈ 𝒜 → f t ≤ f t + f (insert a t)
⊢ f t ≤ f t + if insert a t ∈ 𝒜 then f (insert a t) else 0
have neg : insert a t ∉ 𝒜 → f t ≤ f t + 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h : insert a t ∉ 𝒜
⊢ f t ≤ f t + 0
have neg : f t ≤ f t
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
⊢ f t ≤ collapse 𝒜 a f s
have rw : f t ≤ (if s ∈ 𝒜 then f s else 0) + f t
Tactic: rw [collapse_eq ha, ← hts, if_pos ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
⊢ f t ≤ (if s ∈ 𝒜 then f s else 0) + f t
have pos : s ∈ 𝒜 → f t ≤ f s + f t
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
pos : s ∈ 𝒜 → f t ≤ f s + f t
⊢ f t ≤ (if s ∈ 𝒜 then f s else 0) + f t
have neg : s ∉ 𝒜 → f t ≤ 0 + f t
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h : s ∉ 𝒜
⊢ f t ≤ 0 + f t
have neg : f t ≤ f t
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have this : s ⊆ insert a u
Tactic: have := hsu.trans <| subset_insert a _
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this : s ⊆ insert a u
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have this₁ : t ⊆ insert a u
Tactic: have := htu.trans <| subset_insert a _
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this : t ⊆ insert a u
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have this₁ : insert a s ⊆ insert a u
Tactic: have := insert_subset_insert a hsu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this : insert a s ⊆ insert a u
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have this₁ : insert a t ⊆ insert a u
Tactic: have := insert_subset_insert a htu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this : insert a t ⊆ insert a u
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have has : a ∉ s
Tactic: have has := notMem_mono hsu hu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this : insert a t ⊆ insert a u
has : a ∉ s
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have hat : a ∉ t
Tactic: have hat := notMem_mono htu hu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have this₁ : a ∉ s ∩ t
Tactic: have : a ∉ s ∩ t := notMem_mono (inter_subset_left.trans hsu) hu
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this : a ∉ s ∩ t
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have this₁ : a ∉ s ∪ t
Tactic: have := notMem_union.2 ⟨has, hat⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have rw : ((if s ∈ 𝒜 then f₁ s else 0) + if insert a s ∈ 𝒜 then f₁ (insert a s) else 0) * collapse ℬ a f₂ t ≤
  collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Tactic: rw [collapse_eq has]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.FourFunctions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : CommSemiring β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst_4 : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this_1 : s ⊆ insert a u
this_2 : t ⊆ insert a u
this_3 : insert a s ⊆ insert a u
this_4 : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this_5 : a ∉ s ∩ t
this : a ∉ s ∪ t
⊢ ((if s ∈ 𝒜 then f₁ s else 0) + if insert a s ∈ 𝒜 then f₁ (insert a s) else 0) * collapse ℬ a f₂ t ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
have pos : s ∈ 𝒜 →
  insert a s ∈ 𝒜 →
    (f₁ s + f₁ (insert a s)) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Tactic: split_ifs