awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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)
⊢ 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)
have 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) : 𝕜))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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) : 𝕜))
⊢ 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)
have x₂ : Eq.{u_2 + 1} (α := 𝕜) (if Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a : α) then 1 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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
⊢ f x = ∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y)
have symm : ∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y) = f x
Tactic: symm
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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, f z : 𝕜))
    (∑ y ∈ Ici x,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜)
        (∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z) : 𝕜))
have 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) : 𝕜)
Tactic: congr with y
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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 : α
⊢ 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) : 𝕜)
have rw : ∀ (z : α) (hz : z ∈ Ici y), f z = HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z)
Tactic: rw [sum_congr rfl fun z hz ↦ ?_]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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
⊢ f z = HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z)
have rw : f z = (if y ≤ z then 1 else 0) * f z
Tactic: rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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
⊢ f z = HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z)
have rw₁ : f z = 1 * f z
Tactic: rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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
⊢ f z = HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z)
have rw₂ : f z = f z
Tactic: rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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,
      ∑ 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)
have 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)
Tactic: rw [sum_sigma' (Ici x) fun y ↦ Ici y]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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 ∈ (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)
have 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 : α) ↦ α)))
Tactic: rw [sum_sigma' (Ici x) fun z ↦ Icc x z]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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 ∈ (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 : α) ↦ α)))
have 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)
Tactic: simp only [mul_boole, zero_mul, ite_mul, zeta_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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 ∈ (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)
have hi : ∀ (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: apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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
hi :
  ∀ (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 :
          (_ : α) × α)
⊢ 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)
have hj : ∀ (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: apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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
hi :
  ∀ (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 :
          (_ : α) × α)
hj :
  ∀ (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 :
          (_ : α) × α)
⊢ 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)
have left_neg : ∀ (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: apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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
hi :
  ∀ (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 :
          (_ : α) × α)
hj :
  ∀ (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 :
          (_ : α) × α)
left_neg :
  ∀ (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
⊢ 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)
have right_neg : ∀ (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: apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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} (α := 𝕜)
    (∑ 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))
have 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)
Tactic: simp_rw [mul_apply, sum_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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} (α := 𝕜)
    (∑ 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))
have simp : Eq.{u_2 + 1} (α := 𝕜) (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) 0
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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 ∈ Ici x, ∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((1 : (a : α) → α → 𝕜) x z : 𝕜) (f z) = f x
have simp : Eq.{u_2 + 1} (α := 𝕜) (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) 0
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]