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 : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : CommSemiring 𝕜
inst_4 : CommSemiring 𝕝
inst_5 : Algebra 𝕜 𝕝
c d : 𝕜
rw :
  HSMul.hSMul (β := IncidenceAlgebra 𝕝 α)
      (HAdd.hAdd (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝)) 1 =
    HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 +
      HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1
⊢ HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) (c + d) : 𝕝) 1 =
    HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 +
      HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1
have rw₁ : HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 +
    HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1 =
  HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 +
    HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1
Tactic: rw [map_add, add_smul]
-- 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 : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : CommSemiring 𝕜
inst_4 : CommSemiring 𝕝
inst_5 : Algebra 𝕜 𝕝
c : 𝕜
f : IncidenceAlgebra 𝕝 α
⊢ 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 =
    HMul.hMul (β := IncidenceAlgebra 𝕝 α) f
      (({
              toFun := fun (c : 𝕜) ↦
                HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : 𝕜) → IncidenceAlgebra 𝕝 α)
          c :
        IncidenceAlgebra 𝕝 α)
have h : ∀ (a b : α) (hab : a ≤ b),
  Eq.{u_3 + 1} (α := 𝕝)
    ((HMul.hMul (α := IncidenceAlgebra 𝕝 α)
            (({
                    toFun := fun (c : 𝕜) ↦
                      HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
                    map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry : 𝕜 →+* IncidenceAlgebra 𝕝 α } :
                  (a : 𝕜) → IncidenceAlgebra 𝕝 α)
                c :
              IncidenceAlgebra 𝕝 α)
            f :
          (a : α) → α → 𝕝)
        a b :
      𝕝)
    ((HMul.hMul (β := IncidenceAlgebra 𝕝 α) f
            (({
                    toFun := fun (c : 𝕜) ↦
                      HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
                    map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry : 𝕜 →+* IncidenceAlgebra 𝕝 α } :
                  (a : 𝕜) → IncidenceAlgebra 𝕝 α)
                c :
              IncidenceAlgebra 𝕝 α) :
          (a : α) → α → 𝕝)
        a b :
      𝕝)
Tactic: ext a b hab
-- 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 : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : CommSemiring 𝕜
inst_4 : CommSemiring 𝕝
inst_5 : Algebra 𝕜 𝕝
c : 𝕜
f : IncidenceAlgebra 𝕝 α
⊢ 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 =
    HMul.hMul (β := IncidenceAlgebra 𝕝 α) f
      (({
              toFun := fun (c : 𝕜) ↦
                HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : 𝕜) → IncidenceAlgebra 𝕝 α)
          c :
        IncidenceAlgebra 𝕝 α)
have h : ∀ (a b : α) (hab : a ≤ b),
  Eq.{u_3 + 1} (α := 𝕝)
    ((HMul.hMul (α := IncidenceAlgebra 𝕝 α)
            (({
                    toFun := fun (c : 𝕜) ↦
                      HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
                    map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry : 𝕜 →+* IncidenceAlgebra 𝕝 α } :
                  (a : 𝕜) → IncidenceAlgebra 𝕝 α)
                c :
              IncidenceAlgebra 𝕝 α)
            f :
          (a : α) → α → 𝕝)
        a b :
      𝕝)
    ((HMul.hMul (β := IncidenceAlgebra 𝕝 α) f
            (({
                    toFun := fun (c : 𝕜) ↦
                      HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
                    map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry : 𝕜 →+* IncidenceAlgebra 𝕝 α } :
                  (a : 𝕜) → IncidenceAlgebra 𝕝 α)
                c :
              IncidenceAlgebra 𝕝 α) :
          (a : α) → α → 𝕝)
        a b :
      𝕝)
Tactic: classical ext a b hab; simp [if_pos hab, constSMul_apply, mul_comm]
-- 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 : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : CommSemiring 𝕜
inst_4 : CommSemiring 𝕝
inst_5 : Algebra 𝕜 𝕝
c : 𝕜
f : IncidenceAlgebra 𝕝 α
⊢ 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
have 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' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry : 𝕜 →+* IncidenceAlgebra 𝕝 α } :
                  (a : 𝕜) → IncidenceAlgebra 𝕝 α)
                c :
              IncidenceAlgebra 𝕝 α)
            f :
          (a : α) → α → 𝕝)
        a b :
      𝕝)
Tactic: ext a b hab
-- 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 : PartialOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : CommSemiring 𝕜
inst_4 : CommSemiring 𝕝
inst_5 : Algebra 𝕜 𝕝
c : 𝕜
f : IncidenceAlgebra 𝕝 α
⊢ 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
have 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' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry : 𝕜 →+* IncidenceAlgebra 𝕝 α } :
                  (a : 𝕜) → IncidenceAlgebra 𝕝 α)
                c :
              IncidenceAlgebra 𝕝 α)
            f :
          (a : α) → α → 𝕝)
        a b :
      𝕝)
Tactic: classical ext a b hab; simp [if_pos hab, constSMul_apply, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : NonAssocSemiring 𝕜
inst_1 : Preorder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableLE α
a b : α
⊢ Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
    ((↑(#(Icc a b)) : 𝕜) : 𝕜)
have rw : Eq.{u_2 + 1} (α := 𝕜)
  (∑ x ∈ Icc a b, HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜))
  (∑ x ∈ Icc a b, 1)
Tactic: rw [mul_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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)
have refine : ∀ (x : α) (hx : x ∈ Icc a b),
  HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) = 1
Tactic: refine sum_congr rfl fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (hypothesis)
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
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) = 1
have hx₁ : a ≤ x ∧ x ≤ b
Tactic: rw [mem_Icc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) = 1
have rw : HMul.hMul (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) = 1
Tactic: rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) = 1
have rw₁ : HMul.hMul (α := 𝕜) 1 1 = 1
Tactic: rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
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
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) = 1
have rw₂ : Eq.{u_2 + 1} (α := 𝕜) 1 1
Tactic: rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]
-- 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 : α
⊢ muFun 𝕜 a b = if a = b then 1 else -∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)
have rw : Eq.{u_2 + 1} (α := 𝕜)
  (if a = b then 1
  else
    -∑ x ∈ (Ico a b).attach,
        have h := sorry;
        have this := sorry;
        muFun 𝕜 a (↑x : α))
  (if a = b then 1 else -∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α))
Tactic: rw [muFun]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (hypothesis)
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
⊢ a ≤ b
have h₁ : ¬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
Cleared hypotheses: h
-- 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 : α
h : ¬Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)) 0
⊢ a ≤ b
have pos : ∀ (hab : a = b) (h : ¬Eq.{u_2 + 1} (α := 𝕜) 1 0), a ≤ b
Tactic: split_ifs at h with hab
Cleared hypotheses: h
-- 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 : α
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
⊢ a ≤ b
have neg : ∀ (hab : ¬a = b) (h : ¬Eq.{u_2 + 1} (α := 𝕜) (-∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)) 0), a ≤ b
Tactic: split_ifs at h with hab
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (hypothesis)
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
⊢ a ≤ b
have h₁ : ¬Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)) 0
Tactic: rw [neg_eq_zero] at h
Cleared hypotheses: h
-- 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 ∈ (Ico a b).attach, muFun 𝕜 a (↑x : α)) 0
⊢ a ≤ b
have neg : ∀ (x : α) (hx : x ∈ Ico 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 ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜)
have rw : Eq.{u_2 + 1} (α := 𝕜) (({ toFun := muFun 𝕜, eq_zero_of_not_le' := sorry } : (a : α) → α → 𝕜) a b : 𝕜)
  (if a = b then 1 else -∑ x ∈ Ico a b, ({ toFun := muFun 𝕜, eq_zero_of_not_le' := sorry } : (a : α) → α → 𝕜) a 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 := 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 : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1 else -∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜)
have rw₁ : muFun 𝕜 a b = if a = b then 1 else -∑ x ∈ Ico a b, muFun 𝕜 a 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 := 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
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1 else -∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜)
have 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)
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 := 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)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a b : 𝕜)
    (if a = b then 1 else -∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜)
have 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)
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 : α
hab : a ≠ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (-∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜)
have 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)
Tactic: rw [mu_apply, if_neg 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 : 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)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (-∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜)
have rw₁ : Eq.{u_2 + 1} (α := 𝕜) (-∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) (-∑ x ∈ Ico a b, (mu 𝕜 : (a : α) → α → 𝕜) a x)
Tactic: rw [mu_apply, if_neg 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 : α
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) (if a = b then 1 else 0)
have pos : ∀ (hab : a = b), Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) 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 : α) → α → 𝕜) a x) 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) (if a = b then 1 else 0)
have neg : ∀ (hab : ¬a = b), Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) 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 : α) → α → 𝕜) a x) 0
have pos : ∀ (hab : a ≤ b), Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) 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 : α) → α → 𝕜) a x) 0
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) 0
have neg : ∀ (hab : ¬a ≤ b), Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x) 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 : Preorder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
⊢ muFun' 𝕜 b a = if a = b then 1 else -∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α)
have rw : Eq.{u_2 + 1} (α := 𝕜)
  (if a = b then 1
  else
    -∑ x ∈ (Ioc a b).attach,
        have h := sorry;
        have this := sorry;
        muFun' 𝕜 b (↑x : α))
  (if a = b then 1 else -∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α))
Tactic: rw [muFun']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (hypothesis)
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
⊢ a ≤ b
have h₁ : ¬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
Cleared hypotheses: h
-- 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 : α
h : ¬Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else -∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α)) 0
⊢ a ≤ b
have pos : ∀ (hab : a = b) (h : ¬Eq.{u_2 + 1} (α := 𝕜) 1 0), a ≤ b
Tactic: split_ifs at h with hab
Cleared hypotheses: h
-- 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 : α
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
⊢ a ≤ b
have neg : ∀ (hab : ¬a = b) (h : ¬Eq.{u_2 + 1} (α := 𝕜) (-∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α)) 0), a ≤ b
Tactic: split_ifs at h with hab
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (hypothesis)
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 h₁ : ¬Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b (↑x : α)) 0
Tactic: rw [neg_eq_zero] at h
Cleared hypotheses: h