awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab_1 : ¬a = b
hab : ¬a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) 0

Tactic:
sum_eq_zero fun x hx ↦ apply_eq_zero_of_not_le
      (fun hxb ↦ hab <| (mem_Icc.1 hx).1.trans hxb) _

Premises used: Finset.sum_eq_zero, IncidenceAlgebra.apply_eq_zero_of_not_le, Finset.mem_Icc, _private.0.IncidenceAlgebra.mu', And.left, Iff.mp, LE.le.trans
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : One 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
a b : α
hab_1 : ¬a = b
hab : ¬a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) 0

Tactic:
exact sum_eq_zero fun x hx ↦ apply_eq_zero_of_not_le
      (fun hxb ↦ hab <| (mem_Icc.1 hx).1.trans hxb) _

Premises used: Finset.sum_eq_zero, IncidenceAlgebra.apply_eq_zero_of_not_le, Finset.mem_Icc, And.left, Iff.mp, LE.le.trans
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
h :
  ∀ (a b : α),
    a ≤ b →
      Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
        ((1 : (a : α) → α → 𝕜) a b : 𝕜)
⊢ HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) = 1

Tactic:
ext a b
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
rw :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ Icc a b, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜))
    (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
    (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜)

Tactic:
rw [mul_apply]

Premises used: IncidenceAlgebra.mul_apply
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
a₁ :
  ∀ (x : α) (hx : x ∈ Icc a b),
    HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) =
      (mu 𝕜 : (a : α) → α → 𝕜) a x
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ Icc a b, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜))
    (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x)

Tactic:
congr! with x hx
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) =
    (mu 𝕜 : (a : α) → α → 𝕜) a x

Tactic:
simp [(mem_Icc.1 hx).2]

Premises used: Finset.mem_Icc, And.right, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((1 : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
sum_Icc_mu_right ..

Premises used: IncidenceAlgebra.sum_Icc_mu_right, ite
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
_ :
  Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
    (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) a x : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (zeta 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
    ((1 : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
calc
    _ = ∑ x ∈ Icc a b, mu 𝕜 a x := by rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).2]
    _ = (1 : IncidenceAlgebra 𝕜 α) a b := sum_Icc_mu_right ..

Premises used: IncidenceAlgebra.sum_Icc_mu_right, Finset.Icc, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
h :
  ∀ (a b : α),
    a ≤ b →
      Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
        ((1 : (a : α) → α → 𝕜) a b : 𝕜)
⊢ HMul.hMul (α := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) = 1

Tactic:
ext a b
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
rw :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ Icc a b,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜))
    (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
    (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)

Tactic:
rw [mul_apply]

Premises used: IncidenceAlgebra.mul_apply
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
a₁ :
  ∀ (x : α) (hx : x ∈ Icc a b),
    HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) =
      (mu' 𝕜 : (a : α) → α → 𝕜) x b
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ Icc a b,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜))
    (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b)

Tactic:
congr! with x hx
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a x : 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) =
    (mu' 𝕜 : (a : α) → α → 𝕜) x b

Tactic:
simp [(mem_Icc.1 hx).1]

Premises used: Finset.mem_Icc, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜) ((1 : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
sum_Icc_mu'_left ..

Premises used: _private.0.IncidenceAlgebra.sum_Icc_mu'_left, ite
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddCommGroup 𝕜
inst_1 : MulOneClass 𝕜
inst_2 : PartialOrder α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
inst_5 : DecidableLE α
a b : α
h : a ≤ b
_ :
  Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
    (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((HMul.hMul (α := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) : (a : α) → α → 𝕜) a b : 𝕜)
    ((1 : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
calc
    _ = ∑ x ∈ Icc a b, mu' 𝕜 x b := by rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).1]
    _ = (1 : IncidenceAlgebra 𝕜 α) a b := sum_Icc_mu'_left ..

Premises used: Finset.Icc, OfNat.ofNat, DFunLike.coe, _private.0.IncidenceAlgebra.sum_Icc_mu'_left
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
⊢ Eq (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (mu' 𝕜)

Tactic:
left_inv_eq_right_inv (mu_mul_zeta _ _) (zeta_mul_mu' _ _)

Premises used: left_inv_eq_right_inv, IncidenceAlgebra.mu_mul_zeta, _private.0.IncidenceAlgebra.zeta_mul_mu'
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
⊢ Eq (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (mu' 𝕜)

Tactic:
exact left_inv_eq_right_inv (mu_mul_zeta _ _) (zeta_mul_mu' _ _)

Premises used: left_inv_eq_right_inv
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
⊢ Eq (α := IncidenceAlgebra 𝕜 α) (mu 𝕜) (mu' 𝕜)

Tactic:
classical
  exact left_inv_eq_right_inv (mu_mul_zeta _ _) (zeta_mul_mu' _ _)

Premises used: left_inv_eq_right_inv
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : α
hab : a ≠ b
rw : Eq.{u_2 + 1} (α := 𝕜) ((mu' 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := 𝕜) (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) (-∑ x ∈ Ioc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) a b : 𝕜) (-∑ x ∈ Ioc a b, (mu 𝕜 : (a : α) → α → 𝕜) x b : 𝕜)

Tactic:
rw [mu_eq_mu', mu'_eq_sum_Ioc_of_ne hab]

Premises used: _private.0.IncidenceAlgebra.mu'_eq_sum_Ioc_of_ne, _private.0.IncidenceAlgebra.mu_eq_mu'
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
inst_4 : DecidableLE α
rw : HMul.hMul (α := IncidenceAlgebra 𝕜 α) (β := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu' 𝕜) = 1
rw₁ rw₂ : Eq (α := IncidenceAlgebra 𝕜 α) 1 1
⊢ HMul.hMul (α := IncidenceAlgebra 𝕜 α) (β := IncidenceAlgebra 𝕜 α) (zeta 𝕜) (mu 𝕜) = 1

Tactic:
rw [mu_eq_mu', zeta_mul_mu']

Premises used: _private.0.IncidenceAlgebra.zeta_mul_mu', _private.0.IncidenceAlgebra.mu_eq_mu'
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : α
rw : Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu' 𝕜 : (a : α) → α → 𝕜) x b) (if a = b then 1 else 0)
rw₁ rw₂ : Eq.{u_2 + 1} (α := 𝕜) (if a = b then 1 else 0) (if a = b then 1 else 0)
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mu 𝕜 : (a : α) → α → 𝕜) x b) (if a = b then 1 else 0)

Tactic:
rw [mu_eq_mu', sum_Icc_mu'_left]

Premises used: _private.0.IncidenceAlgebra.mu_eq_mu', _private.0.IncidenceAlgebra.sum_Icc_mu'_left
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a_1 b_1 : α
this : DecidableLE α := Classical.decRel LE.le
a b : αᵒᵈ
hab : ¬a ≤ b
⊢ ¬LE.le (α := α) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a : α)

Tactic:
hab
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a_1 b_1 : α
this : DecidableLE α := Classical.decRel LE.le
a b : αᵒᵈ
hab : ¬a ≤ b
⊢ ¬LE.le (α := α) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a : α)

Tactic:
exact hab
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : α
this_1 : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
this : mu 𝕜 = mud
simp_rw :
  Eq.{u_2 + 1} (α := 𝕜)
    ((mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b) : 𝕜)
    ((mu 𝕜 : (a : α) → α → 𝕜) b a : 𝕜)
simp_rw₁ :
  Eq.{u_2 + 1} (α := 𝕜)
    (({
            toFun := fun (a b : αᵒᵈ) ↦
              (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
            eq_zero_of_not_le' := ⋯ } :
          (a : αᵒᵈ) → αᵒᵈ → 𝕜)
        ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b) :
      𝕜)
    ((mu 𝕜 : (a : α) → α → 𝕜) b a : 𝕜)
simp_rw₂ :
  Eq.{u_2 + 1} (α := 𝕜)
    ((mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) : α)
        ((ofDual : (a : αᵒᵈ) → α) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)) :
      𝕜)
    ((mu 𝕜 : (a : α) → α → 𝕜) b a : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜)
    ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b) : 𝕜)
    ((mu 𝕜 : (a : α) → α → 𝕜) b a : 𝕜)

Tactic:
simp_rw [this, mud, coe_mk, ofDual_toDual]

Premises used: OrderDual.ofDual_toDual, IncidenceAlgebra.coe_mk
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
suffices : mu 𝕜 = mud
⊢ Eq.{u_2 + 1} (α := 𝕜)
    ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b) : 𝕜)
    ((mu 𝕜 : (a : α) → α → 𝕜) b a : 𝕜)

Tactic:
suffices mu 𝕜 = mud by simp_rw [this, mud, coe_mk, ofDual_toDual]
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : α
this_1 : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 = 1
⊢ mud * zeta 𝕜 = HMul.hMul (α := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mu 𝕜) (zeta 𝕜)

Tactic:
rw [← mu_mul_zeta] at this

Premises used: IncidenceAlgebra.mu_mul_zeta
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : α
this_1 : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 = HMul.hMul (α := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mu 𝕜) (zeta 𝕜)
⊢ HMul.hMul (β := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mud * zeta 𝕜) (mu 𝕜) =
    HMul.hMul (α := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mu 𝕜) (zeta 𝕜) * mu 𝕜

Tactic:
apply_fun (· * mu 𝕜) at this

Premises used: HMul.hMul, IncidenceAlgebra.mu
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : α
this_1 : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
this :
  HMul.hMul (β := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mud * zeta 𝕜) (mu 𝕜) =
    HMul.hMul (α := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mu 𝕜) (zeta 𝕜) * mu 𝕜
symm : mud = mu 𝕜
⊢ mu 𝕜 = mud

Tactic:
symm
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : α
this_1 : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
this :
  HMul.hMul (β := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mud * zeta 𝕜) (mu 𝕜) =
    HMul.hMul (α := IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ) (mu 𝕜) (zeta 𝕜) * mu 𝕜
⊢ mud = mu 𝕜

Tactic:
simpa [mul_assoc, zeta_mul_mu] using this

Premises used: mul_assoc, IncidenceAlgebra.zeta_mul_mu
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
a b : α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
suffices : mud * zeta 𝕜 = 1
⊢ mu 𝕜 = mud

Tactic:
suffices mud * zeta 𝕜 = 1 by
    rw [← mu_mul_zeta] at this
    apply_fun (· * mu 𝕜) at this
    symm
    simpa [mul_assoc, zeta_mul_mu] using this
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
h :
  ∀ (a b : αᵒᵈ),
    a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((mud * zeta 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a b : 𝕜) ((1 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a b : 𝕜)
⊢ mud * zeta 𝕜 = 1

Tactic:
ext a b
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
h_1 : a ≤ b
h : Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, if x ≤ b then (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x else 0) (if a = b then 1 else 0)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mud * zeta 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a b : 𝕜) ((1 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a b : 𝕜)

Tactic:
simp only [mul_boole, one_apply, mul_apply, zeta_apply]

Premises used: IncidenceAlgebra.one_apply, IncidenceAlgebra.mul_apply, mul_boole, IncidenceAlgebra.zeta_apply
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
h : a ≤ b
a₁ :
  ∀ (x : αᵒᵈ) (hx : x ∈ Icc a b),
    Eq.{u_2 + 1} (α := 𝕜) (if x ≤ b then (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x else 0 : 𝕜)
      ((mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, if x ≤ b then (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x else 0)
    (∑ x ∈ Icc a b, (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x)

Tactic:
congr! with x hx
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
h : a ≤ b
x : αᵒᵈ
hx : x ∈ Icc a b
⊢ Eq.{u_2 + 1} (α := 𝕜) (if x ≤ b then (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x else 0 : 𝕜) ((mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x : 𝕜)

Tactic:
if_pos (mem_Icc.1 hx).2

Premises used: Finset.mem_Icc, if_pos, And.right, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
h : a ≤ b
x : αᵒᵈ
hx : x ∈ Icc a b
⊢ Eq.{u_2 + 1} (α := 𝕜) (if x ≤ b then (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x else 0 : 𝕜) ((mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x : 𝕜)

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

Premises used: Finset.mem_Icc, if_pos, And.right, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x ∈ Icc a b, (mud : (a : αᵒᵈ) → αᵒᵈ → 𝕜) a x)
    (∑ x ∈ (Icc ((ofDual : (a : αᵒᵈ) → α) b) ((ofDual : (a : αᵒᵈ) → α) a) : Finset α),
      ((mu 𝕜 : (a : α) → α → 𝕜) x ((ofDual : (a : αᵒᵈ) → α) a) : 𝕜))

Tactic:
simp [Icc_orderDual_def, mud]

Premises used: Finset.Icc_orderDual_def
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ (Icc ((ofDual : (a : αᵒᵈ) → α) b) ((ofDual : (a : αᵒᵈ) → α) a) : Finset α),
      ((mu 𝕜 : (a : α) → α → 𝕜) x ((ofDual : (a : αᵒᵈ) → α) a) : 𝕜))
    (if Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a : α) then 1 else 0)

Tactic:
sum_Icc_mu_left ..

Premises used: IncidenceAlgebra.sum_Icc_mu_left
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra.{u_2, u_5} 𝕜 αᵒᵈ :=
  { toFun := fun (a b : αᵒᵈ) ↦ (mu 𝕜 : (a : α) → α → 𝕜) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a),
    eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) (if Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) b : α) ((ofDual : (a : αᵒᵈ) → α) a : α) then 1 else 0)
    (if a = b then 1 else 0)

Tactic:
simp [eq_comm]

Premises used: eq_comm