Theorem: IncidenceAlgebra.mu_toDual (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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ (mu 𝕜) (toDual a) (toDual b) = (mu 𝕜) b a
Tactic:
let mud : IncidenceAlgebra 𝕜 αᵒᵈ :=
  { toFun := fun a b ↦ mu 𝕜 (ofDual b) (ofDual a)
    eq_zero_of_not_le' := fun a b hab ↦ apply_eq_zero_of_not_le (by exact hab) _ }
State after:
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ (mu 𝕜) (toDual a) (toDual b) = (mu 𝕜) b a

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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ (mu 𝕜) (toDual a) (toDual b) = (mu 𝕜) b a
Tactic:
suffices mu 𝕜 = mud by rw [this]; rfl
State after:
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ mu 𝕜 = mud

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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ mud * zeta 𝕜 = 1
Tactic:
clear a b
State after:
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ mud * zeta 𝕜 = 1

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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ mud * zeta 𝕜 = 1
Tactic:
ext a b
State after:
case h
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
⊢ (mud * zeta 𝕜) a b = 1 a b

State before:
case h
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
⊢ (mud * zeta 𝕜) a b = 1 a b
Tactic:
simp only [mul_boole, one_apply, mul_apply, coe_mk, zeta_apply]
State after:
case h
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
⊢ (∑ x ∈ Icc a b, if x ≤ b then mud a x else 0) = if a = b then 1 else 0

State before:
case h
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
⊢ (∑ x ∈ Icc a b, if x ≤ b then mud a x else 0) = if a = b then 1 else 0
Tactic:
obtain rfl | h := eq_or_ne a b
State after:
case h.inl
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a : αᵒᵈ
a✝ : a ≤ a
⊢ (∑ x ∈ Icc a a, if x ≤ a then mud a x else 0) = if a = a then 1 else 0

case h.inr
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
h : a ≠ b
⊢ (∑ x ∈ Icc a b, if x ≤ b then mud a x else 0) = if a = b then 1 else 0

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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a✝ b✝ : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
a b : αᵒᵈ
hab : ¬a ≤ b
⊢ ¬ofDual b ≤ ofDual a
Tactic:
exact hab
State after:
no goals

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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mu 𝕜 = mud
⊢ (mu 𝕜) (toDual a) (toDual b) = (mu 𝕜) b a
Tactic:
rw [this]
State after:
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mu 𝕜 = mud
⊢ mud (toDual a) (toDual b) = (mu 𝕜) b a

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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mu 𝕜 = mud
⊢ mud (toDual a) (toDual b) = (mu 𝕜) b a
Tactic:
rfl
State after:
no goals

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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 = 1
⊢ mu 𝕜 = mud
Tactic:
rw [← mu_mul_zeta] at this
State after:
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 = mu 𝕜 * zeta 𝕜
⊢ mu 𝕜 = mud

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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 * mu 𝕜 = mu 𝕜 * zeta 𝕜 * mu 𝕜
⊢ mu 𝕜 = mud
Tactic:
symm
State after:
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 * mu 𝕜 = mu 𝕜 * zeta 𝕜 * mu 𝕜
⊢ mud = mu 𝕜

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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 * mu 𝕜 = mu 𝕜 * zeta 𝕜 * mu 𝕜
⊢ mud = mu 𝕜
Tactic:
simpa [mul_assoc, zeta_mul_mu] using this
State after:
no goals

State before:
case h.inl
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a : αᵒᵈ
a✝ : a ≤ a
⊢ (∑ x ∈ Icc a a, if x ≤ a then mud a x else 0) = if a = a then 1 else 0
Tactic:
simp [mud]
State after:
no goals

State before:
case h.inr
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
h : a ≠ b
⊢ (∑ x ∈ Icc a b, if x ≤ b then mud a x else 0) = if a = b then 1 else 0
Tactic:
rw [if_neg h]
State after:
case h.inr
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
h : a ≠ b
⊢ (∑ x ∈ Icc a b, if x ≤ b then mud a x else 0) = 0

State before:
case h.inr
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
h : a ≠ b
⊢ (∑ x ∈ Icc a b, if x ≤ b then mud a x else 0) = 0
Tactic:
convert_to ∑ x in Icc (ofDual b) (ofDual a), mu 𝕜 x a = 0
State after:
case h.e'_2
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
h : a ≠ b
⊢ (∑ x ∈ Icc a b, if x ≤ b then mud a x else 0) = ∑ x ∈ Icc (ofDual b) (ofDual a), (mu 𝕜) x a

case h.inr
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
h : a ≠ b
⊢ ∑ x ∈ Icc (ofDual b) (ofDual a), (mu 𝕜) x a = 0

State before:
case h.e'_2
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
h : a ≠ b
⊢ (∑ x ∈ Icc a b, if x ≤ b then mud a x else 0) = ∑ x ∈ Icc (ofDual b) (ofDual a), (mu 𝕜) x a

case h.inr
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
h : a ≠ b
⊢ ∑ x ∈ Icc (ofDual b) (ofDual a), (mu 𝕜) x a = 0
Tactic:
sorry
State after:
case h.inr
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
h : a ≠ b
⊢ ∑ x ∈ Icc (ofDual b) (ofDual a), (mu 𝕜) x a = 0

State before:
case h.inr
𝕄 : 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✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
h : a ≠ b
⊢ ∑ x ∈ Icc (ofDual b) (ofDual a), (mu 𝕜) x a = 0
Tactic:
sorry
State after:
no goals