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

Goal state before:
pp: case h₁
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ InjOn g (t \ t')

Tactic:
intro x

Goal state after:
case h₁
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
⊢ x ∈ t \ t' → ∀ ⦃x₂ : α⦄, x₂ ∈ t \ t' → g x = g x₂ → x = x₂
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : BorelSpace α
inst✝⁸ : LinearOrder α
inst✝⁷ : OrderTopology α
inst✝⁶ : PolishSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : LinearOrder β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := ⋯
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ ContinuousOn g (t \ t')

Tactic:
intro x

Goal state after:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹¹ : TopologicalSpace α
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : BorelSpace α
inst✝⁸ : LinearOrder α
inst✝⁷ : OrderTopology α
inst✝⁶ : PolishSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : LinearOrder β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
⊢ x ∈ t \ t' → ContinuousWithinAt g (t \ t') x
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case mp
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
⊢ x✝ ∈ ⇑f '' (fun x ↦ g * x) ⁻¹' s → x✝ ∈ (fun x ↦ f g * x) ⁻¹' ⇑f '' s

Tactic:
rintro ⟨y, hy, rfl⟩
        exact ⟨g * y, hy, by simp⟩

Goal state after:
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 μ
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ ∫⁻ (z : β × α), f z.swap ∂ν.prod μ = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν

Tactic:
exact lintegral_prod _ hf.prod_swap

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 μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y ↦ ((fun z ↦ z * x) ⁻¹' s).indicator (fun x ↦ 1) y
⊢ ∀ (x y : G), s.indicator (fun x ↦ 1) (y * x) = ((fun z ↦ z * x) ⁻¹' s).indicator (fun b ↦ 1) y

Tactic:
intro x

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y ↦ ((fun z ↦ z * x) ⁻¹' s).indicator (fun x ↦ 1) y
x : G
⊢ ∀ (y : G), s.indicator (fun x ↦ 1) (y * x) = ((fun z ↦ z * x) ⁻¹' s).indicator (fun b ↦ 1) y
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
⊢ s ⊆ t ∪ {x | f x = 0}

Tactic:
intro x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
⊢ x ∈ s → x ∈ t ∪ {x | f x = 0}
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mp.htc
α : 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:
ae_restrict_iff' A.compl

Goal state after:
case mp.htc
α : 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 : α) ∂μ, x ∈ {x | f' x ≠ 0}ᶜ → (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hfi : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (-f) μ

Tactic:
simpa [hasFiniteIntegral_iff_enorm] using hfi

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

Goal state before:
pp: α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hfi : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (fun x ↦ ‖f x‖ₑ) μ

Tactic:
simpa [hasFiniteIntegral_iff_enorm] using hfi

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 : α → β
hfi : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (fun a ↦ ‖f a‖) μ

Tactic:
simpa [hasFiniteIntegral_iff_enorm] using hfi

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
ha : a ≠ 0
h : ∀ (x : K), a * (x * x) + b * x + c < 0
⊢ ∀ (x : K), 0 < -a * (x * x) + -b * x + -c

Tactic:
simpa only [neg_mul, ← neg_add, neg_pos]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂μ.restrict {x | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
⊢ ∀ (a : α), g a = AEMeasurable.mk g hg a → (f' * g') a = (f' * g) a

Tactic:
intro x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂μ.restrict {x | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
x : α
⊢ g x = AEMeasurable.mk g hg x → (f' * g') x = (f' * g) x
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace β
μ : Measure α
inst✝³ : SemilatticeSup ι
inst✝² : Nonempty ι
inst✝¹ : Countable ι
f : ι → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
⊢ ∃ t, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ

Tactic:
by
  have ⟨t, _, ht, htendsto⟩ :=
    tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist hf MeasurableSet.univ
    (measure_ne_top μ Set.univ) (by filter_upwards [hfg] with _ htendsto _ using htendsto) hε
  refine ⟨_, ht, ?_⟩
  rwa [Set.compl_eq_univ_sdiff]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet {x | f' x ≠ 0}ᶜ
⊢ ∀ a ∈ {x | f' x ≠ 0}ᶜ, (f' * g') a = (f' * g) a

Tactic:
intro x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet {x | f' x ≠ 0}ᶜ
x : α
⊢ x ∈ {x | f' x ≠ 0}ᶜ → (f' * g') x = (f' * g) x
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∀ (a : α), f a = AEMeasurable.mk f hf a → (f' * g) a = (f * g) a

Tactic:
intro x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
x : α
⊢ f x = AEMeasurable.mk f hf x → (f' * g) x = (f * g) x
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
⊢ (fun x ↦ (f x)⁻¹ * i x) ≤ g

Tactic:
intro x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
x : α
⊢ (fun x ↦ (f x)⁻¹ * i x) x ≤ g x
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)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)

Tactic:
← ENNReal.ofReal_zero

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
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 (ENNReal.ofReal 0))
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
x : α
⊢ i x * (f x)⁻¹ ≤ g x

Tactic:
← div_eq_mul_inv

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
x : α
⊢ i x / f x ≤ g x
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
⊢ ∀ (a : α), f a < ∞ → i a ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) a

Tactic:
intro x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
⊢ f x < ∞ → i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∀ (a : α), f a < ∞ → f a = AEMeasurable.mk f hf a → AEMeasurable.mk f hf a < ∞

Tactic:
intro x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
x : α
⊢ f x < ∞ → f x = AEMeasurable.mk f hf x → AEMeasurable.mk f hf x < ∞
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∀ (a : α), f a = AEMeasurable.mk f hf a → (f' * g) a = (f * g) a

Tactic:
intro x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
x : α
⊢ f x = AEMeasurable.mk f hf x → (f' * g) x = (f * g) x
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: ⊢ Monotone ofReal

Tactic:
intro x

Goal state after:
x : ℝ
⊢ ∀ ⦃b : ℝ⦄, x ≤ b → ↑x ≤ ↑b
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ 1 / I = -I

Tactic:
div_I,

Goal state after:
⊢ -(1 * I) = -I
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ ‖-f‖ = ‖f‖

Tactic:
by
  simp only [norm_def, coe_neg, norm_neg, Pi.neg_apply]

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
⊢ Function.Involutive star

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x : ↥(unitary R)
⊢ star (star x) = x
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
⊢ ∀ (r s : ↥(unitary R)), star (r * s) = star s * star r

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x : ↥(unitary R)
⊢ ∀ (s : ↥(unitary R)), star (x * s) = star s * star x
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
⊢ f₂.comp (φ.comp (ι f₁ g₁)) = g₂.comp (φ.comp (ι f₁ g₁))

Tactic:
by
    simp only [← comp_assoc, ← hf, ← hg]
    simp only [comp_assoc, comp_ι_eq f₁ g₁]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : DivisionSemiring γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
⊢ ∑'[L] (i : β), g • f i = g • ∑'[L] (i : β), f i

Tactic:
rcases eq_or_ne g 0 with rfl | hg

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : DivisionSemiring γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
⊢ ∑'[L] (i : β), 0 • f i = 0 • ∑'[L] (i : β), f i

case inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : DivisionSemiring γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hg : g ≠ 0
⊢ ∑'[L] (i : β), g • f i = g • ∑'[L] (i : β), f i
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ (1 • x).re = x.re

Tactic:
simp [smul_re, smul_im, one_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ (1 • x).im = x.im

Tactic:
simp [smul_re, smul_im, one_smul]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (‖z‖ ^ 2)⁻¹ * re z = re z / ‖z‖ ^ 2

Tactic:
div_eq_inv_mul

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (‖z‖ ^ 2)⁻¹ * re z = (‖z‖ ^ 2)⁻¹ * re z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (‖z‖ ^ 2)⁻¹ * -im z = -im z / ‖z‖ ^ 2

Tactic:
div_eq_inv_mul

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (‖z‖ ^ 2)⁻¹ * -im z = (‖z‖ ^ 2)⁻¹ * -im z
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ Injective Subtype.val

Tactic:
exact Subtype.val_injective

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : Y → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (b : Y) in map (↑e) (𝓝[s] x), p b

Tactic:
rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.nhdsWithin_target_inter (e.mapsTo hx)]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ LipschitzWith 1 ⇑re

Tactic:
intro x

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ ∀ (y : K), edist (re x) (re y) ≤ ↑1 * edist x y
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ LipschitzWith 1 ⇑im

Tactic:
intro x

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ ∀ (y : K), edist (im x) (im y) ≤ ↑1 * edist x y
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (x y : ℝ), (algebraMap ℝ 𝕜) (x + y) = (algebraMap ℝ 𝕜) x + (algebraMap ℝ 𝕜) y

Tactic:
subst h''; exact h.algebraMap.map_add'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g ∧ g =O[l] f → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd) ∧ (g ∘ Prod.snd) =O[l' ×ˢ l] (f ∘ Prod.snd)

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.comp_snd l', h₂.comp_snd l'⟩

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂

Tactic:
exact forall₂_congr fun c _hc => isBigOWith_congr (Eq.refl c) hf hg

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
⊢ ∀ (a : α), a ∈ {x | (fun x ↦ ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x}

Tactic:
intro x

Goal state after:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
x : α
⊢ x ∈ {x | (fun x ↦ ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖) x}
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case refine_2
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : ∀ x ∈ s, f'' x = 0
⊢ f'' =o[𝓟 s] g'

Tactic:
apply (isLittleO_zero g' _).congr' ?_ EventuallyEq.rfl

Goal state after:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : ∀ x ∈ s, f'' x = 0
⊢ (fun _x ↦ 0) =ᶠ[𝓟 s] f''
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case hgf
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atTop
⊢ ∀ (x : α), 1 ≤ g x / f x → g x = 0 → f x = 0

Tactic:
intro x

Goal state after:
case hgf
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atTop
x : α
⊢ 1 ≤ g x / f x → g x = 0 → f x = 0
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (sinh ↑x).im = 0

Tactic:
rw [← ofReal_sinh_ofReal_re, ofReal_im]

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

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

Tactic:
← neg_sub,

Goal state after:
x : ℂ
⊢ -(cosh x - sinh x) = -cexp (-x)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
have h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2 := by ring

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
⊢ ∀ (x : α), C⁻¹ ≤ ((fun a ↦ ‖a‖) ∘ fun x ↦ g x / f x) x → ‖f x‖ ≤ C * ‖g x‖

Tactic:
intro x

Goal state after:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
⊢ C⁻¹ ≤ ((fun a ↦ ‖a‖) ∘ fun x ↦ g x / f x) x → ‖f x‖ ≤ C * ‖g x‖