-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
@[simp]
lemma mu_toDual (a b : α) : mu 𝕜 (toDual a) (toDual b) = mu 𝕜 b a

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ mud * zeta 𝕜 = 1

Tactic:
ext a b

Result:
case h
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
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

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
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) = ∑ x ∈ Icc a b, mud a x

Tactic:
congr! with x hx

Result:
case a
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
x : αᵒᵈ
hx : x ∈ Icc a b
⊢ (if x ≤ b then mud a x else 0) = mud a x

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
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

Result:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
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 𝕜

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
⊢ (if ofDual b = ofDual a then 1 else 0) = if a = b then 1 else 0

Tactic:
simp [eq_comm]

Result:
no goals

Proof state:
case a
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
x : αᵒᵈ
hx : x ∈ Icc a b
⊢ (if x ≤ b then mud a x else 0) = mud a x

Tactic:
exact if_pos (mem_Icc.1 hx).2

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
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

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
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]

Result:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
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

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
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, mud a x = ∑ x ∈ Icc (ofDual b) (ofDual a), (mu 𝕜) x (ofDual a)

Tactic:
simp [Icc_orderDual_def, mud]

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ mud * zeta 𝕜 = 1

Tactic:
clear a b

Result:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ mud * zeta 𝕜 = 1

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
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

Result:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b => (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
⊢ mu 𝕜 = mud

Proof state:
case h
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
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]

Result:
case h
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
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

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a✝ b✝ : α
this : DecidableRel fun x1 x2 => x1 ≤ x2 := Classical.decRel fun x1 x2 => x1 ≤ x2
a b : αᵒᵈ
hab : ¬a ≤ b
⊢ ¬ofDual b ≤ ofDual a

Tactic:
exact hab

Result:
no goals