Theorem: IncidenceAlgebra.mu_mul_zeta (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✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
⊢ mu 𝕜 * 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✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
⊢ (mu 𝕜 * 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✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
⊢ (mu 𝕜 * zeta 𝕜) a b = 1 a b
Tactic:
rw [mul_apply, one_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✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x * (zeta 𝕜) x b = 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✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x * (zeta 𝕜) x b = if a = b then 1 else 0
Tactic:
split_ifs with he
State after:
case pos
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
he : a = b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x * (zeta 𝕜) x b = 1

case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
he : ¬a = b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x * (zeta 𝕜) x b = 0

State before:
case pos
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
he : a = b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x * (zeta 𝕜) x b = 1
Tactic:
simp [he]
State after:
no goals

State before:
case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
he : ¬a = b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x * (zeta 𝕜) x b = 0
Tactic:
simp only [mul_one, zeta_apply, mul_ite]
State after:
case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
he : ¬a = b
⊢ (∑ x ∈ Icc a b, if x ≤ b then (mu 𝕜) a x else (mu 𝕜) a x * 0) = 0

State before:
case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
he : ¬a = b
⊢ (∑ x ∈ Icc a b, if x ≤ b then (mu 𝕜) a x else (mu 𝕜) a x * 0) = 0
Tactic:
convert mu_spec_of_ne_right he
State after:
case h.e'_2.a
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝¹ : a ≤ b
he : ¬a = b
x✝ : α
a✝ : x✝ ∈ Icc a b
⊢ (if x✝ ≤ b then (mu 𝕜) a x✝ else (mu 𝕜) a x✝ * 0) = (mu 𝕜) a x✝

case neg.convert_3
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
he : ¬a = b
⊢ One 𝕜

State before:
case h.e'_2.a
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝¹ : a ≤ b
he : ¬a = b
x✝ : α
a✝ : x✝ ∈ Icc a b
⊢ (if x✝ ≤ b then (mu 𝕜) a x✝ else (mu 𝕜) a x✝ * 0) = (mu 𝕜) a x✝

case neg.convert_3
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
a✝ : a ≤ b
he : ¬a = b
⊢ One 𝕜
Tactic:
rw [if_pos (mem_Icc.mp ‹_›).2]
State after:
no goals