awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab : ¬a = b
h : ¬Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α)) 0
⊢ a ≤ b
have neg : ∀ (x : α) (hx : x ∈ Ioc a b), a ≤ b
Tactic: obtain ⟨⟨x, hx⟩, -⟩ := exists_ne_zero_of_sum_ne_zero h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1 else -∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
have rw : Eq.{u_2 + 1} (α := 𝕜) (({ toFun := fun (a b : α) ↦ muFun' 𝕜 b a, eq_zero_of_not_le' := sorry } : (a : α) → α → 𝕜) a b : 𝕜)
  (if a = b then 1
    else -∑ x ∈ Ioc a b, ({ toFun := fun (a b : α) ↦ muFun' 𝕜 b a, eq_zero_of_not_le' := sorry } : (a : α) → α → 𝕜) x b :
    𝕜)
Tactic: rw [mu', coe_mk, muFun'_apply, sum_attach]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
rw :
  Eq.{u_2 + 1} (α := 𝕜) (({ toFun := fun (a b : α) ↦ muFun' 𝕜 b a, eq_zero_of_not_le' := ⋯ } : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1
      else -∑ x ∈ Ioc a b, ({ toFun := fun (a b : α) ↦ muFun' 𝕜 b a, eq_zero_of_not_le' := ⋯ } : (a : α) → α → 𝕜) x b :
      𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1 else -∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
have rw₁ : muFun' 𝕜 b a = if a = b then 1 else -∑ x ∈ Ioc a b, muFun' 𝕜 b x
Tactic: rw [mu', coe_mk, muFun'_apply, sum_attach]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
rw :
  Eq.{u_2 + 1} (α := 𝕜) (({ toFun := fun (a b : α) ↦ muFun' 𝕜 b a, eq_zero_of_not_le' := ⋯ } : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1
      else -∑ x ∈ Ioc a b, ({ toFun := fun (a b : α) ↦ muFun' 𝕜 b a, eq_zero_of_not_le' := ⋯ } : (a : α) → α → 𝕜) x b :
      𝕜)
rw₁ : muFun' 𝕜 b a = if a = b then 1 else -∑ x ∈ Ioc a b, muFun' 𝕜 b x
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1 else -∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
have rw₂ : Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α))
  (if a = b then 1 else -∑ x ∈ Ioc a b, muFun' 𝕜 b x)
Tactic: rw [mu', coe_mk, muFun'_apply, sum_attach]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
rw :
  Eq.{u_2 + 1} (α := 𝕜) (({ toFun := fun (a b : α) ↦ muFun' 𝕜 b a, eq_zero_of_not_le' := ⋯ } : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1
      else -∑ x ∈ Ioc a b, ({ toFun := fun (a b : α) ↦ muFun' 𝕜 b a, eq_zero_of_not_le' := ⋯ } : (a : α) → α → 𝕜) x b :
      𝕜)
rw₁ : muFun' 𝕜 b a = if a = b then 1 else -∑ x ∈ Ioc a b, muFun' 𝕜 b x
rw₂ :
  Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α))
    (if a = b then 1 else -∑ x ∈ Ioc a b, muFun' 𝕜 b x)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1 else -∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
have rw₃ : Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ Ioc a b, muFun' 𝕜 b x)
  (if a = b then 1 else -∑ x ∈ Ioc a b, muFun' 𝕜 b x)
Tactic: rw [mu', coe_mk, muFun'_apply, sum_attach]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
h : a ≠ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
have rw : Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b)
  (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b)
Tactic: rw [mu'_apply, if_neg h]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
h : a ≠ b
rw :
  Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b)
    (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
have rw₁ : Eq.{u_2 + 1} (α := 𝕜) (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b)
Tactic: rw [mu'_apply, if_neg h]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) (if a = b then 1 else 0)
have pos : ∀ (hab : a = b), Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) 1
Tactic: split_ifs with hab
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
pos : ∀ (hab : a = b), Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) (if a = b then 1 else 0)
have neg : ∀ (hab : ¬a = b), Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) 0
Tactic: split_ifs with hab
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab : ¬a = b
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) 0
have pos : ∀ (hab : a ≤ b), Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) 0
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab : ¬a = b
pos : ∀ (hab : a ≤ b), Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) 0
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) 0
have neg : ∀ (hab : ¬a ≤ b), Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) 0
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
⊢ HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) = 1
have h : ∀ (a b : α),
  a ≤ b →
    Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
      ((1 : (a : α) → α → 𝕜) a b : 𝕜)
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
    (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜)
