mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
⊢ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} ⊆ D f K

Tactic:
by
  intro x hx
  rw [D, mem_iInter]
  intro e
  have : (0 : ℝ) < (1 / 2) ^ e := by positivity
  rcases mem_A_of_differentiable this hx.1 with ⟨R, R_pos, hR⟩
  obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2) ^ n < R :=
    exists_pow_lt_of_lt_one R_pos (by norm_num : (1 : ℝ) / 2 < 1)
  simp only [mem_iUnion, mem_iInter, B, mem_inter_iff]
  refine ⟨n, fun p hp q hq => ⟨fderiv 𝕜 f x, hx.2, ⟨?_, ?_⟩⟩⟩ <;>
    · refine hR _ ⟨by positivity, lt_of_le_of_lt ?_ hn⟩
      exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by assumption)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ ↑i + 1
⊢ |x ^ (i + 1)| / |↑i + 1| = |x| ^ (i + 1) / (↑i + 1)

Tactic:
← pow_abs,

Goal state after:
x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ ↑i + 1
⊢ |x| ^ (i + 1) / |↑i + 1| = |x| ^ (i + 1) / (↑i + 1)
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (fun x ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε

Tactic:
have δpos : 0 < δ := half_pos εpos

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (fun x ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : ↥f.domain), φ ↑x = ↑f x
hφ₂ : ∀ (x : E), φ x ≤ gauge s x
⊢ φ x₀ = 1

Tactic:
← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _),

Goal state after:
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : ↥f.domain), φ ↑x = ↑f x
hφ₂ : ∀ (x : E), φ x ≤ gauge s x
⊢ φ ↑⟨x₀, ⋯⟩ = 1
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
⊢ ∃ f u, (∀ a ∈ s, re (f a) < u) ∧ ∀ b ∈ t, u < re (f b)

Tactic:
have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
  obtain ⟨f, u, h⟩ := _root_.geometric_hahn_banach_open_open hs₁ hs₂ ht₁ ht₃ disj
  use f.extendRCLikeₗ
  simpa [f.extendRCLikeₗ_apply] using Exists.intro u h

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + ((G y)⁻¹ * G z) • (x - y) + (G z + ((G y)⁻¹ * G z - 1 * G z)) • (y - x) = z

Tactic:
simp only [smul_sub, one_mul, add_sub_cancel]

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + (((G y)⁻¹ * G z) • x - ((G y)⁻¹ * G z) • y) + (((G y)⁻¹ * G z) • y - ((G y)⁻¹ * G z) • x) = z
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
⊢ ∃ i,
    ∀ i_1 ≥ i,
      ∀ i_3 ≥ i, ∃ i, ∃ (_ : i ∈ K), x ∈ A f i ((1 / 2) ^ i_1) ((1 / 2) ^ e) ∧ x ∈ A f i ((1 / 2) ^ i_3) ((1 / 2) ^ e)

Tactic:
refine ⟨n, fun p hp q hq => ⟨derivWithin f (Ici x) x, hx.2, ⟨?_, ?_⟩⟩⟩ <;>
    · refine hR _ ⟨pow_pos (by norm_num) _, lt_of_le_of_lt ?_ hn⟩
      exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by assumption)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
c : ℝ
hc : c ≠ 0
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
⊢ IntervalIntegrable (fun x ↦ f (c * x)) volume (a / c) (b / c) ↔ IntervalIntegrable f volume a b

Tactic:
by
  exact ⟨fun h ↦ by simpa [hc] using h.comp_mul_left (c := c⁻¹) h' (by simp),
    (comp_mul_left · h h')⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ + ∫ (x : ℝ) in c..a, f x ∂μ = 0

Tactic:
simp only [intervalIntegral, sub_add_sub_comm, sub_eq_zero]

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ ∫ (x : ℝ) in Ioc a b, f x ∂μ + ∫ (x : ℝ) in Ioc b c, f x ∂μ + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    ∫ (x : ℝ) in Ioc b a, f x ∂μ + ∫ (x : ℝ) in Ioc c b, f x ∂μ + ∫ (x : ℝ) in Ioc a c, f x ∂μ
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : CompleteSpace F
inst✝² : LocallyCompactSpace 𝕜
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
⊢ deriv (f p.1) p.2 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f p.1 '' univ))

Tactic:
apply range_deriv_subset_closure_span_image _ dense_univ (mem_range_self _)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
⊢ ¬IntegrableOn g k volume

