awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s : Set (Set α)
inst : Nonempty.{u1 + 1} (↑s : Type u1)
inst_1 : ∀ (t : (↑s : Type u1)), Small.{u, u1} (↑(↑t : Set α) : Type u1)
⊢ Small.{u, u1} (↑(⋂₀ s) : Type u1)

Tactic:
let ⟨t⟩ : Nonempty s := inferInstance
  small_sInter t.prop

Premises used: inferInstance, Set.Elem, small_sInter, Subtype.prop, _private.0.small_sInter'.match_1, Set.sInter, Small
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
ι : Type u4
s : Set ι
i : ι
hi : i ∈ s
f : (i : ι) → i ∈ s → Set α
inst : Small.{u, u1} (↑(f i hi) : Type u1)
⊢ Small.{u, u1} (↑(⋂ (i : ι), ⋂ (hi : i ∈ s), f i hi) : Type u1)

Tactic:
Set.biInter_eq_iInter s f ▸ small_iInter _ ⟨i, hi⟩

Premises used: Set.biInter_eq_iInter, Eq.rec, Subtype.mk, Eq.symm, small_iInter
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s : Set ι
inst : Nonempty.{u4 + 1} (↑s : Type u4)
f : (i : ι) → i ∈ s → Set α
inst_1 : ∀ (i : ι) (hi : i ∈ s), Small.{u, u1} (↑(f i hi) : Type u1)
⊢ Small.{u, u1} (↑(⋂ (i : ι), ⋂ (hi : i ∈ s), f i hi) : Type u1)

Tactic:
let ⟨t⟩ : Nonempty s := inferInstance
  small_biInter t.prop f

Premises used: small_biInter, Set.iInter, inferInstance, Set.Elem, Subtype.prop, _private.0.small_biInter'.match_1, Small
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
⊢ Small.{u, u1} (↑∅ : Type u1)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
x : α
⊢ Small.{u, u1} (↑{x} : Type u1)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
x y : α
⊢ Small.{u, u1} (↑{x, y} : Type u1)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u
⊢ Nonempty.{max 1 u} (Unique α) ↔ ∃! x : α, True

Tactic:
⟨fun ⟨u⟩ ↦ ⟨u.default, trivial, fun a _ ↦ u.uniq a⟩,
   fun ⟨a, _, h⟩ ↦ ⟨⟨⟨a⟩, fun _ ↦ h _ trivial⟩⟩⟩

Premises used: Inhabited.default, trivial, Unique.mk, Unique, _private.0.unique_iff_existsUnique.match_2, Nonempty.intro, ExistsUnique, _private.0.unique_iff_existsUnique.match_1, And.intro, True, Iff.intro, Exists.intro, Unique.uniq, Nonempty, Inhabited.mk
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
p : α → Prop
h : ∃! a : α, p a
a : α
ha : (fun (a : α) ↦ p a) a
he : ∀ (y : α), (fun (a : α) ↦ p a) y → y = a
x : Subtype p
b : α
hb : p b
e_val : b = a
⊢ Eq.{max 1 u_1} (Subtype.mk (p := p) b hb) default.{max 1 u_1}

Tactic:
congr
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
p : α → Prop
h : ∃! a : α, p a
a : α
ha : (fun (a : α) ↦ p a) a
he : ∀ (y : α), (fun (a : α) ↦ p a) y → y = a
x : Subtype p
b : α
hb : p b
⊢ b = a

Tactic:
he b hb
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
p : α → Prop
h : ∃! a : α, p a
a : α
ha : (fun (a : α) ↦ p a) a
he : ∀ (y : α), (fun (a : α) ↦ p a) y → y = a
x : Subtype p
b : α
hb : p b
⊢ b = a

Tactic:
exact he b hb
-- Module: Mathlib.Logic.Unique
Goal:
⊢ default = unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
inst : Unique α
a : α
⊢ a = default

Tactic:
uniq _ a

Premises used: Unique.uniq
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
inst : Unique α
a : α
⊢ default = a

Tactic:
(uniq _ a).symm

Premises used: Unique.uniq, Eq.symm
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
inst : Unique α
⊢ Subsingleton α

Tactic:
subsingleton_of_forall_eq _ eq_default

Premises used: subsingleton_of_forall_eq, Unique.eq_default
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
inst : Unique α
p : α → Prop
h : p default
x : α
rwa rwa₁ rwa₂ rwa₃ : p default
⊢ p x

Tactic:
rwa [Unique.eq_default x]

Premises used: Unique.eq_default
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
inst : Unique α
p : α → Prop
⊢ Exists p ↔ p default

Tactic:
⟨fun ⟨a, ha⟩ ↦ eq_default a ▸ ha, Exists.intro default⟩

Premises used: Inhabited.default, _private.0.Unique.exists_iff.match_1, Eq.rec, Unique.eq_default, Iff.intro, Exists.intro
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq : ∀ (a : α), a = default
e_toInhabited : x = y
⊢ Eq.{max 1 u_1} { default := x, uniq := h : Unique α } { default := y, uniq := uniq }

Tactic:
congr
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq : ∀ (a : α), a = default
e_toInhabited : default = y
e_toInhabited₁ e_toInhabited₂ : Eq.{u_1} (α := α) default default
⊢ x = y

Tactic:
rw [h x, h y]
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
⊢ Subsingleton.{max 1 u_1} (Unique α)

Tactic:
⟨Unique.subsingleton_unique'⟩

Premises used: Unique.subsingleton_unique', Subsingleton.intro
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u
inst : Subsingleton α
inst_1 : Nonempty α
inhabit : ∀ (inhabited_h : Inhabited α), Nonempty.{max 1 u} (Unique α)
⊢ Nonempty.{max 1 u} (Unique α)

Tactic:
inhabit α
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u
inst : Subsingleton α
inst_1 : Nonempty α
inhabited_h : Inhabited α
⊢ Nonempty.{max 1 u} (Unique α)

Tactic:
⟨Unique.mk' α⟩

Premises used: Nonempty.intro, Unique.mk'
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u
inst : Subsingleton α
inst_1 : Nonempty α
inhabited_h : Inhabited α
⊢ Nonempty.{max 1 u} (Unique α)

Tactic:
exact ⟨Unique.mk' α⟩
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u
h : Nonempty.{max 1 u} (Unique α)
u : Unique α
left : Subsingleton α
right : Nonempty α
⊢ Subsingleton α ∧ Nonempty α

Tactic:
constructor
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u
h : Nonempty.{max 1 u} (Unique α)
u : Unique α
⊢ Subsingleton α

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u
h : Nonempty.{max 1 u} (Unique α)
u : Unique α
⊢ Subsingleton α

Tactic:
exact inferInstance
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u
h : Nonempty.{max 1 u} (Unique α)
u : Unique α
⊢ Nonempty α

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u
h : Nonempty.{max 1 u} (Unique α)
u : Unique α
⊢ Nonempty α

Tactic:
exact inferInstance
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
β : α → Sort v
inst : (a : α) → Inhabited.{v} (β a)
⊢ Eq (α := (a : α) → β a) default fun (a : α) ↦ default

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
β : α → Sort v
inst : (a : α) → Inhabited.{v} (β a)
a : α
⊢ Eq.{v} (α := β a) (default a) default

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
β : Sort u_2
inst : Subsingleton α
f : α → β
a : α
⊢ f = Function.const α (f a)

Tactic:
funext fun x ↦ Subsingleton.elim x a ▸ rfl

Premises used: Eq.rec, funext, Subsingleton.elim, rfl
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
β : Sort u_2
inst : Unique α
f : α → β
⊢ f = Function.const α (f default)

Tactic:
eq_const_of_subsingleton ..

Premises used: eq_const_of_subsingleton
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
inst : Unique α
β : α → Sort v
f : (a : α) → β a
i x : α
h : i ≍ x
rw : HEq (α := β default) (f default) (β := β default) (Function.const α (f default) x)
⊢ HEq (f i) (β := β default) (Function.const α (f default) x)

Tactic:
rw [Subsingleton.elim i default]

Premises used: Inhabited.default, Subsingleton.elim
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
inst : Unique α
β : α → Sort v
f : (a : α) → β a
i x : α
h : i ≍ x
⊢ HEq (α := β default) (f default) (β := β default) (Function.const α (f default) x)

Tactic:
rfl
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
hf : Injective f
inst : Subsingleton β
⊢ Subsingleton α

Tactic:
⟨fun _ _ ↦ hf <| Subsingleton.elim _ _⟩

Premises used: Subsingleton.intro, Subsingleton.elim
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
inst : Subsingleton α
hf : Surjective f
⊢ Subsingleton β

Tactic:
⟨hf.forall₂.2 fun x y ↦ congr_arg f <| Subsingleton.elim x y⟩

Premises used: Iff.mpr, congr_arg, Subsingleton.intro, Subsingleton.elim, Function.Surjective.forall₂
-- Module: Mathlib.Logic.Unique
Goal:
α_1 : Sort u_1
ι : Sort u_2
α : ι → Sort u_3
inst : Unique ι
x : α default
i : ι
rw : α default
⊢ α i

Tactic:
rw [Unique.eq_default i]

Premises used: Unique.eq_default
-- Module: Mathlib.Logic.Unique
Goal:
α_1 : Sort u_1
ι : Sort u_2
α : ι → Sort u_3
inst : Unique ι
x : α default
i : ι
⊢ α default

Tactic:
exact x
-- Module: Mathlib.Logic.Unique
Goal:
ι : Sort u_2
α : ι → Sort u_3
x_1 : Unique ι
x : α default
⊢ uniqueElim (α := α) x default = x

Tactic:
rfl

Premises used: Eq.mpr, uniqueElim, rfl
-- Module: Mathlib.Logic.Unique
Goal:
ι : Sort u_2
β : Sort u_4
x_1 : Unique ι
x : β
i : ι
⊢ uniqueElim (α := fun (x : ι) ↦ β) x i = x

Tactic:
rfl

Premises used: Eq.mpr, uniqueElim, rfl
-- Module: Mathlib.Logic.Unique
Goal:
A : Sort u_2
B : Sort u_3
inst : Unique A
inst_1 : Unique B
f : A → B
rw : ∃ (g : B → A), Function.LeftInverse g f ∧ Function.RightInverse g f
⊢ Function.Bijective f

Tactic:
rw [Function.bijective_iff_has_inverse]

Premises used: Function.bijective_iff_has_inverse
-- Module: Mathlib.Logic.Unique
Goal:
A : Sort u_2
B : Sort u_3
inst : Unique A
inst_1 : Unique B
f : A → B
⊢ ∃ (g : B → A), Function.LeftInverse g f ∧ Function.RightInverse g f

Tactic:
⟨default, ?_, ?_⟩

Premises used: Inhabited.default, And.intro, Exists.intro
-- Module: Mathlib.Logic.Unique
Goal:
A : Sort u_2
B : Sort u_3
inst : Unique A
inst_1 : Unique B
f : A → B
refine_1 : Function.LeftInverse default f
refine_2 : Function.RightInverse default f
⊢ ∃ (g : B → A), Function.LeftInverse g f ∧ Function.RightInverse g f

Tactic:
refine ⟨default, ?_, ?_⟩
-- Module: Mathlib.Logic.Unique
Goal:
A : Sort u_2
B : Sort u_3
inst : Unique A
inst_1 : Unique B
f : A → B
x : A
⊢ default (f x) = x

Tactic:
simp
-- Module: Mathlib.Logic.Unique
Goal:
A : Sort u_2
B : Sort u_3
inst : Unique A
inst_1 : Unique B
f : A → B
x : B
⊢ f (default x) = x

Tactic:
simp
-- Module: Mathlib.Logic.Unique
Goal:
α : Type u
⊢ Subsingleton.{u + 1} (Option α) ↔ IsEmpty α

Tactic:
⟨fun h ↦ ⟨fun x ↦ Option.noConfusion rfl (heq_of_eq (@Subsingleton.elim _ h x none))⟩,
   fun h ↦ ⟨fun x y ↦
     Option.casesOn x (Option.casesOn y rfl fun x ↦ h.elim x) fun x ↦ h.elim x⟩⟩

Premises used: Option.noConfusion, Option.casesOn, Option.some, IsEmpty.mk, Option.none, heq_of_eq, Subsingleton.intro, Iff.intro, Subsingleton.elim, rfl
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
y : α
x_1 : { x : α // x = y }
x : α
hx : x = y
⊢ Eq.{max 1 u_1} (Subtype.mk (p := fun (x : α) ↦ x = y) x hx) (Subtype.mk (p := fun (x : α) ↦ x = y) y ⋯)

Tactic:
congr
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
y : α
x_1 : { x : α // y = x }
x : α
hx : y = x
subst : Eq.{max 1 u_1} (Subtype.mk (p := fun (x : α) ↦ y = x) y ⋯) (Subtype.mk (p := fun (x : α) ↦ y = x) y ⋯)
⊢ Eq.{max 1 u_1} (Subtype.mk (p := fun (x : α) ↦ y = x) x hx) (Subtype.mk (p := fun (x : α) ↦ y = x) y ⋯)

Tactic:
subst hx
-- Module: Mathlib.Logic.Unique
Goal:
α : Sort u_1
y : α
x : { x : α // y = x }
⊢ Eq.{max 1 u_1} (Subtype.mk (p := fun (x : α) ↦ y = x) y ⋯) (Subtype.mk (p := fun (x : α) ↦ y = x) y ⋯)

Tactic:
congr
-- Module: Mathlib.Logic.UnivLE
Goal:
α : Type w
hα : Small.{u, w} α
h : UnivLE.{u, v}
⊢ Small.{v, w} α

Tactic:
let ⟨β, ⟨f⟩⟩ := hα.equiv_small
  let ⟨_, ⟨g⟩⟩ := (h.small β).equiv_small
  ⟨_, ⟨f.trans g⟩⟩

Premises used: Equiv.trans, Small.equiv_small, _private.0.Small.trans_univLE.match_1, _private.0.Small.trans_univLE.match_2, Small.mk, Nonempty.intro, Exists.intro, Small
-- Module: Mathlib.Logic.UnivLE
Goal:
⊢ UnivLE.{u, u}

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, UnivLE.mk
-- Module: Mathlib.Logic.UnivLE
Goal:
⊢ UnivLE.{0, u}

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, UnivLE.mk
-- Module: Mathlib.Logic.UnivLE
Goal:
inst : UnivLE.{u, v}
⊢ UnivLE.{u, v + 1}

Tactic:
@UnivLE.trans _ ⟨inferInstance⟩

Premises used: UnivLE.trans
-- Module: Mathlib.Logic.UnivLE
Goal:
inst : UnivLE.{max u v, v}
⊢ UnivLE.{u, v}

Tactic:
@UnivLE.trans univLE_max ‹_›

Premises used: UnivLE.trans
-- Module: Mathlib.Logic.UnivLE
Goal:
⊢ UnivLE.{v, max v u}

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.UnivLE
Goal:
⊢ UnivLE.{v, max u v}

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.UnivLE
Goal:
⊢ UnivLE.{u, max v u}

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.UnivLE
Goal:
⊢ UnivLE.{u, max u v}

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.UnivLE
Goal:
⊢ UnivLE.{u, u + 1}

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.UnivLE
Goal:
⊢ UnivLE.{2, 5}

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.UnivLE
Goal:
simp : ∃ (x : Type (u + 1)), ∀ (x_1 : Type u), ¬Nonempty.{u + 2} (x ≃ x_1)
⊢ ¬UnivLE.{u + 1, u}

Tactic:
simp only [univLE_iff, small_iff, not_forall, not_exists]

Premises used: not_exists, univLE_iff, small_iff, Classical.not_forall
-- Module: Mathlib.Logic.UnivLE
Goal:
⊢ ∃ (x : Type (u + 1)), ∀ (x_1 : Type u), ¬Nonempty.{u + 2} (x ≃ x_1)

Tactic:
⟨Type u, fun α => fun ⟨f⟩ => Function.not_surjective_Type.{u, u} f.symm f.symm.surjective⟩

Premises used: False, _private.0._example.match_4, Function.not_surjective_Type, Exists.intro, Equiv.surjective, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Logic.UnivLE
Goal:
⊢ ∃ (x : Type (u + 1)), ∀ (x_1 : Type u), ¬Nonempty.{u + 2} (x ≃ x_1)

Tactic:
exact ⟨Type u, fun α => fun ⟨f⟩ => Function.not_surjective_Type.{u, u} f.symm f.symm.surjective⟩
-- Module: Mathlib.MeasureTheory.Category.MeasCat
Goal:
X : Type u
inst : MeasurableSpace X
⊢ { carrier := X, str := inst : MeasCat.{u} }.carrier = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Category.MeasCat
Goal:
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
hf : Measurable (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x
hg : Measurable (β := ℝ≥0∞) fun (m : MeasureTheory.Measure ℝ≥0∞) ↦ ∫⁻ (x : ℝ≥0∞), x ∂m
rw : AEMeasurable (β := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ x) μ.join
⊢ ∫⁻ (x : ℝ≥0∞), x ∂μ.join =
    ∫⁻ (x : ℝ≥0∞), x ∂Measure.map (fun (m : MeasureTheory.Measure ℝ≥0∞) ↦ ∫⁻ (x : ℝ≥0∞), x ∂m) μ

Tactic:
rw [Measure.lintegral_join, lintegral_map]

Premises used: MeasureTheory.lintegral_map, MeasureTheory.Measure.lintegral_join
-- Module: Mathlib.MeasureTheory.Category.MeasCat
Goal:
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x

Tactic:
apply_rules [Measurable.aemeasurable, measurable_id, Measure.measurable_lintegral]

Premises used: Measurable.aemeasurable, measurable_id, MeasureTheory.Measure.measurable_lintegral
-- Module: Mathlib.MeasureTheory.Category.MeasCat
Goal:
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (m : MeasureTheory.Measure ℝ≥0∞) ↦ ∫⁻ (x : ℝ≥0∞), x ∂m

Tactic:
apply_rules [Measurable.aemeasurable, measurable_id, Measure.measurable_lintegral]

Premises used: Measurable.aemeasurable, measurable_id, MeasureTheory.Measure.measurable_lintegral
-- Module: Mathlib.MeasureTheory.Category.MeasCat
Goal:
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ x) μ.join

Tactic:
apply_rules [Measurable.aemeasurable, measurable_id, Measure.measurable_lintegral]

Premises used: Measurable.aemeasurable, measurable_id, MeasureTheory.Measure.measurable_lintegral
-- Module: Mathlib.MeasureTheory.Constructions.AddChar
Goal:
A : Type u_1
M : Type u_2
inst : AddMonoid A
inst_1 : Monoid M
inst_2 : MeasurableSpace A
inst_3 : MeasurableSpace M
inst_4 : DiscreteMeasurableSpace A
inst_5 : Finite A
⊢ DiscreteMeasurableSpace (AddChar A M)

Tactic:
⟨fun _ ↦ trivial⟩

Premises used: trivial, DiscreteMeasurableSpace.mk
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
⊢ Antitone (@borel α)

Tactic:
fun _ _ h =>
  MeasurableSpace.generateFrom_le fun _ hs => .basic _ (h _ hs)

Premises used: MeasurableSpace.GenerateMeasurable.basic, Antitone, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
⊢ borel α = ⊤

Tactic:
top_le_iff.1 fun s _ => GenerateMeasurable.basic s (isOpen_discrete s)

Premises used: MeasurableSpace.GenerateMeasurable.basic, isOpen_discrete, top_le_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : TopologicalSpace.IsOpen u
⊢ TopologicalSpace.IsOpen u

Tactic:
rw [hs] at hu
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u_1 u : Set α
hu : u ∈ s
⊢ MeasurableSet u

Tactic:
GenerateMeasurable.basic u hu

Premises used: MeasurableSet, MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u_1 u : Set α
hu : u ∈ s
⊢ MeasurableSet u

Tactic:
exact GenerateMeasurable.basic u hu

Premises used: MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
⊢ MeasurableSet.{u_1} (α := α) univ

Tactic:
@MeasurableSet.univ α (generateFrom s)

Premises used: MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
⊢ MeasurableSet.{u_1} (α := α) univ

Tactic:
exact @MeasurableSet.univ α (generateFrom s)

Premises used: MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u s₁ s₂ : Set α
h : GenerateOpen s s₁
h_1 : GenerateOpen s s₂
hs₁ : MeasurableSet s₁
hs₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∩ s₂)

Tactic:
@MeasurableSet.inter α (generateFrom s) _ _ hs₁ hs₂

Premises used: MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u s₁ s₂ : Set α
h : GenerateOpen s s₁
h_1 : GenerateOpen s s₂
hs₁ : MeasurableSet s₁
hs₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∩ s₂)

Tactic:
exact @MeasurableSet.inter α (generateFrom s) _ _ hs₁ hs₂

Premises used: MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
rwa rwa₁ rwa₂ rwa₃ : ∀ s_1 ∈ f, IsOpen[TopologicalSpace.generateFrom s] s_1
⊢ ∀ s ∈ f, IsOpen[t] s

Tactic:
rwa [hs]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
sUnion : ∀ (v : Set (Set α)) (hv : v.Countable) (vf : v ⊆ f) (vu : ⋃₀ v = ⋃₀ f), MeasurableSet (⋃₀ f)
⊢ MeasurableSet (⋃₀ f)

Tactic:
rcases isOpen_sUnion_countable f (by rwa [hs]) with ⟨v, hv, vf, vu⟩

Premises used: TopologicalSpace.isOpen_sUnion_countable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
v : Set (Set α)
hv : v.Countable
vf : v ⊆ f
vu : ⋃₀ v = ⋃₀ f
sUnion : MeasurableSet (⋃₀ v)
⊢ MeasurableSet (⋃₀ f)

Tactic:
rw [← vu]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
v : Set (Set α)
hv : v.Countable
vf : v ⊆ f
vu : ⋃₀ v = ⋃₀ f
⊢ MeasurableSet (⋃₀ v)

Tactic:
@MeasurableSet.sUnion α (generateFrom s) _ hv fun x xv => ih _ (vf xv)

Premises used: MeasurableSet.sUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
v : Set (Set α)
hv : v.Countable
vf : v ⊆ f
vu : ⋃₀ v = ⋃₀ f
⊢ MeasurableSet (⋃₀ v)

Tactic:
exact @MeasurableSet.sUnion α (generateFrom s) _ hv fun x xv => ih _ (vf xv)

Premises used: MeasurableSet.sUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : TopologicalSpace.IsOpen u
basic : ∀ (u : Set α) (hu : u ∈ s), MeasurableSet u
univ : MeasurableSet.{u_1} (α := α) Set.univ
inter :
  ∀ (s₁ s₂ : Set α),
    GenerateOpen s s₁ → GenerateOpen s s₂ → ∀ (hs₁ : MeasurableSet s₁) (hs₂ : MeasurableSet s₂), MeasurableSet (s₁ ∩ s₂)
sUnion :
  ∀ (f : Set (Set α)) (hf : ∀ s_1 ∈ f, GenerateOpen s s_1) (ih : ∀ s_1 ∈ f, MeasurableSet s_1), MeasurableSet (⋃₀ f)
⊢ MeasurableSet u

Tactic:
induction hu with
      | basic u hu => exact GenerateMeasurable.basic u hu
      | univ => exact @MeasurableSet.univ α (generateFrom s)
      | inter s₁ s₂ _ _ hs₁ hs₂ => exact @MeasurableSet.inter α (generateFrom s) _ _ hs₁ hs₂
      | sUnion f hf ih =>
        rcases isOpen_sUnion_countable f (by rwa [hs]) with ⟨v, hv, vf, vu⟩
        rw [← vu]
        exact @MeasurableSet.sUnion α (generateFrom s) _ hv fun x xv => ih _ (vf xv)

Premises used: Set.univ, Set.sUnion, MeasurableSpace.GenerateMeasurable.basic, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : u ∈ s
rw : TopologicalSpace.IsOpen u
⊢ TopologicalSpace.IsOpen u

Tactic:
rw [hs]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : u ∈ s
⊢ TopologicalSpace.IsOpen u

Tactic:
GenerateOpen.basic _ hu

Premises used: TopologicalSpace.GenerateOpen.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : u ∈ s
⊢ TopologicalSpace.IsOpen u

Tactic:
exact GenerateOpen.basic _ hu

Premises used: TopologicalSpace.GenerateOpen.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
s : Set (Set α)
hs : IsTopologicalBasis s
⊢ borel α = MeasurableSpace.generateFrom s

Tactic:
borel_eq_generateFrom_of_subbasis hs.eq_generateFrom

Premises used: borel_eq_generateFrom_of_subbasis, TopologicalSpace.IsTopologicalBasis.eq_generateFrom
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsPiSystem.{u_1} (α := α) {s : Set α | IsOpen[inst] s}

Tactic:
fun _s hs _t ht _ => IsOpen.inter hs ht

Premises used: Set.Mem, setOf, IsPiSystem, IsOpen.inter, IsOpen
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsPiSystem.{u_1} (α := α) {s : Set α | IsClosed[inst] s}

Tactic:
fun _s hs _t ht _ ↦ IsClosed.inter hs ht

Premises used: Set.Mem, setOf, IsPiSystem, IsClosed.inter