awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
h : a ≤ b
x :
  Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, if x ≤ b then (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x else 0)
    (∑ x ∈ Icc a b, (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x)
x₁ :
  Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x)
    (∑ x ∈ (Icc ((ofDual : (a : αᵒᵈ) → α) b) ((ofDual : (a : αᵒᵈ) → α) a) : Finset α),
      ((mu 𝕜 : (a : α) → α → 𝕜) x ((ofDual : (a : αᵒᵈ) → α) a) : 𝕜))
x₂ :
  Eq.{u_2 + 1} (α := 𝕜) (if Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a : α) then 1 else 0)
    (if a = b then 1 else 0)
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, if x ≤ b then (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x else 0) (if a = b then 1 else 0)

Tactic:
calc
    ∑ x ∈ Icc a b, (if x ≤ b then mud a x else 0) = ∑ x ∈ Icc a b, mud a x := by
      congr! with x hx; exact if_pos (mem_Icc.1 hx).2
    _ = ∑ x ∈ Icc (ofDual b) (ofDual a), mu 𝕜 x (ofDual a) := by simp [Icc_orderDual_def, mud]
    _ = if ofDual b = ofDual a then 1 else 0 := sum_Icc_mu_left ..
    _ = if a = b then 1 else 0 := by simp [eq_comm]

Premises used: OrderDual.ofDual, IncidenceAlgebra.sum_Icc_mu_left, Finset.Icc, DFunLike.coe
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : αᵒᵈ
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b) : 𝕜)
    ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) b a : 𝕜)

Tactic:
(mu_toDual ..).symm

Premises used: Eq.symm, IncidenceAlgebra.mu_toDual
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
inst_4 : BoundedOrder α
⊢ eulerChar.{u_2, u_5} 𝕜 αᵒᵈ = eulerChar 𝕜 α

Tactic:
simp [eulerChar, ← mu_toDual 𝕜 (α := α)]

Premises used: IncidenceAlgebra.eulerChar, IncidenceAlgebra.mu_toDual
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
symm : ∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y) = f x
⊢ f x = ∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y)

Tactic:
symm
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y))
    (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜))

Tactic:
simp_rw [h]
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
e_f :
  ∀ (y : α),
    HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜) =
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜)
        (∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z) : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜))
    (∑ y ∈ Ici x,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜)
        (∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z) : 𝕜))

Tactic:
congr with y
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
y : α
rw : ∀ (z : α) (hz : z ∈ Ici y), f z = HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z)
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜)
      (∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z) : 𝕜)

Tactic:
rw [sum_congr rfl fun z hz ↦ ?_]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
y z : α
hz : z ∈ Ici y
rw : f z = (if y ≤ z then 1 else 0) * f z
rw₁ : f z = 1 * f z
rw₂ rw₃ : f z = f z
⊢ f z = HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z)

Tactic:
rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]

Premises used: Finset.mem_Ici, if_pos, Iff.mp, IncidenceAlgebra.zeta_apply, one_mul
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ y ∈ Ici x,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜)
        (∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z) : 𝕜))
    (∑ y ∈ Ici x,
      ∑ z ∈ Ici y,
        HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)

Tactic:
simp [mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
rw :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ x_1 ∈ (Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x (x_1.fst (β := fun (i : α) ↦ α)) : 𝕜)
          ((zeta 𝕜 : (a : α) → α → 𝕜) (x_1.fst (β := fun (i : α) ↦ α)) (x_1.snd (β := fun (i : α) ↦ α)) : 𝕜) *
        f (x_1.snd (β := fun (i : α) ↦ α)))
    (∑ z ∈ Ici x,
      ∑ y ∈ Icc x z,
        HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ y ∈ Ici x,
      ∑ z ∈ Ici y,
        HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)
    (∑ z ∈ Ici x,
      ∑ y ∈ Icc x z,
        HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)

Tactic:
rw [sum_sigma' (Ici x) fun y ↦ Ici y]

Premises used: Finset.Ici, Finset.sum_sigma'
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
rw :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ x_1 ∈ (Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x (x_1.fst (β := fun (i : α) ↦ α)) : 𝕜)
          ((zeta 𝕜 : (a : α) → α → 𝕜) (x_1.fst (β := fun (i : α) ↦ α)) (x_1.snd (β := fun (i : α) ↦ α)) : 𝕜) *
        f (x_1.snd (β := fun (i : α) ↦ α)))
    (∑ x_1 ∈ (Ici x).sigma (α := fun (z : α) ↦ α) fun (z : α) ↦ Icc x z,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x (x_1.snd (β := fun (i : α) ↦ α)) : 𝕜)
          ((zeta 𝕜 : (a : α) → α → 𝕜) (x_1.snd (β := fun (i : α) ↦ α)) (x_1.fst (β := fun (i : α) ↦ α)) : 𝕜) *
        f (x_1.fst (β := fun (i : α) ↦ α)))
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x_1 ∈ (Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x (x_1.fst (β := fun (i : α) ↦ α)) : 𝕜)
          ((zeta 𝕜 : (a : α) → α → 𝕜) (x_1.fst (β := fun (i : α) ↦ α)) (x_1.snd (β := fun (i : α) ↦ α)) : 𝕜) *
        f (x_1.snd (β := fun (i : α) ↦ α)))
    (∑ z ∈ Ici x,
      ∑ y ∈ Icc x z,
        HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)

Tactic:
rw [sum_sigma' (Ici x) fun z ↦ Icc x z]

Premises used: Finset.Ici, Finset.Icc, Finset.sum_sigma'
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
simp :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ x_1 ∈ (Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y,
      if x_1.fst (β := fun (i : α) ↦ α) ≤ x_1.snd (β := fun (i : α) ↦ α) then
        HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x (x_1.fst (β := fun (i : α) ↦ α)) : 𝕜)
          (f (x_1.snd (β := fun (i : α) ↦ α)))
      else 0)
    (∑ x_1 ∈ (Ici x).sigma (α := fun (z : α) ↦ α) fun (z : α) ↦ Icc x z,
      if x_1.snd (β := fun (i : α) ↦ α) ≤ x_1.fst (β := fun (i : α) ↦ α) then
        HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x (x_1.snd (β := fun (i : α) ↦ α)) : 𝕜)
          (f (x_1.fst (β := fun (i : α) ↦ α)))
      else 0)
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x_1 ∈ (Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x (x_1.fst (β := fun (i : α) ↦ α)) : 𝕜)
          ((zeta 𝕜 : (a : α) → α → 𝕜) (x_1.fst (β := fun (i : α) ↦ α)) (x_1.snd (β := fun (i : α) ↦ α)) : 𝕜) *
        f (x_1.snd (β := fun (i : α) ↦ α)))
    (∑ x_1 ∈ (Ici x).sigma (α := fun (z : α) ↦ α) fun (z : α) ↦ Icc x z,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x (x_1.snd (β := fun (i : α) ↦ α)) : 𝕜)
          ((zeta 𝕜 : (a : α) → α → 𝕜) (x_1.snd (β := fun (i : α) ↦ α)) (x_1.fst (β := fun (i : α) ↦ α)) : 𝕜) *
        f (x_1.fst (β := fun (i : α) ↦ α)))

Tactic:
simp only [mul_boole, zero_mul, ite_mul, zeta_apply]

Premises used: MulZeroClass.zero_mul, mul_boole, ite_mul, IncidenceAlgebra.zeta_apply
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y) a →
      Membership.mem (α := (_ : α) × α) (γ := Finset ((_ : α) × α))
        ((Ici x).sigma (α := fun (z : α) ↦ α) fun (z : α) ↦ Icc x z)
        (match (motive := (_ : α) × α → (_ : α) × α) a with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a :
          (_ : α) × α)

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

Premises used: mul_assoc, le_trans
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Ici x).sigma (α := fun (z : α) ↦ α) fun (z : α) ↦ Icc x z) a →
      Membership.mem (α := (_ : α) × α) (γ := Finset ((_ : α) × α))
        ((Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y)
        (match (motive := (_ : α) × α → (_ : α) × α) a with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a :
          (_ : α) × α)

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

Premises used: mul_assoc, le_trans
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y) a →
      (match (motive := (_ : α) × α → (_ : α) × α)
          match (motive := (_ : α) × α → (_ : α) × α) a with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) =
        a

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

Premises used: mul_assoc, le_trans
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Ici x).sigma (α := fun (z : α) ↦ α) fun (z : α) ↦ Icc x z) a →
      (match (motive := (_ : α) × α → (_ : α) × α)
          match (motive := (_ : α) × α → (_ : α) × α) a with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) =
        a

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

Premises used: mul_assoc, le_trans
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Ici x).sigma (α := fun (y : α) ↦ α) fun (y : α) ↦ Ici y) a →
      (if a.fst (β := fun (i : α) ↦ α) ≤ a.snd (β := fun (i : α) ↦ α) then
          HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x (a.fst (β := fun (i : α) ↦ α)) : 𝕜)
            (f (a.snd (β := fun (i : α) ↦ α)))
        else 0) =
        if
            LE.le.{u_5} (α := α)
              (Sigma.snd (β := fun (i : α) ↦ α)
                  (match (motive := (_ : α) × α → (_ : α) × α) a with
                  | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) :
                α)
              (Sigma.fst (β := fun (i : α) ↦ α)
                  (match (motive := (_ : α) × α → (_ : α) × α) a with
                  | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) :
                α) then
          HMul.hMul (α := 𝕜)
            ((mu 𝕜 : (a : α) → α → 𝕜) x
                (Sigma.snd (β := fun (i : α) ↦ α)
                  (match (motive := (_ : α) × α → (_ : α) × α) a with
                  | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a)) :
              𝕜)
            (f
              (Sigma.fst (β := fun (i : α) ↦ α)
                (match (motive := (_ : α) × α → (_ : α) × α) a with
                | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a)))
        else 0

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

Premises used: mul_assoc, le_trans
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
simp_rw :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ z ∈ Ici x,
      ∑ y ∈ Icc x z,
        HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)
    (∑ x_1 ∈ Ici x,
      (∑ x_2 ∈ Icc x x_1,
          HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x x_2 : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x_2 x_1 : 𝕜)) *
        f x_1)
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ z ∈ Ici x,
      ∑ y ∈ Icc x z,
        HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)
    (∑ z ∈ Ici x,
      HMul.hMul (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) x z : 𝕜) (f z))

Tactic:
simp_rw [mul_apply, sum_mul]

Premises used: IncidenceAlgebra.mul_apply, Finset.sum_mul
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
simp : Eq.{u_2 + 1} (α := 𝕜) (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) 0
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ z ∈ Ici x,
      HMul.hMul (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) x z : 𝕜) (f z))
    (∑ y ∈ Ici x, ∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((1 : (a : α) → α → 𝕜) x z : 𝕜) (f z))

Tactic:
simp only [mu_mul_zeta 𝕜, one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici, le_refl,
        ↓reduceIte, ← add_sum_Ioi_eq_sum_Ici, left_eq_add]

Premises used: le_refl, left_eq_add, Finset.mem_Ici, IncidenceAlgebra.one_apply, MulZeroClass.zero_mul, Finset.add_sum_Ioi_eq_sum_Ici, ite_mul, IncidenceAlgebra.mu_mul_zeta, reduceIte, Finset.sum_ite_eq, one_mul
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) 0

Tactic:
sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge

Premises used: Finset.sum_eq_zero, Finset.mem_Ioi, Iff.mp, LT.lt.not_ge, if_neg
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) 0

Tactic:
exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge

Premises used: Finset.sum_eq_zero, Finset.mem_Ioi, Iff.mp, LT.lt.not_ge, if_neg
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
simp : Eq.{u_2 + 1} (α := 𝕜) (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) 0
⊢ ∑ y ∈ Ici x, ∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((1 : (a : α) → α → 𝕜) x z : 𝕜) (f z) = f x

Tactic:
simp only [one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici,
        ← add_sum_Ioi_eq_sum_Ici, le_refl, ↓reduceIte, add_eq_left]

Premises used: le_refl, Finset.mem_Ici, IncidenceAlgebra.one_apply, MulZeroClass.zero_mul, Finset.add_sum_Ioi_eq_sum_Ici, add_eq_left, ite_mul, reduceIte, Finset.sum_ite_eq, one_mul
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x : α
⊢ f x = ∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) x y : 𝕜) (g y)

Tactic:
moebius_inversion_top (α := αᵒᵈ) f g h x

Premises used: IncidenceAlgebra.moebius_inversion_top
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x : α
h₁ : ∀ x_1 ∈ Ici x, Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x_1 x : 𝕜) ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) x x_1 : 𝕜)
⊢ f x = ∑ y ∈ Iic x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) y x : 𝕜) (g y)

Tactic:
convert! moebius_inversion_top (α := αᵒᵈ) f g h x using 3

Premises used: IncidenceAlgebra.moebius_inversion_top
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x x_1 : α
h_1 : x_1 ∈ Ici x
h₁ :
  Eq.{u_2 + 1} (α := 𝕜)
    ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) ((toDual : (a : α) → αᵒᵈ) x : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) x_1) : 𝕜)
    ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) x x_1 : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x_1 x : 𝕜) ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) x x_1 : 𝕜)

Tactic:
rw [← mu_toDual]

Premises used: IncidenceAlgebra.mu_toDual
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x x_1 : α
h_1 : x_1 ∈ Ici x
⊢ Eq.{u_2 + 1} (α := 𝕜)
    ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) ((toDual : (a : α) → αᵒᵈ) x : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) x_1) : 𝕜)
    ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) x x_1 : 𝕜)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : DecidableLE α
inst_4 : DecidableLE β
a b : α × β
⊢ (zeta 𝕜 : (a : α × β) → α × β → 𝕜) a b =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a.1 b.1 : 𝕜) ((zeta 𝕜 : (a : β) → β → 𝕜) a.2 b.2 : 𝕜)

Tactic:
simp [← ite_and, Prod.le_def, and_comm]

Premises used: and_comm, ite_and, Prod.le_def
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : DecidableLE α
inst_4 : DecidableLE β
a₁ a₂ : α
b₁ b₂ : β
⊢ (zeta 𝕜 : (a : α × β) → α × β → 𝕜) (a₁, b₁) (a₂, b₂) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a₁ a₂ : 𝕜) ((zeta 𝕜 : (a : β) → β → 𝕜) b₁ b₂ : 𝕜)

Tactic:
zeta_prod_apply _ _ _

Premises used: IncidenceAlgebra.zeta_prod_apply
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x ≤ y
⊢ ¬x.1 ≤ y.1 ∨ ¬x.2 ≤ y.2

Tactic:
rw [Prod.le_def, not_and_or] at hxy

Premises used: not_and_or, Prod.le_def
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x.1 ≤ y.1 ∨ ¬x.2 ≤ y.2
inl :
  ∀ (hxy : ¬x.1 ≤ y.1),
    HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) x.1 y.1 : 𝕜) ((g : (a : β) → β → 𝕜) x.2 y.2 : 𝕜) = 0
inr :
  ∀ (hxy : ¬x.2 ≤ y.2),
    HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) x.1 y.1 : 𝕜) ((g : (a : β) → β → 𝕜) x.2 y.2 : 𝕜) = 0
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) x.1 y.1 : 𝕜) ((g : (a : β) → β → 𝕜) x.2 y.2 : 𝕜) = 0

Tactic:
obtain hxy | hxy := hxy