-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ext_of_generateFrom_of_cover_subset {S T : Set (Set α)} (h_gen : ‹_› = generateFrom S)
    (h_inter : IsPiSystem S) (h_sub : T ⊆ S) (hc : T.Countable) (hU : ⋃₀ T = univ)
    (htop : ∀ s ∈ T, μ s ≠ ∞) (h_eq : ∀ s ∈ S, μ s = ν s) : μ = ν

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ⊤
h_eq : ∀ s ∈ S, μ s = ν s
⊢ ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)

Tactic:
intro t ht s hs

Result:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ⊤
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
⊢ μ (s ∩ t) = ν (s ∩ t)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ⊤
h_eq : ∀ s ∈ S, μ s = ν s
⊢ μ = ν

Tactic:
refine ext_of_generateFrom_of_cover h_gen hc h_inter hU htop ?_ fun t ht => h_eq t (h_sub ht)

Result:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ⊤
h_eq : ∀ s ∈ S, μ s = ν s
⊢ ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)

Proof state:
case inr
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ⊤
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
H : (s ∩ t).Nonempty
⊢ μ (s ∩ t) = ν (s ∩ t)

Tactic:
exact h_eq _ (h_inter _ hs _ (h_sub ht) H)

Result:
no goals

Proof state:
case inl
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ⊤
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
H : s ∩ t = ∅
⊢ μ (s ∩ t) = ν (s ∩ t)

Tactic:
simp only [H, measure_empty]

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ⊤
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
⊢ μ (s ∩ t) = ν (s ∩ t)

Tactic:
rcases (s ∩ t).eq_empty_or_nonempty with H | H

Result:
case inl
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ⊤
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
H : s ∩ t = ∅
⊢ μ (s ∩ t) = ν (s ∩ t)

case inr
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
h_inter : IsPiSystem S
h_sub : T ⊆ S
hc : T.Countable
hU : ⋃₀ T = univ
htop : ∀ s ∈ T, μ s ≠ ⊤
h_eq : ∀ s ∈ S, μ s = ν s
t : Set α
ht : t ∈ T
s : Set α
hs : s ∈ S
H : (s ∩ t).Nonempty
⊢ μ (s ∩ t) = ν (s ∩ t)