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: α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
⊢ AnalyticSet (⋂ n, s n)

Tactic:
have t_closed : IsClosed t := by
    apply isClosed_iInter
    intro n
    exact
      isClosed_eq ((f_cont n).comp (continuous_apply n)) ((f_cont i₀).comp (continuous_apply i₀))

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝²] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed[Pi.topologicalSpace] t
⊢ AnalyticSet (⋂ n, s n)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∈ s
⊢ (dirac a) s = s.indicator 1 a

Tactic:
dirac_apply_of_mem h,

Goal state after:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∈ s
⊢ 1 = s.indicator 1 a
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∉ s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Tactic:
· have : s ∩ {a} = ∅ := inter_singleton_eq_empty.2 ha
    simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : Nonempty α
⊢ count ≠ 0

Tactic:
rintro h; simpa using congr($h .univ)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Subsingleton α
i : α
⊢ count.restrict univ = count.restrict {i}

Tactic:
congr; ext j; simp [Subsingleton.elim j i]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
mα : MeasurableSpace α✝
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (b.1 + b.2) s

Tactic:
Measure.coe_add,

Goal state after:
α✝ : Type u_1
β : Type u_2
mα : MeasurableSpace α✝
mβ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (⇑b.1 + ⇑b.2) s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Fintype α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α) in ↑Finset.univ, f x ∂μ

Tactic:
Finset.coe_univ,

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Fintype α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α) in univ, f x ∂μ
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 ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst✝⁴] u
v_open : IsOpen[inst✝³] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ 0 < (μ.prod ν) (u ×ˢ v)

Tactic:
simp only [prod_prod, CanonicallyOrderedAdd.mul_pos]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁵ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst✝¹ : ν.IsOpenPosMeasure
inst✝ : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst✝⁴] u
v_open : IsOpen[inst✝³] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ 0 < μ u ∧ 0 < ν v
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 ν✝
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ IsFiniteMeasure (μ.prod ν)

Tactic:
by
  constructor
  rw [← univ_prod_univ, prod_prod]
  finiteness

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : (hSK.equiv g₁).1 = (hSK.equiv g₂).1
⊢ (↑(hSK.equiv g₁).1 * ↑(hSK.equiv g₁).2)⁻¹ * (↑(hSK.equiv g₂).1 * ↑(hSK.equiv g₂).2) ∈ K

Tactic:
← h,

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : (hSK.equiv g₁).1 = (hSK.equiv g₂).1
⊢ (↑(hSK.equiv g₁).1 * ↑(hSK.equiv g₁).2)⁻¹ * (↑(hSK.equiv g₁).1 * ↑(hSK.equiv g₂).2) ∈ K
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ ↑(hHT.equiv g₂).1 * ↑(hHT.equiv g₂).2 * (↑(hHT.equiv g₁).1 * ↑(hHT.equiv g₁).2)⁻¹ ∈ H

Tactic:
← h,

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ ↑(hHT.equiv g₂).1 * ↑(hHT.equiv g₁).2 * (↑(hHT.equiv g₁).1 * ↑(hHT.equiv g₁).2)⁻¹ ∈ H
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ A
HA : μ A < ∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
⊢ A = A ∩ ⋃ i, s i

Tactic:
univ_subset_iff.mp h'',

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ A
HA : μ A < ∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
⊢ A = A ∩ univ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
⊢ μ = ν

Tactic:
ext s hs
  have h_univ : μ univ = ν univ := by
    simp_rw [← univ_prod_univ]
    exact h .univ .univ .univ
  have : IsFiniteMeasure ν := ⟨by simp [← h_univ]⟩
  let C₂ := image2 (· ×ˢ ·) { t : Set β | MeasurableSet t } { u : Set γ | MeasurableSet u }
  let C := image2 (· ×ˢ ·) { s : Set α | MeasurableSet s } C₂
  refine MeasurableSpace.induction_on_inter (s := C) ?_ ?_ (by simp) ?_ ?_ ?_ s hs
  · refine (generateFrom_eq_prod (C := { s : Set α | MeasurableSet s }) (D := C₂) (by simp)
      generateFrom_prod isCountablySpanning_measurableSet ?_).symm
    exact isCountablySpanning_measurableSet.prod isCountablySpanning_measurableSet
  · exact MeasurableSpace.isPiSystem_measurableSet.prod isPiSystem_prod
  · rintro - ⟨s, hs, -, ⟨t, ht, u, hu, rfl⟩, rfl⟩
    exact h hs ht hu
  · intro t ht h
    simp_rw [measure_compl ht (measure_ne_top _ _), h, h_univ]
  · intro f h_disj hf h_eq
    simp_rw [measure_iUnion h_disj hf, h_eq]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
⊢ H.IsComplement' (MulAction.stabilizer G a)

Tactic:
refine isComplement_iff_existsUnique.mpr fun g => ?_

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
⊢ ∃! x, ↑x.1 * ↑x.2 = g
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
g : G
h : ↥H
hh : h • g • a = a
hh' : (↑h * g) • a = a
⊢ ∀ (y : ↑↑H × ↑↑(MulAction.stabilizer G a)), (fun x ↦ ↑x.1 * ↑x.2 = g) y → y = (h⁻¹, ⟨↑h * g, hh'⟩)

Tactic:
rintro ⟨h', g, hg : g • a = a⟩ rfl

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
h : ↥H
h' : ↑↑H
g : G
hg : g • a = a
hh : h • (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2) • a = a
hh' : (↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2)) • a = a
⊢ (h', ⟨g, hg⟩) = (h⁻¹, ⟨↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2), hh'⟩)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ F ∩ univ = F

Tactic:
Set.inter_univ

Goal state after:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ F = F
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 μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y ↦ μ ((fun x ↦ (x, y)) ⁻¹' (fun z ↦ (1, z.1 * z.2)) ⁻¹' univ ×ˢ s)
⊢ Measurable fun x ↦ μ ((fun y ↦ y * x) ⁻¹' s)

Tactic:
by convert! this using 1; ext1 x; congr 1 with y : 1; simp

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

Goal state before:
pp: case succ
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 := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
IH : IsClosed[inst✝⁷] (L n)
⊢ IsClosed[inst✝⁷] (L (n + 1))

Tactic:
simp_rw [L, iterate_succ']
      apply IsClosed.union IH (Kclosed.smul (g (L n)))

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
⊢ ∀ (i : Set α), K ⊆ i → IsOpen[inst✝⁴] i → μ K ≤ μ i

Tactic:
exact fun U KU _ ↦ measure_mono KU

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
μ✝ : Measure α
X : Type u_3
inst✝⁵ : TopologicalSpace X
inst✝⁴ : PseudoMetrizableSpace X
inst✝³ : SigmaCompactSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
⊢ μ.Regular

Tactic:
exact ⟨(InnerRegularWRT.isCompact_isClosed μ).trans (InnerRegularWRT.of_pseudoMetrizableSpace μ)⟩

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✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
⊢ QuasiMeasurePreserving Inv.inv μ μ

Tactic:
← μ.inv_inv

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
⊢ QuasiMeasurePreserving Inv.inv μ.inv.inv μ.inv.inv
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✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ QuasiMeasurePreserving (fun h ↦ g / h) μ μ

Tactic:
← μ.inv_inv

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ QuasiMeasurePreserving (fun h ↦ g / h) μ.inv.inv μ.inv.inv
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ

Tactic:
by simp only [edist_zero_right]

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), 0 < a * (x * x) + b * x + c
⊢ discrim a b c < 0

Tactic:
by
  have : ∀ x : K, 0 ≤ a * (x * x) + b * x + c := fun x => le_of_lt (h x)
  refine lt_of_le_of_ne (discrim_le_zero this) fun h' ↦ ?_
  have := h (-b / (2 * a))
  have : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0 := by
    rw [mul_assoc, quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]
  linarith

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : √x = y
⊢ x = y * y

Tactic:
← h,

Goal state after:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : √x = y
⊢ x = √x * √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∞ := ⋯
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ‖F n a - f a‖ ≤ ‖F n a‖ + ‖f a‖

Tactic:
apply norm_sub_le

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqConj f).lim.im = ((starRingEnd ℂ) f.lim).im

Tactic:
by simp [cauSeqConj, (lim_im _).symm, cauSeqIm, (lim_neg _).symm]; rfl

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : MeasurableSet s
hf_ne_zero : μ {a | f a = 0} = 0
hμs : μ {a | a ∈ s ∧ ¬f a = 0} = 0
hle : s ⊆ {a | a ∈ s ∧ ¬f a = 0} ∪ {a | f a = 0}
⊢ μ s = 0

Tactic:
exact measure_mono_null hle <| nonpos_iff_eq_zero.1 <| le_trans (measure_union_le _ _)
    <| hμs.symm ▸ zero_add _ |>.symm ▸ hf_ne_zero.le

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

Goal state before:
pp: z w : ℂ
⊢ ¬z.re < w.re ∨ ¬z.im = w.im ↔ w.re ≤ z.re ∨ z.im ≠ w.im

Tactic:
not_lt

Goal state after:
z w : ℂ
⊢ w.re ≤ z.re ∨ ¬z.im = w.im ↔ w.re ≤ z.re ∨ z.im ≠ w.im
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z : ℂ
⊢ z.re = -‖z‖ ↔ z ≤ 0

Tactic:
rw [← neg_eq_iff_eq_neg, neg_re_eq_norm]

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

Goal state before:
pp: case a
α : Type u_1
q : ℚ≥0
⊢ (↑q).re = (↑q.num / ↑q.den).re

Tactic:
simp [NNRat.cast_def, div_re, div_im, mul_div_mul_comm]

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

Goal state before:
pp: case a
α : Type u_1
q : ℚ≥0
⊢ (↑q).im = (↑q.num / ↑q.den).im

Tactic:
simp [NNRat.cast_def, div_re, div_im, mul_div_mul_comm]

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

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

Tactic:
simp only [I_re, zero_sub, I_im', zero_mul, mul_re]

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

Goal state before:
pp: z : ℂ
⊢ ‖equivRealProd z‖ ≤ ‖z‖

Tactic:
simp [Prod.norm_def, abs_re_le_norm, abs_im_le_norm]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ adjoin ℝ (⇑(liftAux I' hI') '' {I}) = ℝ[I']

Tactic:
Set.image_singleton,

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ ℝ[(liftAux I' hI') I] = ℝ[I']
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x

Tactic:
exact ⟨x / ‖x‖, by simp [norm_ne_zero_iff.2, hx]⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : RCLike K
n : ℕ
inst✝ : n.AtLeastTwo
z : K
⊢ re (OfNat.ofNat n * z) = OfNat.ofNat n * re z

Tactic:
rw [← ofReal_ofNat, re_ofReal_mul]

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
hx : x ∈ e.source
x' : X
hx' : ↑e.symm (↑e x') = x'
h : ↑e x' = ↑e x
⊢ x' = ↑e.symm (↑e x)

Tactic:
← h,

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
x' : X
hx' : ↑e.symm (↑e x') = x'
h : ↑e x' = ↑e x
⊢ x' = ↑e.symm (↑e x')
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
c : ℝ
f'' : α → E''
g'' : α → F''
l : Filter α
h : IsBigOWith c l f'' g''
x : α
hx : ‖f'' x‖ ≤ c * ‖g'' x‖
hg : g'' x = 0
⊢ ‖f'' x‖ ≤ 0

Tactic:
simpa [hg] using hx

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

Goal state before:
pp: x y : ℂ
⊢ (cexp x - cexp (-x)) * (cexp y + cexp (-y)) + 2 * cosh x * (cexp y - cexp (-y)) =
    2 * (cexp x * cexp y - cexp (-x) * cexp (-y))

Tactic:
two_cosh

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

Goal state before:
pp: x : ℂ
⊢ tan (x * I) = tanh x * I

Tactic:
by
  rw [tan, sin_mul_I, cos_mul_I, mul_div_right_comm, tanh_eq_sinh_div_cosh]

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

Goal state before:
pp: x : ℝ
⊢ ↑(sinh (2 * x)) = ↑(2 * sinh x * cosh x)

Tactic:
simp [sinh_two_mul]

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

Goal state before:
pp: n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
rm : ℝ
er : ↑m = rm
h : |rexp 1 - expNear m 1 ((a₁ - 1) * rm)| ≤ |1| ^ m / ↑m.factorial * (b₁ * rm)
⊢ |rexp 1 - expNear n 1 a₁| ≤ |1| ^ n / ↑n.factorial * b₁

Tactic:
subst er
  refine exp_approx_succ _ en _ _ ?_ h
  simp
  field_simp [show (m : ℝ) ≠ 0 by norm_cast; lia]
  simp

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

Goal state before:
pp: n : ℕ
t : ℝ
ht' : t ≤ ↑n
⊢ (1 - t / ↑n) ^ n ≤ rexp (-t)

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inl
t : ℝ
ht' : t ≤ ↑0
⊢ (1 - t / ↑0) ^ 0 ≤ rexp (-t)

case inr
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ (1 - t / ↑n) ^ n ≤ rexp (-t)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
⊢ ‖↑(Real.exp x)‖ = Real.exp x

Tactic:
exact Complex.norm_of_nonneg (le_of_lt (Real.exp_pos _))

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ ¬a - (Nat.find h).pred • ε < f i
⊢ ∃ i, ∀ j ≥ i, |f j - f i| < ε

Tactic:
not_lt

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
⊢ ∃ i, ∀ j ≥ i, |f j - f i| < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: b c : ℝ
n : ℕ
hb : 0 < b
⊢ Tendsto (fun x ↦ (b * rexp x + c) / x ^ n) atTop atTop

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inl
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ (b * rexp x + c) / x ^ 0) atTop atTop

case inr
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x ↦ (b * rexp x + c) / x ^ n) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: k : ℕ
r : ℝ
hr : 0 < r
⊢ -r < 0

Tactic:
neg_lt_zero

Goal state after:
k : ℕ
r : ℝ
hr : 0 < r
⊢ 0 < r
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = cthickening δ s

Tactic:
hs.cthickening_eq_biUnion_closedBall hδ

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = ⋃ x ∈ s, closedBall x δ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cexp (↑π / 2 * I) = I

Tactic:
rw [← cos_add_sin_I, cos_pi_div_two, sin_pi_div_two, one_mul, zero_add]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

Tactic:
simp_rw [sub_eq_add_neg, neg_ball, ball_add_ball hε hδ]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ 𝓝 f = ⨅ s, ⨅ (_ : IsCompact s), comap (restrict s) (𝓝 (restrict s f))

Tactic:
rw [compactOpen_eq_iInf_induced]
  simp only [nhds_iInf, nhds_induced]

Goal state after: