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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g h : IncidenceAlgebra 𝕝 α
h₁ :
  ∀ (a b : α),
    a ≤ b → Eq.{u_3 + 1} (α := 𝕝) ((f • (g + h) : (a : α) → α → 𝕝) a b : 𝕝) ((f • g + f • h : (a : α) → α → 𝕝) a b : 𝕝)
⊢ f • (g + h) = f • g + f • h

Tactic:
ext
-- 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g h : IncidenceAlgebra 𝕝 α
a b : α
h_1 : a ≤ b
⊢ Eq.{u_3 + 1} (α := 𝕝) ((f • (g + h) : (a : α) → α → 𝕝) a b : 𝕝) ((f • g + f • h : (a : α) → α → 𝕝) a b : 𝕝)

Tactic:
Eq.trans (sum_congr rfl fun x _ ↦ smul_add _ _ _) sum_add_distrib

Premises used: Finset.sum_add_distrib, DFunLike.coe, Finset.sum_congr, smul_add, rfl, Eq.trans
-- 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g h : IncidenceAlgebra 𝕝 α
a b : α
h_1 : a ≤ b
⊢ Eq.{u_3 + 1} (α := 𝕝) ((f • (g + h) : (a : α) → α → 𝕝) a b : 𝕝) ((f • g + f • h : (a : α) → α → 𝕝) a b : 𝕝)

Tactic:
exact Eq.trans (sum_congr rfl fun x _ ↦ smul_add _ _ _) sum_add_distrib

Premises used: Finset.sum_add_distrib, Finset.sum_congr, smul_add, rfl, Eq.trans
-- 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f g : IncidenceAlgebra 𝕜 α
h : IncidenceAlgebra 𝕝 α
h₁ :
  ∀ (a b : α),
    a ≤ b → Eq.{u_3 + 1} (α := 𝕝) (((f + g) • h : (a : α) → α → 𝕝) a b : 𝕝) ((f • h + g • h : (a : α) → α → 𝕝) a b : 𝕝)
⊢ (f + g) • h = f • h + g • h

Tactic:
ext
-- 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f g : IncidenceAlgebra 𝕜 α
h : IncidenceAlgebra 𝕝 α
a b : α
h_1 : a ≤ b
⊢ Eq.{u_3 + 1} (α := 𝕝) (((f + g) • h : (a : α) → α → 𝕝) a b : 𝕝) ((f • h + g • h : (a : α) → α → 𝕝) a b : 𝕝)

Tactic:
Eq.trans (sum_congr rfl fun x _ ↦ add_smul _ _ _) sum_add_distrib

Premises used: Finset.sum_add_distrib, add_smul, DFunLike.coe, Finset.sum_congr, rfl, Eq.trans
-- 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f g : IncidenceAlgebra 𝕜 α
h : IncidenceAlgebra 𝕝 α
a b : α
h_1 : a ≤ b
⊢ Eq.{u_3 + 1} (α := 𝕝) (((f + g) • h : (a : α) → α → 𝕝) a b : 𝕝) ((f • h + g • h : (a : α) → α → 𝕝) a b : 𝕝)

Tactic:
exact Eq.trans (sum_congr rfl fun x _ ↦ add_smul _ _ _) sum_add_distrib

Premises used: Finset.sum_add_distrib, add_smul, Finset.sum_congr, rfl, Eq.trans
-- 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕝 α
h :
  ∀ (a b : α),
    a ≤ b →
      Eq.{u_3 + 1} (α := 𝕝) ((HSMul.hSMul (α := IncidenceAlgebra 𝕜 α) 0 f : (a : α) → α → 𝕝) a b : 𝕝)
        ((0 : (a : α) → α → 𝕝) a b : 𝕝)
⊢ HSMul.hSMul (α := IncidenceAlgebra 𝕜 α) 0 f = 0

Tactic:
ext
-- 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕝 α
a b : α
h : a ≤ b
⊢ Eq.{u_3 + 1} (α := 𝕝) ((HSMul.hSMul (α := IncidenceAlgebra 𝕜 α) 0 f : (a : α) → α → 𝕝) a b : 𝕝)
    ((0 : (a : α) → α → 𝕝) a b : 𝕝)

Tactic:
sum_eq_zero fun x _ ↦ zero_smul _ _

Premises used: Multiset.sum, Multiset.foldr, Finset.sum_eq_zero, zero_smul, DFunLike.coe, Finset.sum
-- 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕝 α
a b : α
h : a ≤ b
⊢ Eq.{u_3 + 1} (α := 𝕝) ((HSMul.hSMul (α := IncidenceAlgebra 𝕜 α) 0 f : (a : α) → α → 𝕝) a b : 𝕝)
    ((0 : (a : α) → α → 𝕝) a b : 𝕝)

Tactic:
exact sum_eq_zero fun x _ ↦ zero_smul _ _

Premises used: Finset.sum_eq_zero, zero_smul
-- 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 𝕜 𝕝
h :
  ∀ (a b : α),
    a ≤ b →
      Eq.{u_3 + 1} (α := 𝕝)
        ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) 1 : 𝕝) 1 : (a : α) → α → 𝕝) a
            b :
          𝕝)
        ((1 : (a : α) → α → 𝕝) a b : 𝕝)
⊢ HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) 1 : 𝕝) 1 = 1

Tactic:
ext
-- 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 𝕜 𝕝
a b : α
h : a ≤ b
⊢ Eq.{u_3 + 1} (α := 𝕝)
    ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) 1 : 𝕝) 1 : (a : α) → α → 𝕝) a b :
      𝕝)
    ((1 : (a : α) → α → 𝕝) a b : 𝕝)

Tactic:
simp only [mul_boole, one_apply, smul_eq_mul, constSMul_apply, map_one]

Premises used: IncidenceAlgebra.constSMul_apply, IncidenceAlgebra.one_apply, mul_boole, map_one, smul_eq_mul
-- 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 d : 𝕜
h :
  ∀ (a b : α),
    a ≤ b →
      Eq.{u_3 + 1} (α := 𝕝)
        ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) (c * d) : 𝕝) 1 :
              (a : α) → α → 𝕝)
            a b :
          𝕝)
        ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 *
                HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1 :
              (a : α) → α → 𝕝)
            a b :
          𝕝)
⊢ HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) (c * d) : 𝕝) 1 =
    HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 *
      HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1

Tactic:
ext a b
-- 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 d : 𝕜
a b : α
h_1 : a ≤ b
h :
  a ≤ a →
    Eq.{u_3 + 1} (α := 𝕝)
      ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) (c * d) : 𝕝) 1 :
            (a : α) → α → 𝕝)
          a a :
        𝕝)
      ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 *
              HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1 :
            (a : α) → α → 𝕝)
          a a :
        𝕝)
h₁ :
  ∀ (h : a ≠ b),
    Eq.{u_3 + 1} (α := 𝕝)
      ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) (c * d) : 𝕝) 1 :
            (a : α) → α → 𝕝)
          a b :
        𝕝)
      ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 *
              HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1 :
            (a : α) → α → 𝕝)
          a b :
        𝕝)
⊢ Eq.{u_3 + 1} (α := 𝕝)
    ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) (c * d) : 𝕝) 1 : (a : α) → α → 𝕝)
        a b :
      𝕝)
    ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 *
            HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1 :
          (a : α) → α → 𝕝)
        a b :
      𝕝)

Tactic:
obtain rfl | h := eq_or_ne a b

Premises used: eq_or_ne, rfl
-- 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 d : 𝕜
a : α
h_1 : a ≤ a
h :
  (HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) *
      if True then 1 else 0) =
    ∑ x ∈ {a},
      HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) (if a = x then 1 else 0 : 𝕝) *
        HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) (if a = x then 1 else 0 : 𝕝)
⊢ Eq.{u_3 + 1} (α := 𝕝)
    ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) (c * d) : 𝕝) 1 : (a : α) → α → 𝕝)
        a a :
      𝕝)
    ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 *
            HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1 :
          (a : α) → α → 𝕝)
        a a :
      𝕝)

Tactic:
simp only [one_apply, smul_eq_mul, mul_apply, constSMul_apply, map_mul,
            eq_comm, Icc_self]

Premises used: IncidenceAlgebra.constSMul_apply, IncidenceAlgebra.one_apply, IncidenceAlgebra.mul_apply, eq_comm, map_mul, Finset.Icc_self, smul_eq_mul
-- 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 d : 𝕜
a : α
h : a ≤ a
⊢ (HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) *
      if True then 1 else 0) =
    ∑ x ∈ {a},
      HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) (if a = x then 1 else 0 : 𝕝) *
        HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) (if a = x then 1 else 0 : 𝕝)

Tactic:
simp
-- 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 d : 𝕜
a b : α
h_1 : a ≤ b
h : a ≠ b
h₁ :
  Eq.{u_3 + 1} (α := 𝕝) 0
    (∑ x ∈ Icc a b,
      if x = b ∧ a = x then
        HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝)
      else 0)
⊢ Eq.{u_3 + 1} (α := 𝕝)
    ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) (c * d) : 𝕝) 1 : (a : α) → α → 𝕝)
        a b :
      𝕝)
    ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 *
            HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1 :
          (a : α) → α → 𝕝)
        a b :
      𝕝)

Tactic:
simp only [one_apply, mul_one, smul_eq_mul, mul_apply, zero_mul,
            constSMul_apply, ← ite_and, ite_mul, mul_ite, map_mul, mul_zero, if_neg h]

Premises used: IncidenceAlgebra.constSMul_apply, IncidenceAlgebra.one_apply, IncidenceAlgebra.mul_apply, MulZeroClass.zero_mul, mul_ite, MulZeroClass.mul_zero, map_mul, ite_mul, smul_eq_mul, mul_one, ite_and, if_neg
-- 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 d : 𝕜
a b : α
h_1 : a ≤ b
h : a ≠ b
⊢ Eq.{u_3 + 1} (α := 𝕝) 0
    (∑ x ∈ Icc a b,
      if x = b ∧ a = x then
        HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝)
      else 0)

Tactic:
(sum_eq_zero fun x _ ↦ ?_).symm

Premises used: Finset.sum_eq_zero, Eq.symm
-- 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 d : 𝕜
a b : α
h_1 : a ≤ b
h : a ≠ b
h₁ :
  ∀ x ∈ Icc a b,
    (if x = b ∧ a = x then
        HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝)
      else 0) =
      0
⊢ Eq.{u_3 + 1} (α := 𝕝) 0
    (∑ x ∈ Icc a b,
      if x = b ∧ a = x then
        HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝)
      else 0)

Tactic:
refine (sum_eq_zero fun x _ ↦ ?_).symm

Premises used: Finset.sum_eq_zero, Eq.symm
-- 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 d : 𝕜
a b : α
h_1 : a ≤ b
h : a ≠ b
x : α
h_2 : x ∈ Icc a b
⊢ (if x = b ∧ a = x then
      HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝)
    else 0) =
    0

Tactic:
if_neg fun hx ↦ h <| hx.2.trans hx.1

Premises used: if_neg
-- 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 d : 𝕜
a b : α
h_1 : a ≤ b
h : a ≠ b
x : α
h_2 : x ∈ Icc a b
⊢ (if x = b ∧ a = x then
      HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝)
    else 0) =
    0

Tactic:
exact if_neg fun hx ↦ h <| hx.2.trans hx.1

Premises used: if_neg
-- 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 𝕜 𝕝
rw : HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) 0 1 = 0
rw₁ rw₂ : Eq (α := IncidenceAlgebra 𝕝 α) 0 0
⊢ HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) 0 : 𝕝) 1 = 0

Tactic:
rw [map_zero, zero_smul]

Premises used: map_zero, zero_smul
-- 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 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
rw₁ 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
⊢ HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) (c + d) : 𝕝) 1 =
    HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 +
      HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1

Tactic:
rw [map_add, add_smul]

Premises used: map_add, add_smul
-- 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} (α := 𝕝)
      ((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 :
        𝕝)
      ((HMul.hMul (β := IncidenceAlgebra 𝕝 α) f
              (({
                      toFun := fun (c : 𝕜) ↦
                        HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : 𝕜 →+* IncidenceAlgebra 𝕝 α } :
                    (a : 𝕜) → IncidenceAlgebra 𝕝 α)
                  c :
                IncidenceAlgebra 𝕝 α) :
            (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 =
    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 𝕝 α)

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} (α := 𝕝)
    ((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 :
      𝕝)
    ((HMul.hMul (β := IncidenceAlgebra 𝕝 α) f
            (({
                    toFun := fun (c : 𝕜) ↦
                      HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
                    map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : 𝕜 →+* IncidenceAlgebra 𝕝 α } :
                  (a : 𝕜) → IncidenceAlgebra 𝕝 α)
                c :
              IncidenceAlgebra 𝕝 α) :
          (a : α) → α → 𝕝)
        a b :
      𝕝)

Tactic:
simp [if_pos hab, constSMul_apply, mul_comm]

Premises used: IncidenceAlgebra.constSMul_apply, if_pos, mul_comm
-- 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} (α := 𝕝)
      ((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 :
        𝕝)
      ((HMul.hMul (β := IncidenceAlgebra 𝕝 α) f
              (({
                      toFun := fun (c : 𝕜) ↦
                        HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1,
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : 𝕜 →+* IncidenceAlgebra 𝕝 α } :
                    (a : 𝕜) → IncidenceAlgebra 𝕝 α)
                  c :
                IncidenceAlgebra 𝕝 α) :
            (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 =
    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 𝕝 α)

Tactic:
classical ext a b hab; simp [if_pos hab, constSMul_apply, mul_comm]

Premises used: IncidenceAlgebra.constSMul_apply, mul_comm