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 : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
h₁ :
  ∀ (a b : α),
    a ≤ b → Eq.{u_2 + 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 : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) (((f + g) * h : (a : α) → α → 𝕜) a b : 𝕜) ((f * h + g * h : (a : α) → α → 𝕜) a b : 𝕜)

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

Premises used: Finset.sum_add_distrib, right_distrib, 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 : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) (((f + g) * h : (a : α) → α → 𝕜) a b : 𝕜) ((f * h + g * h : (a : α) → α → 𝕜) a b : 𝕜)

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

Premises used: Finset.sum_add_distrib, right_distrib, 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 : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((0 * f : (a : α) → α → 𝕜) a b : 𝕜) ((0 : (a : α) → α → 𝕜) a b : 𝕜)
⊢ 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 : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((0 * f : (a : α) → α → 𝕜) a b : 𝕜) ((0 : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
sum_eq_zero fun x _ ↦ zero_mul _

Premises used: Multiset.sum, Multiset.foldr, MulZeroClass.zero_mul, Finset.sum_eq_zero, 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 : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((0 * f : (a : α) → α → 𝕜) a b : 𝕜) ((0 : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
exact sum_eq_zero fun x _ ↦ zero_mul _

Premises used: Finset.sum_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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f * 0 : (a : α) → α → 𝕜) a b : 𝕜) ((0 : (a : α) → α → 𝕜) a b : 𝕜)
⊢ f * 0 = 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 : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f * 0 : (a : α) → α → 𝕜) a b : 𝕜) ((0 : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
sum_eq_zero fun x _ ↦ mul_zero _

Premises used: Multiset.sum, Multiset.foldr, Finset.sum_eq_zero, MulZeroClass.mul_zero, 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 : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f * 0 : (a : α) → α → 𝕜) a b : 𝕜) ((0 : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
exact sum_eq_zero fun x _ ↦ mul_zero _

Premises used: Finset.sum_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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((1 * f : (a : α) → α → 𝕜) a b : 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜)
⊢ 1 * f = f

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 : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((1 * f : (a : α) → α → 𝕜) a b : 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜)

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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f * 1 : (a : α) → α → 𝕜) a b : 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜)
⊢ f * 1 = f

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 : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f * 1 : (a : α) → α → 𝕜) a b : 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜)

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

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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
h₁ :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
      HMul.hMul (β := 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a (x.snd (β := fun (i : α) ↦ α)) : 𝕜)
          ((g : (a : α) → α → 𝕜) (x.snd (β := fun (i : α) ↦ α)) (x.fst (β := fun (i : α) ↦ α)) : 𝕜))
        ((h : (a : α) → α → 𝕜) (x.fst (β := fun (i : α) ↦ α)) b : 𝕜))
    (∑ x ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) fun (a : α) ↦ Icc a b,
      HMul.hMul (α := 𝕜) ((f : (a : α) → α → 𝕜) a (x.fst (β := fun (i : α) ↦ α)) : 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜)
          ((g : (a : α) → α → 𝕜) (x.fst (β := fun (i : α) ↦ α)) (x.snd (β := fun (i : α) ↦ α)) : 𝕜)
          ((h : (a : α) → α → 𝕜) (x.snd (β := fun (i : α) ↦ α)) b : 𝕜)))
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f * g * h : (a : α) → α → 𝕜) a b : 𝕜) ((f * (g * h) : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
simp only [mul_apply, sum_mul, mul_sum, sum_sigma']

Premises used: Finset.mul_sum, IncidenceAlgebra.mul_apply, Finset.sum_sigma', Finset.sum_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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
⊢ ∀ a_1 ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
    Membership.mem (α := (_ : α) × α) (γ := Finset ((_ : α) × α))
      ((Icc a b).sigma (α := fun (a : α) ↦ α) fun (a : α) ↦ Icc a b)
      (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a :
        (_ : α) × α)

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

Premises used: mul_assoc, le_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 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
⊢ ∀ (a_1 : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Icc a b).sigma (α := fun (a : α) ↦ α) fun (a : α) ↦ Icc a b) a_1 →
      Membership.mem (α := (_ : α) × α) ((Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a))
        (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a :
          (_ : α) × α)

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

Premises used: mul_assoc, le_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 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
⊢ ∀ a_1 ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
    (match (motive := (_ : α) × α → (_ : α) × α)
        match (motive := (_ : α) × α → (_ : α) × α) a_1 with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a with
      | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) =
      a_1

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

Premises used: mul_assoc, le_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 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
⊢ ∀ (a_1 : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Icc a b).sigma (α := fun (a : α) ↦ α) fun (a : α) ↦ Icc a b) a_1 →
      (match (motive := (_ : α) × α → (_ : α) × α)
          match (motive := (_ : α) × α → (_ : α) × α) a_1 with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) =
        a_1

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

Premises used: mul_assoc, le_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 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
⊢ ∀ a_1 ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
    HMul.hMul (β := 𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a (a_1.snd (β := fun (i : α) ↦ α)) : 𝕜)
          ((g : (a : α) → α → 𝕜) (a_1.snd (β := fun (i : α) ↦ α)) (a_1.fst (β := fun (i : α) ↦ α)) : 𝕜))
        ((h : (a : α) → α → 𝕜) (a_1.fst (β := fun (i : α) ↦ α)) b : 𝕜) =
      HMul.hMul (α := 𝕜)
        ((f : (a : α) → α → 𝕜) a
            (Sigma.fst (β := fun (i : α) ↦ α)
              (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
              | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a)) :
          𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜)
          ((g : (a : α) → α → 𝕜)
              (Sigma.fst (β := fun (i : α) ↦ α)
                (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
                | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a))
              (Sigma.snd (β := fun (i : α) ↦ α)
                (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
                | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a)) :
            𝕜)
          ((h : (a : α) → α → 𝕜)
              (Sigma.snd (β := fun (i : α) ↦ α)
                  (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
                  | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) :
                α)
              b :
            𝕜))

Tactic:
aesop (add simp mul_assoc) (add unsafe le_trans)

Premises used: mul_assoc, le_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 : AddCommMonoid 𝕜
inst_3 : AddCommMonoid 𝕝
inst_4 : SMul 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
a b : α
h : ¬a ≤ b
rw :
  Eq.{u_3 + 1} (α := 𝕝)
    (∑ x ∈ ∅,
      HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := 𝕝) ((f : (a : α) → α → 𝕜) a x : 𝕜) ((g : (a : α) → α → 𝕝) x b : 𝕝))
    0
rw₁ rw₂ : Eq.{u_3 + 1} (α := 𝕝) 0 0
⊢ Eq.{u_3 + 1} (α := 𝕝)
    (∑ x ∈ Icc a b,
      HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := 𝕝) ((f : (a : α) → α → 𝕜) a x : 𝕜) ((g : (a : α) → α → 𝕝) x b : 𝕝))
    0

Tactic:
rw [Icc_eq_empty h, sum_empty]

Premises used: Finset.Icc_eq_empty, Finset.sum_empty
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
𝕝 : Type u_3
α : Type u_5
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : AddCommMonoid 𝕜
inst_3 : AddCommMonoid 𝕝
inst_4 : SMul 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
a b : α
⊢ Eq.{u_3 + 1} (α := 𝕝) ((f • g : (a : α) → α → 𝕝) a b : 𝕝)
    (∑ x ∈ Icc a b,
        HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := 𝕝) ((f : (a : α) → α → 𝕜) a x : 𝕜) ((g : (a : α) → α → 𝕝) x b : 𝕝) :
      𝕝)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.sum, 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : AddCommMonoid 𝕜
inst_3 : Monoid 𝕜
inst_4 : Semiring 𝕝
inst_5 : AddCommMonoid 𝕞
inst_6 : SMul 𝕜 𝕝
inst_7 : Module 𝕝 𝕞
inst_8 : DistribMulAction 𝕜 𝕞
inst_9 : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
h₁ :
  ∀ (a b : α),
    a ≤ b → Eq.{u_4 + 1} (α := 𝕞) (((f • g) • h : (a : α) → α → 𝕞) a b : 𝕞) ((f • g • h : (a : α) → α → 𝕞) a b : 𝕞)
⊢ (f • g) • h = f • g • h

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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : AddCommMonoid 𝕜
inst_3 : Monoid 𝕜
inst_4 : Semiring 𝕝
inst_5 : AddCommMonoid 𝕞
inst_6 : SMul 𝕜 𝕝
inst_7 : Module 𝕝 𝕞
inst_8 : DistribMulAction 𝕜 𝕞
inst_9 : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
h_1 : a ≤ b
h₁ :
  Eq.{u_4 + 1} (α := 𝕞)
    (∑ x ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
      HSMul.hSMul (β := 𝕞)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := 𝕝) ((f : (a : α) → α → 𝕜) a (x.snd (β := fun (i : α) ↦ α)) : 𝕜)
          ((g : (a : α) → α → 𝕝) (x.snd (β := fun (i : α) ↦ α)) (x.fst (β := fun (i : α) ↦ α)) : 𝕝))
        ((h : (a : α) → α → 𝕞) (x.fst (β := fun (i : α) ↦ α)) b : 𝕞))
    (∑ x ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) fun (a : α) ↦ Icc a b,
      HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜) ((f : (a : α) → α → 𝕜) a (x.fst (β := fun (i : α) ↦ α)) : 𝕜)
        (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕝) (β := 𝕞)
          ((g : (a : α) → α → 𝕝) (x.fst (β := fun (i : α) ↦ α)) (x.snd (β := fun (i : α) ↦ α)) : 𝕝)
          ((h : (a : α) → α → 𝕞) (x.snd (β := fun (i : α) ↦ α)) b : 𝕞)))
⊢ Eq.{u_4 + 1} (α := 𝕞) (((f • g) • h : (a : α) → α → 𝕞) a b : 𝕞) ((f • g • h : (a : α) → α → 𝕞) a b : 𝕞)

Tactic:
simp only [smul_apply, sum_smul, smul_sum, sum_sigma']

Premises used: Finset.sum_smul, IncidenceAlgebra.smul_apply, Finset.sum_sigma', Finset.smul_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 : AddCommMonoid 𝕜
inst_3 : Monoid 𝕜
inst_4 : Semiring 𝕝
inst_5 : AddCommMonoid 𝕞
inst_6 : SMul 𝕜 𝕝
inst_7 : Module 𝕝 𝕞
inst_8 : DistribMulAction 𝕜 𝕞
inst_9 : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
h_1 : a ≤ b
⊢ ∀ a_1 ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
    Membership.mem (α := (_ : α) × α) (γ := Finset ((_ : α) × α))
      ((Icc a b).sigma (α := fun (a : α) ↦ α) fun (a : α) ↦ Icc a b)
      (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a :
        (_ : α) × α)

Tactic:
aesop (add unsafe le_trans)

Premises used: le_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 : AddCommMonoid 𝕜
inst_3 : Monoid 𝕜
inst_4 : Semiring 𝕝
inst_5 : AddCommMonoid 𝕞
inst_6 : SMul 𝕜 𝕝
inst_7 : Module 𝕝 𝕞
inst_8 : DistribMulAction 𝕜 𝕞
inst_9 : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
h_1 : a ≤ b
⊢ ∀ (a_1 : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Icc a b).sigma (α := fun (a : α) ↦ α) fun (a : α) ↦ Icc a b) a_1 →
      Membership.mem (α := (_ : α) × α) ((Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a))
        (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a :
          (_ : α) × α)

Tactic:
aesop (add unsafe le_trans)

Premises used: le_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 : AddCommMonoid 𝕜
inst_3 : Monoid 𝕜
inst_4 : Semiring 𝕝
inst_5 : AddCommMonoid 𝕞
inst_6 : SMul 𝕜 𝕝
inst_7 : Module 𝕝 𝕞
inst_8 : DistribMulAction 𝕜 𝕞
inst_9 : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
h_1 : a ≤ b
⊢ ∀ a_1 ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
    (match (motive := (_ : α) × α → (_ : α) × α)
        match (motive := (_ : α) × α → (_ : α) × α) a_1 with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a with
      | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) =
      a_1

Tactic:
aesop (add unsafe le_trans)

Premises used: le_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 : AddCommMonoid 𝕜
inst_3 : Monoid 𝕜
inst_4 : Semiring 𝕝
inst_5 : AddCommMonoid 𝕞
inst_6 : SMul 𝕜 𝕝
inst_7 : Module 𝕝 𝕞
inst_8 : DistribMulAction 𝕜 𝕞
inst_9 : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
h_1 : a ≤ b
⊢ ∀ (a_1 : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) ((Icc a b).sigma (α := fun (a : α) ↦ α) fun (a : α) ↦ Icc a b) a_1 →
      (match (motive := (_ : α) × α → (_ : α) × α)
          match (motive := (_ : α) × α → (_ : α) × α) a_1 with
          | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a with
        | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) =
        a_1

Tactic:
aesop (add unsafe le_trans)

Premises used: le_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 : AddCommMonoid 𝕜
inst_3 : Monoid 𝕜
inst_4 : Semiring 𝕝
inst_5 : AddCommMonoid 𝕞
inst_6 : SMul 𝕜 𝕝
inst_7 : Module 𝕝 𝕞
inst_8 : DistribMulAction 𝕜 𝕞
inst_9 : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
h_1 : a ≤ b
⊢ ∀ a_1 ∈ (Icc a b).sigma (α := fun (a : α) ↦ α) (Icc a),
    HSMul.hSMul (β := 𝕞)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := 𝕝) ((f : (a : α) → α → 𝕜) a (a_1.snd (β := fun (i : α) ↦ α)) : 𝕜)
          ((g : (a : α) → α → 𝕝) (a_1.snd (β := fun (i : α) ↦ α)) (a_1.fst (β := fun (i : α) ↦ α)) : 𝕝))
        ((h : (a : α) → α → 𝕞) (a_1.fst (β := fun (i : α) ↦ α)) b : 𝕞) =
      HSMul.hSMul.{u_2, u_4, u_4} (α := 𝕜)
        ((f : (a : α) → α → 𝕜) a
            (Sigma.fst (β := fun (i : α) ↦ α)
              (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
              | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a)) :
          𝕜)
        (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕝) (β := 𝕞)
          ((g : (a : α) → α → 𝕝)
              (Sigma.fst (β := fun (i : α) ↦ α)
                (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
                | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a))
              (Sigma.snd (β := fun (i : α) ↦ α)
                (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
                | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a)) :
            𝕝)
          ((h : (a : α) → α → 𝕞)
              (Sigma.snd (β := fun (i : α) ↦ α)
                  (match (motive := (_ : α) × α → (_ : α) × α) a_1 with
                  | ⟨a, b⟩ => Sigma.mk (β := fun (i : α) ↦ α) b a) :
                α)
              b :
            𝕞))

Tactic:
aesop (add unsafe le_trans)

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

Tactic:
simp [ite_smul, hab]

Premises used: ite_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 : 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 𝕝 α) f 0 : (a : α) → α → 𝕝) a b : 𝕝)
        ((0 : (a : α) → α → 𝕝) a b : 𝕝)
⊢ HSMul.hSMul (β := IncidenceAlgebra 𝕝 α) f 0 = 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 𝕝 α) f 0 : (a : α) → α → 𝕝) a b : 𝕝)
    ((0 : (a : α) → α → 𝕝) a b : 𝕝)

Tactic:
sum_eq_zero fun x _ ↦ smul_zero _

Premises used: Multiset.sum, Multiset.foldr, Finset.sum_eq_zero, smul_zero, 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 𝕝 α) f 0 : (a : α) → α → 𝕝) a b : 𝕝)
    ((0 : (a : α) → α → 𝕝) a b : 𝕝)

Tactic:
exact sum_eq_zero fun x _ ↦ smul_zero _

Premises used: Finset.sum_eq_zero, smul_zero