awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : ¬p = 0
neg : (ofTree p.insidePart.toTree).nest + ofTree p.outsidePart.toTree = p
⊢ ofTree (if p = 0 then Tree.nil else node () p.insidePart.toTree p.outsidePart.toTree) = p

Tactic:
simp_rw [h, ite_false, ofTree]

Premises used: ite_false, DyckWord.ofTree
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : ¬p = 0
neg : p.insidePart.nest + p.outsidePart = p
⊢ (ofTree p.insidePart.toTree).nest + ofTree p.outsidePart.toTree = p

Tactic:
rw [ofTree_toTree p.insidePart, ofTree_toTree p.outsidePart]

Premises used: DyckWord.outsidePart, DyckWord.insidePart
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : ¬p = 0
⊢ p.insidePart.nest + p.outsidePart = p

Tactic:
nest_insidePart_add_outsidePart h

Premises used: DyckWord.nest_insidePart_add_outsidePart
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : ¬p = 0
⊢ p.insidePart.nest + p.outsidePart = p

Tactic:
exact nest_insidePart_add_outsidePart h

Premises used: DyckWord.nest_insidePart_add_outsidePart
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h_1 :
  ∀ (y : DyckWord), InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : DyckWord) ↦ x.semilength) y p → ofTree y.toTree = y
h : ¬p = 0
⊢ p.insidePart.semilength < p.semilength

Tactic:
semilength_insidePart_lt h

Premises used: DyckWord.semilength_insidePart_lt
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h_1 :
  ∀ (y : DyckWord), InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : DyckWord) ↦ x.semilength) y p → ofTree y.toTree = y
h : ¬p = 0
⊢ p.outsidePart.semilength < p.semilength

Tactic:
semilength_outsidePart_lt h

Premises used: DyckWord.semilength_outsidePart_lt
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h_1 :
  ∀ (y : DyckWord), InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : DyckWord) ↦ x.semilength) y p → ofTree y.toTree = y
h : ¬p = 0
⊢ p.insidePart.semilength < p.semilength

Tactic:
exacts [semilength_insidePart_lt h, semilength_outsidePart_lt h]

Premises used: DyckWord.semilength_outsidePart_lt, DyckWord.semilength_insidePart_lt
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h_1 :
  ∀ (y : DyckWord), InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : DyckWord) ↦ x.semilength) y p → ofTree y.toTree = y
h : ¬p = 0
⊢ p.insidePart.semilength < p.semilength

Tactic:
decreasing_by exacts [semilength_insidePart_lt h, semilength_outsidePart_lt h]

Premises used: DyckWord.semilength_outsidePart_lt, DyckWord.semilength_insidePart_lt
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
⊢ (ofTree Tree.nil).toTree = Tree.nil

Tactic:
simp [ofTree, toTree]

Premises used: DyckWord.toTree, DyckWord.ofTree
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
value : Unit
left right : Tree Unit
⊢ (ofTree (node value left right)).toTree = node value left right

Tactic:
simp [ofTree, toTree, toTree_ofTree]

Premises used: DyckWord.toTree, DyckWord.ofTree
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
pos : ∀ (h : p = 0), p.toTree.numNodes = p.semilength
neg : ∀ (h : ¬p = 0), p.toTree.numNodes = p.semilength
⊢ p.toTree.numNodes = p.semilength

Tactic:
by_cases h : p = 0
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p = 0
⊢ p.toTree.numNodes = p.semilength

Tactic:
simp [h, toTree]

Premises used: DyckWord.toTree
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : ¬p = 0
neg : (if p = 0 then Tree.nil else node () p.insidePart.toTree p.outsidePart.toTree).numNodes = p.semilength
⊢ p.toTree.numNodes = p.semilength

Tactic:
rw [toTree]

Premises used: DyckWord.toTree
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : ¬p = 0
neg : p.insidePart.toTree.numNodes + p.outsidePart.toTree.numNodes + 1 = p.semilength
⊢ (if p = 0 then Tree.nil else node () p.insidePart.toTree p.outsidePart.toTree).numNodes = p.semilength

Tactic:
simp_rw [h, ite_false, numNodes]

Premises used: Tree.numNodes, ite_false
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : ¬p = 0
neg :
  p.insidePart.toTree.numNodes + p.outsidePart.toTree.numNodes + 1 =
    p.insidePart.semilength + p.outsidePart.semilength + 1
neg₁ :
  p.insidePart.semilength + p.outsidePart.toTree.numNodes + 1 = p.insidePart.semilength + p.outsidePart.semilength + 1
neg₂ neg₃ :
  p.insidePart.semilength + p.outsidePart.semilength + 1 = p.insidePart.semilength + p.outsidePart.semilength + 1
⊢ p.insidePart.toTree.numNodes + p.outsidePart.toTree.numNodes + 1 = p.semilength

Tactic:
rw [← semilength_insidePart_add_semilength_outsidePart_add_one h,
      numNodes_toTree p.insidePart, numNodes_toTree p.outsidePart]

Premises used: DyckWord.outsidePart, DyckWord.semilength_insidePart_add_semilength_outsidePart_add_one, DyckWord.insidePart
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h_1 :
  ∀ (y : DyckWord),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : DyckWord) ↦ x.semilength) y p → y.toTree.numNodes = y.semilength
h : ¬p = 0
⊢ p.insidePart.semilength < p.semilength

Tactic:
semilength_insidePart_lt h

Premises used: DyckWord.semilength_insidePart_lt
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h_1 :
  ∀ (y : DyckWord),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : DyckWord) ↦ x.semilength) y p → y.toTree.numNodes = y.semilength
h : ¬p = 0
⊢ p.outsidePart.semilength < p.semilength

Tactic:
semilength_outsidePart_lt h

Premises used: DyckWord.semilength_outsidePart_lt
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h_1 :
  ∀ (y : DyckWord),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : DyckWord) ↦ x.semilength) y p → y.toTree.numNodes = y.semilength
h : ¬p = 0
⊢ p.insidePart.semilength < p.semilength

Tactic:
exacts [semilength_insidePart_lt h, semilength_outsidePart_lt h]

Premises used: DyckWord.semilength_outsidePart_lt, DyckWord.semilength_insidePart_lt
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h_1 :
  ∀ (y : DyckWord),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : DyckWord) ↦ x.semilength) y p → y.toTree.numNodes = y.semilength
h : ¬p = 0
⊢ p.insidePart.semilength < p.semilength

Tactic:
decreasing_by exacts [semilength_insidePart_lt h, semilength_outsidePart_lt h]

Premises used: DyckWord.semilength_outsidePart_lt, DyckWord.semilength_insidePart_lt
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
n : ℕ
⊢ ∀ (a : DyckWord),
    a.semilength = n ↔
      Membership.mem (α := Tree Unit) (treesOfNumNodesEq n) ((equivTree : (a : DyckWord) → Tree Unit) a : Tree Unit)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
n : ℕ
rw : Fintype.card ↥(treesOfNumNodesEq n) = (treesOfNumNodesEq n).card
⊢ Fintype.card { p : DyckWord // p.semilength = n } = catalan n

Tactic:
rw [← Fintype.ofEquiv_card (equivTreesOfNumNodesEq n), ← treesOfNumNodesEq_card_eq_catalan]

Premises used: Tree.treesOfNumNodesEq_card_eq_catalan, Fintype.ofEquiv_card, DyckWord.equivTreesOfNumNodesEq
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
n : ℕ
⊢ Fintype.card ↥(treesOfNumNodesEq n) = (treesOfNumNodesEq n).card

Tactic:
Fintype.card_coe _

Premises used: Fintype.card_coe
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
n : ℕ
⊢ Fintype.card ↥(treesOfNumNodesEq n) = (treesOfNumNodesEq n).card

Tactic:
convert! Fintype.card_coe _

Premises used: Fintype.card_coe
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Zero 𝕜
inst_1 : LE α
a b : α
f g : IncidenceAlgebra 𝕜 α
h : f.toFun = g.toFun
mk :
  ∀ (toFun : α → α → 𝕜) (eq_zero_of_not_le' : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun a b = 0)
    (h : { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α }.toFun = g.toFun),
    { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Zero 𝕜
inst_1 : LE α
a b : α
g : IncidenceAlgebra 𝕜 α
toFun : α → α → 𝕜
eq_zero_of_not_le' : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun a b = 0
h : { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α }.toFun = g.toFun
mk :
  ∀ (toFun_1 : α → α → 𝕜) (eq_zero_of_not_le'_1 : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun_1 a b = 0)
    (h :
      { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α }.toFun =
        { toFun := toFun_1, eq_zero_of_not_le' := eq_zero_of_not_le'_1 : IncidenceAlgebra 𝕜 α }.toFun),
    { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α } =
      { toFun := toFun_1, eq_zero_of_not_le' := eq_zero_of_not_le'_1 }
⊢ { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α } = g

Tactic:
cases g
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Zero 𝕜
inst_1 : LE α
a b : α
toFun : α → α → 𝕜
eq_zero_of_not_le' : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun a b = 0
toFun_1 : α → α → 𝕜
eq_zero_of_not_le'_1 : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun_1 a b = 0
h :
  { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α }.toFun =
    { toFun := toFun_1, eq_zero_of_not_le' := eq_zero_of_not_le'_1 : IncidenceAlgebra 𝕜 α }.toFun
⊢ { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' : IncidenceAlgebra 𝕜 α } =
    { toFun := toFun_1, eq_zero_of_not_le' := eq_zero_of_not_le'_1 }

Tactic:
congr
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
a b : α
h : ¬a ≤ b
f : IncidenceAlgebra 𝕜 α
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) (0 : 𝕜)

Tactic:
eq_zero_of_not_le' _ h

Premises used: IncidenceAlgebra.eq_zero_of_not_le'
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
a b : α
f : IncidenceAlgebra 𝕜 α
⊢ Ne.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) (0 : 𝕜) → a ≤ b

Tactic:
not_imp_comm.1 fun h ↦ apply_eq_zero_of_not_le h _

Premises used: not_imp_comm, IncidenceAlgebra.apply_eq_zero_of_not_le, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f : IncidenceAlgebra 𝕜 α
⊢ f.toFun = (⇑f : (a : α) → α → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f : α → α → 𝕜
h : ∀ ⦃a b : α⦄, ¬a ≤ b → f a b = 0
⊢ (⇑{ toFun := f, eq_zero_of_not_le' := h : IncidenceAlgebra 𝕜 α } : (a : α) → α → 𝕜) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
⊢ Eq (α := (a : α) → α → 𝕜) (⇑f : (a : α) → α → 𝕜) (⇑g : (a : α) → α → 𝕜) ↔ f = g

Tactic:
DFunLike.coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, DFunLike.coe_injective
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)
⊢ f = g

Tactic:
DFunLike.coe_injective' (funext₂ fun a b ↦ ?_)

Premises used: funext₂, DFunLike.coe_injective'
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)
refine : ∀ (a b : α), Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
⊢ f = g

Tactic:
refine DFunLike.coe_injective' (funext₂ fun a b ↦ ?_)

Premises used: funext₂, DFunLike.coe_injective'
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)
a b : α
pos : ∀ (hab : a ≤ b), Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
neg : ∀ (hab : ¬a ≤ b), Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)

Tactic:
by_cases hab : a ≤ b
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)
a b : α
hab : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)

Tactic:
h _ _ hab
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)
a b : α
hab : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)

Tactic:
exact h _ _ hab
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)
a b : α
hab : ¬a ≤ b
neg : Eq.{u_2 + 1} (α := 𝕜) (0 : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)
neg₁ neg₂ : Eq.{u_2 + 1} (α := 𝕜) 0 0
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f : (a b : α) → 𝕜) a b : 𝕜) ((g : (a b : α) → 𝕜) a b : 𝕜)

Tactic:
rw [apply_eq_zero_of_not_le hab, apply_eq_zero_of_not_le hab]

Premises used: IncidenceAlgebra.apply_eq_zero_of_not_le
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
f : IncidenceAlgebra 𝕜 α
h : ∀ ⦃a b : α⦄, ¬a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) (0 : 𝕜)
⊢ { toFun := (⇑f : (a : α) → α → 𝕜), eq_zero_of_not_le' := h : IncidenceAlgebra 𝕜 α } = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
⊢ Eq (α := (a : α) → α → 𝕜) (⇑0 : (a : α) → α → 𝕜) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Zero 𝕜
inst_1 : LE α
a b : α
⊢ Eq.{u_2 + 1} (α := 𝕜) ((0 : (a : α) → α → 𝕜) a b : 𝕜) (0 : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : AddZeroClass 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
simp_rw : HAdd.hAdd (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜) = 0
simp_rw₁ : HAdd.hAdd (α := 𝕜) 0 0 = 0
⊢ HAdd.hAdd (α := (a : α) → α → 𝕜) (β := (a : α) → α → 𝕜) (⇑f : (a : α) → α → 𝕜) (⇑g : (a : α) → α → 𝕜) a b = 0

Tactic:
simp_rw [Pi.add_apply, apply_eq_zero_of_not_le h, zero_add]

Premises used: IncidenceAlgebra.apply_eq_zero_of_not_le, zero_add, Pi.add_apply
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddZeroClass 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
⊢ (⇑(f + g) : (a : α) → α → 𝕜) = HAdd.hAdd (α := (a : α) → α → 𝕜) (⇑f : (a : α) → α → 𝕜) (⇑g : (a : α) → α → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddZeroClass 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
⊢ (f + g : (a : α) → α → 𝕜) a b =
    HAdd.hAdd (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
M : Type u_7
inst : Zero 𝕜
inst_1 : LE α
inst_2 : SMulZeroClass M 𝕜
c : M
f : IncidenceAlgebra 𝕜 α
a b : α
hab : ¬a ≤ b
simp_rw : HSMul.hSMul (β := 𝕜) c ((f : (a : α) → α → 𝕜) a b : 𝕜) = 0
simp_rw₁ : HSMul.hSMul (β := 𝕜) c 0 = 0
⊢ HSMul.hSMul (β := (a : α) → α → 𝕜) c (⇑f : (a : α) → α → 𝕜) a b = 0

Tactic:
simp_rw [Pi.smul_apply, apply_eq_zero_of_not_le hab, smul_zero]

Premises used: IncidenceAlgebra.apply_eq_zero_of_not_le, smul_zero, Pi.smul_apply
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
M : Type u_7
inst : Zero 𝕜
inst_1 : LE α
inst_2 : SMulZeroClass M 𝕜
c : M
h :
  ∀ (a b : α),
    a ≤ b →
      Eq.{u_2 + 1} (α := 𝕜) ((HSMul.hSMul (β := IncidenceAlgebra 𝕜 α) c 0 : (a : α) → α → 𝕜) a b : 𝕜)
        ((0 : (a : α) → α → 𝕜) a b : 𝕜)
⊢ HSMul.hSMul (β := IncidenceAlgebra 𝕜 α) c 0 = 0

Tactic:
ext
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
M : Type u_7
inst : Zero 𝕜
inst_1 : LE α
inst_2 : SMulZeroClass M 𝕜
c : M
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((HSMul.hSMul (β := IncidenceAlgebra 𝕜 α) c 0 : (a : α) → α → 𝕜) a b : 𝕜)
    ((0 : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
M : Type u_7
inst : Zero 𝕜
inst_1 : LE α
inst_2 : SMulZeroClass M 𝕜
c : M
a b : α
h : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((HSMul.hSMul (β := IncidenceAlgebra 𝕜 α) c 0 : (a : α) → α → 𝕜) a b : 𝕜)
    ((0 : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
exact smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
M : Type u_7
inst : Zero 𝕜
inst_1 : LE α
inst_2 : SMulZeroClass M 𝕜
c : M
f : IncidenceAlgebra 𝕜 α
⊢ (⇑(c • f) : (a : α) → α → 𝕜) = HSMul.hSMul (β := (a : α) → α → 𝕜) c (⇑f : (a : α) → α → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
M : Type u_7
inst : Zero 𝕜
inst_1 : LE α
inst_2 : SMulZeroClass M 𝕜
c : M
f : IncidenceAlgebra 𝕜 α
a b : α
⊢ (c • f : (a : α) → α → 𝕜) a b = HSMul.hSMul (β := 𝕜) c ((f : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : AddGroup 𝕜
inst_1 : LE α
f : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
simp_rw : Eq.{u_2 + 1} (α := 𝕜) (-(f : (a : α) → α → 𝕜) a b : 𝕜) (0 : 𝕜)
simp_rw₁ : Eq.{u_2 + 1} (α := 𝕜) (-0) 0
⊢ Eq.{u_2 + 1} (α := 𝕜) ((-(⇑f : (a : α) → α → 𝕜)) a b : 𝕜) (0 : 𝕜)

Tactic:
simp_rw [Pi.neg_apply, apply_eq_zero_of_not_le h, neg_zero]

Premises used: IncidenceAlgebra.apply_eq_zero_of_not_le, neg_zero, Pi.neg_apply
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : AddGroup 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
simp_rw : HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜) = 0
simp_rw₁ : HSub.hSub (α := 𝕜) 0 0 = 0
⊢ HSub.hSub (α := (a : α) → α → 𝕜) (β := (a : α) → α → 𝕜) (⇑f : (a : α) → α → 𝕜) (⇑g : (a : α) → α → 𝕜) a b = 0

Tactic:
simp_rw [Pi.sub_apply, apply_eq_zero_of_not_le h, sub_zero]

Premises used: sub_zero, IncidenceAlgebra.apply_eq_zero_of_not_le, Pi.sub_apply
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddGroup 𝕜
inst_1 : LE α
f : IncidenceAlgebra 𝕜 α
⊢ Eq (α := (a : α) → α → 𝕜) (⇑(-f) : (a : α) → α → 𝕜) (-(⇑f : (a : α) → α → 𝕜))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddGroup 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
⊢ (⇑(f - g) : (a : α) → α → 𝕜) = HSub.hSub (α := (a : α) → α → 𝕜) (⇑f : (a : α) → α → 𝕜) (⇑g : (a : α) → α → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddGroup 𝕜
inst_1 : LE α
f : IncidenceAlgebra 𝕜 α
a b : α
⊢ Eq.{u_2 + 1} (α := 𝕜) ((-f : (a : α) → α → 𝕜) a b : 𝕜) (-(f : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : AddGroup 𝕜
inst_1 : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
⊢ (f - g : (a : α) → α → 𝕜) a b =
    HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a b : 𝕜) ((g : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Preorder α
inst_1 : DecidableEq α
inst_2 : Zero 𝕜
inst_3 : One 𝕜
a b : α
⊢ Eq.{u_2 + 1} (α := 𝕜) ((1 : (a : α) → α → 𝕜) a b : 𝕜) (if a = b then 1 else 0 : 𝕜)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : AddCommMonoid 𝕜
inst_3 : Mul 𝕜
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
rw :
  Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ ∅, HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a x : 𝕜) ((g : (a : α) → α → 𝕜) x b : 𝕜)) 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := 𝕜) 0 0
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (∑ x ∈ Icc a b, HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a x : 𝕜) ((g : (a : α) → α → 𝕜) x b : 𝕜)) 0

Tactic:
rw [Icc_eq_empty h, sum_empty]

Premises used: Finset.Icc_eq_empty, Finset.sum_empty
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
𝕜 : Type u_2
α : Type u_5
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : AddCommMonoid 𝕜
inst_3 : Mul 𝕜
f g : IncidenceAlgebra 𝕜 α
a b : α
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f * g : (a : α) → α → 𝕜) a b : 𝕜)
    (∑ x ∈ Icc a b, HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : α) → α → 𝕜) a x : 𝕜) ((g : (a : α) → α → 𝕜) x b : 𝕜) : 𝕜)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.sum, rfl
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
h₁ :
  ∀ (a b : α),
    a ≤ b → Eq.{u_2 + 1} (α := 𝕜) ((f * (g + h) : (a : α) → α → 𝕜) a b : 𝕜) ((f * g + f * h : (a : α) → α → 𝕜) a b : 𝕜)
⊢ f * (g + h) = f * g + f * h

Tactic:
ext
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f * (g + h) : (a : α) → α → 𝕜) a b : 𝕜) ((f * g + f * h : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
Eq.trans (sum_congr rfl fun x _ ↦ left_distrib _ _ _) sum_add_distrib

Premises used: Finset.sum_add_distrib, DFunLike.coe, Finset.sum_congr, rfl, Eq.trans, left_distrib
-- Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Goal:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
h_1 : a ≤ b
⊢ Eq.{u_2 + 1} (α := 𝕜) ((f * (g + h) : (a : α) → α → 𝕜) a b : 𝕜) ((f * g + f * h : (a : α) → α → 𝕜) a b : 𝕜)

Tactic:
exact Eq.trans (sum_congr rfl fun x _ ↦ left_distrib _ _ _) sum_add_distrib

Premises used: Finset.sum_add_distrib, Finset.sum_congr, rfl, Eq.trans, left_distrib