Tactic:
by
  intro hgi
  obtain ⟨C, hC₀, s, hsl, hsub, hfd, hg⟩ :
    ∃ (C : ℝ) (_ : 0 ≤ C), ∃ s ∈ l, (∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k) ∧
      (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
        ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖ := by
    rcases hfg.exists_nonneg with ⟨C, C₀, hC⟩
    have h : ∀ᶠ x : ℝ × ℝ in l ×ˢ l,
        ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ k :=
      (tendsto_fst.uIcc tendsto_snd).eventually ((hd.and hC.bound).and hl).smallSets
    rcases mem_prod_self_iff.1 h with ⟨s, hsl, hs⟩
    simp only [prod_subset_iff, mem_ofPred_eq] at hs
    exact ⟨C, C₀, s, hsl, fun x hx y hy z hz => (hs x hx y hy z hz).2, fun x hx y hy z hz =>
      (hs x hx y hy z hz).1.1, fun x hx y hy z hz => (hs x hx y hy z hz).1.2⟩
  replace hgi : IntegrableOn (fun x ↦ C * ‖g x‖) k := by exact hgi.norm.smul C
  obtain ⟨c, hc, d, hd, hlt⟩ : ∃ c ∈ s, ∃ d ∈ s, (‖f c‖ + ∫ y in k, C * ‖g y‖) < ‖f d‖ := by
    rcases Filter.nonempty_of_mem hsl with ⟨c, hc⟩
    have : ∀ᶠ x in l, (‖f c‖ + ∫ y in k, C * ‖g y‖) < ‖f x‖ :=
      hf.eventually (eventually_gt_atTop _)
    exact ⟨c, hc, (this.and hsl).exists.imp fun d hd => ⟨hd.2, hd.1⟩⟩
  specialize hsub c hc d hd; specialize hfd c hc d hd
  replace hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖ :=
    fun z hz => hg c hc d hd z ⟨hz.1.le, hz.2⟩
  have hg_ae : ∀ᵐ x ∂volume.restrict (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖ :=
    (ae_restrict_mem measurableSet_uIoc).mono hg
  have hsub' : Ι c d ⊆ k := Subset.trans Ioc_subset_Icc_self hsub
  have hfi : IntervalIntegrable (deriv f) volume c d := by
    rw [intervalIntegrable_iff]
    have : IntegrableOn (fun x ↦ C * ‖g x‖) (Ι c d) := IntegrableOn.mono hgi hsub' le_rfl
    exact Integrable.mono' this (aestronglyMeasurable_deriv _ _) hg_ae
  refine hlt.not_ge (sub_le_iff_le_add'.1 ?_)
  calc
    ‖f d‖ - ‖f c‖ ≤ ‖f d - f c‖ := norm_sub_norm_le _ _
    _ = ‖∫ x in c..d, deriv f x‖ := congr_arg _ (integral_deriv_eq_sub hfd hfi).symm
    _ = ‖∫ x in Ι c d, deriv f x‖ := norm_integral_eq_norm_integral_uIoc _
    _ ≤ ∫ x in Ι c d, ‖deriv f x‖ := norm_integral_le_integral_norm _
    _ ≤ ∫ x in Ι c d, C * ‖g x‖ :=
      setIntegral_mono_on hfi.norm.def' (hgi.mono_set hsub') measurableSet_uIoc hg
    _ ≤ ∫ x in k, C * ‖g x‖ := by
      apply setIntegral_mono_set hgi
        (ae_of_all _ fun x => mul_nonneg hC₀ (norm_nonneg _)) hsub'.eventuallyLE

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a

Tactic:
simp only [uIcc_of_ge, hab, uIoo_of_ge] at hcont hderiv
    rw [integral_symm, integral_eq_sub_of_hasDerivAt_of_le hab hcont
        (fun x hx => (hderiv x hx).hasDerivAt) hint.symm, neg_sub]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: case neg.neZeroV
G : Type u_1
inst✝¹⁵ : Group G
inst✝¹⁴ : MeasurableSpace G
inst✝¹³ : TopologicalSpace G
inst✝¹² : IsTopologicalGroup G
inst✝¹¹ : BorelSpace G
inst✝¹⁰ : PolishSpace G
Γ : Subgroup G
inst✝⁹ : Γ.Normal
inst✝⁸ : T2Space (G ⧸ Γ)
inst✝⁷ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁶ : ν.IsMulLeftInvariant
inst✝⁵ : Countable ↥Γ
inst✝⁴ : ν.IsMulRightInvariant
inst✝³ : SigmaFinite ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : SigmaFinite μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain (↥Γ.op) G ν
s : Set G
h : ν s = μ univ
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
finiteCovol : μ univ < ∞
meas_s_ne_zero : ¬ν s = 0
⊢ μ univ ≠ 0

Tactic:
rw [← h]
    exact meas_s_ne_zero

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable QuotientGroup.mk
⊢ ∀ (γ : ↥Γ.op) (x : G), (g ∘ QuotientGroup.mk) (γ • x) = (g ∘ QuotientGroup.mk) x

Tactic:
intro ⟨γ, hγ⟩ x

Goal state after:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable QuotientGroup.mk
γ : Gᵐᵒᵖ
hγ : γ ∈ Γ.op
x : G
⊢ (g ∘ QuotientGroup.mk) (⟨γ, hγ⟩ • x) = (g ∘ QuotientGroup.mk) x
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Icc a a₀) a

Tactic:
have h_int : IntervalIntegrable f μ a a₀ :=
      (intervalIntegrable_iff_integrableOn_Ico_of_le ha).2 <| hf.mono_set Ico_subset_Iio_self

Goal state after:
case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
h_int : IntervalIntegrable f μ a a₀
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Icc a a₀) a
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
p q r : Prop
h1 : r → p
⊢ (r ↔ p ∧ q) ↔ (p ∧ r ↔ p ∧ q)

