awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.PiSystem
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
⊢ ∃ (k : ι), p n ≤ p k ∧ p m ≤ p k

Tactic:
hp_directed n m
-- Module: Mathlib.MeasureTheory.PiSystem
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
obtain : ∀ (k : ι) (hpnk : p n ≤ p k) (hpmk : p m ≤ p k), ∃ (i : ι), t1 ∩ t2 ∈ p i
⊢ ∃ (i : ι), t1 ∩ t2 ∈ p i

Tactic:
obtain ⟨k, hpnk, hpmk⟩ : ∃ k, p n ≤ p k ∧ p m ≤ p k := hp_directed n m
-- Module: Mathlib.MeasureTheory.PiSystem
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
k : ι
hpnk : p n ≤ p k
hpmk : p m ≤ p k
⊢ ∃ (i : ι), t1 ∩ t2 ∈ p i

Tactic:
⟨k, hp_pi k t1 (hpnk ht1) t2 (hpmk ht2) h⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.PiSystem
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
k : ι
hpnk : p n ≤ p k
hpmk : p m ≤ p k
⊢ ∃ (i : ι), t1 ∩ t2 ∈ p i

Tactic:
exact ⟨k, hp_pi k t1 (hpnk ht1) t2 (hpmk ht2) h⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
ι : Type u_4
inst : SemilatticeSup ι
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_mono : Monotone p
⊢ IsPiSystem.{u_3} (α := α) (⋃ (n : ι), p n)

Tactic:
isPiSystem_iUnion_of_directed_le p hp_pi (Monotone.directed_le hp_mono)

Premises used: isPiSystem_iUnion_of_directed_le, Monotone.directed_le
-- Module: Mathlib.MeasureTheory.PiSystem
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₂)
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₂))
⊢ 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₂)

Tactic:
rw [prod_inter_prod] at hst ⊢

Premises used: Set.prod_inter_prod
-- Module: Mathlib.MeasureTheory.PiSystem
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
⊢ (s₁ ∩ s₂).Nonempty ∧ (t₁ ∩ t₂).Nonempty

Tactic:
rw [prod_nonempty_iff] at hst

Premises used: Set.prod_nonempty_iff
-- Module: Mathlib.MeasureTheory.PiSystem
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₂).Nonempty ∧ (t₁ ∩ t₂).Nonempty
⊢ Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)
    ((s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂))

Tactic:
mem_image2_of_mem (hC _ hs₁ _ hs₂ hst.1) (hD _ ht₁ _ ht₂ hst.2)

Premises used: And.right, And.left, Set.mem_image2_of_mem
-- Module: Mathlib.MeasureTheory.PiSystem
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₂).Nonempty ∧ (t₁ ∩ t₂).Nonempty
⊢ Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)
    ((s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂))

Tactic:
exact mem_image2_of_mem (hC _ hs₁ _ hs₂ hst.1) (hD _ ht₁ _ ht₂ hst.2)

Premises used: And.right, And.left, Set.mem_image2_of_mem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t : Finset (Set α)
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:
simpa using ht
-- Module: Mathlib.MeasureTheory.PiSystem
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)
cons : ∀ (h' : (a ∩ ⋂ x ∈ t, x).Nonempty) (ht : ∀ (s : Set α), s = a ∨ s ∈ t → s ∈ S), a ∩ ⋂ x ∈ t, x ∈ S
⊢ ⋂ s ∈ Finset.cons a t hat, s ∈ S

Tactic:
simp only [Finset.cons_eq_insert, Finset.mem_insert, iInter_iInter_eq_or_left] at h' ht ⊢

Premises used: Finset.mem_insert, Finset.cons_eq_insert, Set.iInter_iInter_eq_or_left
-- Module: Mathlib.MeasureTheory.PiSystem
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

Tactic:
h_pi _ (ht a (Or.inl rfl)) _ ?_ h'

Premises used: Or.inl, rfl
-- Module: Mathlib.MeasureTheory.PiSystem
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
cons : ⋂ x ∈ t, x ∈ S
⊢ a ∩ ⋂ x ∈ t, x ∈ S

Tactic:
refine h_pi _ (ht a (Or.inl rfl)) _ ?_ h'

Premises used: Or.inl, rfl
-- Module: Mathlib.MeasureTheory.PiSystem
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

Tactic:
ih (fun s hs ↦ ?_) h'.right

Premises used: Set.Nonempty.right
-- Module: Mathlib.MeasureTheory.PiSystem
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
cons : ∀ (s : Set α) (hs : s ∈ t), s ∈ S
⊢ ⋂ x ∈ t, x ∈ S

Tactic:
refine ih (fun s hs ↦ ?_) h'.right

Premises used: Set.Nonempty.right
-- Module: Mathlib.MeasureTheory.PiSystem
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
s : Set α
hs : s ∈ t
⊢ s ∈ S

Tactic:
ht s (Or.inr hs)

Premises used: Or.inr
-- Module: Mathlib.MeasureTheory.PiSystem
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
s : Set α
hs : s ∈ t
⊢ s ∈ S

Tactic:
exact ht s (Or.inr hs)

Premises used: Or.inr
-- Module: Mathlib.MeasureTheory.PiSystem
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
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
⊢ ⋂ s ∈ t, 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)

Premises used: Finset.mem_insert, IsPiSystem.singleton, Finset.cons_eq_insert, Set.iInter_iInter_eq_or_left
-- Module: Mathlib.MeasureTheory.PiSystem
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
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
⊢ ⋂ s ∈ t, 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)

Premises used: Finset.mem_insert, IsPiSystem.singleton, Finset.cons_eq_insert, Set.iInter_iInter_eq_or_left
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Iio a ∩ Iio b ∈ Iio '' s

Tactic:
⟨a ⊓ b, inf_ind a b ha hb, Iio_inter_Iio.symm⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, Set.Iio_inter_Iio, Eq.symm, Min.min, inf_ind
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Iio a ∩ Iio b ∈ Iio '' s

Tactic:
exact ⟨a ⊓ b, inf_ind a b ha hb, Iio_inter_Iio.symm⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
⊢ IsPiSystem.{u_1} (α := α) (range Iio)

Tactic:
@image_univ α _ Iio ▸ isPiSystem_image_Iio univ

Premises used: Set.image_univ, Set.univ, Eq.rec, isPiSystem_image_Iio
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
⊢ IsPiSystem (Ioi '' s)

Tactic:
@isPiSystem_image_Iio αᵒᵈ _ s

Premises used: Set.Ioi, setOf, isPiSystem_image_Iio, OrderDual
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
⊢ IsPiSystem.{u_1} (α := α) (range Ioi)

Tactic:
@image_univ α _ Ioi ▸ isPiSystem_image_Ioi univ

Premises used: Set.image_univ, Set.univ, isPiSystem_image_Ioi, Eq.rec
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Iic a ∩ Iic b ∈ Iic '' s

Tactic:
⟨a ⊓ b, inf_ind a b ha hb, Iic_inter_Iic.symm⟩

Premises used: Set.Mem, setOf, Set.Iic_inter_Iic, And.intro, Exists.intro, Set.image, Eq.symm, Min.min, inf_ind
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Iic a ∩ Iic b ∈ Iic '' s

Tactic:
exact ⟨a ⊓ b, inf_ind a b ha hb, Iic_inter_Iic.symm⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
⊢ IsPiSystem.{u_1} (α := α) (range Iic)

Tactic:
@image_univ α _ Iic ▸ isPiSystem_image_Iic univ

Premises used: isPiSystem_image_Iic, Set.image_univ, Set.univ, Eq.rec
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
⊢ IsPiSystem (Ici '' s)

Tactic:
@isPiSystem_image_Iic αᵒᵈ _ s

Premises used: isPiSystem_image_Iic, Set.Ici, setOf, OrderDual
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
⊢ IsPiSystem.{u_1} (α := α) (range Ici)

Tactic:
@image_univ α _ Ici ▸ isPiSystem_image_Ici univ

Premises used: Set.image_univ, Set.univ, Eq.rec, isPiSystem_image_Ici
-- Module: Mathlib.MeasureTheory.PiSystem
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₂
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₂))
⊢ (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₂)

Tactic:
simp only [Hi]
-- Module: Mathlib.MeasureTheory.PiSystem
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 (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:
fun H => ⟨l₁ ⊔ l₂, sup_ind l₁ l₂ hls₁ hls₂, u₁ ⊓ u₂, inf_ind u₁ u₂ hut₁ hut₂, Hne H, rfl⟩

Premises used: Set.Mem, setOf, Max.max, And.intro, Exists.intro, sup_ind, Min.min, rfl, inf_ind
-- Module: Mathlib.MeasureTheory.PiSystem
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 (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:
exact fun H => ⟨l₁ ⊔ l₂, sup_ind l₁ l₂ hls₁ hls₂, u₁ ⊓ u₂, inf_ind u₁ u₂ hut₁ hut₂, Hne H, rfl⟩
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
ι : Sort u_3
ι' : Sort u_4
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₂)
f : ι → α
g : ι' → α
⊢ IsPiSystem.{u_1} (α := α) {S : Set α | ∃ (i : ι) (j : ι'), p (f i) (g j) ∧ Ixx (f i) (g j) = S}

Tactic:
simpa only [exists_range_iff] using isPiSystem_Ixx_mem (@Hne) (@Hi) (range f) (range g)

Premises used: isPiSystem_Ixx_mem, Set.exists_range_iff, Set.range
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
⊢ IsPiSystem.{u_1} (α := α) {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ioo l u = S}

Tactic:
isPiSystem_Ixx_mem (Ixx := Ioo) (fun ⟨_, hax, hxb⟩ => hax.trans hxb) Ioo_inter_Ioo s t

Premises used: isPiSystem_Ixx_mem, Set.Ioo_inter_Ioo
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
ι : Sort u_3
ι' : Sort u_4
inst : LinearOrder α
f : ι → α
g : ι' → α
⊢ IsPiSystem.{u_1} (α := α) {S : Set α | ∃ (l : ι) (u : ι'), f l < g u ∧ Ioo (f l) (g u) = S}

Tactic:
isPiSystem_Ixx (Ixx := Ioo) (fun ⟨_, hax, hxb⟩ => hax.trans hxb) Ioo_inter_Ioo f g

Premises used: isPiSystem_Ixx, Set.Ioo_inter_Ioo
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
⊢ IsPiSystem.{u_1} (α := α) {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ioc l u = S}

Tactic:
isPiSystem_Ixx_mem (Ixx := Ioc) (fun ⟨_, hax, hxb⟩ => hax.trans_le hxb) Ioc_inter_Ioc s t

Premises used: setOf, Set.Ioc_inter_Ioc, isPiSystem_Ixx_mem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
ι : Sort u_3
ι' : Sort u_4
inst : LinearOrder α
f : ι → α
g : ι' → α
⊢ IsPiSystem.{u_1} (α := α) {S : Set α | ∃ (i : ι) (j : ι'), f i < g j ∧ Ioc (f i) (g j) = S}

Tactic:
isPiSystem_Ixx (Ixx := Ioc) (fun ⟨_, hax, hxb⟩ => hax.trans_le hxb) Ioc_inter_Ioc f g

Premises used: isPiSystem_Ixx, setOf, Set.Ioc_inter_Ioc
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
⊢ IsPiSystem.{u_1} (α := α) {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S}

Tactic:
isPiSystem_Ixx_mem (Ixx := Ico) (fun ⟨_, hax, hxb⟩ => hax.trans_lt hxb) Ico_inter_Ico s t

Premises used: Set.Ico_inter_Ico, isPiSystem_Ixx_mem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
ι : Sort u_3
ι' : Sort u_4
inst : LinearOrder α
f : ι → α
g : ι' → α
⊢ IsPiSystem.{u_1} (α := α) {S : Set α | ∃ (i : ι) (j : ι'), f i < g j ∧ Ico (f i) (g j) = S}

Tactic:
isPiSystem_Ixx (Ixx := Ico) (fun ⟨_, hax, hxb⟩ => hax.trans_lt hxb) Ico_inter_Ico f g

Premises used: isPiSystem_Ixx, Set.Ico_inter_Ico
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
a₁ b₁ a₂ b₂ : α
⊢ Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (max a₁ a₂) (min b₁ b₂)

Tactic:
Icc_inter_Icc

Premises used: Set.Icc_inter_Icc
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
⊢ ∀ {a₁ b₁ a₂ b₂ : α}, Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (max a₁ a₂) (min b₁ b₂)

Tactic:
exact Icc_inter_Icc

Premises used: Set.Icc_inter_Icc
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
ι : Sort u_3
ι' : Sort u_4
inst : LinearOrder α
f : ι → α
g : ι' → α
a₁ b₁ a₂ b₂ : α
⊢ Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (max a₁ a₂) (min b₁ b₂)

Tactic:
Icc_inter_Icc

Premises used: Set.Icc_inter_Icc
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
ι : Sort u_3
ι' : Sort u_4
inst : LinearOrder α
f : ι → α
g : ι' → α
⊢ ∀ {a₁ b₁ a₂ b₂ : α}, Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (max a₁ a₂) (min b₁ b₂)

Tactic:
exact Icc_inter_Icc

Premises used: Set.Icc_inter_Icc
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
⊢ IsPiSystem (generatePiSystem S)

Tactic:
fun _ h_s _ h_t h_nonempty => generatePiSystem.inter h_s h_t h_nonempty

Premises used: Set.Mem, IsPiSystem, generatePiSystem.inter
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
⊢ S ⊆ generatePiSystem S

Tactic:
fun _ =>
  generatePiSystem.base

Premises used: Set.Mem, generatePiSystem.base, Set.Subset
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s : Set α
h_s : s ∈ S
⊢ s ∈ S

Tactic:
h_s
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s : Set α
h_s : s ∈ S
⊢ s ∈ S

Tactic:
exact h_s
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s t : Set α
h_s_1 : generatePiSystem S s
h_t : generatePiSystem S t
h_nonempty : (s ∩ t).Nonempty
h_s : s ∈ S
h_u : t ∈ S
⊢ s ∩ t ∈ S

Tactic:
h_S _ h_s _ h_u h_nonempty
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s t : Set α
h_s_1 : generatePiSystem S s
h_t : generatePiSystem S t
h_nonempty : (s ∩ t).Nonempty
h_s : s ∈ S
h_u : t ∈ S
⊢ s ∩ t ∈ S

Tactic:
exact h_S _ h_s _ h_u h_nonempty
-- Module: Mathlib.MeasureTheory.PiSystem
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
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
⊢ x ∈ 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
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
⊢ generatePiSystem S = S

Tactic:
Set.Subset.antisymm (generatePiSystem_subset_self h_pi) (subset_generatePiSystem_self S)

Premises used: Set.Subset.antisymm, generatePiSystem_subset_self, subset_generatePiSystem_self
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s : Set α
h_s : s ∈ S
⊢ s ∈ generatePiSystem T

Tactic:
generatePiSystem.base (Set.mem_of_subset_of_mem hST h_s)

Premises used: Set.Mem, generatePiSystem.base, Set.mem_of_subset_of_mem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s : Set α
h_s : s ∈ S
⊢ s ∈ generatePiSystem T

Tactic:
exact generatePiSystem.base (Set.mem_of_subset_of_mem hST h_s)

Premises used: generatePiSystem.base, Set.mem_of_subset_of_mem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s t_1 : Set α
h_s_1 : generatePiSystem S s
h_t : generatePiSystem S t_1
h_nonempty : (s ∩ t_1).Nonempty
h_s : s ∈ generatePiSystem T
h_u : t_1 ∈ generatePiSystem T
⊢ s ∩ t_1 ∈ generatePiSystem T

Tactic:
isPiSystem_generatePiSystem T _ h_s _ h_u h_nonempty

Premises used: isPiSystem_generatePiSystem
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s t_1 : Set α
h_s_1 : generatePiSystem S s
h_t : generatePiSystem S t_1
h_nonempty : (s ∩ t_1).Nonempty
h_s : s ∈ generatePiSystem T
h_u : t_1 ∈ generatePiSystem T
⊢ s ∩ t_1 ∈ generatePiSystem T

Tactic:
exact isPiSystem_generatePiSystem T _ h_s _ h_u h_nonempty

Premises used: isPiSystem_generatePiSystem
-- Module: Mathlib.MeasureTheory.PiSystem
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
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
⊢ 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
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ s ∈ S, MeasurableSet s
t s : Set α
h_s : s ∈ S
⊢ MeasurableSet s

Tactic:
apply h_meas_S _ h_s
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ s ∈ S, MeasurableSet s
t s t_1 : Set α
h_s_1 : generatePiSystem S s
h_t : generatePiSystem S t_1
h_nonempty : (s ∩ t_1).Nonempty
h_s : MeasurableSet s
h_u : MeasurableSet t_1
⊢ MeasurableSet (s ∩ t_1)

Tactic:
apply MeasurableSet.inter h_s h_u

Premises used: MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.PiSystem
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
inter :
  ∀ {s t : Set α},
    generatePiSystem S s →
      generatePiSystem S t → (s ∩ t).Nonempty → ∀ (h_s : MeasurableSet s) (h_u : MeasurableSet t), MeasurableSet (s ∩ t)
⊢ MeasurableSet 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
-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_1
g : Set (Set α)
t : Set α
ht : t ∈ generatePiSystem g
⊢ MeasurableSet t

Tactic:
@generatePiSystem_measurableSet α (generateFrom g) g
    (fun _ h_s_in_g => measurableSet_generateFrom h_s_in_g) t ht

Premises used: generatePiSystem_measurableSet, MeasurableSpace.measurableSet_generateFrom