mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous[inst✝¹, inst✝²] f
h✝ : Nonempty β
⊢ AnalyticSet (range f)

Tactic:
rw [AnalyticSet]
    obtain ⟨g, g_cont, hg⟩ : ∃ g : (ℕ → ℕ) → β, Continuous g ∧ Surjective g :=
      exists_nat_nat_continuous_surjective β
    refine Or.inr ⟨f ∘ g, f_cont.comp g_cont, ?_⟩
    rw [hg.range_comp]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : AnalyticSet s
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous[_, inst✝] f ∧ range f = s

Tactic:
rw [AnalyticSet] at h

Goal state after:
case mp
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅ ∨ ∃ f, Continuous[_, inst✝] f ∧ range f = s
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous[_, inst✝] f ∧ range f = s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : s = ∅
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous[_, inst✝] f ∧ range f = s

pp: case mp.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : ∃ f, Continuous[_, inst✝] f ∧ range f = s
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous[_, inst✝] f ∧ range f = s

Tactic:
· refine ⟨Empty, inferInstance, inferInstance, Empty.elim, continuous_bot, ?_⟩
      rw [h]
      exact range_eq_empty _

Goal state after:
case mp.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : ∃ f, Continuous[_, inst✝] f ∧ range f = s
⊢ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous[_, inst✝] f ∧ range f = s
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < μ s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ μ sᶜ < 1 - p

Tactic:
· rw [prob_compl_eq_one_sub s_mble]
    apply ENNReal.sub_lt_of_sub_lt prob_le_one (Or.inl one_ne_top)
    convert! hμs
    exact ENNReal.sub_sub_cancel one_ne_top (lt_of_lt_of_le hμs prob_le_one).le

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

Goal state before:
pp: case e_f
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
a : α
⊢ μ (t ∩ {a}) = μ {a} • (dirac a) t

Tactic:
by_cases ha : a ∈ t

Goal state after:
case pos
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
a : α
ha : a ∈ t
⊢ μ (t ∩ {a}) = μ {a} • (dirac a) t

case neg
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
a : α
ha : a ∉ t
⊢ μ (t ∩ {a}) = μ {a} • (dirac a) t
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : μ = ∑ a ∈ s, μ {a} • dirac a
⊢ ∀ᵐ (a : α) ∂∑ a ∈ s, μ {a} • dirac a, a ∈ s

Tactic:
ae_finsetSum_measure_iff

Goal state after:
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : μ = ∑ a ∈ s, μ {a} • dirac a
⊢ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ {i} • dirac i, x ∈ s
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: case succ
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * ε)) ≤ ↑C ^ n * μ (closedBall x ε)
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ (n + 1) * ε)) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)

Tactic:
replace ihn := eventually_nhdsGT_zero_mul_left (two_pos : 0 < (2 : ℝ)) ihn

Goal state after:
case succ
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ (n + 1) * ε)) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
⊢ ∀ {f : α × β → ℝ≥0∞}, Measurable f → Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν

Tactic:
by
  have m := @measurable_prodMk_left
  refine Measurable.ennreal_induction (motive := fun f ↦ Measurable fun (x : α) ↦ ∫⁻ y, f (x, y) ∂ν)
    ?_ ?_ ?_
  · intro c s hs
    simp only [← indicator_comp_right]
    suffices Measurable fun x => c * ν (Prod.mk x ⁻¹' s) by simpa [lintegral_indicator (m hs)]
    exact (measurable_measure_prodMk_left hs).const_mul _
  · rintro f g - hf - h2f h2g
    simp only [Pi.add_apply]
    conv => enter [1, x]; erw [lintegral_add_left (hf.comp m)]
    exact h2f.add h2g
  · intro f hf h2f h3f
    have : ∀ x, Monotone fun n y => f n (x, y) := fun x i j hij y => h2f hij (x, y)
    conv => enter [1, x]; erw [lintegral_iSup (fun n => (hf n).comp m) (this x)]
    exact .iSup h3f

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
g : G
x✝ : g ∈ ⊤
⊢ g ∈ H ⊔ K

Tactic:
obtain ⟨⟨h, k⟩, rfl⟩ := h.2 g

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h✝ : H.IsComplement' K
h : ↑↑H
k : ↑↑K
x✝ : (fun x ↦ ↑x.1 * ↑x.2) (h, k) ∈ ⊤
⊢ (fun x ↦ ↑x.1 * ↑x.2) (h, k) ∈ H ⊔ K
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.prod ν) s = ∫⁻ (y : β), μ ((fun x ↦ (x, y)) ⁻¹' s) ∂ν

Tactic:
rw [← prod_swap, map_apply measurable_swap hs, prod_apply (measurable_swap hs)]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), μ (Prod.mk x ⁻¹' Prod.swap ⁻¹' s) ∂ν = ∫⁻ (y : β), μ ((fun x ↦ (x, y)) ⁻¹' s) ∂ν
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
⊢ map (⇑MeasurableEquiv.prodAssoc) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ)

Tactic:
by
  have : sum (fun (p : ℕ × ℕ × ℕ) ↦
        (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)))
      = sum (fun (p : (ℕ × ℕ) × ℕ) ↦
        (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))) := by
    ext s hs
    rw [sum_apply _ hs, sum_apply _ hs, ← (Equiv.prodAssoc _ _ _).tsum_eq]
    simp only [Equiv.prodAssoc_apply]
  rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, ← sum_sfiniteSeq τ, prod_sum, prod_sum,
    map_sum MeasurableEquiv.prodAssoc.measurable.aemeasurable, prod_sum, prod_sum, this]
  congr
  ext1 i
  refine (prod_eq_generateFrom generateFrom_measurableSet generateFrom_prod
    isPiSystem_measurableSet isPiSystem_prod ((sfiniteSeq μ i.1.1)).toFiniteSpanningSetsIn
    ((sfiniteSeq ν i.1.2).toFiniteSpanningSetsIn.prod (sfiniteSeq τ i.2).toFiniteSpanningSetsIn)
      ?_).symm
  rintro s hs _ ⟨t, ht, u, hu, rfl⟩; rw [mem_ofPred_eq] at hs ht hu
  simp_rw [map_apply (MeasurableEquiv.measurable _) (hs.prod (ht.prod hu)),
    MeasurableEquiv.prodAssoc, MeasurableEquiv.coe_mk, Equiv.prod_assoc_preimage, prod_prod,
    mul_assoc]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CocompactMap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ⇑f
⊢ Tendsto (⇑f) (cocompact α) (cocompact β)

Tactic:
exact f.cocompact_tendsto'

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
⊢ MeasurableSet (f '' s)

Tactic:
rcases exists_opensMeasurableSpace_of_countablySeparated α with ⟨τ, _, _, _⟩

Goal state after:
γ : Type u_3
α : Type u_4
inst✝³ : MeasurableSpace α
s : Set γ
f : γ → α
inst✝² : MeasurableSpace.CountablySeparated α
inst✝¹ : MeasurableSpace γ
inst✝ : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
right✝ : OpensMeasurableSpace α
⊢ MeasurableSet (f '' s)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 ↦ f x_1 x) l ×ˢ map (fun x_1 ↦ f x_1 x) l).HasAntitoneBasis fun n ↦
      ((fun x_1 ↦ f x_1 x) '' u n) ×ˢ ((fun x_1 ↦ f x_1 x) '' u n)
⊢ MeasurableSet
    (⋂ i,
      ⋂ (_ : True),
        {x |
          ∃ i_2, True ∧ ((fun n ↦ f n x) '' u i_2) ×ˢ ((fun n ↦ f n x) '' u i_2) ⊆ {p | dist p.1 p.2 < 1 / (↑i + 1)}})

Tactic:
refine MeasurableSet.biInter Set.countable_univ fun K _ => ?_

Goal state after:
case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 ↦ f x_1 x) l ×ˢ map (fun x_1 ↦ f x_1 x) l).HasAntitoneBasis fun n ↦
      ((fun x_1 ↦ f x_1 x) '' u n) ×ˢ ((fun x_1 ↦ f x_1 x) '' u n)
K : ℕ
x✝ : K ∈ fun i ↦ True
⊢ MeasurableSet
    {x | ∃ i, True ∧ ((fun n ↦ f n x) '' u i) ×ˢ ((fun n ↦ f n x) '' u i) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}}
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ ρ.snd univ = ρ univ

Tactic:
by rw [snd_apply MeasurableSet.univ, preimage_univ]

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

Goal state before:
pp: case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst✝⁴] U), μ U ≤ μ K

Tactic:
apply le_of_forall_gt
    simpa only [iInf_lt_iff, exists_prop, exists_and_left] using hK.exists_isOpen_lt_of_lt

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
h1 : μ s = 0 ∨ ν univ = 0
⊢ μ s = 0

Tactic:
measure_univ_eq_zero.not.mpr hν,

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
h1 : μ s = 0 ∨ False
⊢ μ s = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous[inst✝⁴, inst✝¹] f
s : Set β
hs : MeasurableSet s
h's : (map f μ) s ≠ ∞
⊢ μ (f ⁻¹' s) ≠ ∞

Tactic:
rwa [map_apply hf.measurable hs] at h's

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

Goal state before:
pp: case mp.ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x

Tactic:
rw [EventuallyEq, ae_withDensity_iff' hf.coe_nnreal_ennreal] at hg'
      rw [ae_restrict_iff' A]
      filter_upwards [hg', hf'_ae] with a ha h'a h_a_nonneg
      have : (f' a : ℝ≥0∞) ≠ 0 := by simpa only [Ne, ENNReal.coe_eq_zero] using h_a_nonneg
      rw [← h'a] at this ⊢
      rw [ha this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
a : α
hn : 0 ≤ f a
ha : f a ≤ g a
⊢ ‖f a‖ ≤ ‖g a‖

Tactic:
apply norm_le_norm_of_abs_le_abs

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
a : α
hn : 0 ≤ f a
ha : f a ≤ g a
⊢ |f a| ≤ |g a|
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inr.inl.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
⊢ b * b - 4 * 0 * c ≤ 0

Tactic:
have := h ((-c - 1) / b)
      rw [mul_div_cancel₀ _ hb] at this
      linarith

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ b * b - 4 * a * c = -(4 * a * (a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c))

Tactic:
field

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ ↑(NNReal.sqrt x.toNNReal) * ↑(NNReal.sqrt x.toNNReal) = x

Tactic:
← NNReal.coe_mul,

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ ↑(NNReal.sqrt x.toNNReal * NNReal.sqrt x.toNNReal) = x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(NNReal.sqrt (x * y).toNNReal) = ↑(NNReal.sqrt x.toNNReal) * ↑(NNReal.sqrt y.toNNReal)

Tactic:
← NNReal.coe_mul,

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(NNReal.sqrt (x * y).toNNReal) = ↑(NNReal.sqrt x.toNNReal * NNReal.sqrt y.toNNReal)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: a : ℕ
⊢ ⌊√↑a⌋₊ = a.sqrt

Tactic:
rw [Nat.floor_eq_iff (sqrt_nonneg a)]
  exact ⟨nat_sqrt_le_real_sqrt, real_sqrt_lt_nat_sqrt_succ⟩

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

Goal state before:
pp: z : ℂ
hz : ¬z = 0
⊢ |z.re / ‖z‖| ≤ 1

Tactic:
abs_div,

Goal state after:
z : ℂ
hz : ¬z = 0
⊢ |z.re| / |‖z‖| ≤ 1
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : DistribMulAction ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
q : ℚ≥0
a : α
⊢ |q • a| = q • |a|

Tactic:
by
  obtain ha | ha := le_total a 0 <;>
    simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos]

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

Goal state before:
pp: ⊢ Monotone ofReal

Tactic:
intro x y hxy
  simp only [real_le_real, hxy]

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

Goal state before:
pp: z : ℂ
⊢ (z * (starRingEnd ℂ) z).re = (↑(normSq z)).re ∧ (z * (starRingEnd ℂ) z).im = (↑(normSq z)).im

Tactic:
by simp [normSq, mul_comm, sub_eq_neg_add, add_comm, ofReal]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ s.indicator f x = ∑' (i : ℕ), s.indicator 1 x

Tactic:
then

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: α : Type u_1
n : ℚ
z : ℂ
⊢ (n • z).re = (↑n * z).re ∧ (n • z).im = (↑n * z).im

Tactic:
by simp [Rat.smul_def, smul_re, smul_im]

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

Goal state before:
pp: a₁ a₂ b : ℝ
⊢ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]] = [[a₁, a₂]] ×ℂ {b}

Tactic:
rw [← preimage_equivRealProd_prod]
  ext x
  constructor
  · intro hx
    obtain ⟨x₁, hx₁, hx₁'⟩ := hx
    simp [← hx₁', mem_preimage, mem_prod, hx₁]
  · intro hx
    obtain ⟨x₁, hx₁, hx₁', hx₁''⟩ := hx
    refine ⟨x.re, x₁, by simp⟩

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

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ v ∈ f.ker ↔ f v = 0

Tactic:
by
  rw [ker, f.toAddMonoidHom.mem_ker, coe_toAddMonoidHom]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
x✝ : im z = 0
h : im z = 0 := x✝
| z

Tactic:
← re_add_im z,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
x✝ : im z = 0
h : im z = 0 := x✝
| ↑(re z) + ↑(im z) * I
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
hx : 0 ≤ x
⊢ ↑‖x‖ = x

Tactic:
by
  rw [← RCLike.ofReal_eq_complex_ofReal]
  exact RCLike.norm_of_nonneg' hx

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ |re z / ‖z‖| ≤ 1

Tactic:
abs_div,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |re z| / |‖z‖| ≤ 1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z / ‖z‖| ≤ 1

Tactic:
abs_div,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z| / |‖z‖| ≤ 1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
h : I = 0
z : K
⊢ im z = 0

Tactic:
← re_add_im z,

Goal state after:
K : Type u_1
inst✝ : RCLike K
h : I = 0
z : K
⊢ im (↑(re z) + ↑(im z) * I) = 0
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Finset.range n'.succ = Finset.cons n' (Finset.range n') ⋯

Tactic:
Finset.range_add_one,

Goal state after:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ insert n' (Finset.range n') = Finset.cons n' (Finset.range n') ⋯
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
c : S
hc : c ≠ 0
f : α → S
l : Filter α
⊢ IsBigOWith ‖c‖⁻¹ l f fun x ↦ c * f x

Tactic:
simp [IsBigOWith, inv_mul_cancel_left₀ (norm_ne_zero_iff.mpr hc)]

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

Goal state before:
pp: x : ℂ
⊢ cexp (-x) = (cexp x)⁻¹

Tactic:
by
  rw [← mul_right_inj' (exp_ne_zero x), ← exp_add]; simp

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

Goal state before:
pp: x y : ℂ
⊢ sinh (x - y) = sinh x * cosh y - cosh x * sinh y

Tactic:
simp [sub_eq_add_neg, sinh_add, sinh_neg, cosh_neg]

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

Goal state before:
pp: x : ℂ
⊢ cexp x * (cosh x - sinh x) = 1

Tactic:
cosh_sub_sinh,

Goal state after:
x : ℂ
⊢ cexp x * cexp (-x) = 1
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
⊢ f =O[l] g ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x / g x‖

Tactic:
by
  refine ⟨div_isBoundedUnder_of_isBigO, fun h => ?_⟩
  obtain ⟨c, hc⟩ := h
  simp only [eventually_map, norm_div] at hc
  refine IsBigO.of_bound c (hc.mp <| hgf.mono fun x hx₁ hx₂ => ?_)
  by_cases hgx : g x = 0
  · simp [hx₁ hgx, hgx]
  · exact (div_le_iff₀ (norm_pos_iff.2 hgx)).mp hx₂

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

Goal state before:
pp: case calc_1.e_a
x y : ℂ
⊢ x = (x + y) / 2 + (x - y) / 2

Tactic:
field

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

Goal state before:
pp: case calc_1.e_a
x y : ℂ
⊢ y = (x + y) / 2 - (x - y) / 2

Tactic:
field

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:
exp_eq_exp_re_mul_sin_add_cos

Goal state after:
x : ℂ
⊢ (cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).re = Real.exp x.re * Real.cos x.im
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
exp_eq_exp_re_mul_sin_add_cos

Goal state after:
x : ℂ
⊢ (cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).im = Real.exp x.re * Real.sin x.im
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ c, IsBigOWith c l (fun x ↦ f x * g x) h) ↔ ∃ c, IsBigOWith c l g fun x ↦ h x / f x

Tactic:
simp [isBigOWith_mul_iff_isBigOWith_div hf]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x ↦ f x * g x) h) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g fun x ↦ h x / f x

Tactic:
simp [isBigOWith_mul_iff_isBigOWith_div hf]

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

Goal state before:
pp: x y : ℝ
⊢ sinh (x - y) = sinh x * cosh y - cosh x * sinh y

Tactic:
simp [sub_eq_add_neg, sinh_add, sinh_neg, cosh_neg]

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

Goal state before:
pp: x : ℝ
⊢ tanh x < 1

Tactic:
rw [tanh_eq]
  field_simp
  grind [exp_pos]

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

Goal state before:
pp: x : ℝ
⊢ -1 < tanh x

Tactic:
rw [tanh_eq]
  field_simp
  grind [exp_pos]

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

Goal state before:
pp: n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m) = |x| ^ m * (↑m.succ / (↑m.factorial * ↑m))

pp: n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ 0 < m

Tactic:
· simp [field]

Goal state after:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ 0 < m
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case e'_3
n : ℕ
⊢ (1 + (↑n)⁻¹) ^ n = (1 - -1 / ↑n) ^ n

Tactic:
field

Goal state after: