awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞)
rw₃ : Eq (α := ℝ≥0∞) (⨅ (_ : f ⁻¹' s = ∅), 0 : ℝ≥0∞) (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞)
rw₄ : Eq (α := ℝ≥0∞) (⨅ (_ : f ⁻¹' s = ∅), 0) (⨅ (_ : f '' f ⁻¹' s = ∅), 0)
⊢ Eq (α := ℝ≥0∞) ((((map f : (a : OuterMeasure α) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw₅ : Eq (α := ℝ≥0∞) (⨅ (_ : f ⁻¹' s = ∅), 0) (⨅ (_ : f ⁻¹' s = ∅), 0)
Tactic: rw [map_apply, restrict_apply, ← image_preimage_eq_inter_range, top_apply', top_apply',
      Set.image_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ Eq.{u_2 + 1} (α := OuterMeasure β) ((map f : (a : OuterMeasure α) → OuterMeasure β) ⊤) ⊤
have rw : Eq (α := OuterMeasure β) ((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β)
  (⊤ : OuterMeasure β)
Tactic: rw [map_top, hf.range_eq, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
rw :
  Eq (α := OuterMeasure β) ((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β)
    (⊤ : OuterMeasure β)
⊢ Eq.{u_2 + 1} (α := OuterMeasure β) ((map f : (a : OuterMeasure α) → OuterMeasure β) ⊤) ⊤
have rw₁ : Eq.{u_2 + 1} (α := OuterMeasure β) ((restrict univ : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β)
  (⊤ : OuterMeasure β)
Tactic: rw [map_top, hf.range_eq, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
rw :
  Eq (α := OuterMeasure β) ((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β)
    (⊤ : OuterMeasure β)
rw₁ :
  Eq.{u_2 + 1} (α := OuterMeasure β) ((restrict univ : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β)
    (⊤ : OuterMeasure β)
⊢ Eq.{u_2 + 1} (α := OuterMeasure β) ((map f : (a : OuterMeasure α) → OuterMeasure β) ⊤) ⊤
have rw₂ : Eq.{u_2 + 1} (α := OuterMeasure β) ⊤ ⊤
Tactic: rw [map_top, hf.range_eq, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S s : Set α
h_s : Membership.mem (γ := Set (Set α)) {S} s
t : Set α
h_t : Membership.mem (γ := Set (Set α)) {S} t
h : (s ∩ t).Nonempty
⊢ Membership.mem (γ := Set (Set α)) {S} (s ∩ t)
have rw : Membership.mem (γ := Set (Set α)) {S} (S ∩ t)
Tactic: rw [Set.mem_singleton_iff.1 h_s, Set.mem_singleton_iff.1 h_t, Set.inter_self,
    Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S s : Set α
h_s : Membership.mem (γ := Set (Set α)) {S} s
t : Set α
h_t : Membership.mem (γ := Set (Set α)) {S} t
h : (s ∩ t).Nonempty
rw : Membership.mem (γ := Set (Set α)) {S} (S ∩ t)
⊢ Membership.mem (γ := Set (Set α)) {S} (s ∩ t)
have rw₁ : Membership.mem (γ := Set (Set α)) {S} (S ∩ S)
Tactic: rw [Set.mem_singleton_iff.1 h_s, Set.mem_singleton_iff.1 h_t, Set.inter_self,
    Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S s : Set α
h_s : Membership.mem (γ := Set (Set α)) {S} s
t : Set α
h_t : Membership.mem (γ := Set (Set α)) {S} t
h : (s ∩ t).Nonempty
rw : Membership.mem (γ := Set (Set α)) {S} (S ∩ t)
rw₁ : Membership.mem (γ := Set (Set α)) {S} (S ∩ S)
⊢ Membership.mem (γ := Set (Set α)) {S} (s ∩ t)
have rw₂ : Membership.mem (γ := Set (Set α)) {S} S
Tactic: rw [Set.mem_singleton_iff.1 h_s, Set.mem_singleton_iff.1 h_t, Set.inter_self,
    Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S s : Set α
h_s : Membership.mem (γ := Set (Set α)) {S} s
t : Set α
h_t : Membership.mem (γ := Set (Set α)) {S} t
h : (s ∩ t).Nonempty
rw : Membership.mem (γ := Set (Set α)) {S} (S ∩ t)
rw₁ : Membership.mem (γ := Set (Set α)) {S} (S ∩ S)
rw₂ : Membership.mem (γ := Set (Set α)) {S} S
⊢ Membership.mem (γ := Set (Set α)) {S} (s ∩ t)
have rw₃ : S = S
Tactic: rw [Set.mem_singleton_iff.1 h_s, Set.mem_singleton_iff.1 h_t, Set.inter_self,
    Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert ∅ S
t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
⊢ s ∩ t ∈ insert ∅ S
have inl : ∀ (hs : s = ∅), s ∩ t ∈ insert ∅ S
Tactic: rcases hs with hs | hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert ∅ S
t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
inl : ∀ (hs : s = ∅), s ∩ t ∈ insert ∅ S
⊢ s ∩ t ∈ insert ∅ S
have inr : ∀ (hs : s ∈ S), s ∩ t ∈ insert ∅ S
Tactic: rcases hs with hs | hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ S
have inr : ∀ (ht : t = ∅), s ∩ t ∈ insert ∅ S
Tactic: rcases ht with ht | ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
inr : ∀ (ht : t = ∅), s ∩ t ∈ insert ∅ S
⊢ s ∩ t ∈ insert ∅ S
have inr₁ : ∀ (ht : t ∈ S), s ∩ t ∈ insert ∅ S
Tactic: rcases ht with ht | ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
⊢ s ∩ t ∈ insert univ S
have inl : ∀ (hs : s = univ), s ∩ t ∈ insert univ S
Tactic: rcases hs with hs | hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
inl : ∀ (hs : s = univ), s ∩ t ∈ insert univ S
⊢ s ∩ t ∈ insert univ S
have inr : ∀ (hs : s ∈ S), s ∩ t ∈ insert univ S
Tactic: rcases hs with hs | hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s = univ
⊢ s ∩ t ∈ insert univ S
have inl : ∀ (ht : t = univ), s ∩ t ∈ insert univ S
Tactic: rcases ht with ht | ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s = univ
inl : ∀ (ht : t = univ), s ∩ t ∈ insert univ S
⊢ s ∩ t ∈ insert univ S
have inl₁ : ∀ (ht : t ∈ S), s ∩ t ∈ insert univ S
Tactic: rcases ht with ht | ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert univ S
have inr : ∀ (ht : t = univ), s ∩ t ∈ insert univ S
Tactic: rcases ht with ht | ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
inr : ∀ (ht : t = univ), s ∩ t ∈ insert univ S
⊢ s ∩ t ∈ insert univ S
have inr₁ : ∀ (ht : t ∈ S), s ∩ t ∈ insert univ S
Tactic: rcases ht with ht | ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' s ∩ f ⁻¹' t).Nonempty
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ t ∈ S, f ⁻¹' t = s} (f ⁻¹' s ∩ f ⁻¹' t)
have rw : ∀ (hst : (f ⁻¹' (s ∩ t)).Nonempty), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ t ∈ S, f ⁻¹' t = s} (f ⁻¹' (s ∩ t))
Tactic: rw [← Set.preimage_inter] at hst ⊢
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
s : ℕ → Set α
C : Set (Set α)
hC : IsPiSystem C
h : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ∀ (h' : (dissipate s n).Nonempty), dissipate s n ∈ C
h' : (dissipate s (n + 1)).Nonempty
⊢ dissipate s (n + 1) ∈ C
have succ : ∀ (h' : (dissipate s n ∩ s (n + 1)).Nonempty), dissipate s n ∩ s (n + 1) ∈ C
Tactic: rw [dissipate_succ] at h' ⊢
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
s : ℕ → Set α
C : Set (Set α)
hC : IsPiSystem C
h : ∀ (n : ℕ), s n ∈ C
n : ℕ
h' : (dissipate s n).Nonempty
⊢ dissipate s n ∈ C
have zero : ∀ (h' : (dissipate s 0).Nonempty), dissipate s 0 ∈ C
Tactic: induction n with
  | zero => simpa using h 0
  | succ n hn =>
    rw [dissipate_succ] at h' ⊢
    exact hC (dissipate s n) (hn h'.left) (s (n + 1)) (h (n + 1)) h'
Cleared hypotheses: n, h'
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
s : ℕ → Set α
C : Set (Set α)
hC : IsPiSystem C
h : ∀ (n : ℕ), s n ∈ C
n : ℕ
h' : (dissipate s n).Nonempty
zero : ∀ (h' : (dissipate s 0).Nonempty), dissipate s 0 ∈ C
⊢ dissipate s n ∈ C
have succ : ∀ (n : ℕ) (hn : ∀ (h' : (dissipate s n).Nonempty), dissipate s n ∈ C) (h' : (dissipate s (n + 1)).Nonempty),
  dissipate s (n + 1) ∈ C
Tactic: induction n with
  | zero => simpa using h 0
  | succ n hn =>
    rw [dissipate_succ] at h' ⊢
    exact hC (dissipate s n) (hn h'.left) (s (n + 1)) (h (n + 1)) h'
Cleared hypotheses: n, h'
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun (x1 x2 : Set (Set α)) ↦ x1 ≤ x2) p
t1 : Set α
ht1 : Membership.mem (γ := Set (Set α)) (⋃ (n : ι), p n) t1
t2 : Set α
ht2 : Membership.mem (γ := Set (Set α)) (⋃ (n : ι), p n) t2
h : (t1 ∩ t2).Nonempty
⊢ Membership.mem (γ := Set (Set α)) (⋃ (n : ι), p n) (t1 ∩ t2)
have rw : ∀ (ht1 : ∃ (i : ι), t1 ∈ p i) (t2 : Set α) (ht2 : ∃ (i : ι), t2 ∈ p i) (h : (t1 ∩ t2).Nonempty),
  ∃ (i : ι), t1 ∩ t2 ∈ p i
Tactic: rw [Set.mem_iUnion] at ht1 ht2 ⊢
Cleared hypotheses: ht1, t2, ht2, h
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun (x1 x2 : Set (Set α)) ↦ x1 ≤ x2) p
t1 : Set α
ht1 : ∃ (i : ι), t1 ∈ p i
t2 : Set α
ht2 : ∃ (i : ι), t2 ∈ p i
h : (t1 ∩ t2).Nonempty
⊢ ∃ (i : ι), t1 ∩ t2 ∈ p i
have obtain : ∀ (n : ι) (ht1 : t1 ∈ p n), ∃ (i : ι), t1 ∩ t2 ∈ p i
Tactic: obtain ⟨n, ht1⟩ := ht1
Cleared hypotheses: ht1
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun (x1 x2 : Set (Set α)) ↦ x1 ≤ x2) p
t1 t2 : Set α
ht2 : ∃ (i : ι), t2 ∈ p i
h : (t1 ∩ t2).Nonempty
n : ι
ht1 : t1 ∈ p n
⊢ ∃ (i : ι), t1 ∩ t2 ∈ p i
have obtain : ∀ (m : ι) (ht2 : t2 ∈ p m), ∃ (i : ι), t1 ∩ t2 ∈ p i
Tactic: obtain ⟨m, ht2⟩ := ht2
Cleared hypotheses: ht2
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun (x1 x2 : Set (Set α)) ↦ x1 ≤ x2) p
t1 t2 : Set α
h : (t1 ∩ t2).Nonempty
n : ι
ht1 : t1 ∈ p n
m : ι
ht2 : t2 ∈ p m
⊢ ∃ (i : ι), t1 ∩ t2 ∈ p i
have obtain : ∀ (k : ι) (hpnk : p n ≤ p k) (hpmk : p m ≤ p k), ∃ (i : ι), t1 ∩ t2 ∈ p i
Tactic: obtain ⟨k, hpnk, hpmk⟩ : ∃ k, p n ≤ p k ∧ p m ≤ p k := hp_directed n m
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
hs₁ : s₁ ∈ C
t₁ : Set β
ht₁ : t₁ ∈ D
s₂ : Set α
hs₂ : s₂ ∈ C
t₂ : Set β
ht₂ : t₂ ∈ D
hst :
  Set.Nonempty (α := α × β)
    ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s₁ t₁ ∩ (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s₂ t₂)
⊢ Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)
    ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s₁ t₁ ∩ (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s₂ t₂)
have rw : ∀ (hst : ((s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)).Nonempty),
  Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)
    ((s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂))
Tactic: rw [prod_inter_prod] at hst ⊢
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (hypothesis)
Goal:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
hs₁ : s₁ ∈ C
t₁ : Set β
ht₁ : t₁ ∈ D
s₂ : Set α
hs₂ : s₂ ∈ C
t₂ : Set β
ht₂ : t₂ ∈ D
hst : ((s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)).Nonempty
⊢ Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)
    ((s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂))
have hst₁ : (s₁ ∩ s₂).Nonempty ∧ (t₁ ∩ t₂).Nonempty
Tactic: rw [prod_nonempty_iff] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t_1 : Finset (Set α)
a : Set α
t : Finset (Set α)
hat : a ∉ t
t_ne : t.Nonempty
ih : ∀ (ht : ∀ s ∈ t, s ∈ S) (h' : Set.Nonempty.{u_1} (α := α) (⋂ s ∈ t, s)), ⋂ s ∈ t, s ∈ S
ht : ∀ s ∈ Finset.cons a t hat, s ∈ S
h' : Set.Nonempty.{u_1} (α := α) (⋂ s ∈ Finset.cons a t hat, s)
⊢ ⋂ s ∈ Finset.cons a t hat, s ∈ S
have cons : ∀ (h' : (a ∩ ⋂ x ∈ t, x).Nonempty) (ht : ∀ (s : Set α), s = a ∨ s ∈ t → s ∈ S), a ∩ ⋂ x ∈ t, x ∈ S
Tactic: simp only [Finset.cons_eq_insert, Finset.mem_insert, iInter_iInter_eq_or_left] at h' ht ⊢
Cleared hypotheses: ht, h'
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t_1 : Finset (Set α)
a : Set α
t : Finset (Set α)
hat : a ∉ t
t_ne : t.Nonempty
ih : ∀ (ht : ∀ s ∈ t, s ∈ S) (h' : Set.Nonempty.{u_1} (α := α) (⋂ s ∈ t, s)), ⋂ s ∈ t, s ∈ S
h' : (a ∩ ⋂ x ∈ t, x).Nonempty
ht : ∀ (s : Set α), s = a ∨ s ∈ t → s ∈ S
⊢ a ∩ ⋂ x ∈ t, x ∈ S
have cons : ⋂ x ∈ t, x ∈ S
Tactic: refine h_pi _ (ht a (Or.inl rfl)) _ ?_ h'
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t_1 : Finset (Set α)
a : Set α
t : Finset (Set α)
hat : a ∉ t
t_ne : t.Nonempty
ih : ∀ (ht : ∀ s ∈ t, s ∈ S) (h' : Set.Nonempty.{u_1} (α := α) (⋂ s ∈ t, s)), ⋂ s ∈ t, s ∈ S
h' : (a ∩ ⋂ x ∈ t, x).Nonempty
ht : ∀ (s : Set α), s = a ∨ s ∈ t → s ∈ S
⊢ ⋂ x ∈ t, x ∈ S
have cons : ∀ (s : Set α) (hs : s ∈ t), s ∈ S
Tactic: refine ih (fun s hs ↦ ?_) h'.right
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t : Finset (Set α)
t_ne : t.Nonempty
ht : ∀ s ∈ t, s ∈ S
h' : Set.Nonempty.{u_1} (α := α) (⋂ s ∈ t, s)
⊢ ⋂ s ∈ t, s ∈ S
have singleton : ∀ (a : Set α) (ht : ∀ (s : Set α), Membership.mem (γ := Finset (Set α)) {a} s → s ∈ S)
  (h' : Set.Nonempty.{u_1} (α := α) (⋂ (s : Set α), ⋂ (_ : Membership.mem (γ := Finset (Set α)) {a} s), s)),
  ⋂ (s : Set α), ⋂ (_ : Membership.mem (γ := Finset (Set α)) {a} s), s ∈ S
Tactic: induction t_ne using Finset.Nonempty.cons_induction with
  | singleton a => simpa using ht
  | cons a t hat t_ne ih =>
    simp only [Finset.cons_eq_insert, Finset.mem_insert, iInter_iInter_eq_or_left] at h' ht ⊢
    refine h_pi _ (ht a (Or.inl rfl)) _ ?_ h'
    refine ih (fun s hs ↦ ?_) h'.right
    exact ht s (Or.inr hs)
Cleared hypotheses: t_ne, ht, h'
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t : Finset (Set α)
t_ne : t.Nonempty
ht : ∀ s ∈ t, s ∈ S
h' : Set.Nonempty.{u_1} (α := α) (⋂ s ∈ t, s)
singleton :
  ∀ (a : Set α) (ht : ∀ (s : Set α), Membership.mem (γ := Finset (Set α)) {a} s → s ∈ S)
    (h' : Set.Nonempty.{u_1} (α := α) (⋂ (s : Set α), ⋂ (_ : Membership.mem (γ := Finset (Set α)) {a} s), s)),
    ⋂ (s : Set α), ⋂ (_ : Membership.mem (γ := Finset (Set α)) {a} s), s ∈ S
⊢ ⋂ s ∈ t, s ∈ S
have cons : ∀ (a : Set α) (t : Finset (Set α)) (hat : a ∉ t) (t_ne : t.Nonempty)
  (ih : ∀ (ht : ∀ s ∈ t, s ∈ S) (h' : Set.Nonempty.{u_1} (α := α) (⋂ s ∈ t, s)), ⋂ s ∈ t, s ∈ S)
  (ht : ∀ s ∈ Finset.cons a t hat, s ∈ S) (h' : Set.Nonempty.{u_1} (α := α) (⋂ s ∈ Finset.cons a t hat, s)),
  ⋂ s ∈ Finset.cons a t hat, s ∈ S
Tactic: induction t_ne using Finset.Nonempty.cons_induction with
  | singleton a => simpa using ht
  | cons a t hat t_ne ih =>
    simp only [Finset.cons_eq_insert, Finset.mem_insert, iInter_iInter_eq_or_left] at h' ht ⊢
    refine h_pi _ (ht a (Or.inl rfl)) _ ?_ h'
    refine ih (fun s hs ↦ ?_) h'.right
    exact ht s (Or.inr hs)
Cleared hypotheses: t_ne, ht, h'
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t : Finset (Set α)
t_ne : t.Nonempty
ht : ∀ s ∈ t, s ∈ S
h' : Set.Nonempty.{u_1} (α := α) (⋂ s ∈ t, s)
⊢ ⋂ s ∈ t, s ∈ S
have singleton : ∀ (a : Set α) (ht : ∀ (s : Set α), Membership.mem (γ := Finset (Set α)) {a} s → s ∈ S)
  (h' : Set.Nonempty.{u_1} (α := α) (⋂ (s : Set α), ⋂ (_ : Membership.mem (γ := Finset (Set α)) {a} s), s)),
  ⋂ (s : Set α), ⋂ (_ : Membership.mem (γ := Finset (Set α)) {a} s), s ∈ S
Tactic: classical
  induction t_ne using Finset.Nonempty.cons_induction with
  | singleton a => simpa using ht
  | cons a t hat t_ne ih =>
    simp only [Finset.cons_eq_insert, Finset.mem_insert, iInter_iInter_eq_or_left] at h' ht ⊢
    refine h_pi _ (ht a (Or.inl rfl)) _ ?_ h'
    refine ih (fun s hs ↦ ?_) h'.right
    exact ht s (Or.inr hs)
Cleared hypotheses: t_ne, ht, h'
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t : Finset (Set α)
t_ne : t.Nonempty
ht : ∀ s ∈ t, s ∈ S
h' : Set.Nonempty.{u_1} (α := α) (⋂ s ∈ t, s)
singleton :
  ∀ (a : Set α) (ht : ∀ (s : Set α), Membership.mem (γ := Finset (Set α)) {a} s → s ∈ S)
    (h' : Set.Nonempty.{u_1} (α := α) (⋂ (s : Set α), ⋂ (_ : Membership.mem (γ := Finset (Set α)) {a} s), s)),
    ⋂ (s : Set α), ⋂ (_ : Membership.mem (γ := Finset (Set α)) {a} s), s ∈ S
⊢ ⋂ s ∈ t, s ∈ S
have cons : ∀ (a : Set α) (t : Finset (Set α)) (hat : a ∉ t) (t_ne : t.Nonempty)
  (ih : ∀ (ht : ∀ s ∈ t, s ∈ S) (h' : Set.Nonempty.{u_1} (α := α) (⋂ s ∈ t, s)), ⋂ s ∈ t, s ∈ S)
  (ht : ∀ s ∈ Finset.cons a t hat, s ∈ S) (h' : Set.Nonempty.{u_1} (α := α) (⋂ s ∈ Finset.cons a t hat, s)),
  ⋂ s ∈ Finset.cons a t hat, s ∈ S
Tactic: classical
  induction t_ne using Finset.Nonempty.cons_induction with
  | singleton a => simpa using ht
  | cons a t hat t_ne ih =>
    simp only [Finset.cons_eq_insert, Finset.mem_insert, iInter_iInter_eq_or_left] at h' ht ⊢
    refine h_pi _ (ht a (Or.inl rfl)) _ ?_ h'
    refine ih (fun s hs ↦ ?_) h'.right
    exact ht s (Or.inr hs)
Cleared hypotheses: t_ne, ht, h'
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
inst : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
s t : Set α
l₁ : α
hls₁ : l₁ ∈ s
u₁ : α
hut₁ : u₁ ∈ t
left : p l₁ u₁
l₂ : α
hls₂ : l₂ ∈ s
u₂ : α
hut₂ : u₂ ∈ t
left_1 : p l₂ u₂
⊢ (Ixx l₁ u₁ ∩ Ixx l₂ u₂).Nonempty →
    Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S} (Ixx l₁ u₁ ∩ Ixx l₂ u₂)
have simp : (Ixx (max l₁ l₂) (min u₁ u₂)).Nonempty →
  Membership.mem (γ := Set (Set α)) {S : Set α | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S} (Ixx (max l₁ l₂) (min u₁ u₂))
Tactic: simp only [Hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x : Set α
h : x ∈ generatePiSystem S
⊢ x ∈ S
have base : ∀ {s : Set α} (h_s : s ∈ S), s ∈ S
Tactic: induction h with
  | base h_s => exact h_s
  | inter _ _ h_nonempty h_s h_u => exact h_S _ h_s _ h_u h_nonempty
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x : Set α
h : x ∈ generatePiSystem S
base : ∀ {s : Set α} (h_s : s ∈ S), s ∈ S
⊢ x ∈ S
have inter : ∀ {s t : Set α},
  generatePiSystem S s → generatePiSystem S t → ∀ (h_nonempty : (s ∩ t).Nonempty) (h_s : s ∈ S) (h_u : t ∈ S), s ∩ t ∈ S
Tactic: induction h with
  | base h_s => exact h_s
  | inter _ _ h_nonempty h_s h_u => exact h_S _ h_s _ h_u h_nonempty
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t : Set α
ht : t ∈ generatePiSystem S
⊢ t ∈ generatePiSystem T
have base : ∀ {s : Set α} (h_s : s ∈ S), s ∈ generatePiSystem T
Tactic: induction ht with
  | base h_s => exact generatePiSystem.base (Set.mem_of_subset_of_mem hST h_s)
  | inter _ _ h_nonempty h_s h_u => exact isPiSystem_generatePiSystem T _ h_s _ h_u h_nonempty
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t : Set α
ht : t ∈ generatePiSystem S
base : ∀ {s : Set α} (h_s : s ∈ S), s ∈ generatePiSystem T
⊢ t ∈ generatePiSystem T
have inter : ∀ {s t : Set α},
  generatePiSystem S s →
    generatePiSystem S t →
      ∀ (h_nonempty : (s ∩ t).Nonempty) (h_s : s ∈ generatePiSystem T) (h_u : t ∈ generatePiSystem T),
        s ∩ t ∈ generatePiSystem T
Tactic: induction ht with
  | base h_s => exact generatePiSystem.base (Set.mem_of_subset_of_mem hST h_s)
  | inter _ _ h_nonempty h_s h_u => exact isPiSystem_generatePiSystem T _ h_s _ h_u h_nonempty
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ s ∈ S, MeasurableSet s
t : Set α
h_in_pi : t ∈ generatePiSystem S
base : ∀ {s : Set α} (h_s : s ∈ S), MeasurableSet s
⊢ MeasurableSet t
have inter : ∀ {s t : Set α},
  generatePiSystem S s →
    generatePiSystem S t → (s ∩ t).Nonempty → ∀ (h_s : MeasurableSet s) (h_u : MeasurableSet t), MeasurableSet (s ∩ t)
Tactic: induction h_in_pi with
  | base h_s => apply h_meas_S _ h_s
  | inter _ _ _ h_s h_u => apply MeasurableSet.inter h_s h_u
Cleared hypotheses: h_in_pi
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
g : Set (Set α)
⊢ generateFrom (generatePiSystem g) = generateFrom g
have a : generateFrom (generatePiSystem g) ≤ generateFrom g
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
g : Set (Set α)
a : generateFrom (generatePiSystem g) ≤ generateFrom g
⊢ generateFrom (generatePiSystem g) = generateFrom g
have a₁ : generateFrom g ≤ generateFrom (generatePiSystem g)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
g : Set (Set α)
⊢ generateFrom (generatePiSystem g) ≤ generateFrom g
have a : ∀ t ∈ generatePiSystem g, MeasurableSet t
Tactic: apply generateFrom_le
-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_1
g : Set (Set α)
⊢ generateFrom g ≤ generateFrom (generatePiSystem g)
have a : ∀ t ∈ g, MeasurableSet t
Tactic: apply generateFrom_le