awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ f₁.sum h ≤ f₂.sum h
have rw : ∑ x ∈ f₁.support ∪ f₂.support, h x ((f₁ : (a : ι) → α) x) ≤ f₂.sum h
Tactic: classical
  rw [sum_of_support_subset _ Finset.subset_union_left _ hh₀,
    sum_of_support_subset _ Finset.subset_union_right _ hh₀]
  gcongr with i hi
  exact hh _ hi <| hf _
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
rw : ∑ x ∈ f₁.support ∪ f₂.support, h x ((f₁ : (a : ι) → α) x) ≤ f₂.sum h
⊢ f₁.sum h ≤ f₂.sum h
have rw₁ : LE.le.{u_4} (α := β) (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₁ : (a : ι) → α) x))
  (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₂ : (a : ι) → α) x))
Tactic: classical
  rw [sum_of_support_subset _ Finset.subset_union_left _ hh₀,
    sum_of_support_subset _ Finset.subset_union_right _ hh₀]
  gcongr with i hi
  exact hh _ hi <| hf _
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
rw : ∑ x ∈ f₁.support ∪ f₂.support, h x ((f₁ : (a : ι) → α) x) ≤ f₂.sum h
rw₁ rw₂ rw₃ :
  LE.le.{u_4} (α := β) (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₁ : (a : ι) → α) x))
    (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₂ : (a : ι) → α) x))
⊢ f₁.sum h ≤ f₂.sum h
have h₁ : ∀ (i : ι) (hi : i ∈ f₁.support ∪ f₂.support), h i ((f₁ : (a : ι) → α) i) ≤ h i ((f₂ : (a : ι) → α) i)
Tactic: classical
  rw [sum_of_support_subset _ Finset.subset_union_left _ hh₀,
    sum_of_support_subset _ Finset.subset_union_right _ hh₀]
  gcongr with i hi
  exact hh _ hi <| hf _
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : Zero α
inst_1 : LE α
inst_2 : Std.Refl fun (x1 x2 : α) ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ embDomain f g₁ ≤ embDomain f g₂ ↔ g₁ ≤ g₂
have mp : embDomain f g₁ ≤ embDomain f g₂ → g₁ ≤ g₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : Zero α
inst_1 : LE α
inst_2 : Std.Refl fun (x1 x2 : α) ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
mp : embDomain f g₁ ≤ embDomain f g₂ → g₁ ≤ g₂
⊢ embDomain f g₁ ≤ embDomain f g₂ ↔ g₁ ≤ g₂
have mpr : g₁ ≤ g₂ → embDomain f g₁ ≤ embDomain f g₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : LE.le (α := α → M → N) 0 fun (x1 : α) (x2 : M) ↦ g x1 x2
a : α
⊢ sum (single a ((f : (a : α) → M) a)) g ≤ f.sum g
have inl : ∀ (H : Eq.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)), sum (single a ((f : (a : α) → M) a)) g ≤ f.sum g
Tactic: rcases eq_or_ne (f a) 0 with H | H
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : LE.le (α := α → M → N) 0 fun (x1 : α) (x2 : M) ↦ g x1 x2
a : α
inl : ∀ (H : Eq.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)), sum (single a ((f : (a : α) → M) a)) g ≤ f.sum g
⊢ sum (single a ((f : (a : α) → M) a)) g ≤ f.sum g
have inr : ∀ (H : Ne.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)), sum (single a ((f : (a : α) → M) a)) g ≤ f.sum g
Tactic: rcases eq_or_ne (f a) 0 with H | H
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : LE.le (α := α → M → N) 0 fun (x1 : α) (x2 : M) ↦ g x1 x2
a : α
H : Eq.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ sum (single a ((f : (a : α) → M) a)) g ≤ f.sum g
have inl : 0 ≤ f.sum g
Tactic: rw [H, single_zero, sum_zero_index]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : LE.le (α := α → M → N) 0 fun (x1 : α) (x2 : M) ↦ g x1 x2
a : α
H : Ne.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ sum (single a ((f : (a : α) → M) a)) g ≤ f.sum g
have inr : g a ((f : (a : α) → M) a) ≤ f.sum g
Tactic: rw [sum, support_single _ H, sum_singleton, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : LE.le (α := α → M → N) 0 fun (x1 : α) (x2 : M) ↦ g x1 x2
a : α
H : Ne.{u_6 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ g a ((f : (a : α) → M) a) ≤ f.sum g
have inr : a ∈ f.support
Tactic: apply Finset.single_le_sum (fun i hi ↦ h i (f i))
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
α : Type u_5
M : Type u_6
N : Type u_7
inst : Zero M
inst_1 : AddCommMonoid N
inst_2 : PartialOrder N
inst_3 : IsOrderedAddMonoid N
f : α →₀ M
g : M → N
hg : g 0 = 0
h : LE.le (α := M → N) 0 fun (x : M) ↦ g x
a : α
⊢ g ((f : (a : α) → M) a) ≤ f.sum fun (x : α) (m : M) ↦ g m
have simp : LE.le.{u_7} (α := N) (sum.{u_5, u_6, u_7} (M := M) (single a ((f : (a : α) → M) a) : α →₀ M) fun (x : α) (m : M) ↦ g m)
  (f.sum fun (x : α) (m : M) ↦ g m)
Tactic: simp only [← sum_single_index (h := fun (_ : α) m ↦ g m) (a := a) (b := f a) hg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
s : Finset ι
hf : f.support ⊆ s
⊢ f ≤ g ↔ ∀ i ∈ s, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)
have refine : ∀ (h : ∀ i ∈ s, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)) (s : ι),
  LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)
Tactic: refine ⟨fun h s _ ↦ h s, fun h s ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
s_1 : Finset ι
hf : f.support ⊆ s_1
h : ∀ i ∈ s_1, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)
s : ι
⊢ LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)
have pos : ∀ (H : s ∈ f.support), LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)
Tactic: by_cases H : s ∈ f.support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
s_1 : Finset ι
hf : f.support ⊆ s_1
h : ∀ i ∈ s_1, LE.le.{u_3} (α := α) ((f : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)
s : ι
pos : ∀ (H : s ∈ f.support), LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)
⊢ LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)
have neg : ∀ (H : s ∉ f.support), LE.le.{u_3} (α := α) ((f : (a : ι) → α) s : α) ((g : (a : ι) → α) s : α)
Tactic: by_cases H : s ∈ f.support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
f g : ι →₀ α
h : f ≤ g
a : ι
ha : a ∈ f.support
⊢ a ∈ g.support
have rw : ∀ (ha : LT.lt.{u_3} (α := α) (0 : α) ((f : (a : ι) → α) a : α)), LT.lt.{u_3} (α := α) (0 : α) ((g : (a : ι) → α) a : α)
Tactic: rw [mem_support_iff, ← pos_iff_ne_zero] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
i : ι
a b : α
⊢ single i (a - b) = HSub.hSub (α := ι →₀ α) (single i a) (single i b)
have h : ∀ (j : ι),
  Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
i : ι
a b : α
j : ι
⊢ Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)
have h : Eq.{u_3 + 1} (α := α) ((single j (a - b) : (a : ι) → α) j : α)
  ((HSub.hSub (α := ι →₀ α) (single j a) (single j b) : (a : ι) → α) j : α)
Tactic: obtain rfl | h := eq_or_ne j i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
i : ι
a b : α
j : ι
h :
  Eq.{u_3 + 1} (α := α) ((single j (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single j a) (single j b) : (a : ι) → α) j : α)
⊢ Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)
have h₁ : ∀ (h : j ≠ i),
  Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)
Tactic: obtain rfl | h := eq_or_ne j i
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
j : ι
⊢ Eq.{u_3 + 1} (α := α) ((single j (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single j a) (single j b) : (a : ι) → α) j : α)
have h : (single j (a - b) : (a : ι) → α) j =
  HSub.hSub (α := α) (β := α) ((single j a : (a : ι) → α) j : α) ((single j b : (a : ι) → α) j : α)
Tactic: rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
j : ι
h :
  (single j (a - b) : (a : ι) → α) j =
    HSub.hSub (α := α) (β := α) ((single j a : (a : ι) → α) j : α) ((single j b : (a : ι) → α) j : α)
⊢ Eq.{u_3 + 1} (α := α) ((single j (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single j a) (single j b) : (a : ι) → α) j : α)
have h₁ : a - b = HSub.hSub (α := α) (β := α) ((single j a : (a : ι) → α) j : α) ((single j b : (a : ι) → α) j : α)
Tactic: rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
j : ι
h :
  (single j (a - b) : (a : ι) → α) j =
    HSub.hSub (α := α) (β := α) ((single j a : (a : ι) → α) j : α) ((single j b : (a : ι) → α) j : α)
h₁ : a - b = HSub.hSub (α := α) (β := α) ((single j a : (a : ι) → α) j : α) ((single j b : (a : ι) → α) j : α)
⊢ Eq.{u_3 + 1} (α := α) ((single j (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single j a) (single j b) : (a : ι) → α) j : α)
have h₂ : a - b = HSub.hSub (β := α) a ((single j b : (a : ι) → α) j : α)
Tactic: rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
j : ι
h :
  (single j (a - b) : (a : ι) → α) j =
    HSub.hSub (α := α) (β := α) ((single j a : (a : ι) → α) j : α) ((single j b : (a : ι) → α) j : α)
h₁ : a - b = HSub.hSub (α := α) (β := α) ((single j a : (a : ι) → α) j : α) ((single j b : (a : ι) → α) j : α)
h₂ : a - b = HSub.hSub (β := α) a ((single j b : (a : ι) → α) j : α)
⊢ Eq.{u_3 + 1} (α := α) ((single j (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single j a) (single j b) : (a : ι) → α) j : α)
have h₃ : a - b = a - b
Tactic: rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
i : ι
a b : α
j : ι
h : j ≠ i
⊢ Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)
have h₁ : (single i (a - b) : (a : ι) → α) j =
  HSub.hSub (α := α) (β := α) ((single i a : (a : ι) → α) j : α) ((single i b : (a : ι) → α) j : α)
Tactic: rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
i : ι
a b : α
j : ι
h : j ≠ i
h₁ :
  (single i (a - b) : (a : ι) → α) j =
    HSub.hSub (α := α) (β := α) ((single i a : (a : ι) → α) j : α) ((single i b : (a : ι) → α) j : α)
⊢ Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)
have h₂ : 0 = HSub.hSub (α := α) (β := α) ((single i a : (a : ι) → α) j : α) ((single i b : (a : ι) → α) j : α)
Tactic: rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
i : ι
a b : α
j : ι
h : j ≠ i
h₁ :
  (single i (a - b) : (a : ι) → α) j =
    HSub.hSub (α := α) (β := α) ((single i a : (a : ι) → α) j : α) ((single i b : (a : ι) → α) j : α)
h₂ : 0 = HSub.hSub (α := α) (β := α) ((single i a : (a : ι) → α) j : α) ((single i b : (a : ι) → α) j : α)
⊢ Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)
have h₃ : 0 = HSub.hSub (α := α) (β := α) (0 : α) ((single i b : (a : ι) → α) j : α)
Tactic: rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
i : ι
a b : α
j : ι
h : j ≠ i
h₁ :
  (single i (a - b) : (a : ι) → α) j =
    HSub.hSub (α := α) (β := α) ((single i a : (a : ι) → α) j : α) ((single i b : (a : ι) → α) j : α)
h₂ : 0 = HSub.hSub (α := α) (β := α) ((single i a : (a : ι) → α) j : α) ((single i b : (a : ι) → α) j : α)
h₃ : 0 = HSub.hSub (α := α) (β := α) (0 : α) ((single i b : (a : ι) → α) j : α)
⊢ Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)
have h₄ : 0 = HSub.hSub (α := α) 0 0
Tactic: rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
i : ι
a b : α
j : ι
h : j ≠ i
h₁ :
  (single i (a - b) : (a : ι) → α) j =
    HSub.hSub (α := α) (β := α) ((single i a : (a : ι) → α) j : α) ((single i b : (a : ι) → α) j : α)
h₂ : 0 = HSub.hSub (α := α) (β := α) ((single i a : (a : ι) → α) j : α) ((single i b : (a : ι) → α) j : α)
h₃ : 0 = HSub.hSub (α := α) (β := α) (0 : α) ((single i b : (a : ι) → α) j : α)
h₄ : 0 = HSub.hSub (α := α) 0 0
⊢ Eq.{u_3 + 1} (α := α) ((single i (a - b) : (a : ι) → α) j : α)
    ((HSub.hSub (α := ι →₀ α) (single i a) (single i b) : (a : ι) → α) j : α)
have h₅ : Eq.{u_3 + 1} (α := α) 0 0
Tactic: rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
⊢ mapDomain f (f1 - f2) = mapDomain f f1 - mapDomain f f2
have h₁ : ∀ (y : κ),
  Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
    ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
y : κ
⊢ Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
    ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)
have pos : ∀ (hy : y ∉ Set.range f),
  Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
    ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)
Tactic: by_cases! hy : y ∉ Set.range f
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
y : κ
pos :
  ∀ (hy : y ∉ Set.range f),
    Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
      ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)
⊢ Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
    ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)
have neg : ∀ (hy : y ∈ Set.range f),
  Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
    ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)
Tactic: by_cases! hy : y ∉ Set.range f
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
y : κ
hy : y ∈ Set.range f
⊢ Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) y : α)
    ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) y : α)
have neg : ∀ (x : ι),
  Eq.{u_3 + 1} (α := α) ((mapDomain f (f1 - f2) : (a : κ) → α) (f x) : α)
    ((mapDomain f f1 - mapDomain f f2 : (a : κ) → α) (f x) : α)
Tactic: obtain ⟨x, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
f : ι ↪ κ
f1 f2 : ι →₀ α
⊢ embDomain f (f1 - f2) = embDomain f f1 - embDomain f f2
have simp_rw : mapDomain (⇑f : (a : ι) → κ) (f1 - f2) =
  HSub.hSub (α := κ →₀ α) (mapDomain (⇑f : (a : ι) → κ) f1) (mapDomain (⇑f : (a : ι) → κ) f2)
Tactic: simp_rw [embDomain_eq_mapDomain, mapDomain_tsub f.injective]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsBotZeroClass α
inst_3 : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊓ g).support = f.support ∩ g.support
have h : ∀ (a : ι), a ∈ (f ⊓ g).support ↔ a ∈ f.support ∩ g.support
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsBotZeroClass α
inst_3 : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊔ g).support = f.support ∪ g.support
have h : ∀ (a : ι), a ∈ (f ⊔ g).support ↔ a ∈ f.support ∪ g.support
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
u : ι →₀ ℕ
i : ι
h : Ne (α := ℕ) ((u : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
⊢ u - single i 1 + single i 1 = u
have rw : u + single i 1 - single i 1 = u
Tactic: rw [sub_single_one_add h, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
u : ι →₀ ℕ
i : ι
h : Ne (α := ℕ) ((u : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
rw : u + single i 1 - single i 1 = u
⊢ u - single i 1 + single i 1 = u
have rw₁ : u = u
Tactic: rw [sub_single_one_add h, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
⊢ Membership.mem (γ := Set (β →₀ ℕ)) (Set.range (embDomain f)) y
have obtain : ∀ (w : β →₀ ℕ) (hw : embDomain f z = y + w), Membership.mem (γ := Set (β →₀ ℕ)) (Set.range (embDomain f)) y
Tactic: obtain ⟨w, hw⟩ := exists_add_of_le h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
⊢ Membership.mem (γ := Set (β →₀ ℕ)) (Set.range (embDomain f)) y
have rw : (↑y.support : Set β) ⊆ Set.range.{u_4, u_3 + 1} (ι := α) (⇑f : (a : α) → β)
Tactic: rw [mem_range_embDomain_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
⊢ (↑y.support : Set β) ⊆ Set.range.{u_4, u_3 + 1} (ι := α) (⇑f : (a : α) → β)
have trans : (↑y.support : Set β) ⊆ (↑(y + w).support : Set β)
Tactic: trans ↑(y + w).support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
trans : (↑y.support : Set β) ⊆ (↑(y + w).support : Set β)
⊢ (↑y.support : Set β) ⊆ Set.range.{u_4, u_3 + 1} (ι := α) (⇑f : (a : α) → β)
have trans₁ : (↑(y + w).support : Set β) ⊆ Set.range.{u_4, u_3 + 1} (ι := α) (⇑f : (a : α) → β)
Tactic: trans ↑(y + w).support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
x : β
⊢ x ∈ (↑y.support : Set β) → x ∈ (↑(y + w).support : Set β)
have simp : ¬Eq (α := ℕ) ((y : (a : β) → ℕ) x : ℕ) (0 : ℕ) →
  Eq (α := ℕ) ((y : (a : β) → ℕ) x : ℕ) (0 : ℕ) → ¬Eq (α := ℕ) ((w : (a : β) → ℕ) x : ℕ) (0 : ℕ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Finsupp.Pointwise (goal)
Goal:
α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst : Semiring β
r : β
f : α → β
m : α →₀ β
⊢ (r • f) • m = r • f • m
have h : ∀ (a : α), Eq.{u₂ + 1} (α := β) (((r • f) • m : (a : α) → β) a : β) ((r • f • m : (a : α) → β) a : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
Goal:
α : Type u_1
M : Type u_3
R : Type u_6
inst : Zero M
inst_1 : MonoidWithZero R
inst_2 : MulActionWithZero R M
a b : α
f : α → M
r : R
⊢ HSMul.hSMul.{u_6, u_3, u_3} (α := R) ((single a r : (a : α) → R) b : R) (f a) = (single a (r • f b) : (a : α) → M) b
have pos : ∀ (h : a = b),
  HSMul.hSMul.{u_6, u_3, u_3} (α := R) ((single a r : (a : α) → R) b : R) (f a) = (single a (r • f b) : (a : α) → M) b
Tactic: by_cases h : a = b