Tactic:
and_iff_right_of_imp h1

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
p q r : Prop
h1 : r → p
⊢ (r ↔ p ∧ q) ↔ (r ↔ p ∧ q)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * π * R * C

Tactic:
exact norm_integral_le_of_norm_le_const hR hf

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
n : ℕ
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      ‖deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t)‖ ≤
        ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n

pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → Summable fun n ↦ ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n

pp: case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ℕ), ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n) volume 0 (2 * π)

pp: case refine_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n ↦ deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t))

Tactic:
· simp [norm_smul, abs_of_pos hR, mul_left_comm R, inv_mul_cancel_left₀ hR.ne', mul_comm ‖_‖]

Goal state after:
case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → Summable fun n ↦ ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n

case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ℕ), ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n) volume 0 (2 * π)

case refine_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n ↦ deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t))
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this✝ :
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ : ∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ Box.Icc J
x✝ : GP.bDistortion = true → J.distortion ≤ c
Hl : J.lower i ∈ Set.Icc (J.lower i) (J.upper i)
Hu : J.upper i ∈ Set.Icc (J.lower i) (J.upper i)
Hi : ∀ x ∈ Set.Icc (J.lower i) (J.upper i), Integrable (J.face i) GP (fun y ↦ f (i.insertNth x y)) BoxAdditiveMap.volume
hJδ' : Box.Icc J ⊆ closedBall x δ ∩ Box.Icc I
Hmaps : ∀ z ∈ Set.Icc (J.lower i) (J.upper i), MapsTo (i.insertNth z) (Box.Icc (J.face i)) (closedBall x δ ∩ Box.Icc I)
this : ∀ (j : Fin (n + 1)), |J.upper j - J.lower j| ≤ 2 * δ
⊢ ∏ j, |J.upper j - J.lower j| ≤ ∏ j, 2 * δ

Tactic:
gcongr with j _; exact this j

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : Preorder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i, (f' i x) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
⊢ Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' ⇑eL ⁻¹' Set.Icc (eL a) (eL b)

Tactic:
eL.symm_preimage_preimage

Goal state after:
E : Type u
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : Preorder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i, (f' i x) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
⊢ Set.Icc (eL a) (eL b) = Set.Icc (eL a) (eL b)
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  ((if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField).prod
        (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField))
      f =
    ((if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField).prod
        (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField))
      g
⊢ f = g

Tactic:
simp only [dif_neg hpq, MonoidHom.prod_apply, Prod.mk_inj] at hfg

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
⊢ f = g
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
r : F[X]
hr : Irreducible r
hr' : ¬r.natDegree = 0
h : (map (algebraMap F (r.comp q).SplittingField) (r.comp q)).degree = 0
⊢ (r.comp q).degree = ↑0

Tactic:
rwa [degree_map] at h

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
⊢ embedRealFun 0 ≤ 0

Tactic:
apply csSup_le (ratLt'_nonempty 0)
    intro x
    unfold ratLt' ratLt
    suffices ∀ (y : ℚ), y.num • (1 : M) < 0 → y = x → x ≤ 0 by simpa using this
    intro y hy hyx
    rw [← hyx, Rat.cast_nonpos, ← Rat.num_nonpos]
    exact (neg_of_smul_neg_right hy zero_le_one).le

Goal state after:
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
H' : ∀ (x : K), v x ≠ 0 → v x = 1
x : K
hx : x ≠ 0
hx' : v x ≠ 1
⊢ False

Tactic:
exact hx' (H' x ((ne_zero_iff v).mpr hx))

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.RankOne

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst✝ : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
x y : (ofClass v).ValueGroup₀
⊢ (MulEquiv.withZero (intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm).toFun x ≤
      (MulEquiv.withZero (intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm).toFun y ↔
    x ≤ y

Tactic:
by
    rw [(WithZero.map'_strictMono (MulEquiv.strictMono_symm (mulintEquivOfZPowersEqTop_strictMono
    (Subgroup.zpowers_inv (g := hv.generator') ▸ hv.generator'_zpowers_eq_top)
    (Left.one_lt_inv_iff.mpr hv.generator'_lt_one)))).le_iff_le]

Goal state after: