mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
μ : Measure α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : MeasurableConstSMul G α
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ NullMeasurableSet (c • s) μ

Tactic:
simpa only [← preimage_smul_inv] using
    hs.preimage (measurePreserving_smul _ _).quasiMeasurePreserving

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

Goal state before:
pp: G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
⊢ (Measure.map (⇑f) μ).IsMulLeftInvariant

Tactic:
by
  refine ⟨fun h => ?_⟩
  rw [map_map (measurable_const_mul _) hf]
  obtain ⟨g, rfl⟩ := h_surj h
  conv_rhs => rw [← map_mul_left_eq_self μ g]
  rw [map_map hf (measurable_const_mul _)]
  congr 2
  ext y
  simp only [comp_apply, map_mul]

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
μ : Measure G
inst✝ : MeasurableInv G
⊢ count.inv = count

Tactic:
ext s hs; rw [count_apply hs, inv_apply, count_apply hs.inv, encard_inv]

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

Goal state before:
pp: case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
⊢ AEMeasurable (∏ i ∈ Finite.toFinset h✝, L.support.mulIndicator (fun i ↦ f i) i.down) μ

Tactic:
refine Finset.aemeasurable_prod _ (fun _ _ ↦ ?_)

Goal state after:
case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝
⊢ AEMeasurable (L.support.mulIndicator (fun i ↦ f i) x✝¹.down) μ
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.InnerRegular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ¬⨆ K, ⨆ (_ : K ⊆ univ), ⨆ (_ : IsCompact K), μ K = 0

Tactic:
ENNReal.iSup_eq_zero,

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.InnerRegular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ¬∀ i ⊆ univ, IsCompact i → μ i = 0
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
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (uncurry fun x y ↦ f (y * x) x⁻¹) (μ.prod ν)
⊢ ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ

Tactic:
lintegral_lintegral h2f,

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
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (uncurry fun x y ↦ f (y * x) x⁻¹) (μ.prod ν)
⊢ ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
⊢ (μ.withDensity f) t = 0

Tactic:
rw [measure_toMeasurable, hs]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
⊢ (c • μ).InnerRegularCompactLTTop

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
⊢ (c • μ).InnerRegularCompactLTTop

Tactic:
· constructor
    intro s hs r hr
    by_cases h's : μ s = 0
    · simp [h's] at hr
    · simp [h'c, h's] at hs

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
⊢ (c • μ).InnerRegularCompactLTTop
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ] g
a : α
ha : 0 = g a
h : {x | f x = 0} a
⊢ {x | g x = 0} a

Tactic:
exact ha.symm

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ¬⨆ K, ⨆ (_ : K ⊆ univ), ⨆ (_ : IsCompact K), μ K = 0

Tactic:
ENNReal.iSup_eq_zero,

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
⊢ (∃ K, IsCompact K ∧ ¬μ K = 0) ↔ ¬∀ i ⊆ univ, IsCompact i → μ i = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : 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}
a : α
ha : f a = f' a
ha_null✝ : a ∈ {x | f' x ≠ 0}ᶜ
ha_null : f' a = 0
⊢ ↑(f a) * g a = ↑(f' a) * g' a

Tactic:
rw [ha_null] at ha ⊢

Goal state after:
α : 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}
a : α
ha : f a = 0
ha_null✝ : a ∈ {x | f' x ≠ 0}ᶜ
ha_null : f' a = 0
⊢ ↑(f a) * g a = ↑0 * g' a
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)

Tactic:
by
  have F_le_bound := all_ae_norm_ofReal_F_le_bound h_bound
  rw [← ae_all_iff] at F_le_bound
  apply F_le_bound.mp ((ae_tendsto_ofReal_norm h_lim).mono _)
  intro a tendsto_norm F_le_bound
  exact le_of_tendsto' tendsto_norm F_le_bound

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

Goal state before:
pp: x : ℝ
⊢ √(x * x) = |x|

Tactic:
rw [← abs_mul_abs_self x, sqrt_mul_self (abs_nonneg _)]

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

Goal state before:
pp: case inl
x : ℝ
h✝ : x < 0
⊢ √x ^ 2 = max x 0

Tactic:
grind [sqrt_eq_zero', sq_sqrt]

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

Goal state before:
pp: case inr.inl
x : ℝ
h✝ : x = 0
⊢ √x ^ 2 = max x 0

Tactic:
grind [sqrt_eq_zero', sq_sqrt]

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

Goal state before:
pp: case inr.inr
x : ℝ
h✝ : 0 < x
⊢ √x ^ 2 = max x 0

Tactic:
grind [sqrt_eq_zero', sq_sqrt]

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)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal (‖F n a‖ + ‖f a‖)

Tactic:
apply ofReal_le_ofReal
          apply norm_sub_le

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

Goal state before:
pp: x : ℝ
h : -1 ≤ x
⊢ 1 + x + (x / 2) ^ 2 = (1 + x / 2) ^ 2

Tactic:
ring

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

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ a✝.re + b✝.re + c✝.re = a✝.re + (b✝.re + c✝.re)

Tactic:
ring

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

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ a✝.im + b✝.im + c✝.im = a✝.im + (b✝.im + c✝.im)

Tactic:
ring

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ = 1
this : z.im * z.im = 1 - z.re * z.re
⊢ (z.re - 1) * (z.re - 1) + (1 - z.re * z.re) = 2 * (1 - z.re)

Tactic:
ring

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

Goal state before:
pp: case a
n✝ : ℕ
x✝ : ℂ
⊢ (↑n✝ + 1) * x✝.re = ↑n✝ * x✝.re + x✝.re

Tactic:
ring

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

Goal state before:
pp: case a
n✝ : ℕ
x✝ : ℂ
⊢ (↑n✝ + 1) * x✝.im = ↑n✝ * x✝.im + x✝.im

Tactic:
ring

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

Goal state before:
pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝ + 1) * a✝.re = ↑n✝ * a✝.re + a✝.re

Tactic:
ring

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

Goal state before:
pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝ + 1) * a✝.im = ↑n✝ * a✝.im + a✝.im

Tactic:
ring

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

Goal state before:
pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (-1 + -↑n✝) * a✝.re = -((↑n✝ + 1) * a✝.re)

Tactic:
ring

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

Goal state before:
pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (-1 + -↑n✝) * a✝.im = -((↑n✝ + 1) * a✝.im)

Tactic:
ring

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

Goal state before:
pp: case a
a✝ b✝ : ℂ
⊢ a✝.re + b✝.re = b✝.re + a✝.re

Tactic:
ring

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

Goal state before:
pp: case a
a✝ b✝ : ℂ
⊢ a✝.im + b✝.im = b✝.im + a✝.im

Tactic:
ring

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

Goal state before:
pp: x y : ℝ
⊢ ↑x < ↑y ↔ x < y

Tactic:
simp [lt_def, ofReal]

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

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.re - (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.im =
    a✝.re * (b✝.re * c✝.re - b✝.im * c✝.im) - a✝.im * (b✝.re * c✝.im + b✝.im * c✝.re)

Tactic:
ring

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

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.im + (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.re =
    a✝.re * (b✝.re * c✝.im + b✝.im * c✝.re) + a✝.im * (b✝.re * c✝.re - b✝.im * c✝.im)

Tactic:
ring

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

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ a✝.re * (b✝.re + c✝.re) - a✝.im * (b✝.im + c✝.im) = a✝.re * b✝.re - a✝.im * b✝.im + (a✝.re * c✝.re - a✝.im * c✝.im)

Tactic:
ring

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

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ a✝.re * (b✝.im + c✝.im) + a✝.im * (b✝.re + c✝.re) = a✝.re * b✝.im + a✝.im * b✝.re + (a✝.re * c✝.im + a✝.im * c✝.re)

Tactic:
ring

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

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re + b✝.re) * c✝.re - (a✝.im + b✝.im) * c✝.im = a✝.re * c✝.re - a✝.im * c✝.im + (b✝.re * c✝.re - b✝.im * c✝.im)

Tactic:
ring

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

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re + b✝.re) * c✝.im + (a✝.im + b✝.im) * c✝.re = a✝.re * c✝.im + a✝.im * c✝.re + (b✝.re * c✝.im + b✝.im * c✝.re)

Tactic:
ring

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

Goal state before:
pp: case a
a✝ b✝ : ℂ
⊢ a✝.re * b✝.re - a✝.im * b✝.im = b✝.re * a✝.re - b✝.im * a✝.im

Tactic:
ring

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

Goal state before:
pp: case a
a✝ b✝ : ℂ
⊢ a✝.re * b✝.im + a✝.im * b✝.re = b✝.re * a✝.im + b✝.im * a✝.re

Tactic:
ring

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

Goal state before:
pp: case a
a b : ℂ
⊢ a.re * b.re - a.im * b.im = b.re * a.re - b.im * a.im

Tactic:
ring

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

Goal state before:
pp: case a
a b : ℂ
⊢ -(a.re * b.im) + -(a.im * b.re) = -(b.re * a.im) + -(b.im * a.re)

Tactic:
ring

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

Goal state before:
pp: z w : ℂ
⊢ (z.re * w.re - z.im * w.im) * (z.re * w.re - z.im * w.im) +
      (z.re * w.im + z.im * w.re) * (z.re * w.im + z.im * w.re) =
    (z.re * z.re + z.im * z.im) * (w.re * w.re + w.im * w.im)

Tactic:
ring

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

Goal state before:
pp: z w : ℂ
⊢ (z.re + w.re) * (z.re + w.re) + (z.im + w.im) * (z.im + w.im) =
    z.re * z.re + z.im * z.im + (w.re * w.re + w.im * w.im) + 2 * (z.re * w.re + z.im * w.im)

Tactic:
ring

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

Goal state before:
pp: z w : ℂ
⊢ normSq z + normSq w + -(2 * (z * (starRingEnd ℂ) w).re) = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re

Tactic:
ring

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ ↑(#s) • a ≤ ∑ i ∈ s, (fun i ↦ f i) i

Tactic:
by
    rw [Nat.cast_smul_eq_nsmul]; exact card_nsmul_le_sum _ _ _ h

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
f : ι → α
hf : f ≤ 0
⊢ 𝔼 i, f i = 0 ↔ f = 0

Tactic:
Finset.expect_eq_zero_iff_of_nonpos (by aesop)

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
f : ι → α
hf : f ≤ 0
⊢ (∀ i ∈ univ, f i = 0) ↔ f = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
⊢ automorphize (g ∘ Quotient.mk' • f) x = (g • automorphize f) x

Tactic:
induction x using Quotient.inductionOn with | _ b

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
⊢ automorphize (g ∘ Quotient.mk' • f) ⟦b⟧ = (g • automorphize f) ⟦b⟧
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x y : 𝕜
⊢ ↑(RCLike.re x) * ↑(RCLike.re y) + ↑(RCLike.re x) * ↑(RCLike.im y) * I + ↑(RCLike.re y) * ↑(RCLike.im x) * I -
      ↑(RCLike.im x) * ↑(RCLike.im y) =
    ↑(RCLike.re x) * ↑(RCLike.re y) + ↑(RCLike.re x) * ↑(RCLike.im y) * I + ↑(RCLike.re y) * ↑(RCLike.im x) * I +
      ↑(RCLike.im x) * ↑(RCLike.im y) * -1

Tactic:
ring

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x y : 𝕜
⊢ ↑(RCLike.re x) + ↑(RCLike.re y) + (↑(RCLike.im x) + ↑(RCLike.im y)) * I =
    ↑(RCLike.re x) + ↑(RCLike.im x) * I + (↑(RCLike.re y) + ↑(RCLike.im y) * I)

Tactic:
ring

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝¹ : ℝ
x✝ : 𝕜
⊢ ↑x✝¹ * ↑(RCLike.im x✝) * I = ↑x✝¹ * (↑(RCLike.im x✝) * I)

Tactic:
ring

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z✝ z w : K
⊢ (re z * re w - im z * im w) * (re z * re w - im z * im w) +
      (re z * im w + im z * re w) * (re z * im w + im z * re w) =
    (re z * re z + im z * im z) * (re w * re w + im w * im w)

Tactic:
ring

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z + re w) * (re z + re w) + (im z + im w) * (im z + im w) =
    re z * re z + im z * im z + (re w * re w + im w * im w) + 2 * (re z * re w - im z * -im w)

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace X'
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Y'
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace Z'
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
⊢ IsEmbedding ⇑(InjOn.toPartialEquiv f univ ⋯).toEquiv

Tactic:
rw [PartialEquiv.toEquiv_eq_codRestrict_restrict]

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace X'
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Y'
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace Z'
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
⊢ IsEmbedding
    (codRestrict ((InjOn.toPartialEquiv f univ ⋯).source.domRestrict ↑(InjOn.toPartialEquiv f univ ⋯))
      (InjOn.toPartialEquiv f univ ⋯).target ⋯)
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
hx : x ∈ e.source
⊢ Tendsto (↑e.symm) (𝓝 (↑e x)) (𝓝 x)

Tactic:
simpa only [ContinuousAt, e.left_inv hx] using e.continuousAt_symm (e.map_source hx)

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝² : RCLike K
𝕜 : Type u_3
𝕜' : Type u_4
inst✝¹ : RCLike 𝕜
inst✝ : RCLike 𝕜'
x✝¹ x✝ : 𝕜
⊢ (algebraMap ℝ 𝕜') (re x✝¹) + (algebraMap ℝ 𝕜') (re x✝) +
      ((algebraMap ℝ 𝕜') (im x✝¹) * I + (algebraMap ℝ 𝕜') (im x✝) * I) =
    ↑(re x✝¹) + ↑(im x✝¹) * I + (↑(re x✝) + ↑(im x✝) * I)

Tactic:
ring

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 =Θ[l] g → (f ∘ Prod.snd) =Θ[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
by
  simp only [IsTheta]
  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
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g → ∀ᶠ (a : α) in l, (fun x ↦ f (a, x)) =O[l'] fun x ↦ g (a, x)

Tactic:
simp only [isBigO_iff, eventually_iff, mem_prod_iff]
  rintro ⟨c, t₁, ht₁, t₂, ht₂, ht⟩
  exact mem_of_superset ht₁ fun _ ha ↦ ⟨c, mem_of_superset ht₂ fun _ hb ↦ ht ⟨ha, hb⟩⟩

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

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
⊢ ((c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f'' x‖) → f'' =O[l] fun _x ↦ c

Tactic:
rintro ⟨hcf, hf⟩

Goal state after:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f'' x‖
⊢ f'' =O[l] fun _x ↦ c
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i)
⊢ IsBigOWith (sSup (C '' ↑s)) l (fun H ↦ ∑ i ∈ s, A i H) fun H ↦ ∑ i ∈ s, ‖B i H‖

Tactic:
by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp [isBigOWith_zero]
  simp only [IsBigOWith_def] at *
  filter_upwards [(eventually_all_finset s).mpr hAB]
    with x hx
  calc
    ‖∑ i ∈ s, A i x‖ ≤ ∑ i ∈ s, ‖A i x‖ := norm_sum_le ..
    _ ≤ ∑ i ∈ s, C i * ‖B i x‖ := Finset.sum_le_sum (fun j hj ↦ hx j hj)
    _ ≤ ∑ i ∈ s, sSup (C '' s) * ‖B i x‖ := by
        refine Finset.sum_le_sum ?_
        intro j hj; gcongr
        rw [← s.sup'_eq_csSup_image hs, Finset.le_sup'_iff]; use j
    _ = sSup (C '' s) * ∑ i ∈ s, ‖B i x‖ := (Finset.mul_sum ..).symm
    _ = sSup (C '' s) * ‖∑ i ∈ s, ‖B i x‖‖ := by
      congr; rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]

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

Goal state before:
pp: a b c d : ℂ
⊢ (a - b) * (c + d) + (a + b) * (c - d) = 2 * (a * c - b * d)

Tactic:
ring

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

Goal state before:
pp: a b c d : ℂ
⊢ (a + b) * (c + d) + (a - b) * (c - d) = 2 * (a * c + b * d)

Tactic:
ring

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

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (cosh ↑x) = cosh ↑x

Tactic:
← cosh_conj,

Goal state after:
x : ℝ
⊢ cosh ((starRingEnd ℂ) ↑x) = cosh ↑x
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
rw [← ofReal_tanh_ofReal_re, ofReal_im]

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

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

Tactic:
cosh_add_sinh,

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

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

Tactic:
← exp_add,

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

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

Tactic:
ring

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

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

Tactic:
ring

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

Goal state before:
pp: x : ℂ
⊢ sinh x * cosh x + cosh x * sinh x = 2 * sinh x * cosh x

Tactic:
ring

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

Goal state before:
pp: x : ℂ
⊢ x + 2 * x = 3 * x

Tactic:
ring

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

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

Tactic:
ring

Goal state after: