mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.RCLike.Extend

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : Dual ℝ F
fc : F → 𝕜 := fun x ↦ ↑(fr x) - I * ↑(fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(fr (↑c • x)) = ↑c * ↑(fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
x : F
h : I * I = -1
⊢ fc (I • x) = I * fc x

Tactic:
· simp [fc, mul_sub, ← mul_assoc, smul_smul, h, add_comm]

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

Goal state before:
pp: case mpr
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
W : Type u_3
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : FiniteDimensional R W
f : W →ₗ[R] V
hf : Injective ⇑f
this : Injective (⇑(ContinuousLinearMap.coeLM R).flip ∘ ⇑f)
⊢ Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap)

Tactic:
← LinearMap.coe_comp

Goal state after:
case mpr
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
W : Type u_3
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : FiniteDimensional R W
f : W →ₗ[R] V
hf : Injective ⇑f
this : Injective ⇑((ContinuousLinearMap.coeLM R).flip ∘ₗ f)
⊢ Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap)
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
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
K : Set (E →L[𝕜] F)
hK : IsComplete K
⊢ MeasurableSet (⋂ e, ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))

Tactic:
aesop
    (add safe apply [MeasurableSet.iUnion, MeasurableSet.iInter, isOpen_B])
    (add unsafe IsOpen.measurableSet)

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hF : SecondCountableTopology F
⊢ StronglyMeasurable (deriv f)

Tactic:
exact (measurable_deriv f).stronglyMeasurable

Goal state after:
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
x y : E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
⊢ ∃ f, re (f x) < re (f y)

Tactic:
by
  obtain ⟨f, s, t, hs, st, ht⟩ :=
    geometric_hahn_banach_compact_closed (𝕜 := 𝕜) (convex_singleton x) isCompact_singleton
      (convex_singleton y) isClosed_singleton (disjoint_singleton.2 hxy)
  exact ⟨f, by linarith [hs x rfl, ht y rfl]⟩

Goal state after:
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
inst✝⁷ : LocallyCompactSpace E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁴ : TopologicalSpace α
f : α → E → F
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
⊢ MeasurableSet {p | p.2 ∈ D (f p.1) K}

Tactic:
simp only [D, mem_iInter, mem_iUnion]

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : LocallyCompactSpace E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁴ : TopologicalSpace α
f : α → E → F
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}
⊢ MeasurableSet
    {p | ∀ (i : ℕ), ∃ i_1, ∀ i_2 ≥ i_1, ∀ i_4 ≥ i_1, p.2 ∈ B (f p.1) K ((1 / 2) ^ i_2) ((1 / 2) ^ i_4) ((1 / 2) ^ i)}
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case inr
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y

Tactic:
have s_closed : IsClosed s := by
    have : ContinuousOn (fun t => (g b - g t, ∫ u in t..b, φ u)) (Icc a b) := by
      rw [← uIcc_of_le hab] at hcont φint ⊢
      exact (continuousOn_const.sub hcont).prodMk (continuousOn_primitive_interval_left φint)
    simp only [s, inter_comm]
    exact this.preimage_isClosed_of_isClosed isClosed_Icc isClosed_le_prod

Goal state after:
case inr
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: α : Type u_1
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : IsStrictOrderedRing α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto ceil (𝓝[≤] ↑n) (pure n)

Tactic:
by
  simpa only [ceil_intCast] using tendsto_ceil_left_pure_ceil (n : α)

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: α : Type u_1
inst✝⁶ : Ring α
inst✝⁵ : LinearOrder α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : IsStrictOrderedRing α
inst✝¹ : OrderClosedTopology α
inst✝ : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[<] ↑n) (𝓝 1)

Tactic:
rw [← sub_sub_cancel (n : α) 1]

Goal state after:
α : Type u_1
inst✝⁶ : Ring α
inst✝⁵ : LinearOrder α
inst✝⁴ : FloorRing α
inst✝³ : TopologicalSpace α
inst✝² : IsStrictOrderedRing α
inst✝¹ : OrderClosedTopology α
inst✝ : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[<] ↑n) (𝓝 (↑n - (↑n - 1)))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
| if ε < T / 2 then Metric.closedBall 0 ε else I

Tactic:
rw [← if_ctx_congr (Iff.rfl : ε < T / 2 ↔ ε < T / 2) h₁ fun _ => rfl, ← hT']

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
| if ε < |T| / 2 then Metric.closedBall 0 ε ∩ I else I
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
⊢ ν s ≠ 0

Tactic:
exact meas_s_ne_zero

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x ↦ ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
⊢ ∫ (y : AddCircle T), f y ∂Measure.map (fun x ↦ ↑↑x) volume =
    ∫ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))

Tactic:
have : ((↑) : Ioc t (t + T) → AddCircle T) = ((↑) : ℝ → AddCircle T) ∘ ((↑) : _ → ℝ) := by
    ext1 x; rfl

Goal state after:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this✝ : ∫ (y : AddCircle T), f y ∂Measure.map (fun x ↦ ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
this : (fun x ↦ ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val
⊢ ∫ (y : AddCircle T), f y ∂Measure.map (fun x ↦ ↑↑x) volume =
    ∫ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
⊢ ∫ (x : ℝ) in t..s + T, f x = (∫ (x : ℝ) in t..s, f x) + ∫ (x : ℝ) in s..s + T, f x

Tactic:
integral_add_adjacent_intervals (h_int t s) (h_int s _)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
⊢ ∫ (x : ℝ) in t..s + T, f x = ∫ (x : ℝ) in t..s + T, f x
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
ι : Type u_3
f : ι → ℂ → E
h : ∀ (i : ι), CircleIntegrable (f i) c R
h₁ : (support f).Finite
⊢ CircleIntegrable (∑ i ∈ h₁.toFinset, f i) c R

Tactic:
exact CircleIntegrable.sum h₁.toFinset (fun i _ ↦ h i)

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

Goal state before:
pp: c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' ↦ circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ‖f θ'‖
this : x⁻¹ ≤ x ^ n
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤ |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖

Tactic:
by
      simp only [smul_eq_mul, norm_mul,
        norm_inv, norm_I, mul_one]
      simpa only [norm_circleMap_zero, norm_zpow, Ne, abs_eq_zero.not.2 hR, not_false_iff,
        inv_mul_cancel_left₀] using this

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

Goal state before:
pp: T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg (LT.lt.ne' hT) h_int
ε : ℝ := Int.fract (t / T) * T
⊢ sInf ((fun t ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0..T, g x ≤
    (∫ (x : ℝ) in 0..ε, g x) + ∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x

Tactic:
rw [hg.intervalIntegral_add_zsmul_eq ⌊t / T⌋ ε (hg.intervalIntegrable₀ hT.ne' h_int),
    hg.intervalIntegral_add_eq ε 0, zero_add, add_le_add_iff_right]

Goal state after:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg (LT.lt.ne' hT) h_int
ε : ℝ := Int.fract (t / T) * T
⊢ sInf ((fun t ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) ≤ ∫ (x : ℝ) in 0..ε, g x
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c w : ℂ
R : ℝ
n : ℤ
⊢ CircleIntegrable (fun z ↦ (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|

Tactic:
by
  constructor
  · intro h; contrapose! h; rcases h with ⟨hR, hn, hw⟩
    simp only [circleIntegrable_iff R, deriv_circleMap]
    rw [← image_circleMap_Ioc] at hw; rcases hw with ⟨θ, hθ, rfl⟩
    replace hθ : θ ∈ [[0, 2 * π]] := Icc_subset_uIcc (Ioc_subset_Icc_self hθ)
    refine not_intervalIntegrable_of_sub_inv_isBigO_punctured ?_ Real.two_pi_pos.ne hθ
    set f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
    have : ∀ᶠ θ' in 𝓝[≠] θ, f θ' ∈ ball (0 : ℂ) 1 \ {0} := by
      suffices ∀ᶠ z in 𝓝[≠] circleMap c R θ, z - circleMap c R θ ∈ ball (0 : ℂ) 1 \ {0} from
        ((differentiable_circleMap c R θ).hasDerivAt.tendsto_nhdsNE
          (deriv_circleMap_ne_zero hR)).eventually this
      filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ball_mem_nhds _ zero_lt_one)]
      simp_all [dist_eq, sub_eq_zero]
    refine (((hasDerivAt_circleMap c R θ).isBigO_sub.mono inf_le_left).inv_rev
      (this.mono fun θ' h₁ h₂ => absurd h₂ h₁.2)).trans ?_
    refine IsBigO.of_bound |R|⁻¹ (this.mono fun θ' hθ' => ?_)
    set x := ‖f θ'‖
    suffices x⁻¹ ≤ x ^ n by
      simp only [smul_eq_mul, norm_mul,
        norm_inv, norm_I, mul_one]
      simpa only [norm_circleMap_zero, norm_zpow, Ne, abs_eq_zero.not.2 hR, not_false_iff,
        inv_mul_cancel_left₀] using this
    have : x ∈ Ioo (0 : ℝ) 1 := by simpa [x, and_comm] using hθ'
    rw [← zpow_neg_one]
    refine (zpow_right_strictAnti₀ this.1 this.2).le_iff_ge.2 (Int.lt_add_one_iff.1 ?_); exact hn
  · rintro (rfl | H)
    exacts [circleIntegrable_zero_radius,
      ((continuousOn_id.sub continuousOn_const).zpow₀ _ fun z hz =>
        H.symm.imp_left fun (hw : w ∉ sphere c |R|) =>
          sub_ne_zero.2 <| ne_of_mem_of_not_mem hz hw).circleIntegrable']

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

Goal state before:
pp: case h_lim
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ₀ : 0 < δ
hRδ : R * δ < ε
i : ι
hi : ∀ x ∈ sphere c R, dist (g x) (f i x) < δ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ R * dist (g (circleMap c R x)) (f i (circleMap c R x)) ≤ R * δ

Tactic:
hi (circleMap c R x) (by simp [hR])

Goal state after:
case h_lim
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ₀ : 0 < δ
hRδ : R * δ < ε
i : ι
hi : ∀ x ∈ sphere c R, dist (g x) (f i x) < δ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ R * δ ≤ R * δ
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
hf : Integrable (fun x ↦ f x.2) (μ.prod ν)
hμ : μ ≠ 0
⊢ Integrable f ν

Tactic:
by
  rcases hf with ⟨hf_meas, hf_fin⟩
  use hf_meas.of_comp_snd hμ
  have := hf_meas.enorm
  aesop (add simp [HasFiniteIntegral, lintegral_prod, ENNReal.mul_lt_top_iff])

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
⊢ ↑R ≤ (cauchyPowerSeries f c ↑R).radius

Tactic:
refine
    (cauchyPowerSeries f c R).le_radius_of_bound
      ((2 * π)⁻¹ * ∫ θ : ℝ in 0..2 * π, ‖f (circleMap c R θ)‖) fun n => ?_
  refine (mul_le_mul_of_nonneg_right (norm_cauchyPowerSeries_le _ _ _ _)
    (pow_nonneg R.coe_nonneg _)).trans ?_
  rw [abs_of_nonneg R.coe_nonneg]
  rcases eq_or_ne (R ^ n : ℝ) 0 with hR | hR
  · rw_mod_cast [hR, mul_zero]
    exact mul_nonneg (inv_nonneg.2 Real.two_pi_pos.le)
      (intervalIntegral.integral_nonneg Real.two_pi_pos.le fun _ _ => norm_nonneg _)
  · rw [inv_pow]
    have : (R : ℝ) ^ n ≠ 0 := by norm_cast at hR ⊢
    rw [inv_mul_cancel_right₀ this]

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : p.Splits
f : p.Gal
x : p.SplittingField
⊢ f x = 1 x

Tactic:
obtain ⟨y, rfl⟩ :=
        Algebra.mem_bot.mp
          ((SetLike.ext_iff.mp ((IsSplittingField.splits_iff _ p).mp h) x).mp Algebra.mem_top)

Goal state after:
F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : p.Splits
f : p.Gal
y : F
⊢ f ((algebraMap F p.SplittingField) y) = 1 ((algebraMap F p.SplittingField) y)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: S : Type u_4
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Fintype σ
n : ℕ
f : R →+* S
⊢ ∑ x ∈ powersetCard n univ, (map f) (∏ i ∈ x, X i) = ∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i

Tactic:
map_prod,

Goal state after:
S : Type u_4
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Fintype σ
n : ℕ
f : R →+* S
⊢ ∑ x ∈ powersetCard n univ, ∏ x ∈ x, (map f) (X x) = ∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x ∈ powersetCard n univ, (rename ⇑e) (∏ i ∈ x, X i) = ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i)

Tactic:
map_prod,

Goal state after:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x ∈ powersetCard n univ, ∏ x ∈ x, (rename ⇑e) (X x) = ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i)
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case pos.inl
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
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : p₁.comp q = 0
h : p₁ = 0
⊢ P (p₁ * p₂)

pp: case pos.inr
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
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : p₁.comp q = 0
h : eval (q.coeff 0) p₁ = 0 ∧ q = C (q.coeff 0)
⊢ P (p₁ * p₂)

Tactic:
· rw [h, zero_mul]
        simp [P]

Goal state after:
case pos.inr
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
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : p₁.comp q = 0
h : eval (q.coeff 0) p₁ = 0 ∧ q = C (q.coeff 0)
⊢ P (p₁ * p₂)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (⇑Finsupp.toMultiset ∘ fun t ↦ ∑ i ∈ t, Finsupp.single i 1) = val
this : ((powersetCard n univ).sup fun x ↦ x).val = (powersetCard n univ).sup val
⊢ (powersetCard n univ).sup val = univ.val

Tactic:
rw [← this]

Goal state after:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (⇑Finsupp.toMultiset ∘ fun t ↦ ∑ i ∈ t, Finsupp.single i 1) = val
this : ((powersetCard n univ).sup fun x ↦ x).val = (powersetCard n univ).sup val
⊢ ((powersetCard n univ).sup fun x ↦ x).val = univ.val
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ (esymm σ R n).degrees = univ.val

Tactic:
classical
    have :
      (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i ∈ t, Finsupp.single i 1) = val := by
      funext
      simp
    rw [degrees_def, support_esymm, sup_image, this]
    have : ((powersetCard n univ).sup (fun (x : Finset σ) => x)).val
        = sup (powersetCard n univ) val := by
      refine apply_sup_eq_sup_comp _ ?_ ?_ <;> simp
    rw [← this]
    obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
    simpa using! powersetCard_sup _ _ (Nat.lt_of_succ_le hn)

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
⊢ ∫ (x : ℝ) in a..b, f' x = ∫ (x : ℝ) in Set.Icc a b, f' x

Tactic:
intervalIntegral.integral_of_le hle,

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
⊢ ∫ (x : ℝ) in Set.Ioc a b, f' x ∂volume = ∫ (x : ℝ) in Set.Icc a b, f' x
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
⊢ AnalyticAt ℂ f z

Tactic:
rcases nhds_basis_closedBall.mem_iff.1 hz with ⟨R, hR0, hRs⟩
  lift R to ℝ≥0 using hR0.le
  exact ((hd.mono hRs).hasFPowerSeriesOnBall hR0).analyticAt

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case mp
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
z : ℂ
⊢ (∃ a, (aeval a) p = 0 ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ) a = z) → (aeval z) p = 0 ∧ z.im = 0

Tactic:
rintro ⟨w, hw, rfl⟩
      exact ⟨by rw [aeval_algHom_apply, hw, map_zero], rfl⟩

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case a
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
z : ℂ
hz1 : (aeval z) p = 0
hz2 : z.im = 0
⊢ ((IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).im = z.im

Tactic:
rw [hz2]; rfl

Goal state after: