awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : CommSemiring 𝕜
inst_4 : CommSemiring 𝕝
inst_5 : Algebra 𝕜 𝕝
c : 𝕜
f : IncidenceAlgebra 𝕝 α
h :
  ∀ (a b : α) (hab : a ≤ b),
    Eq.{u_3 + 1} (α := 𝕝) ((c • f : (a : α) → α → 𝕝) a b : 𝕝)
      ((HMul.hMul (α := IncidenceAlgebra 𝕝 α)
              (({
                      toFun := fun (c : 𝕜) ↦
                        HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : 𝕜 →+* IncidenceAlgebra 𝕝 α } :
                    (a : 𝕜) → IncidenceAlgebra 𝕝 α)
                  c :
                IncidenceAlgebra 𝕝 α)
              f :
            (a : α) → α → 𝕝)
          a b :
        𝕝)
⊢ c • f =
    HMul.hMul (α := IncidenceAlgebra 𝕝 α)
      (({
              toFun := fun (c : 𝕜) ↦
                HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : 𝕜) → IncidenceAlgebra 𝕝 α)
          c :
        IncidenceAlgebra 𝕝 α)
      f

Tactic:
ext a b hab
-- 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 : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : CommSemiring 𝕜
inst_4 : CommSemiring 𝕝
inst_5 : Algebra 𝕜 𝕝
c : 𝕜
f : IncidenceAlgebra 𝕝 α
a b : α
hab : a ≤ b
⊢ Eq.{u_3 + 1} (α := 𝕝) ((c • f : (a : α) → α → 𝕝) a b : 𝕝)
    ((HMul.hMul (α := IncidenceAlgebra 𝕝 α)
            (({
                    toFun := fun (c : 𝕜) ↦
                      HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
                    map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : 𝕜 →+* IncidenceAlgebra 𝕝 α } :
                  (a : 𝕜) → IncidenceAlgebra 𝕝 α)
                c :
              IncidenceAlgebra 𝕝 α)
            f :
          (a : α) → α → 𝕝)
        a b :
      𝕝)

Tactic:
simp [if_pos hab, constSMul_apply, Algebra.smul_def]

Premises used: IncidenceAlgebra.constSMul_apply, if_pos, Algebra.smul_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 : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : CommSemiring 𝕜
inst_4 : CommSemiring 𝕝
inst_5 : Algebra 𝕜 𝕝
c : 𝕜
f : IncidenceAlgebra 𝕝 α
h h₁ :
  ∀ (a b : α) (hab : a ≤ b),
    Eq.{u_3 + 1} (α := 𝕝) ((c • f : (a : α) → α → 𝕝) a b : 𝕝)
      ((HMul.hMul (α := IncidenceAlgebra 𝕝 α)
              (({
                      toFun := fun (c : 𝕜) ↦
                        HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : 𝕜 →+* IncidenceAlgebra 𝕝 α } :
                    (a : 𝕜) → IncidenceAlgebra 𝕝 α)
                  c :
                IncidenceAlgebra 𝕝 α)
              f :
            (a : α) → α → 𝕝)
          a b :
        𝕝)
⊢ c • f =
    HMul.hMul (α := IncidenceAlgebra 𝕝 α)
      (({
              toFun := fun (c : 𝕜) ↦
                HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : 𝕜) → IncidenceAlgebra 𝕝 α)
          c :
        IncidenceAlgebra 𝕝 α)
      f

Tactic:
classical ext a b hab; simp [if_pos hab, constSMul_apply, Algebra.smul_def]

Premises used: IncidenceAlgebra.constSMul_apply, Algebra.smul_def
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : One 𝕜
inst_2 : LE α
inst_3 : DecidableLE α
a b : α
⊢ Eq.{u_2 + 1} (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (if a ≤ b then 1 else 0 : 𝕜)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : One 𝕜
inst_2 : LE α
inst_3 : DecidableLE α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (1 : 𝕜)

Tactic:
if_pos h

Premises used: if_pos, ite
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : NonAssocSemiring 𝕜
inst_1 : Preorder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableLE α
a b : α
rw :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ Icc a b,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜))
    (∑ x ∈ Icc a b, 1)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
    ((↑(#(Icc a b)) : 𝕜) : 𝕜)

Tactic:
rw [mul_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one]

Premises used: Finset.card_eq_sum_ones, IncidenceAlgebra.mul_apply, Nat.cast_sum, Nat.cast_one
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : NonAssocSemiring 𝕜
inst_1 : Preorder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableLE α
a b : α
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ Icc a b,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜))
    (∑ x ∈ Icc a b, 1)

Tactic:
sum_congr rfl fun x hx ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : NonAssocSemiring 𝕜
inst_1 : Preorder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableLE α
a b : α
refine :
  ∀ (x : α) (hx : x ∈ Icc a b),
    HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) = 1
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ Icc a b,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜))
    (∑ x ∈ Icc a b, 1)

Tactic:
refine sum_congr rfl fun x hx ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : NonAssocSemiring 𝕜
inst_1 : Preorder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableLE α
a b x : α
hx : x ∈ Icc a b
⊢ a ≤ x ∧ x ≤ b

Tactic:
rw [mem_Icc] at hx

Premises used: Finset.mem_Icc
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : NonAssocSemiring 𝕜
inst_1 : Preorder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableLE α
a b x : α
hx : a ≤ x ∧ x ≤ b
rw : HMul.hMul (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) = 1
rw₁ : HMul.hMul (α := 𝕜) 1 1 = 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := 𝕜) 1 1
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) = 1

Tactic:
rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]

Premises used: IncidenceAlgebra.zeta_of_le, And.right, And.left, one_mul
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
rw rw₁ :
  Eq.{u_2 + 1} (α := 𝕜)
    (if a = b then 1
    else
      -∑ x ∈ (Ico a b).attach,
          have h := ⋯;
          have this := ⋯;
          muFun 𝕜 a (↑x : α))
    (if a = b then 1 else -∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α))
⊢ muFun 𝕜 a b = if a = b then 1 else -∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)

Tactic:
rw [muFun]

Premises used: _private.0.IncidenceAlgebra.muFun
-- 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 : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
h : ¬muFun 𝕜 a b = 0
⊢ ¬Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)) 0

Tactic:
rw [muFun_apply] at h

Premises used: _private.0.IncidenceAlgebra.muFun_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 : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
h : ¬Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)) 0
pos : ∀ (hab : a = b) (h : ¬Eq.{u_2 + 1} (α := 𝕜) 1 0), a ≤ b
neg : ∀ (hab : ¬a = b) (h : ¬Eq.{u_2 + 1} (α := 𝕜) (-∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)) 0), a ≤ b
⊢ a ≤ b

Tactic:
split_ifs at h with hab
-- 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 : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab : a = b
h : ¬Eq.{u_2 + 1} (α := 𝕜) 1 0
⊢ a ≤ b

Tactic:
hab.le

Premises used: Eq.le
-- 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 : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab : a = b
h : ¬Eq.{u_2 + 1} (α := 𝕜) 1 0
⊢ a ≤ b

Tactic:
exact hab.le

Premises used: Eq.le
-- 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 : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab : ¬a = b
h : ¬Eq.{u_2 + 1} (α := 𝕜) (-∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)) 0
⊢ ¬Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)) 0

Tactic:
rw [neg_eq_zero] at h

Premises used: neg_eq_zero
-- 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 : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab : ¬a = b
h : ¬Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)) 0
neg : ∀ (x : α) (hx : x ∈ Ico a b), a ≤ b
⊢ a ≤ b

Tactic:
obtain ⟨⟨x, hx⟩, -⟩ := exists_ne_zero_of_sum_ne_zero h

Premises used: Finset.exists_ne_zero_of_sum_ne_zero
-- 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 : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab : ¬a = b
h : ¬Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)) 0
x : α
hx : x ∈ Ico a b
⊢ a ≤ b

Tactic:
(nonempty_Ico.1 ⟨x, hx⟩).le

Premises used: LT.lt.le, Exists.intro, Iff.mp, Finset.nonempty_Ico
-- 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 : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab : ¬a = b
h : ¬Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)) 0
x : α
hx : x ∈ Ico a b
⊢ a ≤ b

Tactic:
exact (nonempty_Ico.1 ⟨x, hx⟩).le

Premises used: LT.lt.le, Exists.intro, Iff.mp, Finset.nonempty_Ico
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
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 := muFun 𝕜, eq_zero_of_not_le' := ⋯ } : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1 else -∑ x ∈ Ico a b, ({ toFun := muFun 𝕜, eq_zero_of_not_le' := ⋯ } : (a : α) → α → 𝕜) a x : 𝕜)
rw₁ : muFun 𝕜 a b = if a = b then 1 else -∑ x ∈ Ico a b, muFun 𝕜 a x
rw₂ :
  Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α))
    (if a = b then 1 else -∑ x ∈ Ico a b, muFun 𝕜 a x)
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ Ico a b, muFun 𝕜 a x)
    (if a = b then 1 else -∑ x ∈ Ico a b, muFun 𝕜 a x)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1 else -∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜)

Tactic:
rw [mu, coe_mk, muFun_apply, sum_attach]

Premises used: Finset.sum_attach, IncidenceAlgebra.mu, _private.0.IncidenceAlgebra.muFun_apply, IncidenceAlgebra.coe_mk
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a : α
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a a : 𝕜) (1 : 𝕜)

Tactic:
simp [mu_apply]

Premises used: IncidenceAlgebra.mu_apply
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab : a ≠ b
rw :
  Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x)
    (-∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := 𝕜) (-∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) (-∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (-∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜)

Tactic:
rw [mu_apply, if_neg hab]

Premises used: IncidenceAlgebra.mu_apply, if_neg
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
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 : α) → α → 𝕜) a x) 1
neg : ∀ (hab : ¬a = b), Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) 0
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) (if a = b then 1 else 0)

