mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
x✝ : Ω
⊢ x✝ ∈ ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E ↔ x✝ ∈ E

Tactic:
;

Goal state after:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
x✝ : Ω
⊢ x✝ ∈ ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E ↔ x✝ ∈ E
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) 1, continuous_toFun := ⋯ } a✝ = 1 a✝

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) 1, continuous_toFun := ⋯ } a✝ = 1 a✝
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c₁ c₂ : R
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) (c₁ * c₂), continuous_toFun := ⋯ } a✝ =
    ({ toFun := fun x ↦ (algebraMap R A) c₁, continuous_toFun := ⋯ } *
        { toFun := fun x ↦ (algebraMap R A) c₂, continuous_toFun := ⋯ })
      a✝

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c₁ c₂ : R
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) (c₁ * c₂), continuous_toFun := ⋯ } a✝ =
    ({ toFun := fun x ↦ (algebraMap R A) c₁, continuous_toFun := ⋯ } *
        { toFun := fun x ↦ (algebraMap R A) c₂, continuous_toFun := ⋯ })
      a✝
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) 0, continuous_toFun := ⋯ } a✝ = 0 a✝

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) 0, continuous_toFun := ⋯ } a✝ = 0 a✝
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c₁ c₂ : R
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) (c₁ + c₂), continuous_toFun := ⋯ } a✝ =
    ({ toFun := fun x ↦ (algebraMap R A) c₁, continuous_toFun := ⋯ } +
        { toFun := fun x ↦ (algebraMap R A) c₂, continuous_toFun := ⋯ })
      a✝

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c₁ c₂ : R
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) (c₁ + c₂), continuous_toFun := ⋯ } a✝ =
    ({ toFun := fun x ↦ (algebraMap R A) c₁, continuous_toFun := ⋯ } +
        { toFun := fun x ↦ (algebraMap R A) c₂, continuous_toFun := ⋯ })
      a✝
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c₁ c₂ : R
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) (c₁ + c₂), continuous_toFun := ⋯ } a✝ =
    ({ toFun := fun x ↦ (algebraMap R A) c₁, continuous_toFun := ⋯ } +
        { toFun := fun x ↦ (algebraMap R A) c₂, continuous_toFun := ⋯ })
      a✝

Tactic:
exact (algebraMap R A).map_add _ _

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c : R
f : C(α, A)
x : α
⊢ (C c * f) x = (f * C c) x

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c : R
f : C(α, A)
x : α
⊢ (C c * f) x = (f * C c) x
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c : R
f : C(α, A)
x : α
⊢ (c • f) x = (C c * f) x

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c : R
f : C(α, A)
x : α
⊢ (c • f) x = (C c * f) x
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ univ.pi C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ univ.pi C
hst : (univ.pi fun i ↦ s₁ i ∩ s₂ i).Nonempty
⊢ (univ.pi fun i ↦ s₁ i ∩ s₂ i) ∈ univ.pi '' univ.pi C

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ univ.pi C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ univ.pi C
hst : (univ.pi fun i ↦ s₁ i ∩ s₂ i).Nonempty
⊢ (univ.pi fun i ↦ s₁ i ∩ s₂ i) ∈ univ.pi '' univ.pi C
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ (i : ι), MeasurableSpace.comap (fun b ↦ b i) ((fun i ↦ generateFrom (C i)) i) ≤ generateFrom (univ.pi '' univ.pi C)

Tactic:
;

Goal state after:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ (i : ι), MeasurableSpace.comap (fun b ↦ b i) ((fun i ↦ generateFrom (C i)) i) ≤ generateFrom (univ.pi '' univ.pi C)
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ MeasurableSpace.comap (fun b ↦ b i) ((fun i ↦ generateFrom (C i)) i) ≤ generateFrom (univ.pi '' univ.pi C)

Tactic:
;

Goal state after:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ MeasurableSpace.comap (fun b ↦ b i) ((fun i ↦ generateFrom (C i)) i) ≤ generateFrom (univ.pi '' univ.pi C)
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ ∀ t ∈ (preimage fun b ↦ b i) '' C i, MeasurableSet t

Tactic:
;

Goal state after:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ ∀ t ∈ (preimage fun b ↦ b i) '' C i, MeasurableSet t
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ x✝ ∈ univ.pi (update (fun i' ↦ iUnion (t i')) i (⋃ x, s)) ↔ x✝ ∈ univ.pi fun k ↦ ⋃ j, update (fun i' ↦ t i' j) i s k

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ x✝ ∈ univ.pi (update (fun i' ↦ iUnion (t i')) i (⋃ x, s)) ↔ x✝ ∈ univ.pi fun k ↦ ⋃ j, update (fun i' ↦ t i' j) i s k
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ (∀ (i_1 : ι), x✝ i_1 ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) i_1) ↔
    ∀ (i_1 : ι), x✝ i_1 ∈ ⋃ j, update (fun i' ↦ t i' j) i s i_1

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ (∀ (i_1 : ι), x✝ i_1 ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) i_1) ↔
    ∀ (i_1 : ι), x✝ i_1 ∈ ⋃ j, update (fun i' ↦ t i' j) i s i_1
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ ∀ (a : ι), x✝ a ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) a ↔ x✝ a ∈ ⋃ j, update (fun i' ↦ t i' j) i s a

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ ∀ (a : ι), x✝ a ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) a ↔ x✝ a ∈ ⋃ j, update (fun i' ↦ t i' j) i s a
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ comp id ⋯ (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝) = Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ comp id ⋯ (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝) = Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
i' : ι
s : Set (α i')
hs : s ∈ C i'
⊢ x✝ i' ∈ update (fun i' ↦ iUnion (t i')) i' (⋃ x, s) i' ↔ x✝ i' ∈ ⋃ j, update (fun i' ↦ t i' j) i' s i'

Tactic:
;

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
i' : ι
s : Set (α i')
hs : s ∈ C i'
⊢ x✝ i' ∈ update (fun i' ↦ iUnion (t i')) i' (⋃ x, s) i' ↔ x✝ i' ∈ ⋃ j, update (fun i' ↦ t i' j) i' s i'
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : γ → δ
g' : β → γ
hg : Continuous[inst✝, inst✝²] g
hg' : Continuous[inst✝¹, inst✝] g'
f : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ comp g hg (comp g' hg' (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝)) =
    comp (g ∘ g') ⋯ (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝)

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : γ → δ
g' : β → γ
hg : Continuous[inst✝, inst✝²] g
hg' : Continuous[inst✝¹, inst✝] g'
f : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ comp g hg (comp g' hg' (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝)) =
    comp (g ∘ g') ⋯ (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝)
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
x : α
⊢ ((c₁ * c₂) • f) x = (c₁ • c₂ • f) x

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
x : α
⊢ ((c₁ * c₂) • f) x = (c₁ • c₂ • f) x
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
f : C(α, M)
x : α
⊢ (1 • f) x = f x

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
f : C(α, M)
x : α
⊢ (1 • f) x = f x
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
r : C(α, R)
x : α
⊢ (r • 0) x = 0 x

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
r : C(α, R)
x : α
⊢ (r • 0) x = 0 x
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
c : C(α, R)
f g : C(α, M)
x : α
⊢ (c • (f + g)) x = (c • f + c • g) x

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
c : C(α, R)
f g : C(α, M)
x : α
⊢ (c • (f + g)) x = (c • f + c • g) x
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
x : α
⊢ ((c₁ + c₂) • f) x = (c₁ • f + c₂ • f) x

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
x : α
⊢ ((c₁ + c₂) • f) x = (c₁ • f + c₂ • f) x
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
f : C(α, M)
x : α
⊢ (0 • f) x = 0 x

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
f : C(α, M)
x : α
⊢ (0 • f) x = 0 x
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
this : univ.pi (update (fun i' ↦ iUnion (t i')) i (⋃ x, s)) = univ.pi fun k ↦ ⋃ j, update (fun i' ↦ t i' j) i s k
n : ι → ℕ
⊢ MeasurableSet (univ.pi fun a ↦ update (fun i' ↦ t i' (n a)) i s a)

Tactic:
;

Goal state after:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
this : univ.pi (update (fun i' ↦ iUnion (t i')) i (⋃ x, s)) = univ.pi fun k ↦ ⋃ j, update (fun i' ↦ t i' j) i s k
n : ι → ℕ
⊢ MeasurableSet (univ.pi fun a ↦ update (fun i' ↦ t i' (n a)) i s a)
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ t ∈ univ.pi '' univ.pi C, MeasurableSet t

Tactic:
;

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ t ∈ univ.pi '' univ.pi C, MeasurableSet t
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ univ.pi C
⊢ MeasurableSet (⋂ i, eval i ⁻¹' s i)

Tactic:
;

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ univ.pi C
⊢ MeasurableSet (⋂ i, eval i ⁻¹' s i)
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ univ.pi C
⊢ ∀ (b : ι), MeasurableSet (eval b ⁻¹' s b)

Tactic:
;

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ univ.pi C
⊢ ∀ (b : ι), MeasurableSet (eval b ⁻¹' s b)
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case mk
α : Type u_1
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
ν : Measure β
g : γ → δ
hg : Continuous[inst✝¹, inst✝²] g
f : β →ₘ[ν] γ
φ : α → β
hφ : Measure.QuasiMeasurePreserving φ μ ν
a✝ : { f // AEStronglyMeasurable f ν }
⊢ (comp g hg (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝)).compQuasiMeasurePreserving φ hφ =
    comp g hg (compQuasiMeasurePreserving (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝) φ hφ)

Tactic:
;

Goal state after:
case mk
α : Type u_1
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
ν : Measure β
g : γ → δ
hg : Continuous[inst✝¹, inst✝²] g
f : β →ₘ[ν] γ
φ : α → β
hφ : Measure.QuasiMeasurePreserving φ μ ν
a✝ : { f // AEStronglyMeasurable f ν }
⊢ (comp g hg (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝)).compQuasiMeasurePreserving φ hφ =
    comp g hg (compQuasiMeasurePreserving (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝) φ hφ)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (u a).toReal x
i : α
hi : (u i).toReal ≤ x
⊢ 0 ≤ x

Tactic:
;

Goal state after:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (u a).toReal x
i : α
hi : (u i).toReal ≤ x
⊢ 0 ≤ x
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ → δ
hg : Continuous[instTopologicalSpaceProd, inst✝²] (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ mk (uncurry g ∘ fun x ↦ (↑f₁ x, ↑f₂ x)) ⋯ = mk (fun a ↦ g (↑f₁ a) (↑f₂ a)) ⋯

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ → δ
hg : Continuous[instTopologicalSpaceProd, inst✝²] (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ mk (uncurry g ∘ fun x ↦ (↑f₁ x, ↑f₂ x)) ⋯ = mk (fun a ↦ g (↑f₁ a) (↑f₂ a)) ⋯