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 : 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 𝕞 α
⊢ (f • g) • h = f • g • h
have h₁ : ∀ (a b : α),
  a ≤ b → Eq.{u_4 + 1} (α := 𝕞) (((f • g) • h : (a : α) → α → 𝕞) a b : 𝕞) ((f • g • h : (a : α) → α → 𝕞) a b : 𝕞)
Tactic: ext a b
-- 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 : 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
⊢ Eq.{u_4 + 1} (α := 𝕞) (((f • g) • h : (a : α) → α → 𝕞) a b : 𝕞) ((f • g • h : (a : α) → α → 𝕞) a b : 𝕞)
have 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 : 𝕞)))
Tactic: simp only [smul_apply, sum_smul, smul_sum, sum_sigma']
-- 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 : 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
⊢ 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 : 𝕞)))
have h₁ : ∀ 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: apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩)
-- 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 : 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₁ :
  ∀ 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 :
        (_ : α) × α)
⊢ 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 : 𝕞)))
have h₂ : ∀ (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: apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩)
-- 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 : 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₁ :
  ∀ 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 :
        (_ : α) × α)
h₂ :
  ∀ (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 :
          (_ : α) × α)
⊢ 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 : 𝕞)))
have h₃ : ∀ 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: apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩)
-- 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 : 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₁ :
  ∀ 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 :
        (_ : α) × α)
h₂ :
  ∀ (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 :
          (_ : α) × α)
h₃ :
  ∀ 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
⊢ 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 : 𝕞)))
have h₄ : ∀ (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: apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩)
-- 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕝 α
⊢ HSMul.hSMul (α := IncidenceAlgebra 𝕜 α) 1 f = f
have h : ∀ (a b : α) (hab : a ≤ b),
  Eq.{u_3 + 1} (α := 𝕝) ((HSMul.hSMul (α := IncidenceAlgebra 𝕜 α) 1 f : (a : α) → α → 𝕝) a b : 𝕝)
    ((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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
⊢ HSMul.hSMul (β := IncidenceAlgebra 𝕝 α) f 0 = 0
have h : ∀ (a b : α),
  a ≤ b →
    Eq.{u_3 + 1} (α := 𝕝) ((HSMul.hSMul (β := IncidenceAlgebra 𝕝 α) f 0 : (a : α) → α → 𝕝) a b : 𝕝)
      ((0 : (a : α) → α → 𝕝) a b : 𝕝)
Tactic: ext
-- 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g h : IncidenceAlgebra 𝕝 α
⊢ f • (g + h) = f • g + f • h
have h₁ : ∀ (a b : α),
  a ≤ b → Eq.{u_3 + 1} (α := 𝕝) ((f • (g + h) : (a : α) → α → 𝕝) a b : 𝕝) ((f • g + f • h : (a : α) → α → 𝕝) a b : 𝕝)
Tactic: ext
-- 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f g : IncidenceAlgebra 𝕜 α
h : IncidenceAlgebra 𝕝 α
⊢ (f + g) • h = f • h + g • h
have h₁ : ∀ (a b : α),
  a ≤ b → Eq.{u_3 + 1} (α := 𝕝) (((f + g) • h : (a : α) → α → 𝕝) a b : 𝕝) ((f • h + g • h : (a : α) → α → 𝕝) a b : 𝕝)
Tactic: ext
-- 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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DecidableEq α
inst_3 : Semiring 𝕜
inst_4 : Semiring 𝕝
inst_5 : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕝 α
⊢ HSMul.hSMul (α := IncidenceAlgebra 𝕜 α) 0 f = 0
have h : ∀ (a b : α),
  a ≤ b →
    Eq.{u_3 + 1} (α := 𝕝) ((HSMul.hSMul (α := IncidenceAlgebra 𝕜 α) 0 f : (a : α) → α → 𝕝) a b : 𝕝)
      ((0 : (a : α) → α → 𝕝) a b : 𝕝)
Tactic: ext
-- 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 𝕜 𝕝
⊢ HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) 1 : 𝕝) 1 = 1
have h : ∀ (a b : α),
  a ≤ b →
    Eq.{u_3 + 1} (α := 𝕝)
      ((HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) 1 : 𝕝) 1 : (a : α) → α → 𝕝) a
          b :
        𝕝)
      ((1 : (a : α) → α → 𝕝) a b : 𝕝)
Tactic: ext
-- 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 : 𝕜
⊢ HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) (c * d) : 𝕝) 1 =
    HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 *
      HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1
have 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 :
        𝕝)
Tactic: ext a b
-- 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 : 𝕜
a b : α
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 :
      𝕝)
have 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 :
      𝕝)
Tactic: obtain rfl | h := eq_or_ne a b
Cleared hypotheses: b, 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 : 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 :
        𝕝)
⊢ 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 :
      𝕝)
have 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 :
      𝕝)
Tactic: obtain rfl | h := eq_or_ne a b
-- 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 : 𝕜
a : α
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 :
      𝕝)
have 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 : 𝕝)
Tactic: simp only [one_apply, smul_eq_mul, mul_apply, constSMul_apply, map_mul,
            eq_comm, Icc_self]
-- 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 : 𝕜
a b : α
h_1 : a ≤ b
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 :
      𝕝)
have 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)
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]
-- 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 : 𝕜
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)
have h₁ : ∀ x ∈ Icc a b,
  (if x = b ∧ a = x then
      HMul.hMul (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝)
    else 0) =
    0
Tactic: refine (sum_eq_zero fun x _ ↦ ?_).symm
-- 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 𝕜 𝕝
⊢ HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) 0 : 𝕝) 1 = 0
have rw : HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) 0 1 = 0
Tactic: rw [map_zero, zero_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 𝕜 𝕝
rw : HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) 0 1 = 0
⊢ HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) 0 : 𝕝) 1 = 0
have rw₁ : Eq (α := IncidenceAlgebra 𝕝 α) 0 0
Tactic: rw [map_zero, zero_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 d : 𝕜
⊢ 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 𝕝 α)
    (HAdd.hAdd (α := 𝕝) (β := 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝)) 1 =
  HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) c : 𝕝) 1 +
    HSMul.hSMul (α := 𝕝) (β := IncidenceAlgebra 𝕝 α) ((algebraMap 𝕜 𝕝 : (a : 𝕜) → 𝕝) d : 𝕝) 1
Tactic: rw [map_add, add_smul]