Tactic:
split_ifs with hab
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
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 : α) → α → 𝕜) a x) 1

Tactic:
simp [hab]
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
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 : α) → α → 𝕜) a x) 0
neg : ∀ (hab : ¬a ≤ b), Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) 0
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) 0

Tactic:
by_cases hab : a ≤ b
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab_1 : ¬a = b
hab : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) 0

Tactic:
simp [Icc_eq_cons_Ico hab, mu_eq_neg_sum_Ico_of_ne ‹_›]

Premises used: Finset.Icc_eq_cons_Ico, IncidenceAlgebra.mu_eq_neg_sum_Ico_of_ne
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab_1 : ¬a = b
hab : ¬a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) 0

Tactic:
sum_eq_zero fun x hx ↦ apply_eq_zero_of_not_le
      (fun hax ↦ hab <| hax.trans (mem_Icc.1 hx).2) _

Premises used: Finset.sum_eq_zero, IncidenceAlgebra.apply_eq_zero_of_not_le, Finset.mem_Icc, IncidenceAlgebra.mu, And.right, Iff.mp, LE.le.trans
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab_1 : ¬a = b
hab : ¬a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) 0

Tactic:
exact sum_eq_zero fun x hx ↦ apply_eq_zero_of_not_le
      (fun hax ↦ hab <| hax.trans (mem_Icc.1 hx).2) _

Premises used: Finset.sum_eq_zero, IncidenceAlgebra.apply_eq_zero_of_not_le, Finset.mem_Icc, And.right, Iff.mp, LE.le.trans
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
rw rw₁ :
  Eq.{u_2 + 1} (α := 𝕜)
    (if a = b then 1
    else
      -∑ x ∈ (Ioc a b).attach,
          have h := ⋯;
          have this := ⋯;
          muFun' 𝕜 b (↑x : α))
    (if a = b then 1 else -∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α))
⊢ muFun' 𝕜 b a = if a = b then 1 else -∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α)

Tactic:
rw [muFun']

Premises used: _private.0.IncidenceAlgebra.muFun'
-- 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 : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
h : ¬muFun' 𝕜 b a = 0
⊢ ¬Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α)) 0

Tactic:
rw [muFun'_apply] at h

Premises used: _private.0.IncidenceAlgebra.muFun'_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 : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
h : ¬Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α)) 0
pos : ∀ (hab : a = b) (h : ¬Eq.{u_2 + 1} (α := 𝕜) 1 0), a ≤ b
neg : ∀ (hab : ¬a = b) (h : ¬Eq.{u_2 + 1} (α := 𝕜) (-∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α)) 0), a ≤ b
⊢ a ≤ b

Tactic:
split_ifs at h with hab
-- 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 : 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
⊢ ¬Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α)) 0

Tactic:
rw [neg_eq_zero] at h

Premises used: neg_eq_zero
-- 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 : 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
neg : ∀ (x : α) (hx : x ∈ Ioc a b), a ≤ b
⊢ a ≤ b

Tactic:
obtain ⟨⟨x, hx⟩, -⟩ := exists_ne_zero_of_sum_ne_zero h

Premises used: Finset.exists_ne_zero_of_sum_ne_zero
-- 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 : 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
x : α
hx : x ∈ Ioc a b
⊢ a ≤ b

Tactic:
(nonempty_Ioc.1 ⟨x, hx⟩).le

Premises used: LT.lt.le, Exists.intro, Iff.mp, Finset.nonempty_Ioc
-- 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 : 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
x : α
hx : x ∈ Ioc a b
⊢ a ≤ b

Tactic:
exact (nonempty_Ioc.1 ⟨x, hx⟩).le

Premises used: LT.lt.le, Exists.intro, Iff.mp, Finset.nonempty_Ioc
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
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)
rw₃ 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)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1 else -∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)

Tactic:
rw [mu', coe_mk, muFun'_apply, sum_attach]

Premises used: _private.0.IncidenceAlgebra.muFun'_apply, Finset.sum_attach, _private.0.IncidenceAlgebra.mu', IncidenceAlgebra.coe_mk
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a : α
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) a a : 𝕜) (1 : 𝕜)

Tactic:
simp [mu'_apply]

Premises used: _private.0.IncidenceAlgebra.mu'_apply
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
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)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := 𝕜) (-∑ 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 : 𝕜)

Tactic:
rw [mu'_apply, if_neg h]

Premises used: _private.0.IncidenceAlgebra.mu'_apply, if_neg
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
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
neg : ∀ (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) (if a = b then 1 else 0)

Tactic:
split_ifs with hab
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
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) 1

Tactic:
simp [hab]
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
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
neg : ∀ (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

Tactic:
by_cases hab : a ≤ b
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab_1 : ¬a = b
hab : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) 0

Tactic:
simp [Icc_eq_cons_Ioc hab, mu'_eq_sum_Ioc_of_ne ‹_›]

Premises used: _private.0.IncidenceAlgebra.mu'_eq_sum_Ioc_of_ne, Finset.Icc_eq_cons_Ioc