awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i)
hem :
  MeasurePreserving (α := ℝ × (Fin n → ℝ)) (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) volume
    volume
heπ :
  preimage (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π) =
    SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)
refine :
  ∀ θ ∈ Icc 0 (2 * π),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 fun (x : Fin n) ↦ 2 * π))
        fun (y : Fin n → ℝ) ↦
        HSMul.hSMul (α := ℂ)
          (∏ i : Fin (n + 1),
            (↑(R i) : ℂ) * cexp ((↑((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (θ, y) i) : ℂ) * I) * I)
          (f (torusMap c R ((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (θ, y))))) =
      HSMul.hSMul (β := E) (deriv (circleMap (c i) (R i)) θ)
        (∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove),
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℂ) (circleMap (c i) (R i) θ) y))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (x : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 fun (x : Fin n) ↦ 2 * π))
        fun (y : Fin n → ℝ) ↦
        HSMul.hSMul (α := ℂ)
          (∏ i : Fin (n + 1),
            (↑(R i) : ℂ) * cexp ((↑((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (x, y) i) : ℂ) * I) * I)
          (f (torusMap c R ((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (x, y)))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (θ : ℝ) ↦
      HSMul.hSMul (β := E) (deriv (circleMap (c i) (R i)) θ)
        (∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove),
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℂ) (circleMap (c i) (R i) θ) y)))

Tactic:
refine setIntegral_congr_fun measurableSet_Icc fun θ _ => ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Icc
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i)
hem :
  MeasurePreserving (α := ℝ × (Fin n → ℝ)) (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) volume
    volume
heπ :
  preimage (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π) =
    SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)
θ : ℝ
h : θ ∈ Icc 0 (2 * π)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 fun (x : Fin n) ↦ 2 * π))
      fun (y : Fin n → ℝ) ↦
      ((↑(R i) : ℂ) *
              cexp
                ((↑(((MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i) :
                            ℝ × ((j : Fin n) → ℝ) ≃ᵐ ((j : Fin (n + 1)) → ℝ)) :
                          (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ)
                        (θ, y) i) :
                    ℂ) *
                  I) *
            I *
          ∏ i_1 : Fin n,
            (↑(R (i.succAbove i_1)) : ℂ) *
                cexp
                  ((↑(((MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i) :
                              ℝ × ((j : Fin n) → ℝ) ≃ᵐ ((j : Fin (n + 1)) → ℝ)) :
                            (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ)
                          (θ, y) (i.succAbove i_1)) :
                      ℂ) *
                    I) *
              I) •
        f fun (i_1 : Fin (n + 1)) ↦
          c i_1 +
            (↑(R i_1) : ℂ) *
              cexp
                ((↑(((MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i) :
                            ℝ × ((j : Fin n) → ℝ) ≃ᵐ ((j : Fin (n + 1)) → ℝ)) :
                          (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ)
                        (θ, y) i_1) :
                    ℂ) *
                  I))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 fun (x : Fin n) ↦ 2 * π))
      fun (a : Fin n → ℝ) ↦
      ((↑(R i) : ℂ) * cexp ((↑θ : ℂ) * I) * I *
          ∏ i_1 : Fin n, (↑((R ∘ i.succAbove) i_1) : ℂ) * cexp ((↑(a i_1) : ℂ) * I) * I) •
        f
          (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℂ) (circleMap (c i) (R i) θ) fun (i_1 : Fin n) ↦
            (c ∘ i.succAbove) i_1 + (↑((R ∘ i.succAbove) i_1) : ℂ) * cexp ((↑(a i_1) : ℂ) * I)))

Tactic:
setIntegral_congr_fun measurableSet_Icc fun Θ _ => ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Icc
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i)
hem :
  MeasurePreserving (α := ℝ × (Fin n → ℝ)) (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) volume
    volume
heπ :
  preimage (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π) =
    SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)
θ : ℝ
h : θ ∈ Icc 0 (2 * π)
Θ : Fin n → ℝ
h_1 : Membership.mem (γ := Set (Fin n → ℝ)) (Icc 0 fun (x : Fin n) ↦ 2 * π) Θ
e_a :
  Eq (α := Fin (n + 1) → ℂ)
    (fun (i_1 : Fin (n + 1)) ↦
      c i_1 + (↑(R i_1) : ℂ) * cexp ((↑(i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) θ Θ i_1) : ℂ) * I))
    (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℂ) (circleMap (c i) (R i) θ) fun (i_1 : Fin n) ↦
      c (i.succAbove i_1) + (↑(R (i.succAbove i_1)) : ℂ) * cexp ((↑(Θ i_1) : ℂ) * I))