have rw : Eq.{u_2 + 1} (α := 𝕜)
  (∑ x ∈ Icc a b, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜))
  (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x)
Tactic: rw [mul_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ Icc a b, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜))
    (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x)
have a₁ : ∀ (x : α) (hx : x ∈ Icc a b),
  HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) =
    (mu 𝕜 : (a : α) → α → 𝕜) a x
Tactic: congr! with x hx
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
    ((1 : (a : α) → α → 𝕜) a b : 𝕜)
have _ : Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
  (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜)
Tactic: calc
    _ = ∑ x ∈ Icc a b, mu 𝕜 a x := by rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).2]
    _ = (1 : IncidenceAlgebra 𝕜 α) a b := sum_Icc_mu_right ..
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
⊢ HMul.hMul (α := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) = 1
have h : ∀ (a b : α),
  a ≤ b →
    Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
      ((1 : (a : α) → α → 𝕜) a b : 𝕜)
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
    (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
have rw : Eq.{u_2 + 1} (α := 𝕜)
  (∑ x ∈ Icc a b, HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜))
  (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b)
Tactic: rw [mul_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ Icc a b,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜))
    (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b)
have a₁ : ∀ (x : α) (hx : x ∈ Icc a b),
  HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) =
    (mu' 𝕜 : (a : α) → α → 𝕜) x b
Tactic: congr! with x hx
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
    ((1 : (a : α) → α → 𝕜) a b : 𝕜)
have _ : Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
  (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
Tactic: calc
    _ = ∑ x ∈ Icc a b, mu' 𝕜 x b := by rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).1]
    _ = (1 : IncidenceAlgebra 𝕜 α) a b := sum_Icc_mu'_left ..
-- 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 α
a b : α
hab : a ≠ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (-∑ x ∈ Ioc a b, (mu 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
have rw : Eq.{u_2 + 1} (α := 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
Tactic: rw [mu_eq_mu', mu'_eq_sum_Ioc_of_ne hab]
-- 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 α
a b : α
hab : a ≠ b
rw : Eq.{u_2 + 1} (α := 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (-∑ x ∈ Ioc a b, (mu 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
have rw₁ : Eq.{u_2 + 1} (α := 𝕜) (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b)
Tactic: rw [mu_eq_mu', mu'_eq_sum_Ioc_of_ne hab]
-- 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 α
inst_4 : DecidableLE α
⊢ HMul.hMul (α := IncidenceAlgebra 𝕜 α) (β := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu 𝕜) = 1
have rw : HMul.hMul (α := IncidenceAlgebra 𝕜 α) (β := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) = 1
Tactic: rw [mu_eq_mu', zeta_mul_mu']
-- 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 α
inst_4 : DecidableLE α
rw : HMul.hMul (α := IncidenceAlgebra 𝕜 α) (β := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) = 1
⊢ HMul.hMul (α := IncidenceAlgebra 𝕜 α) (β := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu 𝕜) = 1
have rw₁ : Eq (α := IncidenceAlgebra 𝕜 α) 1 1
Tactic: rw [mu_eq_mu', zeta_mul_mu']
-- 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 α
a b : α
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) x b) (if a = b then 1 else 0)
have rw : Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) (if a = b then 1 else 0)
Tactic: rw [mu_eq_mu', sum_Icc_mu'_left]
-- 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 α
a b : α
rw : Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) (if a = b then 1 else 0)
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) x b) (if a = b then 1 else 0)
have rw₁ : Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else 0) (if a = b then 1 else 0)
Tactic: rw [mu_eq_mu', sum_Icc_mu'_left]
-- 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 α
a b : α
this_1 : 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' := ⋯ }
this : mu 𝕜 = mud
⊢ Eq.{u_2 + 1} (α := 𝕜)
    ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b) : 𝕜)
    ((mu 𝕜 : (a : α) → α → 𝕜) b a : 𝕜)
have simp_rw : Eq.{u_2 + 1} (α := 𝕜) ((mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b) : 𝕜)
  ((mu 𝕜 : (a : α) → α → 𝕜) b a : 𝕜)
Tactic: simp_rw [this, mud, coe_mk, ofDual_toDual]
-- 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 α
a b : α
this_1 : 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' := ⋯ }
this : mu 𝕜 = mud
simp_rw :
  Eq.{u_2 + 1} (α := 𝕜)
    ((mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b) : 𝕜)
    ((mu 𝕜 : (a : α) → α → 𝕜) b a : 𝕜)
simp_rw₁ :
  Eq.{u_2 + 1} (α := 𝕜)
    (({
            toFun := fun (a b : αᵒᵈ) ↦
              (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
            eq_zero_of_not_le' := ⋯ } :
          (a : αᵒᵈ) → αᵒᵈ → 𝕜)
        ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b) :
      𝕜)
    ((mu 𝕜 : (a : α) → α → 𝕜) b a : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜)
    ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b) : 𝕜)
    ((mu 𝕜 : (a : α) → α → 𝕜) b a : 𝕜)
have simp_rw₂ : Eq.{u_2 + 1} (α := 𝕜)
  ((mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) : α)
      ((ofDual : (a : αᵒᵈ) → α) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)) :
    𝕜)
  ((mu 𝕜 : (a : α) → α → 𝕜) b a : 𝕜)
Tactic: simp_rw [this, mud, coe_mk, ofDual_toDual]
-- 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 α
a b : α
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' := ⋯ }
⊢ Eq.{u_2 + 1} (α := 𝕜)
    ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b) : 𝕜)
    ((mu 𝕜 : (a : α) → α → 𝕜) b a : 𝕜)
have suffices : mu 𝕜 = mud
Tactic: suffices mu 𝕜 = mud by simp_rw [this, mud, coe_mk, ofDual_toDual]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (hypothesis)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : α
this_1 : 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' := ⋯ }
this : mud * zeta 𝕜 = 1
⊢ mu 𝕜 = mud
have this₁ : mud * zeta 𝕜 = HMul.hMul (α := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mu 𝕜) (zeta 𝕜)
Tactic: rw [← mu_mul_zeta] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (hypothesis)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : α
this_1 : 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' := ⋯ }
this : mud * zeta 𝕜 = HMul.hMul (α := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mu 𝕜) (zeta 𝕜)
⊢ mu 𝕜 = mud
have this₁ : HMul.hMul (β := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mud * zeta 𝕜) (mu 𝕜) =
  HMul.hMul (α := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mu 𝕜) (zeta 𝕜) * mu 𝕜
Tactic: apply_fun (· * mu 𝕜) at this
Cleared hypotheses: this
-- 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 α
a b : α
this_1 : 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' := ⋯ }
this :
  HMul.hMul (β := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mud * zeta 𝕜) (mu 𝕜) =
    HMul.hMul (α := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mu 𝕜) (zeta 𝕜) * mu 𝕜
⊢ mu 𝕜 = mud
have symm : mud = mu 𝕜
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 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : α
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' := ⋯ }
⊢ mu 𝕜 = mud
have suffices : mud * zeta 𝕜 = 1
Tactic: suffices mud * zeta 𝕜 = 1 by
    rw [← mu_mul_zeta] at this
    apply_fun (· * mu 𝕜) at this
    symm
    simpa [mul_assoc, zeta_mul_mu] using this
-- 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' := ⋯ }
⊢ mud * zeta 𝕜 = 1
have h : ∀ (a b : αᵒᵈ),
  a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((mud * zeta 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a b : 𝕜) ((1 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a b : 𝕜)
Tactic: ext a b
-- 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} (α := 𝕜) ((mud * zeta 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a b : 𝕜) ((1 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a b : 𝕜)
have h : 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: simp only [mul_boole, one_apply, mul_apply, 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 : 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)
    (∑ x ∈ Icc a b, (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x)
have a₁ : ∀ (x : αᵒᵈ) (hx : x ∈ Icc a b),
  Eq.{u_2 + 1} (α := 𝕜) (if x ≤ b then (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x else 0 : 𝕜) ((mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x : 𝕜)
Tactic: congr! with x hx