awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeInf Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ Membership.mem (γ := Set X)
      (Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊓ (D₂ : (a : X) → Y) z) x →
    x ∈ U
have contrapose : x ∉ U → x ∉ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊓ (D₂ : (a : X) → Y) z
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeInf Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊓ (D₂ : (a : X) → Y) z).Finite
have obtain : ∀ (t₁ : Set X) (ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support (U := U)).Finite),
  ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊓ (D₂ : (a : X) → Y) z).Finite
Tactic: obtain ⟨t₁, ht₁⟩ := D₁.supportLocallyFiniteWithinDomain z hz
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeInf Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support (U := U)).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊓ (D₂ : (a : X) → Y) z).Finite
have obtain : ∀ (t₂ : Set X) (ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support (U := U)).Finite),
  ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊓ (D₂ : (a : X) → Y) z).Finite
Tactic: obtain ⟨t₂, ht₂⟩ := D₂.supportLocallyFiniteWithinDomain z hz
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeInf Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support (U := U)).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support (U := U)).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊓ (D₂ : (a : X) → Y) z).Finite
have right : (t₁ ∩ t₂ ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊓ (D₂ : (a : X) → Y) z).Finite
Tactic: use t₁ ∩ t₂, inter_mem ht₁.1 ht₂.1
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeInf Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support (U := U)).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support (U := U)).Finite
⊢ (t₁ ∩ t₂ ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊓ (D₂ : (a : X) → Y) z).Finite
have right : (t₁ ∩ t₂ ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊓ (D₂ : (a : X) → Y) z) ⊆
  t₁ ∩ D₁.support (U := U) ∪ t₂ ∩ D₂.support (U := U)
Tactic: apply Set.Finite.subset (s := (t₁ ∩ D₁.support) ∪ (t₂ ∩ D₂.support)) (ht₁.2.union ht₂.2)
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeInf Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support (U := U)).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support (U := U)).Finite
a : X
ha : a ∈ t₁ ∩ t₂ ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊓ (D₂ : (a : X) → Y) z
⊢ a ∈ t₁ ∩ D₁.support (U := U) ∪ t₂ ∩ D₂.support (U := U)
have right : ∀ (ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) a ⊓ (D₂ : (a : X) → Y) a : Y) (0 : Y)),
  ¬Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) a : Y) (0 : Y) ∨ ¬Eq.{u_2 + 1} (α := Y) ((D₂ : (a : X) → Y) a : Y) (0 : Y)
Tactic: simp_all only [mem_inter_iff, mem_support, ne_eq, mem_union, true_and]
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeInf Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support (U := U)).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support (U := U)).Finite
a : X
ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) a ⊓ (D₂ : (a : X) → Y) a : Y) (0 : Y)
⊢ ¬Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) a : Y) (0 : Y) ∨ ¬Eq.{u_2 + 1} (α := Y) ((D₂ : (a : X) → Y) a : Y) (0 : Y)
have right : ∀
  (hCon :
    Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) a : Y) (0 : Y) ∧
      Eq.{u_2 + 1} (α := Y) ((D₂ : (a : X) → Y) a : Y) (0 : Y)),
  False
Tactic: by_contra! hCon
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Lattice Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
h₁₂ : D₁ ≤ D₂
h₂₁ : D₂ ≤ D₁
⊢ D₁ = D₂
have h : ∀ (x : X), Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) x : Y) ((D₂ : (a : X) → Y) x : Y)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂)⁺ ≤ f₁⁺ + f₂⁺
have rw : (f₁ + f₂) ⊔ 0 ≤ f₁⁺ + f₂⁺
Tactic: rw [posPart_def]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂) ⊔ 0 ≤ f₁⁺ + f₂⁺
have rw : (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂⁺
Tactic: rw [posPart_def]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂⁺
have rw : (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂ ⊔ 0
Tactic: rw [posPart_def]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂)⁺ ≤ f₁⁺ + f₂⁺
have repeat : (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂ ⊔ 0
Tactic: repeat rw [posPart_def]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ LE.le.{u_2} (α := (fun (a : X) ↦ Y) x) (((f₁ + f₂) ⊔ 0 : (a : X) → Y) x : Y) ((f₁ ⊔ 0 + f₂ ⊔ 0 : (a : X) → Y) x : Y)
have simp : HAdd.hAdd (α := Y) (β := Y) ((f₁ : (a : X) → Y) x : Y) ((f₂ : (a : X) → Y) x : Y) ≤
    HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y) ∧
  0 ≤ HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y)
Tactic: simp only [Function.locallyFinsuppWithin.max_apply, Function.locallyFinsuppWithin.coe_add,
    Pi.add_apply, Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, sup_le_iff]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ HAdd.hAdd (α := Y) (β := Y) ((f₁ : (a : X) → Y) x : Y) ((f₂ : (a : X) → Y) x : Y) ≤
      HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y) ∧
    0 ≤ HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y)
have left : HAdd.hAdd (α := Y) (β := Y) ((f₁ : (a : X) → Y) x : Y) ((f₂ : (a : X) → Y) x : Y) ≤
  HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
left :
  HAdd.hAdd (α := Y) (β := Y) ((f₁ : (a : X) → Y) x : Y) ((f₂ : (a : X) → Y) x : Y) ≤
    HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y)
⊢ HAdd.hAdd (α := Y) (β := Y) ((f₁ : (a : X) → Y) x : Y) ((f₂ : (a : X) → Y) x : Y) ≤
      HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y) ∧
    0 ≤ HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y)
have right : 0 ≤ HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂)⁻ ≤ f₁⁻ + f₂⁻
have rw : -(f₁ + f₂) ⊔ 0 ≤ f₁⁻ + f₂⁻
Tactic: rw [negPart_def]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ -(f₁ + f₂) ⊔ 0 ≤ f₁⁻ + f₂⁻
have rw : -(f₁ + f₂) ⊔ 0 ≤ -f₁ ⊔ 0 + f₂⁻
Tactic: rw [negPart_def]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ -(f₁ + f₂) ⊔ 0 ≤ -f₁ ⊔ 0 + f₂⁻
have rw : -(f₁ + f₂) ⊔ 0 ≤ -f₁ ⊔ 0 + -f₂ ⊔ 0
Tactic: rw [negPart_def]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
⊢ (f₁ + f₂)⁻ ≤ f₁⁻ + f₂⁻
have repeat : -(f₁ + f₂) ⊔ 0 ≤ -f₁ ⊔ 0 + -f₂ ⊔ 0
Tactic: repeat rw [negPart_def]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ LE.le.{u_2} (α := (fun (a : X) ↦ Y) x) ((-(f₁ + f₂) ⊔ 0 : (a : X) → Y) x : Y)
    ((-f₁ ⊔ 0 + -f₂ ⊔ 0 : (a : X) → Y) x : Y)
have simp : HAdd.hAdd (α := Y) (β := Y) (-(f₂ : (a : X) → Y) x : Y) (-(f₁ : (a : X) → Y) x : Y) ≤
    HAdd.hAdd (α := Y) (β := Y) (max (-(f₁ : (a : X) → Y) x) 0 : Y) (max (-(f₂ : (a : X) → Y) x) 0 : Y) ∧
  0 ≤ HAdd.hAdd (α := Y) (β := Y) (max (-(f₁ : (a : X) → Y) x) 0 : Y) (max (-(f₂ : (a : X) → Y) x) 0 : Y)
Tactic: simp only [neg_add_rev, Function.locallyFinsuppWithin.max_apply,
    Function.locallyFinsuppWithin.coe_add, Function.locallyFinsuppWithin.coe_neg, Pi.add_apply,
    Pi.neg_apply, Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, sup_le_iff]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ HAdd.hAdd (α := Y) (β := Y) (-(f₂ : (a : X) → Y) x : Y) (-(f₁ : (a : X) → Y) x : Y) ≤
      HAdd.hAdd (α := Y) (β := Y) (max (-(f₁ : (a : X) → Y) x) 0 : Y) (max (-(f₂ : (a : X) → Y) x) 0 : Y) ∧
    0 ≤ HAdd.hAdd (α := Y) (β := Y) (max (-(f₁ : (a : X) → Y) x) 0 : Y) (max (-(f₂ : (a : X) → Y) x) 0 : Y)
have left : HAdd.hAdd (α := Y) (β := Y) (-(f₂ : (a : X) → Y) x : Y) (-(f₁ : (a : X) → Y) x : Y) ≤
  HAdd.hAdd (α := Y) (β := Y) (max (-(f₁ : (a : X) → Y) x) 0 : Y) (max (-(f₂ : (a : X) → Y) x) 0 : Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
left :
  HAdd.hAdd (α := Y) (β := Y) (-(f₂ : (a : X) → Y) x : Y) (-(f₁ : (a : X) → Y) x : Y) ≤
    HAdd.hAdd (α := Y) (β := Y) (max (-(f₁ : (a : X) → Y) x) 0 : Y) (max (-(f₂ : (a : X) → Y) x) 0 : Y)
⊢ HAdd.hAdd (α := Y) (β := Y) (-(f₂ : (a : X) → Y) x : Y) (-(f₁ : (a : X) → Y) x : Y) ≤
      HAdd.hAdd (α := Y) (β := Y) (max (-(f₁ : (a : X) → Y) x) 0 : Y) (max (-(f₂ : (a : X) → Y) x) 0 : Y) ∧
    0 ≤ HAdd.hAdd (α := Y) (β := Y) (max (-(f₁ : (a : X) → Y) x) 0 : Y) (max (-(f₂ : (a : X) → Y) x) 0 : Y)
have right : 0 ≤ HAdd.hAdd (α := Y) (β := Y) (max (-(f₁ : (a : X) → Y) x) 0 : Y) (max (-(f₂ : (a : X) → Y) x) 0 : Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
⊢ (n • f)⁺ = n • f⁺
have h : ∀ (x : X), Eq.{u_2 + 1} (α := Y) (((n • f)⁺ : (a : X) → Y) x : Y) ((n • f⁺ : (a : X) → Y) x : Y)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) (((n • f)⁺ : (a : X) → Y) x : Y) ((n • f⁺ : (a : X) → Y) x : Y)
have h : max (HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max ((f : (a : X) → Y) x) 0 : Y)
Tactic: simp only [posPart, max_apply, coe_nsmul, Pi.smul_apply, coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
⊢ max (HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max ((f : (a : X) → Y) x) 0 : Y)
have pos : ∀ (h : LT.lt.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) (0 : Y)),
  max (HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max ((f : (a : X) → Y) x) 0 : Y)
Tactic: by_cases h : f x < 0
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
pos :
  ∀ (h : LT.lt.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) (0 : Y)),
    max (HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max ((f : (a : X) → Y) x) 0 : Y)
⊢ max (HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max ((f : (a : X) → Y) x) 0 : Y)
have neg : ∀ (h : ¬LT.lt.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) (0 : Y)),
  max (HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max ((f : (a : X) → Y) x) 0 : Y)
Tactic: by_cases h : f x < 0
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
⊢ (n • f)⁻ = n • f⁻
have h : ∀ (x : X), Eq.{u_2 + 1} (α := Y) (((n • f)⁻ : (a : X) → Y) x : Y) ((n • f⁻ : (a : X) → Y) x : Y)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) (((n • f)⁻ : (a : X) → Y) x : Y) ((n • f⁻ : (a : X) → Y) x : Y)
have h : max (-HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max (-(f : (a : X) → Y) x) 0 : Y)
Tactic: simp only [negPart, max_apply, coe_neg, coe_nsmul, Pi.neg_apply, Pi.smul_apply, coe_zero,
    Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
⊢ max (-HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max (-(f : (a : X) → Y) x) 0 : Y)
have pos : ∀ (h : LT.lt.{u_2} (α := Y) (-(f : (a : X) → Y) x : Y) (0 : Y)),
  max (-HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max (-(f : (a : X) → Y) x) 0 : Y)
Tactic: by_cases h : -f x < 0
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
pos :
  ∀ (h : LT.lt.{u_2} (α := Y) (-(f : (a : X) → Y) x : Y) (0 : Y)),
    max (-HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 =
      HSMul.hSMul (β := Y) n (max (-(f : (a : X) → Y) x) 0 : Y)
⊢ max (-HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max (-(f : (a : X) → Y) x) 0 : Y)
have neg : ∀ (h : ¬LT.lt.{u_2} (α := Y) (-(f : (a : X) → Y) x : Y) (0 : Y)),
  max (-HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max (-(f : (a : X) → Y) x) 0 : Y)
Tactic: by_cases h : -f x < 0
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
⊢ ∃ (e : X), single e 1 ≤ D
have obtain : ∀ (z : X) (hz : Ne (α := ℤ) ((D : (a : X) → ℤ) z : ℤ) (0 : ℤ)), ∃ (e : X), single e 1 ≤ D
Tactic: obtain ⟨z, hz⟩ : ∃ z, D z ≠ 0 := by simpa [D.ext_iff] using (ne_of_lt h).symm
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
z : X
hz : Ne (α := ℤ) ((D : (a : X) → ℤ) z : ℤ) (0 : ℤ)
⊢ ∃ (e : X), single e 1 ≤ D
have refine : ∀ (e : X), LE.le (α := (fun (a : X) ↦ ℤ) e) ((single z 1 : (a : X) → ℤ) e : ℤ) ((D : (a : X) → ℤ) e : ℤ)
Tactic: refine ⟨z, fun e ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
z : X
hz : Ne (α := ℤ) ((D : (a : X) → ℤ) z : ℤ) (0 : ℤ)
e : X
⊢ LE.le (α := (fun (a : X) ↦ ℤ) e) ((single z 1 : (a : X) → ℤ) e : ℤ) ((D : (a : X) → ℤ) e : ℤ)
have inl : ∀ (hz : Ne (α := ℤ) ((D : (a : X) → ℤ) e : ℤ) (0 : ℤ)),
  LE.le (α := (fun (a : X) ↦ ℤ) e) ((single e 1 : (a : X) → ℤ) e : ℤ) ((D : (a : X) → ℤ) e : ℤ)
Tactic: obtain (rfl | he) := eq_or_ne e z
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
z : X
hz : Ne (α := ℤ) ((D : (a : X) → ℤ) z : ℤ) (0 : ℤ)
e : X
inl :
  ∀ (hz : Ne (α := ℤ) ((D : (a : X) → ℤ) e : ℤ) (0 : ℤ)),
    LE.le (α := (fun (a : X) ↦ ℤ) e) ((single e 1 : (a : X) → ℤ) e : ℤ) ((D : (a : X) → ℤ) e : ℤ)
⊢ LE.le (α := (fun (a : X) ↦ ℤ) e) ((single z 1 : (a : X) → ℤ) e : ℤ) ((D : (a : X) → ℤ) e : ℤ)
have inr : ∀ (he : e ≠ z), LE.le (α := (fun (a : X) ↦ ℤ) e) ((single z 1 : (a : X) → ℤ) e : ℤ) ((D : (a : X) → ℤ) e : ℤ)
Tactic: obtain (rfl | he) := eq_or_ne e z
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x : X
hx :
  Membership.mem (γ := Set X)
    (Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0) x
⊢ x ∈ V
have hx₁ : x ∈ V ∧ ¬Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)
Tactic: simp_rw [dite_eq_ite, mem_support, ne_eq, ite_eq_right_iff, Classical.not_imp] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
⊢ ∃ t ∈ 𝓝 z,
    (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0).Finite
have obtain : ∀ (t : Set X) (ht : t ∈ 𝓝 z ∧ (t ∩ D.support (U := U)).Finite),
  ∃ t ∈ 𝓝 z,
    (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0).Finite
Tactic: obtain ⟨t, ht⟩ := D.supportLocallyFiniteWithinDomain z (h hz)
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
t : Set X
ht : t ∈ 𝓝 z ∧ (t ∩ D.support (U := U)).Finite
⊢ ∃ t ∈ 𝓝 z,
    (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0).Finite
have right : (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0).Finite
Tactic: use t, ht.1
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
t : Set X
ht : t ∈ 𝓝 z ∧ (t ∩ D.support (U := U)).Finite
⊢ (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0).Finite
have right : (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0) ⊆
  t ∩ D.support (U := U)
Tactic: apply Set.Finite.subset (s := t ∩ D.support) ht.2
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
U V : Set X
hV : V ⊆ U
⊢ Eq (α := locallyFinsuppWithin V Y) (restrict (U := U) (V := V) 0 hV) 0
have h : ∀ (a : X), Eq.{u_2 + 1} (α := Y) ((restrict (U := U) (V := V) 0 hV : (a : X) → Y) a : Y) ((0 : (a : X) → Y) a : Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
U V : Set X
hV : V ⊆ U
a : X
⊢ Eq.{u_2 + 1} (α := Y) ((restrict (U := U) (V := V) 0 hV : (a : X) → Y) a : Y) ((0 : (a : X) → Y) a : Y)
have h : Eq.{u_2 + 1} (α := Y) (if a ∈ V then (0 : (a : X) → Y) a else 0 : Y) ((0 : (a : X) → Y) a : Y)
Tactic: rw [restrict_apply]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
V : Set X
h : V ⊆ U
⊢ Eq (α := locallyFinsuppWithin V Y) (restrict (U := U) (V := V) 0 h) 0
have h₁ : ∀ (x : X), Eq.{u_2 + 1} (α := Y) ((restrict (U := U) (V := V) 0 h : (a : X) → Y) x : Y) ((0 : (a : X) → Y) x : Y)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (D₁ + D₂).restrict (U := U) (V := V) h = D₁.restrict (U := U) (V := V) h + D₂.restrict (U := U) (V := V) h
have h₁ : ∀ (x : X),
  Eq.{u_2 + 1} (α := Y) (((D₁ + D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h + D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) (((D₁ + D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h + D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
have pos : ∀ (hx : x ∈ V),
  Eq.{u_2 + 1} (α := Y) (((D₁ + D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h + D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
Tactic: by_cases hx : x ∈ V