awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y) = f x
have y : Eq.{u_2 + 1} (α := 𝕜) (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y))
  (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜))
Tactic: calc
    ∑ y ∈ Ici x, mu 𝕜 x y * g y = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, f z := by simp_rw [h]
    _ = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, zeta 𝕜 y z * f z := by
      congr with y
      rw [sum_congr rfl fun z hz ↦ ?_]
      rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, mu 𝕜 x y * zeta 𝕜 y z * f z := by simp [mul_sum]
    _ = ∑ z ∈ Ici x, ∑ y ∈ Icc x z, mu 𝕜 x y * zeta 𝕜 y z * f z := by
      rw [sum_sigma' (Ici x) fun y ↦ Ici y]
      rw [sum_sigma' (Ici x) fun z ↦ Icc x z]
      simp only [mul_boole, zero_mul, ite_mul, zeta_apply]
      apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
        aesop (add simp mul_assoc) (add unsafe le_trans)
    _ = ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp_rw [mul_apply, sum_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp only [mu_mul_zeta 𝕜, one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici, le_refl,
        ↓reduceIte, ← add_sum_Ioi_eq_sum_Ici, left_eq_add]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
    _ = f x := by
      simp only [one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici,
        ← add_sum_Ioi_eq_sum_Ici, le_refl, ↓reduceIte, add_eq_left]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
y :
  Eq.{u_2 + 1} (α := 𝕜) (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y))
    (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜))
⊢ ∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y) = f x
have y₁ : Eq.{u_2 + 1} (α := 𝕜)
  (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜))
  (∑ y ∈ Ici x,
    HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜)
      (∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z) : 𝕜))
Tactic: calc
    ∑ y ∈ Ici x, mu 𝕜 x y * g y = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, f z := by simp_rw [h]
    _ = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, zeta 𝕜 y z * f z := by
      congr with y
      rw [sum_congr rfl fun z hz ↦ ?_]
      rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, mu 𝕜 x y * zeta 𝕜 y z * f z := by simp [mul_sum]
    _ = ∑ z ∈ Ici x, ∑ y ∈ Icc x z, mu 𝕜 x y * zeta 𝕜 y z * f z := by
      rw [sum_sigma' (Ici x) fun y ↦ Ici y]
      rw [sum_sigma' (Ici x) fun z ↦ Icc x z]
      simp only [mul_boole, zero_mul, ite_mul, zeta_apply]
      apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
        aesop (add simp mul_assoc) (add unsafe le_trans)
    _ = ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp_rw [mul_apply, sum_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp only [mu_mul_zeta 𝕜, one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici, le_refl,
        ↓reduceIte, ← add_sum_Ioi_eq_sum_Ici, left_eq_add]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
    _ = f x := by
      simp only [one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici,
        ← add_sum_Ioi_eq_sum_Ici, le_refl, ↓reduceIte, add_eq_left]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
y :
  Eq.{u_2 + 1} (α := 𝕜) (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y))
    (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜))
y₁ :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜))
    (∑ y ∈ Ici x,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜)
        (∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z) : 𝕜))
⊢ ∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y) = f x
have y₂ : Eq.{u_2 + 1} (α := 𝕜)
  (∑ y ∈ Ici x,
    HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜)
      (∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z) : 𝕜))
  (∑ y ∈ Ici x,
    ∑ z ∈ Ici y,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)
Tactic: calc
    ∑ y ∈ Ici x, mu 𝕜 x y * g y = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, f z := by simp_rw [h]
    _ = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, zeta 𝕜 y z * f z := by
      congr with y
      rw [sum_congr rfl fun z hz ↦ ?_]
      rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, mu 𝕜 x y * zeta 𝕜 y z * f z := by simp [mul_sum]
    _ = ∑ z ∈ Ici x, ∑ y ∈ Icc x z, mu 𝕜 x y * zeta 𝕜 y z * f z := by
      rw [sum_sigma' (Ici x) fun y ↦ Ici y]
      rw [sum_sigma' (Ici x) fun z ↦ Icc x z]
      simp only [mul_boole, zero_mul, ite_mul, zeta_apply]
      apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
        aesop (add simp mul_assoc) (add unsafe le_trans)
    _ = ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp_rw [mul_apply, sum_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp only [mu_mul_zeta 𝕜, one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici, le_refl,
        ↓reduceIte, ← add_sum_Ioi_eq_sum_Ici, left_eq_add]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
    _ = f x := by
      simp only [one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici,
        ← add_sum_Ioi_eq_sum_Ici, le_refl, ↓reduceIte, add_eq_left]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderTop α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
y :
  Eq.{u_2 + 1} (α := 𝕜) (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y))
    (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜))
y₁ :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ y ∈ Ici x, HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (∑ z ∈ Ici y, f z : 𝕜))
    (∑ y ∈ Ici x,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜)
        (∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z) : 𝕜))
y₂ :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ y ∈ Ici x,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜)
        (∑ z ∈ Ici y, HMul.hMul (α := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) (f z) : 𝕜))
    (∑ y ∈ Ici x,
      ∑ z ∈ Ici y,
        HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)
⊢ ∑ y ∈ Ici x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) (g y) = f x
have y₃ : Eq.{u_2 + 1} (α := 𝕜)
  (∑ y ∈ Ici x,
    ∑ z ∈ Ici y,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)
  (∑ z ∈ Ici x,
    ∑ y ∈ Icc x z,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x y : 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) y z : 𝕜) * f z)
Tactic: calc
    ∑ y ∈ Ici x, mu 𝕜 x y * g y = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, f z := by simp_rw [h]
    _ = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, zeta 𝕜 y z * f z := by
      congr with y
      rw [sum_congr rfl fun z hz ↦ ?_]
      rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, mu 𝕜 x y * zeta 𝕜 y z * f z := by simp [mul_sum]
    _ = ∑ z ∈ Ici x, ∑ y ∈ Icc x z, mu 𝕜 x y * zeta 𝕜 y z * f z := by
      rw [sum_sigma' (Ici x) fun y ↦ Ici y]
      rw [sum_sigma' (Ici x) fun z ↦ Icc x z]
      simp only [mul_boole, zero_mul, ite_mul, zeta_apply]
      apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
        aesop (add simp mul_assoc) (add unsafe le_trans)
    _ = ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp_rw [mul_apply, sum_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp only [mu_mul_zeta 𝕜, one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici, le_refl,
        ↓reduceIte, ← add_sum_Ioi_eq_sum_Ici, left_eq_add]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
    _ = f x := by
      simp only [one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici,
        ← add_sum_Ioi_eq_sum_Ici, le_refl, ↓reduceIte, add_eq_left]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x : α
⊢ f x = ∑ y ∈ Iic x, HMul.hMul (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) y x : 𝕜) (g y)
have h₁ : ∀ x_1 ∈ Ici x, Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x_1 x : 𝕜) ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) x x_1 : 𝕜)
Tactic: convert! moebius_inversion_top (α := αᵒᵈ) f g h x using 3
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : LocallyFiniteOrder α
inst_4 : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x x_1 : α
h_1 : x_1 ∈ Ici x
⊢ Eq.{u_2 + 1} (α := 𝕜) ((mu 𝕜 : (a : α) → α → 𝕜) x_1 x : 𝕜) ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) x x_1 : 𝕜)
have h₁ : Eq.{u_2 + 1} (α := 𝕜)
  ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) ((toDual : (a : α) → αᵒᵈ) x : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) x_1) : 𝕜)
  ((mu 𝕜 : (a : αᵒᵈ) → αᵒᵈ → 𝕜) x x_1 : 𝕜)
Tactic: rw [← mu_toDual]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (hypothesis)
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x ≤ y
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) x.1 y.1 : 𝕜) ((g : (a : β) → β → 𝕜) x.2 y.2 : 𝕜) = 0
have hxy₁ : ¬x.1 ≤ y.1 ∨ ¬x.2 ≤ y.2
Tactic: rw [Prod.le_def, not_and_or] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x.1 ≤ y.1 ∨ ¬x.2 ≤ y.2
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) x.1 y.1 : 𝕜) ((g : (a : β) → β → 𝕜) x.2 y.2 : 𝕜) = 0
have inl : ∀ (hxy : ¬x.1 ≤ y.1),
  HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) x.1 y.1 : 𝕜) ((g : (a : β) → β → 𝕜) x.2 y.2 : 𝕜) = 0
Tactic: obtain hxy | hxy := hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x.1 ≤ y.1 ∨ ¬x.2 ≤ y.2
inl :
  ∀ (hxy : ¬x.1 ≤ y.1),
    HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) x.1 y.1 : 𝕜) ((g : (a : β) → β → 𝕜) x.2 y.2 : 𝕜) = 0
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) x.1 y.1 : 𝕜) ((g : (a : β) → β → 𝕜) x.2 y.2 : 𝕜) = 0
have inr : ∀ (hxy : ¬x.2 ≤ y.2),
  HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) x.1 y.1 : 𝕜) ((g : (a : β) → β → 𝕜) x.2 y.2 : 𝕜) = 0
Tactic: obtain hxy | hxy := hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
inst_3 : LocallyFiniteOrder α
inst_4 : LocallyFiniteOrder β
inst_5 : DecidableLE (α × β)
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    HMul.hMul (α := 𝕜) (β := 𝕜) ((f₁ : (a : α) → α → 𝕜) a₁ a₂ : 𝕜) ((g₁ : (a : β) → β → 𝕜) b₁ b₂ : 𝕜) *
        HMul.hMul (α := 𝕜) (β := 𝕜) ((f₂ : (a : α) → α → 𝕜) a₂ a₃ : 𝕜) ((g₂ : (a : β) → β → 𝕜) b₂ b₃ : 𝕜) =
      HMul.hMul (α := 𝕜) (β := 𝕜) ((f₁ : (a : α) → α → 𝕜) a₁ a₂ : 𝕜) ((f₂ : (a : α) → α → 𝕜) a₂ a₃ : 𝕜) *
        HMul.hMul (α := 𝕜) (β := 𝕜) ((g₁ : (a : β) → β → 𝕜) b₁ b₂ : 𝕜) ((g₂ : (a : β) → β → 𝕜) b₂ b₃ : 𝕜)
⊢ f₁.prod g₁ * f₂.prod g₂ = (f₁ * f₂).prod (g₁ * g₂)
have h₁ : ∀ (x y : α × β),
  x ≤ y →
    Eq.{u_2 + 1} (α := 𝕜) ((f₁.prod g₁ * f₂.prod g₂ : (a : α × β) → α × β → 𝕜) x y : 𝕜)
      (((f₁ * f₂).prod (g₁ * g₂) : (a : α × β) → α × β → 𝕜) x y : 𝕜)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : DecidableEq α
inst_4 : DecidableEq β
⊢ Eq (α := IncidenceAlgebra 𝕜 (α × β)) (IncidenceAlgebra.prod 1 1) 1
have h : ∀ (x y : α × β),
  x ≤ y →
    Eq.{u_2 + 1} (α := 𝕜) ((IncidenceAlgebra.prod 1 1 : (a : α × β) → α × β → 𝕜) x y : 𝕜)
      ((1 : (a : α × β) → α × β → 𝕜) x y : 𝕜)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : DecidableLE α
inst_4 : DecidableLE β
⊢ Eq (α := IncidenceAlgebra 𝕜 (α × β)) (IncidenceAlgebra.prod (zeta 𝕜) (zeta 𝕜)) (zeta 𝕜)
have h : ∀ (x y : α × β) (hxy : x ≤ y),
  Eq.{u_2 + 1} (α := 𝕜) ((IncidenceAlgebra.prod (zeta 𝕜) (zeta 𝕜) : (a : α × β) → α × β → 𝕜) x y : 𝕜)
    ((zeta 𝕜 : (a : α × β) → α × β → 𝕜) x y : 𝕜)
Tactic: ext x y hxy
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : LocallyFiniteOrder α
inst_4 : LocallyFiniteOrder β
inst_5 : DecidableEq α
inst_6 : DecidableEq β
inst_7 : DecidableLE α
inst_8 : DecidableLE β
⊢ Eq (α := IncidenceAlgebra 𝕜 (α × β)) (IncidenceAlgebra.prod (mu 𝕜) (mu 𝕜)) (mu 𝕜)
have refine : HMul.hMul (α := IncidenceAlgebra 𝕜 (α × β)) (IncidenceAlgebra.prod (mu 𝕜) (mu 𝕜)) (zeta 𝕜) = 1
Tactic: refine left_inv_eq_right_inv ?_ zeta_mul_mu
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.IncidenceAlgebra (goal)
Goal:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst : Ring 𝕜
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : LocallyFiniteOrder α
inst_4 : LocallyFiniteOrder β
inst_5 : DecidableEq α
inst_6 : DecidableEq β
inst_7 : DecidableLE α
inst_8 : DecidableLE β
⊢ HMul.hMul (α := IncidenceAlgebra 𝕜 (α × β)) (IncidenceAlgebra.prod (mu 𝕜) (mu 𝕜)) (zeta 𝕜) = 1
have h : ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
  HMul.hMul (α := 𝕜) (β := 𝕜) (((mu 𝕜 : IncidenceAlgebra 𝕜 α) : (a : α) → α → 𝕜) a₁ a₂ : 𝕜)
        (((mu 𝕜 : IncidenceAlgebra 𝕜 β) : (a : β) → β → 𝕜) b₁ b₂ : 𝕜) *
      HMul.hMul (α := 𝕜) (β := 𝕜) ((zeta 𝕜 : (a : α) → α → 𝕜) a₂ a₃ : 𝕜) ((zeta 𝕜 : (a : β) → β → 𝕜) b₂ b₃ : 𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) (((mu 𝕜 : IncidenceAlgebra 𝕜 α) : (a : α) → α → 𝕜) a₁ a₂ : 𝕜)
        ((zeta 𝕜 : (a : α) → α → 𝕜) a₂ a₃ : 𝕜) *
      HMul.hMul (α := 𝕜) (β := 𝕜) (((mu 𝕜 : IncidenceAlgebra 𝕜 β) : (a : β) → β → 𝕜) b₁ b₂ : 𝕜)
        ((zeta 𝕜 : (a : β) → β → 𝕜) b₂ b₃ : 𝕜)
Tactic: rw [← zeta_prod_zeta, prod_mul_prod', mu_mul_zeta, mu_mul_zeta, one_prod_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
have pos : ∀ (ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a),
  Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
Tactic: by_cases ha : a ∈ ⋃ i ∈ s, S i
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
pos :
  ∀ (ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a),
    Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
have neg : ∀ (ha : a ∉ ⋃ i ∈ s, S i),
  Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
Tactic: by_cases ha : a ∈ ⋃ i ∈ s, S i
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha ha' : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
have ha₁ : ∃ i ∈ s, a ∈ S i
Tactic: simp only [Set.mem_iUnion, exists_prop] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha' : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
ha : ∃ i ∈ s, a ∈ S i
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
have pos : ∀ (i : ι) (hi : i ∈ s) (ha : a ∈ S i),
  Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
Tactic: obtain ⟨i, hi, ha⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
have neg : ∀ (i : ι) (hi : i ∈ s),
  Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
Tactic: obtain ⟨i, hi⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) ((S i).indicator 1 a)) 0
have ha₁ : a ∉ S i
Tactic: have ha : a ∉ S i := by aesop
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
⊢ Set.indicator (⋃ i ∈ s, S i) f a =
    ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
have pos : ∀ (ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a),
  Set.indicator (⋃ i ∈ s, S i) f a =
    ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
Tactic: by_cases ha : a ∈ ⋃ i ∈ s, S i
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
pos :
  ∀ (ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a),
    Set.indicator (⋃ i ∈ s, S i) f a =
      ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
⊢ Set.indicator (⋃ i ∈ s, S i) f a =
    ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
have neg : ∀ (ha : a ∉ ⋃ i ∈ s, S i),
  Set.indicator (⋃ i ∈ s, S i) f a =
    ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
Tactic: by_cases ha : a ∈ ⋃ i ∈ s, S i
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ Set.indicator (⋃ i ∈ s, S i) f a =
    ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
have neg : Eq.{u_3 + 1} (α := G) 0
  (∑ x ∈ s.powerset with x.Nonempty, -(HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a))
Tactic: simp only [ha, not_false_eq_true, Set.indicator_of_notMem, Int.reduceNeg, pow_succ, mul_neg,
      mul_one, neg_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ Eq.{u_3 + 1} (α := G) 0
    (∑ x ∈ s.powerset with x.Nonempty, -(HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a))
have neg : Eq.{u_3 + 1} (α := G)
  (∑ x ∈ s.powerset with x.Nonempty, -(HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a)) 0
Tactic: symm
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ Eq.{u_3 + 1} (α := G)
    (∑ x ∈ s.powerset with x.Nonempty, -(HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a)) 0
have neg : ∀ x ∈ {t ∈ s.powerset | t.Nonempty}, -(HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a) = 0
Tactic: apply sum_eq_zero
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ ∀ x ∈ {t ∈ s.powerset | t.Nonempty}, -(HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a) = 0
have neg : ∀ x ⊆ s, x.Nonempty → HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a = 0
Tactic: simp only [Int.reduceNeg, neg_eq_zero, mem_filter, mem_powerset, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a = 0
have neg : HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) 0 = 0
Tactic: rw [Set.indicator_of_notMem]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
neg : HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) 0 = 0
⊢ HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a = 0
have neg₁ : a ∉ ⋂ i ∈ t, S i
Tactic: rw [Set.indicator_of_notMem]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ a ∉ ⋂ i ∈ t, S i
have neg : ∀ (ha : Membership.mem (γ := Set α) (⋂ i ∈ t, S i) a), Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
Tactic: contrapose ha
Cleared hypotheses: ha