harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_tsum {ι : Type*} [Countable ι] {f : ι → α → ℝ≥0∞} (h : ∀ i, Measurable (f i)) :
    μ.withDensity (∑' n, f n) = sum fun n => μ.withDensity (f n)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ μ.withDensity (∑' (n : ι), f n) = sum fun n => μ.withDensity (f n)

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (∑' (n : ι), f n)) s = (sum fun n => μ.withDensity (f n)) s

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, (∑' (n : ι), f n) x ∂μ = ∫⁻ (a : α) in s, ∑' (i : ι), f i a ∂μ

Tactic:
exact lintegral_congr fun x => tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)

Result:
no goals

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (∑' (n : ι), f n) a ∂μ = ∑' (i : ι), ∫⁻ (a : α) in s, f i a ∂μ

Tactic:
change ∫⁻ x in s, (∑' n, f n) x ∂μ = ∑' i, ∫⁻ x, f i x ∂μ.restrict s

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, (∑' (n : ι), f n) x ∂μ = ∑' (i : ι), ∫⁻ (x : α) in s, f i x ∂μ

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, (∑' (n : ι), f n) x ∂μ = ∑' (i : ι), ∫⁻ (x : α) in s, f i x ∂μ

Tactic:
rw [← lintegral_tsum fun i => (h i).aemeasurable]

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, (∑' (n : ι), f n) x ∂μ = ∫⁻ (a : α) in s, ∑' (i : ι), f i a ∂μ

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (∑' (n : ι), f n)) s = (sum fun n => μ.withDensity (f n)) s

Tactic:
simp_rw [sum_apply _ hs, withDensity_apply _ hs]

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (∑' (n : ι), f n) a ∂μ = ∑' (i : ι), ∫⁻ (a : α) in s, f i a ∂μ
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
/-- A functor that preserves biproducts of a pair preserves binary biproducts. -/
lemma preservesBinaryBiproduct_of_preservesBiproduct (F : C ⥤ D)
    [PreservesZeroMorphisms F] (X Y : C) [PreservesBiproduct (pairFunction X Y) F] :
    PreservesBinaryBiproduct X Y F where
  preserves {b} hb := ⟨{
      isLimit :=
        IsLimit.ofIsoLimit
            ((IsLimit.postcomposeHomEquiv (diagramIsoPair _) _).symm
              (isBilimitOfPreserves F (b.toBiconeIsBilimit.symm hb)).isLimit) <|
          Cones.ext (Iso.refl _) fun j => by
            rcases j with ⟨⟨⟩⟩ <;> simp
      isColimit :=
        IsColimit.ofIsoColimit
            ((IsColimit.precomposeInvEquiv (diagramIsoPair _) _).symm
              (isBilimitOfPreserves F (b.toBiconeIsBilimit.symm hb)).isColimit) <|
          Cocones.ext (Iso.refl _) fun j => by
            rcases j with ⟨⟨⟩⟩ <;> simp }⟩

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
            (F.mapBicone b.toBicone).toCone).π.app
      j =
    (Iso.refl
          ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (F.mapBicone b.toBicone).toCone).pt).hom ≫
      (F.mapBinaryBicone b).toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).ι.app
        j ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
theorem ae_eq_zero_restrict_of_forall_setIntegral_eq_zero {f : α → E}
    (hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
    (hf_zero : ∀ s : Set α, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) {t : Set α}
    (ht : MeasurableSet t) (hμt : μ t ≠ ∞) : f =ᵐ[μ.restrict t] 0

Proof state:
case intro.intro
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : Dual ℝ E
⊢ (fun x => c (f x)) =ᶠ[ae (μ.restrict t)] 0

Tactic:
refine ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real ?_ ?_ ht hμt

Result:
case intro.intro.refine_1
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : Dual ℝ E
⊢ ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (fun x => c (f x)) s μ

case intro.intro.refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
u : Set E
u_sep : IsSeparable u
hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u
c : Dual ℝ E
⊢ ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, c (f x) ∂μ = 0
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem coe_of_rat_eq (v_eq_q : v = (↑q : K)) :
    ((IntFractPair.of q).mapFr (↑) : IntFractPair K) = IntFractPair.of v

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ mapFr Rat.cast (IntFractPair.of q) = IntFractPair.of v

Tactic:
simp [IntFractPair.of, v_eq_q]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean
theorem tendsto_lintegral_nn_filter_of_le_const {ι : Type*} {L : Filter ι} [L.IsCountablyGenerated]
    (μ : Measure Ω) [IsFiniteMeasure μ] {fs : ι → Ω →ᵇ ℝ≥0} {c : ℝ≥0}
    (fs_le_const : ∀ᶠ i in L, ∀ᵐ ω : Ω ∂μ, fs i ω ≤ c) {f : Ω → ℝ≥0}
    (fs_lim : ∀ᵐ ω : Ω ∂μ, Tendsto (fun i ↦ fs i ω) L (𝓝 (f ω))) :
    Tendsto (fun i ↦ ∫⁻ ω, fs i ω ∂μ) L (𝓝 (∫⁻ ω, f ω ∂μ))

Proof state:
case refine_1
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))
⊢ ∀ᶠ (n : ι) in L, ∀ᵐ (a : Ω) ∂μ, ↑((fs n) a) ≤ (fun x => ↑c) a

Tactic:
simpa only [Function.comp_apply, ENNReal.coe_le_coe] using fs_le_const

Result:
no goals

Proof state:
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))
⊢ Tendsto (fun i => ∫⁻ (ω : Ω), ↑((fs i) ω) ∂μ) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂μ))

Tactic:
refine tendsto_lintegral_filter_of_dominated_convergence (fun _ ↦ c)
  (Eventually.of_forall fun i ↦ (ENNReal.continuous_coe.comp (fs i).continuous).measurable) ?_
  (@lintegral_const_lt_top _ _ μ _ _ (@ENNReal.coe_ne_top c)).ne ?_

Result:
case refine_1
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))
⊢ ∀ᶠ (n : ι) in L, ∀ᵐ (a : Ω) ∂μ, ↑((fs n) a) ≤ (fun x => ↑c) a

case refine_2
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))
⊢ ∀ᵐ (a : Ω) ∂μ, Tendsto (fun n => ↑((fs n) a)) L (𝓝 ↑(f a))

Proof state:
case refine_2
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))
⊢ ∀ᵐ (a : Ω) ∂μ, Tendsto (fun n => ↑((fs n) a)) L (𝓝 ↑(f a))

Tactic:
simpa only [Function.comp_apply, ENNReal.tendsto_coe] using fs_lim

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem reflection_orthogonal : reflection Kᗮ = .trans (reflection K) (.neg _)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
⊢ reflection Kᗮ = (reflection K).trans (LinearIsometryEquiv.neg 𝕜)

Tactic:
ext

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x✝ : E
⊢ (reflection Kᗮ) x✝ = ((reflection K).trans (LinearIsometryEquiv.neg 𝕜)) x✝

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x✝ : E
⊢ (reflection Kᗮ) x✝ = ((reflection K).trans (LinearIsometryEquiv.neg 𝕜)) x✝

Tactic:
apply reflection_orthogonal_apply

Result:
no goals
-- Mathlib/Probability/StrongLaw.lean
theorem strong_law_aux5 :
    ∀ᵐ ω, (fun n : ℕ => ∑ i ∈ range n, truncation (X i) i ω - ∑ i ∈ range n, X i ω) =o[atTop]
    fun n : ℕ => (n : ℝ)

Proof state:
case neg
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
h : ¬(-↑n < X n ω ∧ X n ω ≤ ↑n)
⊢ 0 = 0 - X n ω

Tactic:
have : -(n : ℝ) < X n ω := by
  apply lt_of_lt_of_le _ (hnonneg n ω)
  simpa only [Right.neg_neg_iff, Nat.cast_pos] using npos

Result:
case neg
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ⊤
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
n : ℕ
hn : X n ω ∉ Set.Ioi ↑n
npos : n ∈ Set.Ioi 0
h : ¬(-↑n < X n ω ∧ X n ω ≤ ↑n)
this : -↑n < X n ω
⊢ 0 = 0 - X n ω
-- Mathlib/Analysis/Seminorm.lean
theorem convex_ball : Convex ℝ (ball p x r)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (p.ball x r)

Tactic:
convert (p.convexOn.translate_left (-x)).convex_lt r

Result:
case h.e'_6
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ p.ball x r = {x_1 | x_1 ∈ (fun z => -x + z) ⁻¹' univ ∧ (⇑p ∘ fun z => z + -x) x_1 < r}

Proof state:
case h.e'_6
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ p.ball x r = {x_1 | x_1 ∈ (fun z => -x + z) ⁻¹' univ ∧ (⇑p ∘ fun z => z + -x) x_1 < r}

Tactic:
ext y

Result:
case h.e'_6.h
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.ball x r ↔ y ∈ {x_1 | x_1 ∈ (fun z => -x + z) ⁻¹' univ ∧ (⇑p ∘ fun z => z + -x) x_1 < r}

Proof state:
case h.e'_6.h
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.ball x r ↔ y ∈ {x_1 | x_1 ∈ (fun z => -x + z) ⁻¹' univ ∧ (⇑p ∘ fun z => z + -x) x_1 < r}

Tactic:
rw [preimage_univ, sep_univ, p.mem_ball, sub_eq_add_neg]

Result:
case h.e'_6.h
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ p (y + -x) < r ↔ y ∈ {x_1 | (⇑p ∘ fun z => z + -x) x_1 < r}

Proof state:
case h.e'_6.h
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ p (y + -x) < r ↔ y ∈ {x_1 | (⇑p ∘ fun z => z + -x) x_1 < r}

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Pointed.lean
theorem toConvexCone_injective : Injective ((↑) : PointedCone 𝕜 E → ConvexCone 𝕜 E) :=
  fun _ _ => by simp [toConvexCone]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x✝¹ x✝ : PointedCone 𝕜 E
⊢ ↑x✝¹ = ↑x✝ → x✝¹ = x✝

Tactic:
simp [toConvexCone]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem setIntegral_condExpL2_indicator (hs : MeasurableSet[m] s) (ht : MeasurableSet t)
    (hμs : μ s ≠ ∞) (hμt : μ t ≠ ∞) :
    ∫ x in s, (condExpL2 ℝ ℝ hm (indicatorConstLp 2 ht hμt 1) : α → ℝ) x ∂μ = (μ (t ∩ s)).toReal :=
  calc
    ∫ x in s, (condExpL2 ℝ ℝ hm (indicatorConstLp 2 ht hμt 1) : α → ℝ) x ∂μ =
        ∫ x in s, indicatorConstLp 2 ht hμt (1 : ℝ) x ∂μ :=
      @integral_condExpL2_eq α _ ℝ _ _ _ _ _ _ _ _ _ hm (indicatorConstLp 2 ht hμt (1 : ℝ)) hs hμs
    _ = (μ (t ∩ s)).toReal • (1 : ℝ) := setIntegral_indicatorConstLp (hm s hs) ht hμt 1
    _ = (μ (t ∩ s)).toReal

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
⊢ (μ (t ∩ s)).toReal • 1 = (μ (t ∩ s)).toReal

Tactic:
rw [smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem exists_rightDescent_of_ne_one {w : W} (hw : w ≠ 1) : ∃ i : B, cs.IsRightDescent w i

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
hw : w ≠ 1
⊢ ∃ i, cs.IsRightDescent w i

Tactic:
simp only [← isLeftDescent_inv_iff]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
hw : w ≠ 1
⊢ ∃ i, cs.IsLeftDescent w⁻¹ i

Proof state:
case hw
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
hw : w ≠ 1
⊢ w⁻¹ ≠ 1

Tactic:
simpa

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
hw : w ≠ 1
⊢ ∃ i, cs.IsLeftDescent w⁻¹ i

Tactic:
apply exists_leftDescent_of_ne_one

Result:
case hw
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
hw : w ≠ 1
⊢ w⁻¹ ≠ 1
-- Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
theorem ContMDiffWithinAt.mfderivWithin {x₀ : N} {f : N → M → M'} {g : N → M}
    {t : Set N} {u : Set M}
    (hf : ContMDiffWithinAt (J.prod I) I' n (Function.uncurry f) (t ×ˢ u) (x₀, g x₀))
    (hg : ContMDiffWithinAt J I m g t x₀) (hx₀ : x₀ ∈ t)
    (hu : MapsTo g t u) (hmn : m + 1 ≤ n) (h'u : UniqueMDiffOn I u) :
    haveI : IsManifold I 1 M := .of_le (le_trans le_add_self hmn)
    haveI : IsManifold I' 1 M' := .of_le (le_trans le_add_self hmn)
    ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
      (inTangentCoordinates I I' g (fun x => f x (g x))
        (fun x => mfderivWithin I I' (f x) u (g x)) x₀) t x₀

Proof state:
case hst
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J n N
Is : IsManifold I n M
I's : IsManifold I' n M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiffOn I u
this✝² : IsManifold I 1 M
this✝¹ : IsManifold I' 1 M'
this✝ : IsManifold J 1 N
this : IsManifold J m N
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
h4f✝ : ContinuousWithinAt (fun x => f x (g x)) t x₀
h4f : (fun x => f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝[t] x₀
h3f : ∀ᶠ (x' : N × M) in 𝓝[t ×ˢ u] (x₀, g x₀), ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) x'
h2f : ∀ᶠ (x₂ : N) in 𝓝[t] x₀, ContMDiffWithinAt I I' 1 (f x₂) u (g x₂)
h2g : g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝[t] x₀
hg' :
  ContinuousWithinAt g t' x₀ ∧
    ContDiffWithinAt 𝕜 m (↑(extChartAt I (g x₀)) ∘ g ∘ ↑(extChartAt J x₀).symm)
      (↑(extChartAt J x₀).symm ⁻¹' t' ∩ range ↑J) (↑(extChartAt J x₀) x₀)
hf' :
  ContinuousWithinAt (uncurry f) (t' ×ˢ u) (x₀, g x₀) ∧
    ContDiffWithinAt 𝕜 n
      (fun x => ↑(extChartAt I' (f x₀ (g x₀))) (f (↑(extChartAt J x₀).symm x.1) (↑(extChartAt I (g x₀)).symm x.2)))
      ((fun p => (↑(extChartAt J x₀).symm p.1, ↑(extChartAt I (g x₀)).symm p.2)) ⁻¹' t' ×ˢ u ∩ range ↑J ×ˢ range ↑I)
      (↑((extChartAt J x₀).prod (extChartAt I (g x₀))) (x₀, g x₀))
a : F
ha : ↑(extChartAt J x₀).symm a ∈ t'
⊢ g (↑(extChartAt J x₀).symm a) ∈ u

Tactic:
exact hu (inter_subset_left ha)

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
theorem ContMDiffAt.comp_of_eq {g : M' → M''} {x : M} {y : M'} (hg : ContMDiffAt I' I'' n g y)
    (hf : ContMDiffAt I I' n f x) (hx : f x = y) : ContMDiffAt I I'' n (g ∘ f) x

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
n : WithTop ℕ∞
g : M' → M''
x : M
y : M'
hg : ContMDiffAt I' I'' n g y
hf : ContMDiffAt I I' n f x
hx : f x = y
⊢ ContMDiffAt I I'' n (g ∘ f) x

Tactic:
subst hx

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
n : WithTop ℕ∞
g : M' → M''
x : M
hf : ContMDiffAt I I' n f x
hg : ContMDiffAt I' I'' n g (f x)
⊢ ContMDiffAt I I'' n (g ∘ f) x

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
n : WithTop ℕ∞
g : M' → M''
x : M
hf : ContMDiffAt I I' n f x
hg : ContMDiffAt I' I'' n g (f x)
⊢ ContMDiffAt I I'' n (g ∘ f) x

Tactic:
exact hg.comp x hf

Result:
no goals