⊢ (((↑(R i) : ℂ) * cexp ((↑θ : ℂ) * I) * I * ∏ x : Fin n, (↑(R (i.succAbove x)) : ℂ) * cexp ((↑(Θ x) : ℂ) * I) * I) •
      f fun (i_1 : Fin (n + 1)) ↦
        c i_1 + (↑(R i_1) : ℂ) * cexp ((↑(i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) θ Θ i_1) : ℂ) * I)) =
    ((↑(R i) : ℂ) * cexp ((↑θ : ℂ) * I) * I * ∏ x : Fin n, (↑(R (i.succAbove x)) : ℂ) * cexp ((↑(Θ x) : ℂ) * I) * I) •
      f
        (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℂ) (circleMap (c i) (R i) θ) fun (i_1 : Fin n) ↦
          c (i.succAbove i_1) + (↑(R (i.succAbove i_1)) : ℂ) * cexp ((↑(Θ i_1) : ℂ) * I))

Tactic:
congr 2
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i)
hem :
  MeasurePreserving (α := ℝ × (Fin n → ℝ)) (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) volume
    volume
heπ :
  preimage (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π) =
    SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)
θ : ℝ
h : θ ∈ Icc 0 (2 * π)
Θ : Fin n → ℝ
h_1 : Membership.mem (γ := Set (Fin n → ℝ)) (Icc 0 fun (x : Fin n) ↦ 2 * π) Θ
⊢ Eq (α := Fin (n + 1) → ℂ)
    (fun (i_1 : Fin (n + 1)) ↦
      c i_1 + (↑(R i_1) : ℂ) * cexp ((↑(i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) θ Θ i_1) : ℂ) * I))
    (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℂ) (circleMap (c i) (R i) θ) fun (i_1 : Fin n) ↦
      c (i.succAbove i_1) + (↑(R (i.succAbove i_1)) : ℂ) * cexp ((↑(Θ i_1) : ℂ) * I))

Tactic:
simp only [funext_iff, i.forall_iff_succAbove, circleMap, Fin.insertNth_apply_same,
      Fin.insertNth_apply_succAbove, imp_true_iff, and_self_iff]

Premises used: Fin.insertNth_apply_succAbove, funext_iff, circleMap, imp_true_iff, Fin.insertNth_apply_same, and_self_iff, Fin.forall_iff_succAbove
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i)
hem :
  MeasurePreserving (α := ℝ × (Fin n → ℝ)) (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) volume
    volume
heπ :
  preimage (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π) =
    SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (θ : Fin (n + 1) → ℝ) ↦
      HSMul.hSMul (α := ℂ) (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ)))
    (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π) volume

Tactic:
have := hf.function_integrable
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
⊢ Eq.{u_1 + 1} (α := E) (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x)
    (∮ (x : ℂ) in C(c 0, R 0),
      ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succ, R ∘ Fin.succ), f (Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℂ) x y))

Tactic:
simpa using torusIntegral_succAbove hf 0

Premises used: OfNat.ofNat, torusIntegral_succAbove
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort uι
s : Set α
m_1 m₁ m₂ : MeasurableSpace α
m' : MeasurableSpace β
f_1 : α → β
g : β → α
f_2 : α → β
m : MeasurableSpace α
f : ℕ → Set β
hf : ∀ (i : ℕ), MeasurableSet (f_2 ⁻¹' f i)
⊢ MeasurableSet (f_2 ⁻¹' ⋃ (i : ℕ), f i)

Tactic:
simpa only [preimage_iUnion] using m.measurableSet_iUnion _ hf

Premises used: MeasurableSpace.measurableSet_iUnion, Set.preimage_iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : α → β
s : Set β
⊢ MeasurableSet s ↔ MeasurableSet (f ⁻¹' s)

Tactic:
Iff.rfl

Premises used: MeasurableSet, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
⊢ MeasurableSpace.map id m = m

Tactic:
MeasurableSpace.ext fun _ => Iff.rfl

Premises used: Iff.rfl, MeasurableSpace.ext
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
f : α → β
g : β → γ
⊢ MeasurableSpace.map g (MeasurableSpace.map f m) = MeasurableSpace.map (g ∘ f) m

Tactic:
MeasurableSpace.ext fun _ => Iff.rfl

Premises used: Iff.rfl, MeasurableSpace.ext
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort uι
s_1 : Set α
m_1 m₁ m₂ : MeasurableSpace α
m' : MeasurableSpace β
f_1 : α → β
g : β → α
f : α → β
m : MeasurableSpace β
s : ℕ → Set α
hs : ∀ (i : ℕ), ∃ (s' : Set β), MeasurableSet s' ∧ f ⁻¹' s' = s i
s' : (x : ℕ) → Set β
hs' : ∀ (x : ℕ), MeasurableSet (s' x) ∧ f ⁻¹' s' x = s x
⊢ f ⁻¹' ⋃ (i : ℕ), s' i = ⋃ (i : ℕ), s i

Tactic:
simp [hs']
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
m : MeasurableSpace β
⊢ MeasurableSet s ↔ ∃ (s' : Set β), MeasurableSet s' ∧ f ⁻¹' s' = s

Tactic:
.rfl

Premises used: MeasurableSet, Iff.rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
f : α → β
⊢ MeasurableSpace.comap f m = generateFrom {t : Set α | ∃ (s : Set β), MeasurableSet s ∧ f ⁻¹' s = t}

Tactic:
(@generateFrom_measurableSet _ (.comap f m)).symm

Premises used: MeasurableSet, setOf, MeasurableSpace.generateFrom_measurableSet, Eq.symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
⊢ MeasurableSpace.comap id m = m

Tactic:
MeasurableSpace.ext fun s => ⟨fun ⟨_, hs', h⟩ => h ▸ hs', fun h => ⟨s, h, rfl⟩⟩

Premises used: MeasurableSet, Eq.rec, _private.0.MeasurableSpace.comap_id.match_1, And.intro, Iff.intro, Exists.intro, MeasurableSpace.ext, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
f : β → α
g : γ → β
⊢ MeasurableSpace.comap g (MeasurableSpace.comap f m) = MeasurableSpace.comap (f ∘ g) m

Tactic:
MeasurableSpace.ext fun _ =>
    ⟨fun ⟨_, ⟨u, h, hu⟩, ht⟩ => ⟨u, h, ht ▸ hu ▸ rfl⟩, fun ⟨t, h, ht⟩ => ⟨f ⁻¹' t, ⟨_, h, rfl⟩, ht⟩⟩

Premises used: MeasurableSet, _private.0.MeasurableSpace.comap_comp.match_2, Eq.rec, _private.0.MeasurableSpace.comap_comp.match_1, Set.preimage, And.intro, Iff.intro, Exists.intro, MeasurableSpace.ext, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
m' : MeasurableSpace β
f : α → β
⊢ MeasurableSpace.comap f m' ≤ m ↔ m' ≤ MeasurableSpace.map f m

Tactic:
⟨fun h _s hs => h _ ⟨_, hs, rfl⟩, fun h _s ⟨_t, ht, heq⟩ => heq ▸ h _ ht⟩

Premises used: MeasurableSet, Eq.rec, _private.0.MeasurableSpace.comap_le_iff_le_map.match_1, Set.preimage, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ GaloisConnection (MeasurableSpace.comap f) (MeasurableSpace.map f)

Tactic:
fun _ _ =>
  comap_le_iff_le_map

Premises used: MeasurableSpace.comap_le_iff_le_map, GaloisConnection
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m₁ m₂ : MeasurableSpace α
f : α → β
h : m₁ ≤ m₂
⊢ MeasurableSpace.map f m₁ ≤ MeasurableSpace.map f m₂

Tactic:
(gc_comap_map f).monotone_u h

Premises used: GaloisConnection.monotone_u, MeasurableSpace.gc_comap_map
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Monotone (MeasurableSpace.map f)

Tactic:
fun _ _ => map_mono

Premises used: MeasurableSpace.map_mono, Monotone
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m₁ m₂ : MeasurableSpace α
g : β → α
h : m₁ ≤ m₂
⊢ MeasurableSpace.comap g m₁ ≤ MeasurableSpace.comap g m₂

Tactic:
(gc_comap_map g).monotone_l h

Premises used: MeasurableSpace.gc_comap_map, GaloisConnection.monotone_l
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
g : β → α
⊢ Monotone (MeasurableSpace.comap g)

Tactic:
fun _ _ h => comap_mono h

Premises used: MeasurableSpace.comap_mono, Monotone
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
g : β → α
⊢ MeasurableSpace.comap g ⊥ = ⊥

Tactic:
(gc_comap_map g).l_bot

Premises used: MeasurableSpace.gc_comap_map, GaloisConnection.l_bot
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m₁ m₂ : MeasurableSpace α
g : β → α
⊢ MeasurableSpace.comap g (m₁ ⊔ m₂) = MeasurableSpace.comap g m₁ ⊔ MeasurableSpace.comap g m₂

Tactic:
(gc_comap_map g).l_sup

Premises used: MeasurableSpace.gc_comap_map, GaloisConnection.l_sup
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort uι
g : β → α
m : ι → MeasurableSpace α
⊢ MeasurableSpace.comap g (⨆ (i : ι), m i) = ⨆ (i : ι), MeasurableSpace.comap g (m i)

Tactic:
(gc_comap_map g).l_iSup

Premises used: GaloisConnection.l_iSup, MeasurableSpace.gc_comap_map
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ MeasurableSpace.map f ⊤ = ⊤

Tactic:
(gc_comap_map f).u_top

Premises used: GaloisConnection.u_top, MeasurableSpace.gc_comap_map
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m₁ m₂ : MeasurableSpace α
f : α → β
⊢ MeasurableSpace.map f (m₁ ⊓ m₂) = MeasurableSpace.map f m₁ ⊓ MeasurableSpace.map f m₂

Tactic:
(gc_comap_map f).u_inf

Premises used: MeasurableSpace.gc_comap_map, GaloisConnection.u_inf
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort uι
f : α → β
m : ι → MeasurableSpace α
⊢ MeasurableSpace.map f (⨅ (i : ι), m i) = ⨅ (i : ι), MeasurableSpace.map f (m i)

Tactic:
(gc_comap_map f).u_iInf

Premises used: GaloisConnection.u_iInf, MeasurableSpace.gc_comap_map
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : α → β
⊢ MeasurableSpace.comap f (MeasurableSpace.map f m) ≤ m

Tactic:
(gc_comap_map f).l_u_le _

Premises used: MeasurableSpace.gc_comap_map, GaloisConnection.l_u_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
g : β → α
⊢ m ≤ MeasurableSpace.map g (MeasurableSpace.comap g m)

Tactic:
(gc_comap_map g).le_u_l _

Premises used: GaloisConnection.le_u_l, MeasurableSpace.gc_comap_map
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
h : MeasurableSet s
rw : MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
⊢ MeasurableSet s

Tactic:
rw [map_def]

Premises used: MeasurableSpace.map_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
h : MeasurableSet s
pos : ∀ (h : b ∈ s), MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
neg : ∀ (h : b ∉ s), MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
⊢ MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)

Tactic:
by_cases h : b ∈ s
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
h_1 : MeasurableSet s
h : b ∈ s
⊢ MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
h_1 : MeasurableSet s
h : b ∉ s
⊢ MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
pos : b ∈ s → MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
neg : b ∉ s → MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)
⊢ MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)

Tactic:
by_cases b ∈ s
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
h : b ∈ s
⊢ MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
h : b ∉ s
⊢ MeasurableSet.{u_1} (α := α) ((fun (_a : α) ↦ b) ⁻¹' s)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
⊢ MeasurableSpace.comap f (generateFrom s) = generateFrom (preimage f '' s)

Tactic:
le_antisymm
    (comap_le_iff_le_map.2 <|
      generateFrom_le fun _t hts => GenerateMeasurable.basic _ <| mem_image_of_mem _ <| hts)
    (generateFrom_le fun _t ⟨u, hu, Eq⟩ => Eq ▸ ⟨u, GenerateMeasurable.basic _ hu, rfl⟩)

Premises used: Iff.mpr, MeasurableSet, Eq.rec, MeasurableSpace.GenerateMeasurable.basic, le_antisymm, Set.preimage, Set.mem_image_of_mem, And.intro, Exists.intro, MeasurableSpace.comap_le_iff_le_map, rfl, MeasurableSpace.generateFrom_le, _private.0.MeasurableSpace.comap_generateFrom.match_1
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m₁ : MeasurableSpace α
m₂ : MeasurableSpace β
f : α → β
⊢ Measurable f ↔ m₂ ≤ MeasurableSpace.map f m₁

Tactic:
Iff.rfl

Premises used: MeasurableSet, Iff.rfl, Measurable, setOf, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m₁ : MeasurableSpace α
m₂ : MeasurableSpace β
f : α → β
⊢ Measurable f ↔ MeasurableSpace.comap f m₂ ≤ m₁

Tactic:
comap_le_iff_le_map.symm

Premises used: MeasurableSet, Measurable, setOf, Set.preimage, MeasurableSpace.comap_le_iff_le_map, Iff.symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
f : α → β
⊢ Measurable f

Tactic:
fun s hs => ⟨s, hs, rfl⟩

Premises used: MeasurableSet, Measurable, And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
f : α → β
g : β → γ
⊢ Measurable f ↔ Measurable (g ∘ f)

Tactic:
simp [measurable_iff_comap_le]

Premises used: measurable_iff_comap_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
ma ma' : MeasurableSpace α
mb mb' : MeasurableSpace β
f : α → β
hf : Measurable f
ha : ma ≤ ma'
hb : mb' ≤ mb
⊢ Measurable f

Tactic:
fun _t ht => ha _ <| hf <| hb _ ht

Premises used: Measurable, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort uι
mα : ι → MeasurableSpace α
x : MeasurableSpace β
f : α → β
i₀ : ι
h : Measurable f
⊢ Measurable f

Tactic:
h.mono (le_iSup mα i₀) le_rfl

Premises used: le_rfl, le_iSup, Measurable.mono
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
mα mα' : MeasurableSpace α
x : MeasurableSpace β
f : α → β
h : Measurable f
⊢ Measurable f

Tactic:
h.mono le_sup_left le_rfl

Premises used: le_rfl, le_sup_left, Measurable.mono
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
mα mα' : MeasurableSpace α
x : MeasurableSpace β
f : α → β
h : Measurable f
⊢ Measurable f

Tactic:
h.mono le_sup_right le_rfl

Premises used: le_rfl, le_sup_right, Measurable.mono
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
m mα : MeasurableSpace α
hm : m ≤ mα
⊢ Measurable.{u_1, u_1} (α := α) id

Tactic:
measurable_id.mono le_rfl hm

Premises used: le_rfl, measurable_id, Measurable.mono
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace β
f : α → β
⊢ Measurable f

Tactic:
fun _ _ => trivial

Premises used: trivial, MeasurableSet, Set.Mem, Set.univ, Measurable, setOf
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
s : Set (Set β)
f : α → β
h : ∀ t ∈ s, MeasurableSet (f ⁻¹' t)
⊢ Measurable f

Tactic:
Measurable.of_le_map <| generateFrom_le h

Premises used: Measurable.of_le_map, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
t : Set α
ht : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) s : Set (Set α)) t
rcases : ∀ (P : Finset (Set α)) (hP : P.Nonempty) (PC : (↑P : Set (Set α)) ⊆ s), MeasurableSet (P.sup' hP id)
⊢ MeasurableSet t

Tactic:
rcases ht with ⟨P, hP, PC, rfl⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
P : Finset (Set α)
hP : P.Nonempty
PC : (↑P : Set (Set α)) ⊆ s
rw : MeasurableSet (⋃₀ (↑P : Set (Set α)))
⊢ MeasurableSet (P.sup' hP id)

Tactic:
rw [Finset.sup'_eq_sup, Finset.sup_id_set_eq_sUnion]

Premises used: Finset.sup'_eq_sup, Finset.sup_id_set_eq_sUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Basic
Goal:
α : Type u_1
s : Set (Set α)
P : Finset (Set α)
hP : P.Nonempty
PC : (↑P : Set (Set α)) ⊆ s
⊢ MeasurableSet (⋃₀ (↑P : Set (Set α)))

Tactic:
MeasurableSet.sUnion (Finset.countable_toSet P)
    (fun s hs ↦ measurableSet_generateFrom (PC hs))

Premises used: MeasurableSet.sUnion, MeasurableSpace.measurableSet_generateFrom, Finset.countable_toSet