-- Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean
theorem inducedOuterMeasure_eq (hC : IsSetSemiring C) (m : AddContent C)
    (m_sigma_subadd : m.IsSigmaSubadditive) (hs : s ∈ C) :
    inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s = m s

Proof state:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
⊢ (AddContent.extend hC m) (⋃ i, f i) ≤ ∑' (i : ℕ), (AddContent.extend hC m) (f i)

Tactic:
rw [m.extend_eq hC hf_mem]

Result:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
⊢ m (⋃ i, f i) ≤ ∑' (i : ℕ), (AddContent.extend hC m) (f i)

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯) s = m s

Tactic:
suffices inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s = m.extend hC s by
  rwa [m.extend_eq hC hs] at this

Result:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯) s = (AddContent.extend hC m) s

Proof state:
case refine_2.e_f.h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
i : ℕ
⊢ m (f i) = (AddContent.extend hC m) (f i)

Tactic:
rw [m.extend_eq hC (hf i)]

Result:
no goals

Proof state:
case refine_3
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ ∀ s ∉ C, (AddContent.extend hC m) s = ⊤

Tactic:
exact fun _ ↦ m.extend_eq_top _

Result:
no goals

Proof state:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (AddContent.extend hC m).IsSigmaSubadditive

Tactic:
intro f hf hf_mem

Result:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
⊢ (AddContent.extend hC m) (⋃ i, f i) ≤ ∑' (i : ℕ), (AddContent.extend hC m) (f i)

Proof state:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
⊢ ∑' (i : ℕ), m (f i) = ∑' (i : ℕ), (AddContent.extend hC m) (f i)

Tactic:
congr with i

Result:
case refine_2.e_f.h
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
i : ℕ
⊢ m (f i) = (AddContent.extend hC m) (f i)

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯) s = (AddContent.extend hC m) s

Tactic:
refine Eq.trans ?_ ((m.extend hC).ofFunction_eq hC ?_ ?_ hs)

Result:
case refine_1
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯) s = (OuterMeasure.ofFunction ⇑(AddContent.extend hC m) ⋯) s

case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (AddContent.extend hC m).IsSigmaSubadditive

case refine_3
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ ∀ s ∉ C, (AddContent.extend hC m) s = ⊤

Proof state:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
⊢ m (⋃ i, f i) ≤ ∑' (i : ℕ), (AddContent.extend hC m) (f i)

Tactic:
refine (m_sigma_subadd hf hf_mem).trans_eq ?_

Result:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_mem : ⋃ i, f i ∈ C
⊢ ∑' (i : ℕ), m (f i) = ∑' (i : ℕ), (AddContent.extend hC m) (f i)

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
this : (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯) s = (AddContent.extend hC m) s
⊢ (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯) s = m s

Tactic:
rwa [m.extend_eq hC hs] at this

Result:
no goals

Proof state:
case refine_1
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯) s = (OuterMeasure.ofFunction ⇑(AddContent.extend hC m) ⋯) s

Tactic:
congr

Result:
no goals