Theorem: tsum_inter_support_eq_tsum_subtype (Matroid/ForMathlib/ENatTopology.lean)

State before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ ∑' (x : ↑(s ∩ support f)), f ↑x = ∑' (x : ↑s), f ↑x
Tactic:
rw [tsum_congr (show ∀ (a : s), f a = (s.indicator f) a from _),
  tsum_congr ((show ∀ (a : ↑ (s ∩ f.support)), f a = (s.indicator f) a from _)),
  tsum_subtype_eq_of_support_subset (by simp), tsum_subtype_eq_of_support_subset (by simp)]
State after:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ ∀ (a : ↑(s ∩ support f)), f ↑a = s.indicator f ↑a

α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ ∀ (a : ↑s), f ↑a = s.indicator f ↑a

State before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ ∀ (a : ↑s), f ↑a = s.indicator f ↑a
Tactic:
rintro ⟨a, ha⟩
State after:
case mk
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
a : α
ha : a ∈ s
⊢ f ↑⟨a, ha⟩ = s.indicator f ↑⟨a, ha⟩

State before:
case mk
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
a : α
ha : a ∈ s
⊢ f ↑⟨a, ha⟩ = s.indicator f ↑⟨a, ha⟩
Tactic:
simp [indicator_of_mem ha]
State after:
no goals

State before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ support (s.indicator f) ⊆ s ∩ support f
Tactic:
simp
State after:
no goals

State before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ support (s.indicator f) ⊆ s
Tactic:
simp
State after:
no goals

State before:
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
⊢ ∀ (a : ↑(s ∩ support f)), f ↑a = s.indicator f ↑a
Tactic:
rintro ⟨a,ha⟩
State after:
case mk
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
a : α
ha : a ∈ s ∩ support f
⊢ f ↑⟨a, ha⟩ = s.indicator f ↑⟨a, ha⟩

State before:
case mk
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
a : α
ha : a ∈ s ∩ support f
⊢ f ↑⟨a, ha⟩ = s.indicator f ↑⟨a, ha⟩
Tactic:
simp [indicator_of_mem ha.1]
State after:
no goals