mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this✝ : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
this :
  (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0
⊢ ∀ x ∈ Finset.univ, ¬((x = i ∧ l = -↑i) ∧ k = -↑j)

Tactic:
rintro - - ⟨⟨-, contra⟩, -⟩

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this✝ : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
this :
  (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0
contra : l = -↑i
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this✝ : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
this :
  (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0
h₁ : ∀ x ∈ Finset.univ, ¬((x = i ∧ l = -↑i) ∧ k = -↑j)
⊢ ∀ x ∈ Finset.univ, ¬((x = j ∧ l = ↑j) ∧ k = ↑i)

Tactic:
rintro - - ⟨⟨-, contra⟩, -⟩

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this✝ : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
this :
  (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0
h₁ : ∀ x ∈ Finset.univ, ¬((x = i ∧ l = -↑i) ∧ k = -↑j)
contra : l = ↑j
⊢ False
Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ x y : TensorAlgebra R M
i : ℕ
hx : x ∈ (ι R).range ^ i
hy : y ∈ (ι R).range ^ i
ihx : ((lift R) (GradedAlgebra.ι R M)) x = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨x, hx⟩
ihy : ((lift R) (GradedAlgebra.ι R M)) y = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨y, hy⟩
⊢ ((lift R) (GradedAlgebra.ι R M)) (x + y) = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨x + y, ⋯⟩

Tactic:
rw [map_add, ihx, ihy, ← map_add]

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ x y : TensorAlgebra R M
i : ℕ
hx : x ∈ (ι R).range ^ i
hy : y ∈ (ι R).range ^ i
ihx : ((lift R) (GradedAlgebra.ι R M)) x = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨x, hx⟩
ihy : ((lift R) (GradedAlgebra.ι R M)) y = (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨y, hy⟩
⊢ (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) (⟨x, hx⟩ + ⟨y, hy⟩) =
    (DirectSum.of (fun i ↦ ↥((ι R).range ^ i)) i) ⟨x + y, ⋯⟩
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case hf
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
⊢ map f (↑e).fixedSubmodule = ⊥

Tactic:
rw [eq_bot_iff]

Goal state after:
case hf
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
⊢ map f (↑e).fixedSubmodule ≤ ⊥
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ ν : Measure ((i : ι) → α i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
⊢ μ univ = ν univ

Tactic:
hμ.measure_univ_eq (∅ : Finset ι),

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ ν : Measure ((i : ι) → α i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
⊢ (P ∅) univ = ν univ
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ tᶜ ∩ s ∈ measurableCylinders α

Tactic:
exact inter_mem_measurableCylinders (compl_mem_measurableCylinders ht) hs

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case refl
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : ⊥ ∈ C
hs_mem : ⊥ ∈ hC.disjointOfDiff hs ht
⊢ False

Tactic:
exact hC.empty_notMem_disjointOfDiff hs ht hs_mem

Goal state after:
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.coe.top.inr.refine_2
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a : ι
hb✝ : ⊤ ∈ Ioi ↑a
ha : (Ioi a).Nonempty
b : ι
bc' : b ∈ c'
hb : b ∈ Ioi a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi ↑b)

Tactic:
apply isOpen_generateFrom_of_mem
            exact ⟨b, by simp [d, bc'], Or.inl rfl⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
⊢ onIocAux f ∅ = 0

Tactic:
rw [onIocAux, dite_eq_right_iff]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
⊢ ∀ (h : ∃ p, p.1 ≤ p.2 ∧ ∅ = Set.Ioc p.1 p.2), f h.choose.2 - f h.choose.1 = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → v t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → w t = 0
t : Set α
hst : t ⊆ sᶜ
ht : ¬MeasurableSet t
⊢ w t = 0

Tactic:
exact not_measurable w ht

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
⊢ UnifIntegrable f p μ

Tactic:
obtain ⟨n, hn⟩ := Finite.exists_equiv_fin ι
  intro ε hε
  let g : Fin n → α → β := f ∘ hn.some.symm
  have hg : ∀ i, MemLp (g i) p μ := fun _ => hf _
  obtain ⟨δ, hδpos, hδ⟩ := unifIntegrable_fin hp_one hp_top hg hε
  refine ⟨δ, hδpos, fun i s hs hμs => ?_⟩
  simpa [g] using hδ (hn.some i) s hs hμs

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ IsFiniteMeasure s.totalVariation

Tactic:
unfold totalVariation; infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ BddBelow s.measureOfNegatives

Tactic:
simp_rw [BddBelow, Set.Nonempty, mem_lowerBounds]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ ∃ x, ∀ x_1 ∈ s.measureOfNegatives, x ≤ x_1
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ Integrable f (μ.restrict i)

pp: case hg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ Integrable g (μ.restrict i)

Tactic:
· exact hf.integrableOn

Goal state after:
case hg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ Integrable g (μ.restrict i)
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f μ
hr : ¬r = 0
⊢ ¬Integrable (r • f) μ

Tactic:
rwa [integrable_smul_iff hr f]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
⊢ μ.withDensityᵥ (r • f) = r • μ.withDensityᵥ f

Tactic:
by
  by_cases hf : Integrable f μ
  · ext1 i hi
    rw [withDensityᵥ_apply (hf.smul r) hi, _root_.smul_apply, withDensityᵥ_apply hf hi, ←
      integral_smul r f]
    simp only [Pi.smul_apply]
  · by_cases hr : r = 0
    · rw [hr, zero_smul, zero_smul, withDensityᵥ_zero]
    · rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, smul_zero]
      rwa [integrable_smul_iff hr f]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
⊢ r • s = r • s.singularPart μ + r • μ.withDensityᵥ (s.rnDeriv μ)

Tactic:
← smul_add,

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
⊢ r • s = r • (s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : m ≤ m0
hfint : ¬Integrable f μ
a : α
⊢ μ[f | m] a ≤ c

Tactic:
simpa [condExp_of_not_integrable hfint]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ((c.singularPart μ) i).im + (μ.withDensityᵥ fun x ↦ (c.rnDeriv μ x).im) i = { re := (re c) i, im := (im c) i }.im

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x ↦ (c.rnDeriv μ x).im) μ

Tactic:
· change (c.im.singularPart μ + μ.withDensityᵥ (c.im.rnDeriv μ)) i = _
      rw [c.im.singularPart_add_withDensity_rnDeriv_eq μ]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ Integrable (fun x ↦ (c.rnDeriv μ x).im) μ
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
⊢ HasOuterApproxClosed X

Tactic:
refine ⟨fun F hF ↦ ?_⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst✝¹] F
⊢ ∃ fseq,
    (∀ (n : ℕ) (x : X), (fseq n) x ≤ 1) ∧
      (∀ (n : ℕ), ∀ x ∈ F, 1 ≤ (fseq n) x) ∧ Tendsto (fun n x ↦ (fseq n) x) atTop (𝓝 (F.indicator fun x ↦ 1))
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ μ.testAgainstNN 0 = 0

Tactic:
simpa only [zero_mul] using! μ.testAgainstNN_const 0

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
a : α
ha : (κ a) (⋂ i ∈ ∅, univ) = ∏ i ∈ ∅, (κ a) univ
⊢ IsProbabilityMeasure (κ a)

Tactic:
exact ⟨by simpa using ha⟩

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case e'_3.e'_5
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
⊢ Measure.map (X ∘ Prod.fst) (μ.prod ν) = Measure.map X μ

Tactic:
← Measure.map_map mX measurable_fst,

Goal state after:
case e'_3.e'_5
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : Measurable X
mY : Measurable Y
⊢ Measure.map X (Measure.map Prod.fst (μ.prod ν)) = Measure.map X μ
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ μ[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f i | Y i ⁻¹' t i]

Tactic:
have : IsProbabilityMeasure (μ : Measure Ω) := hindep.isProbabilityMeasure

Goal state after:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
⊢ μ[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f i | Y i ⁻¹' t i]
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this✝ : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ n, f n
this : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν (⋃ i, f i)))
⊢ ∃ T, (∀ t ∈ T, t ∈ S) ∧ r < ν (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G

Tactic:
← G_eq

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this✝ : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ n, f n
this : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν G))
⊢ ∃ T, (∀ t ∈ T, t ∈ S) ∧ r < ν (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : SecondCountableTopology Ω
inst✝¹ : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst✝ : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst✝³] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
hl : l.NeBot
G : Set Ω
hG : IsOpen[inst✝³] G
r : ℝ≥0
hr : r < ν G
T : Finset (Set Ω)
TS : ∀ t ∈ T, t ∈ S
T_meas : r < ν (⋃ t ∈ T, t)
TG : ⋃ t ∈ T, t ⊆ G
this : Tendsto (fun i ↦ (μ i) (⋃ t ∈ T, t)) l (𝓝 (ν (⋃ t ∈ T, t)))
i : ι
hi : r < (μ i) (⋃ t ∈ T, t)
⊢ r < (μ i) G

Tactic:
exact hi.trans_le <| ProbabilityMeasure.apply_mono _ TG

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
h : ¬MemLp X 2 μ
⊢ Var[X; μ] = 0

Tactic:
exact variance_of_not_memLp hX h

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case pos
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : Integrable f (Measure.map X μ)
hg : Integrable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h1 : ∀ᵐ (ω : Ω) ∂μ, (B (f (X ω))) (g (Y ω)) = 0
⊢ ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
simp [integral_congr_ae h1, integral_congr_ae h]

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case neg
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map X μ)
hg : AEStronglyMeasurable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ * ‖y‖ ≤ ‖(B x) y‖
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
⊢ ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
have hB x y : c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ := by
    rw [← toReal_le_toReal]
    · simpa using hB x y
    all_goals finiteness

Goal state after:
case neg
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map X μ)
hg : AEStronglyMeasurable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB✝ : ∀ (x : E) (y : F), ↑c * ‖x‖ * ‖y‖ ≤ ‖(B x) y‖
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖(B x) y‖ₑ
⊢ ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
A : AEStronglyMeasurable id (Measure.map f μ)
⊢ ∫ (y : γ), id y ∂Measure.map f μ = ∫ (x : β), id (g x) ∂ν

Tactic:
rw [h.map_eq] at A

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
A : AEStronglyMeasurable id (Measure.map g ν)
⊢ ∫ (y : γ), id y ∂Measure.map f μ = ∫ (x : β), id (g x) ∂ν