Theorem: IncidenceAlgebra.zeta_prod_apply (LeanCamCombi/Incidence.lean)

State before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α × β
⊢ (zeta 𝕜) a b = (zeta 𝕜) a.1 b.1 * (zeta 𝕜) a.2 b.2
Tactic:
simp [← ite_and, Prod.le_def, and_comm]
State after:
no goals