mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst✝²] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
this : Tendsto (fun t ↦ ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
t : Finset ℕ
ht : μ (⋃ n, s n) < ∑ k ∈ t, μ (s k) + ε / 2
⊢ ∑' (n : ℕ), (μ (s n) + δ n) = μ (⋃ n, s n) + ∑' (n : ℕ), δ n

Tactic:
by rw [measure_iUnion hsd hsm, ENNReal.tsum_add]

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : BorelSpace G
μ : Measure G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst✝⁶] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst✝⁶] U
hμUk : μ U < μ k + ε
V : Set G
hV1 : V ∈ 𝓝 1
hVkU : V * k ⊆ U
⊢ ∀ᶠ (g : G) in 𝓝 1, μ (g • k \ k) < ε

Tactic:
filter_upwards [hV1] with g hg

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : BorelSpace G
μ : Measure G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst✝⁶] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst✝⁶] U
hμUk : μ U < μ k + ε
V : Set G
hV1 : V ∈ 𝓝 1
hVkU : V * k ⊆ U
g : G
hg : g ∈ V
⊢ μ (g • k \ k) < ε
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable (fun x ↦ (X x, Y x)) μ
⊢ AEMeasurable Y μ

Tactic:
exact measurable_snd.comp_aemeasurable hY

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

Goal state before:
pp: G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := ⋯
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst✝⁷] (L n)
M : ∀ (n : ℕ), μ (L n) = ↑(n + 1) * μ K
N : Tendsto (fun n ↦ μ (L n)) atTop (𝓝 ∞)
⊢ ∞ ≤ μ univ

Tactic:
exact le_of_tendsto' N fun n => measure_mono (subset_univ _)

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ✝ : Measure G
inst✝⁶ : μ✝.IsHaarMeasure
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : T1Space G
inst✝² : WeaklyLocallyCompactSpace G
inst✝¹ : (𝓝[≠] 1).NeBot
μ : Measure G
inst✝ : μ.IsHaarMeasure
⊢ NullSingletonClass μ

Tactic:
cases eq_or_ne (μ 1) 0 with
  | inl h => constructor; simpa
  | inr h =>
    obtain ⟨K, K_compact, K_nhds⟩ : ∃ K : Set G, IsCompact K ∧ K ∈ 𝓝 1 := exists_compact_mem_nhds 1
    have K_inf : Set.Infinite K := infinite_of_mem_nhds (1 : G) K_nhds
    exact absurd (K_inf.meas_eq_top ⟨_, h, fun x _ ↦ (haar_singleton _ _).ge⟩)
      K_compact.measure_lt_top.ne

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ (dirac a).withDensity f = f a • dirac a

Tactic:
by
  ext s hs
  classical
  simp [withDensity_apply f hs, setLIntegral_dirac, Set.indicator]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
N : ι
hN :
  ∀ n_1 ≥ N,
    μ (s ∩ notConvergentSeq f g n n_1) ∈ Icc (0 - ENNReal.ofReal (ε * 2⁻¹ ^ n)) (0 + ENNReal.ofReal (ε * 2⁻¹ ^ n))
⊢ ∃ j, μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)

Tactic:
zero_add

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
N : ι
hN :
  ∀ n_1 ≥ N, μ (s ∩ notConvergentSeq f g n n_1) ∈ Icc (0 - ENNReal.ofReal (ε * 2⁻¹ ^ n)) (ENNReal.ofReal (ε * 2⁻¹ ^ n))
⊢ ∃ j, μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √x * √y⁻¹ = √x / √y

Tactic:
sqrt_inv,

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √x * (√y)⁻¹ = √x / √y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ √x * √y⁻¹ = √x / √y

Tactic:
sqrt_inv,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ √x * (√y)⁻¹ = √x / √y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
⊢ x ^ 2 < y ↔ -√y < x ∧ x < √y

Tactic:
rw [← abs_lt, ← sq_abs, lt_sqrt (abs_nonneg _)]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
⊢ Tendsto (fun n ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)

Tactic:
have hb : ∀ n, ∀ᵐ a ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a := by
    intro n
    filter_upwards [all_ae_norm_ofReal_F_le_bound h_bound n,
      ae_norm_ofReal_f_le_bound h_bound h_lim] with a h₁ h₂
    calc
      ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖ := by
        rw [← ENNReal.ofReal_add]
        · apply ofReal_le_ofReal
          apply norm_sub_le
        · exact norm_nonneg _
        · exact norm_nonneg _
      _ ≤ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) := add_le_add h₁ h₂
      _ = b a := by rw [← two_mul]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
⊢ Tendsto (fun n ↦ ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ ∫⁻ (a : α), b a ∂μ ≠ ∞

pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ 0 ≤ᵐ[μ] bound

Tactic:
· calc
        ∫⁻ a, b a ∂μ = 2 * ∫⁻ a, ENNReal.ofReal (bound a) ∂μ := by
          rw [lintegral_const_mul']
          finiteness
        _ ≠ ∞ := mul_ne_top coe_ne_top bound_hasFiniteIntegral.ne

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ 0 ≤ᵐ[μ] bound
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1
⊢ μ.withDensity 1 ≤ μ

Tactic:
rw [withDensity_one]

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

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
this : ∀ {f : α → ℝ≥0∞}, Measurable f → SFinite (μ.withDensity f)
hfm : ¬Measurable f
⊢ SFinite (μ.withDensity f)

Tactic:
rcases exists_measurable_le_withDensity_eq μ f with ⟨g, hgm, -, h⟩
    exact h ▸ this hgm

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
⊢ SFinite (μ.withDensity f)

Tactic:
by
  wlog hfm : Measurable f generalizing f
  · rcases exists_measurable_le_withDensity_eq μ f with ⟨g, hgm, -, h⟩
    exact h ▸ this hgm
  wlog hμ : IsFiniteMeasure μ generalizing μ
  · rw [← sum_sfiniteSeq μ, withDensity_sum]
    have (n : ℕ) : SFinite ((sfiniteSeq μ n).withDensity f) := this inferInstance
    infer_instance
  set s := {x | f x = ∞}
  have hs : MeasurableSet s := hfm (measurableSet_singleton _)
  have key := calc
    μ.withDensity f = μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) := by
      simp (disch := measurability) [withDensity_indicator, ← restrict_withDensity]
    _ = μ.withDensity (sᶜ.indicator f) + .sum fun _ : ℕ ↦ μ.withDensity (s.indicator 1) := by
      rw [← withDensity_tsum (by measurability)]
      congr 2 with x
      rw [ENNReal.tsum_apply]
      if hx : x ∈ s then simpa [hx, ENNReal.tsum_const_eq_top_of_ne_zero]
      else simp [hx]
  have : SigmaFinite (μ.withDensity (sᶜ.indicator f)) := by
    refine SigmaFinite.withDensity_of_ne_top <| ae_of_all _ fun x hx ↦ ?_
    simp [indicator_apply, ite_eq_iff, s] at hx
  have : SigmaFinite (μ.withDensity (s.indicator 1)) := by
    rw [withDensity_indicator hs]
    exact SigmaFinite.withDensity 1
  rw [key]
  infer_instance

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case mpr
a b₁ b₂ : ℝ
x : ℂ
⊢ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]] → x ∈ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]]

Tactic:
intro hx
    simp only [equivRealProd_apply, singleton_prod, mem_image, Prod.mk.injEq,
      exists_eq_right_right, mem_preimage] at hx
    obtain ⟨x₁, hx₁, hx₁', hx₁''⟩ := hx
    refine ⟨x.im, x₁, by simp⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring B
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring C
inst✝³ : TopologicalSpace C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
g : A ≃A[R] B
f' : A ≃ₐ[R] B
continuous_toFun✝ : Continuous[inst✝⁷, inst✝⁵] f'.toFun
continuous_invFun✝ : Continuous[inst✝⁵, inst✝⁷] f'.invFun
h₁ :
  { toAlgEquiv := f', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toFun = g.toFun
h₂ :
  { toAlgEquiv := f', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.invFun = g.invFun
⊢ { toAlgEquiv := f', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ } = g

Tactic:
obtain ⟨g', _⟩ := g

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring B
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring C
inst✝³ : TopologicalSpace C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f' : A ≃ₐ[R] B
continuous_toFun✝¹ : Continuous[inst✝⁷, inst✝⁵] f'.toFun
continuous_invFun✝¹ : Continuous[inst✝⁵, inst✝⁷] f'.invFun
g' : A ≃ₐ[R] B
continuous_toFun✝ : Continuous[inst✝⁷, inst✝⁵] g'.toFun
continuous_invFun✝ : Continuous[inst✝⁵, inst✝⁷] g'.invFun
h₁ :
  { toAlgEquiv := f', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }.toFun =
    { toAlgEquiv := g', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toFun
h₂ :
  { toAlgEquiv := f', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }.invFun =
    { toAlgEquiv := g', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.invFun
⊢ { toAlgEquiv := f', continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ } =
    { toAlgEquiv := g', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm)
      ({ re := x₁, im := y₁ } * { re := x₂, im := y₂ }) =
    (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) { re := x₁, im := y₁ } *
      (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) { re := x₂, im := y₂ }

Tactic:
rw [mk_mul_mk]

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm)
      { re := x₁ * x₂ - y₁ * y₂, im := x₁ * y₂ + y₁ * x₂ } =
    (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) { re := x₁, im := y₁ } *
      (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) { re := x₂, im := y₂ }
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ x.re = y ↔ x = ↑y

Tactic:
← RCLike.re_eq_complex_re

Goal state after:
x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ RCLike.re x = y ↔ x = ↑y
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ y = x.re ↔ ↑y = x

Tactic:
← RCLike.re_eq_complex_re

Goal state after:
x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ y = RCLike.re x ↔ ↑y = x
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
hx : IsSelfAdjoint x
⊢ 0 ≤ x.re ↔ 0 ≤ x

Tactic:
← RCLike.re_eq_complex_re

Goal state after:
x : ℂ
hx : IsSelfAdjoint x
⊢ 0 ≤ RCLike.re x ↔ 0 ≤ x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ re ↑n = ↑n

Tactic:
by rw [← ofReal_intCast, ofReal_re]

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedField E
inst✝¹ : CharZero E
inst✝ : NormedSpace K E
q : ℚ≥0
x : E
⊢ ‖q • x‖ = q • ‖x‖

Tactic:
simpa [NNRat.cast_smul_eq_nnqsmul] using! norm_smul (q : K) x

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ 0 ≤ x ↔ ∃ s, x = star s * s

Tactic:
by
      rw [nonneg_iff]
      refine ⟨fun h ↦ ⟨√(re x), by simp [ext_iff (K := K), h.1, h.2]⟩, ?_⟩
      rintro ⟨s, rfl⟩
      simp [mul_comm, mul_self_nonneg, add_nonneg]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k : ℕ
hi :
  abv (∑ i ∈ range (k + max n i), f i + -∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (k + max n i), a k + -∑ k ∈ range (max n i), a k
⊢ n ≤ k + max n i

Tactic:
omega

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : f' =o[l] g'
⊢ (fun x ↦ k₁ x • f' x) =o[l] fun x ↦ k₂ x • g' x

Tactic:
by
  simp only [IsLittleO_def] at *
  intro c cpos
  rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩
  exact (hc'.smul (h₂ (div_pos cpos c'pos))).congr_const (mul_div_cancel₀ _ (ne_of_gt c'pos))

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case cons.inl
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (∃ i ∈ L, f i =o[l] g i) →
      (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) L).prod) =o[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) L).prod
h₁ : f i =O[l] g i ∧ ∀ x ∈ L, f x =O[l] g x
hi : f i =o[l] g i
⊢ (fun x ↦ f i x * (List.map (fun x_1 ↦ f x_1 x) L).prod) =o[l] fun x ↦ g i x * (List.map (fun x_1 ↦ g x_1 x) L).prod

Tactic:
| inl hi =>

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
⊢ rexp |x| ≤ rexp x + rexp (-x)

Tactic:
by
  cases le_total x 0 <;> simp [abs_of_nonpos, abs_of_nonneg, exp_nonneg, *]

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x

Tactic:
rw [← h1, cosh_add x (2 * x)]

Goal state after:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * cosh (2 * x) + sinh x * sinh (2 * x) = 4 * cosh x ^ 3 - 3 * cosh x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos (-x) = cos x

Tactic:
simp [cos, exp_neg, add_comm]

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ (cexp x).re = Real.exp x.re * Real.cos x.im

Tactic:
rw [exp_eq_exp_re_mul_sin_add_cos]
  simp [exp_ofReal_re, cos_ofReal_re]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
C : ℝ
hC : 0 ≤ C
⊢ IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun x ↦ f x i) g'

Tactic:
by
  have this (x) : 0 ≤ C * ‖g' x‖ := by positivity
  simp only [isBigOWith_iff, pi_norm_le_iff_of_nonneg (this _), eventually_all]

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ ↑(cos x - cos y) = ↑(-2 * sin ((x + y) / 2) * sin ((x - y) / 2))

Tactic:
simp [cos_sub_cos]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case inr.succ
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
have kn : k + n.succ ≥ n.succ := by
      rw [← zero_add n.succ]; exact add_le_add (Nat.zero_le _) (by simp)

Goal state after:
case inr.succ
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inr
x : ℝ
hx : |x| ≤ π
h : 0 ≤ x
⊢ |sin x| = sin |x|

Tactic:
· rw [abs_of_nonneg h, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi h (abs_le.1 hx).2)]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} / ball 1 δ = ball x δ

Tactic:
rw [singleton_div_ball, div_one]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ infDist (-m) (-↑S) = ⨅ a, ‖m + ↑a‖

Tactic:
neg_coe_set (H := S),

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ infDist (-m) ↑S = ⨅ a, ‖m + ↑a‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 4) = √2 / 2

Tactic:
by
  trans cos (π / 2 ^ 2)
  · congr
    norm_num
  · simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
⊢ (fun x ↦ ‖x‖) ⁻¹' (fun x ↦ x * r) '' id '' Ioo a b = ball 0 (b * r) \ closedBall 0 (a * r)

Tactic:
image_id,

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
⊢ (fun x ↦ ‖x‖) ⁻¹' (fun x ↦ x * r) '' Ioo a b = ball 0 (b * r) \ closedBall 0 (a * r)