-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem spanFinBasis.span : ⊤ ≤ Submodule.span ℤ (Set.range (spanFinBasis C s))

Proof state:
case h.h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ
a✝ : f ∈ ⊤
x : ↑(π C fun x => x ∈ s)
⊢ (if (Finsupp.onFinset Finset.univ f.toFun ⋯) x = 0 then 0 else ↑((Finsupp.onFinset Finset.univ f.toFun ⋯) x) x) = f x

Tactic:
split_ifs with h <;> [exact h.symm; rfl]

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ
a✝ : f ∈ ⊤
⊢ f ∈ Submodule.span ℤ (Set.range (spanFinBasis C s))

Tactic:
rw [Finsupp.mem_span_range_iff_exists_finsupp]

Result:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ
a✝ : f ∈ ⊤
⊢ ∃ c, (c.sum fun i a => a • spanFinBasis C s i) = f

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ
a✝ : f ∈ ⊤
⊢ ∃ c, (c.sum fun i a => a • spanFinBasis C s i) = f

Tactic:
use Finsupp.onFinset (Finset.univ) f.toFun (fun _ _ ↦ Finset.mem_univ _)

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ
a✝ : f ∈ ⊤
⊢ ((Finsupp.onFinset Finset.univ f.toFun ⋯).sum fun i a => a • spanFinBasis C s i) = f

Proof state:
case h.h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ
a✝ : f ∈ ⊤
x : ↑(π C fun x => x ∈ s)
⊢ ((Finsupp.onFinset Finset.univ f.toFun ⋯).sum fun i a => a • spanFinBasis C s i) x = f x

Tactic:
change LocallyConstant.evalₗ ℤ x _ = _

Result:
case h.h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ
a✝ : f ∈ ⊤
x : ↑(π C fun x => x ∈ s)
⊢ (LocallyConstant.evalₗ ℤ x) ((Finsupp.onFinset Finset.univ f.toFun ⋯).sum fun i a => a • spanFinBasis C s i) = f x

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (spanFinBasis C s))

Tactic:
intro f _

Result:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ
a✝ : f ∈ ⊤
⊢ f ∈ Submodule.span ℤ (Set.range (spanFinBasis C s))

Proof state:
case h.h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ
a✝ : f ∈ ⊤
x : ↑(π C fun x => x ∈ s)
⊢ (LocallyConstant.evalₗ ℤ x) ((Finsupp.onFinset Finset.univ f.toFun ⋯).sum fun i a => a • spanFinBasis C s i) = f x

Tactic:
simp only [zsmul_eq_mul, map_finsupp_sum, LocallyConstant.evalₗ_apply,
  LocallyConstant.coe_mul, Pi.mul_apply, spanFinBasis, LocallyConstant.coe_mk, mul_ite, mul_one,
  mul_zero, Finsupp.sum_ite_eq, Finsupp.mem_support_iff, ne_eq, ite_not]

Result:
case h.h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ
a✝ : f ∈ ⊤
x : ↑(π C fun x => x ∈ s)
⊢ (if (Finsupp.onFinset Finset.univ f.toFun ⋯) x = 0 then 0 else ↑((Finsupp.onFinset Finset.univ f.toFun ⋯) x) x) = f x

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ
a✝ : f ∈ ⊤
⊢ ((Finsupp.onFinset Finset.univ f.toFun ⋯).sum fun i a => a • spanFinBasis C s i) = f

Tactic:
ext x

Result:
case h.h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x => x ∈ s) ℤ
a✝ : f ∈ ⊤
x : ↑(π C fun x => x ∈ s)
⊢ ((Finsupp.onFinset Finset.univ f.toFun ⋯).sum fun i a => a • spanFinBasis C s i) x = f x