Theorem: IncidenceAlgebra.mu_spec_of_ne_right (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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Tactic:
have : mu 𝕜 a b = _ := mu_apply_of_ne h
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✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 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✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Tactic:
by_cases hab : a ≤ b
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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0

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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Tactic:
rw [Icc_eq_cons_Ico hab]
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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : a ≤ b
⊢ ∑ x ∈ cons b (Ico a b) ⋯, (mu 𝕜) a x = 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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : a ≤ b
⊢ ∑ x ∈ cons b (Ico a b) ⋯, (mu 𝕜) a x = 0
Tactic:
simp [this, neg_add_self]
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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Tactic:
have : ∀ x ∈ Icc a b, ¬a ≤ x := by
  intro x hx hn
  apply hab
  rw [mem_Icc] at hx
  exact le_trans hn hx.2
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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this✝ : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
this : ∀ x ∈ Icc a b, ¬a ≤ x
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this✝ : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
this : ∀ x ∈ Icc a b, ¬a ≤ x
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Tactic:
convert sum_const_zero
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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this✝ : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
this : ∀ x ∈ Icc a b, ¬a ≤ x
x✝ : α
a✝ : x✝ ∈ Icc a b
⊢ (mu 𝕜) a x✝ = 0

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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this✝ : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
this : ∀ x ∈ Icc a b, ¬a ≤ x
x✝ : α
a✝ : x✝ ∈ Icc a b
⊢ (mu 𝕜) a x✝ = 0
Tactic:
simp [apply_eq_zero_of_not_le (this ‹_› ‹_›)]
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✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
⊢ ∀ x ∈ Icc a b, ¬a ≤ x
Tactic:
intro x hx hn
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✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
x : α
hx : x ∈ Icc a b
hn : a ≤ x
⊢ False

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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
x : α
hx : x ∈ Icc a b
hn : a ≤ x
⊢ False
Tactic:
apply 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✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
x : α
hx : x ∈ Icc a b
hn : a ≤ x
⊢ a ≤ b

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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
x : α
hx : x ∈ Icc a b
hn : a ≤ x
⊢ a ≤ b
Tactic:
rw [mem_Icc] at hx
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✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
x : α
hx : a ≤ x ∧ x ≤ b
hn : a ≤ x
⊢ a ≤ b

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✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
x : α
hx : a ≤ x ∧ x ≤ b
hn : a ≤ x
⊢ a ≤ b
Tactic:
exact le_trans hn hx.2
State after:
no goals