awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ (i : ℕ), s i) ⋯
s u : Set α
h : u ∈ C
⊢ p u ⋯

Tactic:
hC _ ‹_› _
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ (i : ℕ), s i) ⋯
s : Set α
⊢ p ∅ ⋯

Tactic:
empty
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ (i : ℕ), s i) ⋯
s t : Set α
h : GenerateMeasurable C t
a_ih : p t h
⊢ p tᶜ ⋯

Tactic:
compl _ ‹_› ‹_›
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ (i : ℕ), s i) ⋯
s : Set α
f : ℕ → Set α
h : ∀ (n : ℕ), GenerateMeasurable C (f n)
a_ih : ∀ (n : ℕ), p (f n) ⋯
⊢ p (⋃ (i : ℕ), f i) ⋯

Tactic:
iUnion ‹_› ‹_› ‹_›
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
C : Set (Set α)
p : (s : Set α) → MeasurableSet s → Prop
hC : ∀ t ∈ C, ∀ (ht : MeasurableSet t), p t ht
empty : p ∅ ⋯
compl : ∀ (t : Set α) (ht : MeasurableSet t), p t ht → p tᶜ ⋯
iUnion : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)), (∀ (n : ℕ), p (s n) ⋯) → p (⋃ (i : ℕ), s i) ⋯
s u : Set α
h : u ∈ C
⊢ p u ⋯

Tactic:
exacts [hC _ ‹_› _, empty, compl _ ‹_› ‹_›, iUnion ‹_› ‹_› ‹_›]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
s : Set (Set α)
m : MeasurableSpace α
h : ∀ t ∈ s, MeasurableSet t
⊢ generateFrom s ≤ m

Tactic:
fun t (ht : GenerateMeasurable s t) =>
  ht.recOn h .empty (fun _ _ => .compl) fun _ _ hf => .iUnion hf

Premises used: MeasurableSet, MeasurableSpace.GenerateMeasurable.recOn
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
s : Set (Set α)
m : MeasurableSpace α
⊢ generateFrom s ≤ m ↔ s ⊆ {t : Set α | MeasurableSet t}

Tactic:
Iff.intro (fun h _ hu => h _ <| measurableSet_generateFrom hu) fun h => generateFrom_le h

Premises used: MeasurableSpace.measurableSet_generateFrom, Iff.intro, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ generateFrom {s : Set α | MeasurableSet s} = inst

Tactic:
le_antisymm (generateFrom_le fun _ => id) fun _ h => measurableSet_generateFrom h

Premises used: MeasurableSpace.measurableSet_generateFrom, id, le_antisymm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
S : Set (Set α)
x y : α
⊢ (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) ↔ ∀ s ∈ S, x ∈ s ↔ y ∈ s

Tactic:
⟨fun H s hs ↦ H s (.basic s hs), fun H s ↦ ?_⟩

Premises used: MeasurableSpace.GenerateMeasurable.basic, Iff.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
S : Set (Set α)
x y : α
refine : ∀ (H : ∀ s ∈ S, x ∈ s ↔ y ∈ s) (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) ↔ ∀ s ∈ S, x ∈ s ↔ y ∈ s

Tactic:
refine ⟨fun H s hs ↦ H s (.basic s hs), fun H s ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
hC : ∀ t ∈ S, ∀ (ht : MeasurableSet t), x ∈ t ↔ y ∈ t
empty : Membership.mem (γ := Set α) ∅ x ↔ Membership.mem (γ := Set α) ∅ y
compl : ∀ (t : Set α) (ht : MeasurableSet t), (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)
iUnion :
  ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)),
    (∀ (n : ℕ), x ∈ s n ↔ y ∈ s n) →
      (Membership.mem (γ := Set α) (⋃ (i : ℕ), s i) x ↔ Membership.mem (γ := Set α) (⋃ (i : ℕ), s i) y)
⊢ MeasurableSet s → (x ∈ s ↔ y ∈ s)

Tactic:
apply generateFrom_induction
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ t ∈ S, ∀ (ht : MeasurableSet t), x ∈ t ↔ y ∈ t

Tactic:
fun s hs _ ↦ H s hs
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ t ∈ S, ∀ (ht : MeasurableSet t), x ∈ t ↔ y ∈ t

Tactic:
exact fun s hs _ ↦ H s hs
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ Membership.mem (γ := Set α) ∅ x ↔ Membership.mem (γ := Set α) ∅ y

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ (t : Set α) (ht : MeasurableSet t), (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)

Tactic:
fun _ _ ↦ Iff.not

Premises used: Set.Mem, setOf, Iff.not, Not
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ (t : Set α) (ht : MeasurableSet t), (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)

Tactic:
exact fun _ _ ↦ Iff.not

Premises used: Iff.not
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
f : ℕ → Set α
iUnion :
  (∀ (n : ℕ), MeasurableSet (f n)) →
    (∀ (n : ℕ), x ∈ f n ↔ y ∈ f n) →
      (Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x ↔ Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) y)
⊢ ∀ (hs : ∀ (n : ℕ), MeasurableSet (f n)),
    (∀ (n : ℕ), x ∈ f n ↔ y ∈ f n) →
      (Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x ↔ Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) y)

Tactic:
_
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
f : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), x ∈ f n ↔ y ∈ f n
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) x ↔ Membership.mem (γ := Set α) (⋃ (i : ℕ), f i) y

Tactic:
simp only [mem_iUnion, hf]

Premises used: Set.mem_iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
s : Set (Set α)
hs : {t : Set α | MeasurableSet t} = s
⊢ MeasurableSpace.mkOfClosure s hs = generateFrom s

Tactic:
copy_eq _

Premises used: MeasurableSpace.copy_eq
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
s t : Set (Set α)
h : s ⊆ t
⊢ generateFrom s ≤ generateFrom t

Tactic:
giGenerateFrom.gc.monotone_l h

Premises used: MeasurableSpace.giGenerateFrom, GaloisConnection.monotone_l, GaloisInsertion.gc
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
s t : Set (Set α)
⊢ generateFrom s ⊔ generateFrom t = generateFrom (s ∪ t)

Tactic:
(@giGenerateFrom α).gc.l_sup.symm

Premises used: MeasurableSpace.giGenerateFrom, GaloisConnection.l_sup, Eq.symm, GaloisInsertion.gc
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_6
s : ι → Set (Set α)
⊢ Eq.{u_1 + 1} (α := MeasurableSpace α) (⨆ (i : ι), generateFrom (s i)) (generateFrom (⋃ (i : ι), s i))

Tactic:
(@MeasurableSpace.giGenerateFrom α).gc.l_iSup.symm

Premises used: GaloisConnection.l_iSup, MeasurableSpace.giGenerateFrom, Eq.symm, Set.iUnion, GaloisInsertion.gc
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
⊢ ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → MeasurableSet t

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
⊢ ∀ (t : Set α), Membership.mem (γ := Set (Set α)) {∅} t → MeasurableSet t

Tactic:
simp [@MeasurableSet.empty α ⊥]

Premises used: MeasurableSet.empty
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
⊢ ∀ (t : Set α), Membership.mem (γ := Set (Set α)) {univ} t → MeasurableSet t

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
S : Set (Set α)
rw : generateFrom ({univ} ∪ S) = generateFrom S
rw₁ : generateFrom {univ} ⊔ generateFrom S = generateFrom S
rw₂ : ⊥ ⊔ generateFrom S = generateFrom S
rw₃ rw₄ : generateFrom S = generateFrom S
⊢ generateFrom (insert univ S) = generateFrom S

Tactic:
rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_univ, bot_sup_eq]

Premises used: Set.insert_eq, MeasurableSpace.generateFrom_sup_generateFrom, bot_sup_eq, MeasurableSpace.generateFrom_singleton_univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
S : Set (Set α)
rw : generateFrom ({∅} ∪ S) = generateFrom S
rw₁ : generateFrom {∅} ⊔ generateFrom S = generateFrom S
rw₂ : ⊥ ⊔ generateFrom S = generateFrom S
rw₃ rw₄ : generateFrom S = generateFrom S
⊢ generateFrom (insert ∅ S) = generateFrom S

Tactic:
rw [insert_eq, ← generateFrom_sup_generateFrom, generateFrom_singleton_empty, bot_sup_eq]

Premises used: Set.insert_eq, MeasurableSpace.generateFrom_sup_generateFrom, bot_sup_eq, MeasurableSpace.generateFrom_singleton_empty
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
s : Set α
⊢ ∀ (s : Set α), s = ∅ ∨ s = univ → sᶜ = ∅ ∨ sᶜ = univ

Tactic:
simp +contextual [or_imp]

Premises used: or_imp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
s : Set α
⊢ MeasurableSet s

Tactic:
trivial

Premises used: trivial, MeasurableSet, Set.Mem, Set.univ, setOf
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m₂ m₁ : MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s

Tactic:
Iff.rfl

Premises used: MeasurableSet, Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ms : Set (MeasurableSpace α)
s : Set α
⊢ Membership.mem (γ := Set (Set α)) (⋂₀ ((fun (m : MeasurableSpace α) ↦ {t : Set α | MeasurableSet t}) '' ms)) s ↔
    ∀ m ∈ ms, MeasurableSet s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
rw : MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s
rw₁ : (∀ m_1 ∈ range m, MeasurableSet s) ↔ ∀ (i : ι), MeasurableSet s
rw₂ rw₃ : (∀ (i : ι), MeasurableSet s) ↔ ∀ (i : ι), MeasurableSet s
⊢ MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s

Tactic:
rw [iInf, measurableSet_sInf, forall_mem_range]

Premises used: iInf, Set.forall_mem_range, MeasurableSpace.measurableSet_sInf
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
m₁ m₂ : MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ GenerateMeasurable {s : Set α | MeasurableSet s ∨ MeasurableSet s} s

Tactic:
Iff.rfl

Premises used: Set.union, MeasurableSet, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ms : Set (MeasurableSpace α)
s : Set α
⊢ GenerateMeasurable (⋃₀ ((fun (m : MeasurableSpace α) ↦ {t : Set α | MeasurableSet t}) '' ms)) s ↔
    GenerateMeasurable {s : Set α | ∃ m ∈ ms, MeasurableSet s} s

Tactic:
simp [← setOf_exists]

Premises used: Set.setOf_exists
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ GenerateMeasurable {s : Set α | ∃ (i : ι), MeasurableSet s} s

Tactic:
simp only [measurableSet_sSup, exists_range_iff]

Premises used: MeasurableSpace.measurableSet_sSup, Set.exists_range_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
h : ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s
⊢ Eq.{u_1 + 1} (α := MeasurableSpace α) (⨆ (n : ι), m n) (generateFrom {s : Set α | ∃ (n : ι), MeasurableSet s})

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
h : GenerateMeasurable {s : Set α | ∃ (i : ι), MeasurableSet s} s ↔ MeasurableSet s
⊢ MeasurableSet s ↔ MeasurableSet s

Tactic:
rw [measurableSet_iSup]

Premises used: MeasurableSpace.measurableSet_iSup
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ GenerateMeasurable {s : Set α | ∃ (i : ι), MeasurableSet s} s ↔ MeasurableSet s

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := MeasurableSpace α) (generateFrom (⋃ (n : ι), {t : Set α | MeasurableSet t})) (⨆ (n : ι), m n)

Tactic:
(@giGenerateFrom α).l_iSup_u m

Premises used: MeasurableSpace.giGenerateFrom, GaloisInsertion.l_iSup_u, Set.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
x : MeasurableSpace α
⊢ Measurable.{u_1, u_1} (α := α) id

Tactic:
fun _ => id

Premises used: Set.Mem, Measurable, setOf, id, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
x : MeasurableSpace α
⊢ Measurable (β := α) fun (a : α) ↦ a

Tactic:
measurable_id

Premises used: measurable_id
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : MeasurableSpace α
x_1 : MeasurableSpace β
x_2 : MeasurableSpace γ
g : β → γ
f : α → β
hg : Measurable g
hf : Measurable f
⊢ Measurable (g ∘ f)

Tactic:
fun _ h => hf (hg h)

Premises used: Set.Mem, Measurable, setOf, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
x_1 : MeasurableSpace β
a : α
⊢ Measurable.{u_2, u_1} (β := α) fun (x : β) ↦ a

Tactic:
fun s _ => .const (a ∈ s)

Premises used: Set.Mem, Measurable, setOf, Membership.mem, MeasurableSet.const, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
β : Type u_2
α : Type u_7
m m0 : MeasurableSpace α
x : MeasurableSpace β
hm : m ≤ m0
f : α → β
hf : Measurable f
⊢ Measurable f

Tactic:
fun _ hs => hm _ (hf hs)

Premises used: Measurable, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
⊢ DiscreteMeasurableSpace α

Tactic:
@DiscreteMeasurableSpace.mk _ (_) fun _ ↦ MeasurableSpace.measurableSet_top

Premises used: DiscreteMeasurableSpace.mk, MeasurableSpace.measurableSet_top
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : DiscreteMeasurableSpace α
s : Set α
⊢ MeasurableSet s

Tactic:
DiscreteMeasurableSpace.forall_measurableSet _

Premises used: DiscreteMeasurableSpace.forall_measurableSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Defs
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : DiscreteMeasurableSpace α
f : α → β
⊢ Measurable f

Tactic:
fun _ _ ↦ .of_discrete

Premises used: MeasurableSet.of_discrete, Measurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
h : MeasurableSet (f '' s)
⊢ MeasurableSet s

Tactic:
simpa only [hf.injective.preimage_image] using hf.measurable h

Premises used: MeasurableEmbedding.injective, Function.Injective.preimage_image, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs rwa rwa₁ rwa₂ rwa₃ : MeasurableSet s
⊢ MeasurableSet (_root_.id '' s)

Tactic:
rwa [image_id]

Premises used: Set.image_id
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
rwa : MeasurableSet (g '' f '' s)
rwa₁ : MeasurableSet (f '' s)
rwa₂ rwa₃ rwa₄ rwa₅ : MeasurableSet s
⊢ MeasurableSet (g ∘ f '' s)

Tactic:
rwa [image_comp, hg.measurableSet_image, hf.measurableSet_image]

Premises used: MeasurableEmbedding.measurableSet_image, Set.image_comp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
rw : MeasurableSet (f '' univ)
⊢ MeasurableSet (range f)

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
⊢ MeasurableSet (f '' univ)

Tactic:
hf.measurableSet_image' MeasurableSet.univ

Premises used: MeasurableEmbedding.measurableSet_image', MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
⊢ MeasurableSet (f '' univ)

Tactic:
exact hf.measurableSet_image' MeasurableSet.univ

Premises used: MeasurableEmbedding.measurableSet_image', MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set β
rw : MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (f '' f ⁻¹' s)
rw₁ rw₂ : MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (f ⁻¹' s)
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)

Tactic:
rw [← image_preimage_eq_inter_range, hf.measurableSet_image]

Premises used: MeasurableEmbedding.measurableSet_image, Set.image_preimage_eq_inter_range
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
rwa : MeasurableSet (rangeFactorization f '' s)
rwa₁ : MeasurableSet (Subtype.val (p := fun (x : β) ↦ x ∈ range f) '' rangeFactorization f '' s)
rwa₂ : MeasurableSet (Subtype.val (p := fun (x : β) ↦ x ∈ range f) ∘ rangeFactorization f '' s)
rwa₃ : MeasurableSet (f '' s)
rwa₄ rwa₅ rwa₆ rwa₇ : MeasurableSet s
⊢ MeasurableSet (rangeSplitting f ⁻¹' s)

Tactic:
rwa [preimage_rangeSplitting hf.injective,
    ← (subtype_coe hf.measurableSet_range).measurableSet_image, ← image_comp,
    coe_comp_rangeFactorization, hf.measurableSet_image]

Premises used: MeasurableEmbedding.measurableSet_image, Set.coe_comp_rangeFactorization, MeasurableEmbedding.injective, MeasurableEmbedding.measurableSet_range, Set.image_comp, Set.preimage_rangeSplitting, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (extend f g g')

Tactic:
measurable_of_restrict_of_restrict_compl hf.measurableSet_range ?_ ?_

Premises used: MeasurableEmbedding.measurableSet_range, measurable_of_restrict_of_restrict_compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
refine_1 : Measurable ((range f).restrict (π := fun (a : β) ↦ γ) (extend f g g'))
refine_2 : Measurable ((range f)ᶜ.restrict (π := fun (a : β) ↦ γ) (extend f g g'))
⊢ Measurable (extend f g g')

Tactic:
refine measurable_of_restrict_of_restrict_compl hf.measurableSet_range ?_ ?_

Premises used: MeasurableEmbedding.measurableSet_range, measurable_of_restrict_of_restrict_compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
refine_1 :
  Measurable.{u_2, u_3} (β := γ) fun (x : (↑(range f) : Type u_2)) ↦
    g (Exists.choose (p := fun (y : α) ↦ f y = (↑x : β)) ⋯)
⊢ Measurable ((range f).restrict (π := fun (a : β) ↦ γ) (extend f g g'))

Tactic:
rw [restrict_extend_range]

Premises used: Set.restrict_extend_range
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable.{u_2, u_3} (β := γ) fun (x : (↑(range f) : Type u_2)) ↦
    g (Exists.choose (p := fun (y : α) ↦ f y = (↑x : β)) ⋯)

Tactic:
simpa only [rangeSplitting] using hg.comp hf.measurable_rangeSplitting

Premises used: Measurable.comp, MeasurableEmbedding.measurable_rangeSplitting, Set.rangeSplitting
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
refine_2 : Measurable (α := (↑(range f)ᶜ : Type u_2)) (g' ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (range f)ᶜ))
⊢ Measurable ((range f)ᶜ.restrict (π := fun (a : β) ↦ γ) (extend f g g'))

Tactic:
rw [restrict_extend_compl_range]

Premises used: Set.restrict_extend_compl_range
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (α := (↑(range f)ᶜ : Type u_2)) (g' ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (range f)ᶜ))

Tactic:
hg'.comp measurable_subtype_coe

Premises used: measurable_subtype_coe, Measurable.comp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (α := (↑(range f)ᶜ : Type u_2)) (g' ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (range f)ᶜ))

Tactic:
exact hg'.comp measurable_subtype_coe

Premises used: measurable_subtype_coe, Measurable.comp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
hg : Measurable g
hne : ∀ (a : β), Nonempty γ
⊢ ∃ (g' : β → γ), Measurable g' ∧ g' ∘ f = g

Tactic:
⟨extend f g fun x => Classical.choice (hne x),
    hf.measurable_extend hg (measurable_const' fun _ _ => rfl),
    funext fun _ => hf.injective.extend_apply _ _ _⟩

Premises used: Classical.choice, Function.Injective.extend_apply, measurable_const', funext, Function.extend, MeasurableEmbedding.injective, And.intro, Exists.intro, MeasurableEmbedding.measurable_extend, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
⊢ Measurable (g ∘ f) ↔ Measurable f

Tactic:
⟨fun H => ?_, hg.measurable.comp⟩

Premises used: Measurable.comp, Iff.intro, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
refine : ∀ (H : Measurable (g ∘ f)), Measurable f
⊢ Measurable (g ∘ f) ↔ Measurable f

Tactic:
refine ⟨fun H => ?_, hg.measurable.comp⟩