awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
n : ℕ
⊢ Fintype.card { p : DyckWord // p.semilength = n } = catalan n
have rw : Fintype.card ↥(treesOfNumNodesEq n) = (treesOfNumNodesEq n).card
Tactic: rw [← Fintype.ofEquiv_card (equivTreesOfNumNodesEq n), ← treesOfNumNodesEq_card_eq_catalan]
-- 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 : Zero 𝕜
inst_1 : LE α
a b : α
f g : IncidenceAlgebra 𝕜 α
h : f.toFun = g.toFun
⊢ f = g
have mk : ∀ (toFun : α → α → 𝕜) (eq_zero_of_not_le' : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun a b = 0)
  (h : { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α }.toFun = g.toFun),
  { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α } = g
Tactic: cases f
Cleared hypotheses: f, 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 : Zero 𝕜
inst_1 : LE α
a b : α
g : IncidenceAlgebra 𝕜 α
toFun : α → α → 𝕜
eq_zero_of_not_le' : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun a b = 0
h : { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α }.toFun = g.toFun
⊢ { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α } = g
have mk : ∀ (toFun_1 : α → α → 𝕜) (eq_zero_of_not_le'_1 : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun_1 a b = 0)
  (h :
    { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α }.toFun =
      { toFun := toFun_1, eq_zero_of_not_le' := eq_zero_of_not_le'_1 : IncidenceAlgebra 𝕜 α }.toFun),
  { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α } =
    { toFun := toFun_1, eq_zero_of_not_le' := eq_zero_of_not_le'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)
⊢ f = g
have refine : ∀ (a b : α), Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
Tactic: refine DFunLike.coe_injective' (funext₂ fun a b ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)
a b : α
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
have pos : ∀ (hab : a ≤ b), Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)
a b : α
pos : ∀ (hab : a ≤ b), Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
have neg : ∀ (hab : ¬a ≤ b), Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)
a b : α
hab : ¬a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
have neg : Eq.{u_2 + 1} (α := 𝕜) (0 : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
Tactic: rw [apply_eq_zero_of_not_le hab, apply_eq_zero_of_not_le hab]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)
a b : α
hab : ¬a ≤ b
neg : Eq.{u_2 + 1} (α := 𝕜) (0 : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
have neg₁ : Eq.{u_2 + 1} (α := 𝕜) 0 0
Tactic: rw [apply_eq_zero_of_not_le hab, apply_eq_zero_of_not_le 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 : AddZeroClass 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ HAdd.hAdd (α := (a : α) → α → 𝕜) (β := (a : α) → α → 𝕜) (⇑f : (a : α) → α → 𝕜) (⇑g : (a : α) → α → 𝕜) a b = 0
have simp_rw : HAdd.hAdd (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜) = 0
Tactic: simp_rw [Pi.add_apply, apply_eq_zero_of_not_le h, zero_add]
-- 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 : AddZeroClass 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
simp_rw : HAdd.hAdd (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜) = 0
⊢ HAdd.hAdd (α := (a : α) → α → 𝕜) (β := (a : α) → α → 𝕜) (⇑f : (a : α) → α → 𝕜) (⇑g : (a : α) → α → 𝕜) a b = 0
have simp_rw₁ : HAdd.hAdd (α := 𝕜) 0 0 = 0
Tactic: simp_rw [Pi.add_apply, apply_eq_zero_of_not_le h, zero_add]
-- 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
M : Type u_7
inst : Zero 𝕜
inst_1 : LE α
inst_2 : SMulZeroClass M 𝕜
c : M
f : IncidenceAlgebra 𝕜 α
a b : α
hab : ¬a ≤ b
⊢ HSMul.hSMul (β := (a : α) → α → 𝕜) c (⇑f : (a : α) → α → 𝕜) a b = 0
have simp_rw : HSMul.hSMul (β := 𝕜) c ((f : (a : α) → α → 𝕜) a b : 𝕜) = 0
Tactic: simp_rw [Pi.smul_apply, apply_eq_zero_of_not_le hab, smul_zero]
-- 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
M : Type u_7
inst : Zero 𝕜
inst_1 : LE α
inst_2 : SMulZeroClass M 𝕜
c : M
f : IncidenceAlgebra 𝕜 α
a b : α
hab : ¬a ≤ b
simp_rw : HSMul.hSMul (β := 𝕜) c ((f : (a : α) → α → 𝕜) a b : 𝕜) = 0
⊢ HSMul.hSMul (β := (a : α) → α → 𝕜) c (⇑f : (a : α) → α → 𝕜) a b = 0
have simp_rw₁ : HSMul.hSMul (β := 𝕜) c 0 = 0
Tactic: simp_rw [Pi.smul_apply, apply_eq_zero_of_not_le hab, smul_zero]
-- 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
M : Type u_7
inst : Zero 𝕜
inst_1 : LE α
inst_2 : SMulZeroClass M 𝕜
c : M
⊢ HSMul.hSMul (β := IncidenceAlgebra 𝕜 α) c 0 = 0
have h : ∀ (a b : α),
  a ≤ b →
    Eq.{u_2 + 1} (α := 𝕜) ((HSMul.hSMul (β := IncidenceAlgebra 𝕜 α) c 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 : AddGroup 𝕜
inst_1 : LE α
f : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((-(⇑f : (a : α) → α → 𝕜)) a b : 𝕜) (0 : 𝕜)
have simp_rw : Eq.{u_2 + 1} (α := 𝕜) (-(f : (a : α) → α → 𝕜) a b : 𝕜) (0 : 𝕜)
Tactic: simp_rw [Pi.neg_apply, apply_eq_zero_of_not_le h, neg_zero]
-- 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 : AddGroup 𝕜
inst_1 : LE α
f : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
simp_rw : Eq.{u_2 + 1} (α := 𝕜) (-(f : (a : α) → α → 𝕜) a b : 𝕜) (0 : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((-(⇑f : (a : α) → α → 𝕜)) a b : 𝕜) (0 : 𝕜)
have simp_rw₁ : Eq.{u_2 + 1} (α := 𝕜) (-0) 0
Tactic: simp_rw [Pi.neg_apply, apply_eq_zero_of_not_le h, neg_zero]
-- 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 : AddGroup 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ HSub.hSub (α := (a : α) → α → 𝕜) (β := (a : α) → α → 𝕜) (⇑f : (a : α) → α → 𝕜) (⇑g : (a : α) → α → 𝕜) a b = 0
have simp_rw : HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜) = 0
Tactic: simp_rw [Pi.sub_apply, apply_eq_zero_of_not_le h, sub_zero]
-- 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 : AddGroup 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
simp_rw : HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜) = 0
⊢ HSub.hSub (α := (a : α) → α → 𝕜) (β := (a : α) → α → 𝕜) (⇑f : (a : α) → α → 𝕜) (⇑g : (a : α) → α → 𝕜) a b = 0
have simp_rw₁ : HSub.hSub (α := 𝕜) 0 0 = 0
Tactic: simp_rw [Pi.sub_apply, apply_eq_zero_of_not_le h, sub_zero]
-- 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 : Mul 𝕜
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ Icc a b, HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a x : 𝕜) ((g : (a : α) → α → 𝕜) x b : 𝕜)) 0
have rw : Eq.{u_2 + 1} (α := 𝕜)
  (∑ x ∈ ∅, HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a x : 𝕜) ((g : (a : α) → α → 𝕜) x b : 𝕜)) 0
Tactic: rw [Icc_eq_empty h, sum_empty]
-- 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 : Mul 𝕜
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
rw :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ ∅, HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a x : 𝕜) ((g : (a : α) → α → 𝕜) x b : 𝕜)) 0
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ Icc a b, HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a x : 𝕜) ((g : (a : α) → α → 𝕜) x b : 𝕜)) 0
have rw₁ : Eq.{u_2 + 1} (α := 𝕜) 0 0
Tactic: rw [Icc_eq_empty h, sum_empty]
-- 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 : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
⊢ f * (g + h) = f * g + f * h
have h₁ : ∀ (a b : α),
  a ≤ b → Eq.{u_2 + 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 : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
⊢ (f + g) * h = f * h + g * h
have h₁ : ∀ (a b : α),
  a ≤ b → Eq.{u_2 + 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 : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ 0 * f = 0
have h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((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 : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ f * 0 = 0
have h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((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 : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ 1 * f = f
have h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((1 * f : (a : α) → α → 𝕜) a b : 𝕜) ((f : (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 : NonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ f * 1 = f
have h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f * 1 : (a : α) → α → 𝕜) a b : 𝕜) ((f : (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 𝕜
f g h : IncidenceAlgebra 𝕜 α
⊢ f * g * h = f * (g * h)
have h₁ : ∀ (a b : α),
  a ≤ b → Eq.{u_2 + 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 : DecidableEq α
inst_3 : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f * g * h : (a : α) → α → 𝕜) a b : 𝕜) ((f * (g * h) : (a : α) → α → 𝕜) a b : 𝕜)
have 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 : 𝕜)))
Tactic: simp only [mul_apply, sum_mul, mul_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 : DecidableEq α
inst_3 : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
⊢ 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 : 𝕜)))
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 : DecidableEq α
inst_3 : Semiring 𝕜
f g 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_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 : 𝕜)))
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 : DecidableEq α
inst_3 : Semiring 𝕜
f g 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_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 : 𝕜)))
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 : DecidableEq α
inst_3 : Semiring 𝕜
f g 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_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 : 𝕜)))
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 : AddCommMonoid 𝕜
inst_3 : AddCommMonoid 𝕝
inst_4 : SMul 𝕜 𝕝
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
a b : α
h : ¬a ≤ b
⊢ 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
have rw : Eq.{u_3 + 1} (α := 𝕝)
  (∑ x ∈ ∅,
    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]
-- 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 : 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
⊢ 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
have rw₁ : Eq.{u_3 + 1} (α := 𝕝) 0 0
Tactic: rw [Icc_eq_empty h, sum_empty]