mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst✝² : Encodable ι
inst✝¹ : (i : ι) → PseudoMetricSpace (Y i)
inst✝ : TopologicalSpace X
continuous_f : ∀ (i : ι), Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ Continuous[instTopologicalSpaceProd, _] fun x ↦ dist { ofPiNat := x.1 } { ofPiNat := x.2 }

Tactic:
simp only [dist_def]

Goal state after:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst✝² : Encodable ι
inst✝¹ : (i : ι) → PseudoMetricSpace (Y i)
inst✝ : TopologicalSpace X
continuous_f : ∀ (i : ι), Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ Continuous[instTopologicalSpaceProd, _] fun x ↦ ∑' (i : ι), min (2⁻¹ ^ encode i) (dist (f i x.1) (f i x.2))
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst✝² : Encodable ι
inst✝¹ : (i : ι) → PseudoMetricSpace (Y i)
inst✝ : TopologicalSpace X
continuous_f : ∀ (i : ι), Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toPiNat

Tactic:
by
  rw [continuous_iff_continuous_dist]
  simp only [dist_def]
  apply continuous_tsum (by fun_prop) summable_geometric_two_encode <| by simp [abs_of_nonneg]

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

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

Tactic:
rcases pow_unbounded_of_one_lt K one_lt_two with ⟨n, hn⟩
    use C ^ n
    filter_upwards [eventually_mem_nhdsWithin, this n] with ε hε₀ hε x t ht
    rw [mem_Ioi] at hε₀
    grw [ht, hn, ENNReal.coe_pow]
    exact hε x

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

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

Tactic:
induction n with
  | zero => simp
  | succ n ihn =>
    replace ihn := eventually_nhdsGT_zero_mul_left (two_pos : 0 < (2 : ℝ)) ihn
    filter_upwards [ihn, eventually_measure_le_doublingConstant_mul μ] with ε hεn hε x
    grw [pow_succ, mul_assoc, hεn, hε, ← mul_assoc, pow_succ]

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
⊢ μ (closedBall x (t * 0)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x 0)

Tactic:
simp only [mul_zero]

Goal state after:
case inr.inl
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
⊢ μ (closedBall x 0) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x 0)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⟨(0, fun x ↦ 0, fun x ↦ 0), ⋯⟩
p : ℕ → A := fun n ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.2 m = (↑(p (m + 1))).2.2 m
x : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.1 n
hx : x = fun n ↦ (↑(p (n + 1))).2.1 n
y : ℕ → ℕ := fun n ↦ (↑(p (n + 1))).2.2 n
hy : y = fun n ↦ (↑(p (n + 1))).2.2 n
M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n)
u v : Set α
u_open : IsOpen[inst✝³] u
v_open : IsOpen[inst✝³] v
xu : f x ∈ u
yv : g y ∈ v
huv : Disjoint u v
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
⊢ ∃ εx > 0, ball x εx ⊆ f ⁻¹' u

Tactic:
by
    apply Metric.mem_nhds_iff.1
    exact hf.continuousAt.preimage_mem_nhds (u_open.mem_nhds xu)

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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
μ ν : Measure M
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ IsFiniteMeasure (μ ∗ₘ ν)

Tactic:
have h : (μ ∗ₘ ν) Set.univ < ⊤ := by
    unfold mconv
    exact IsFiniteMeasure.measure_univ_lt_top
  exact { measure_univ_lt_top := h }

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
x : M
⊢ ν (HMul.hMul x ⁻¹' s) = 0

Tactic:
apply hν

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
x : M
⊢ ρ (HMul.hMul x ⁻¹' s) = 0
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
⊢ (∀ (g : G), ∃! t, Quotient.mk'' ↑t = Quotient.mk'' g) ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t, Quotient.mk'' ↑t = q

Tactic:
Quotient.forall

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

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < μ (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < μ K
hKrange : K ⊆ range f
⊢ f ⁻¹' K ⊆ U

Tactic:
rw [← hf.injective.preimage_image U]; exact preimage_mono hKU

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ (hST.equiv g).1 = ⟨g, hg⟩

Tactic:
have : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g := by
    rw [equiv, Equiv.ofBijective]; simp

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
this : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g
⊢ (hST.equiv g).1 = ⟨g, hg⟩
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', (∀ (n : ℕ), MeasurableSet (A' n)) ∧ (∀ (n : ℕ), A' n ⊆ s n) ∧ Pairwise (Disjoint on A') ∧ A = ⋃ n, A' n

Tactic:
refine
      ⟨fun n => A ∩ disjointed s n, fun n => hA.inter (MeasurableSet.disjointed hm _), fun n =>
        inter_subset_right.trans (disjointed_subset _ _),
        (disjoint_disjointed s).mono fun k l hkl => hkl.mono inf_le_right inf_le_right, ?_⟩

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 = ⋃ n, (fun n ↦ A ∩ disjointed s n) n
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
F : Type u_2
inst✝² : Group F
inst✝¹ : MulAction F G
inst✝ : QuotientAction F H
f : F
S : H.LeftTransversal
q : G ⧸ H
⊢ ↑(⋯.leftQuotientEquiv q) = f • ↑(⋯.leftQuotientEquiv (f⁻¹ • q))

Tactic:
rw [smul_leftQuotientEquiv, smul_inv_smul]

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

Goal state before:
pp: γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝¹ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this✝ : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
I : ∀ (m n : ℕ), (↑(s m) ∩ ↑(s n)).Nonempty
cauchy_y : CauchySeq y
this : Nonempty γ
z : γ := atTop.limUnder y
y_lim : Tendsto y atTop (𝓝 z)
hne : f z ≠ x
v w : Set β
v_open : IsOpen[inst✝³] v
w_open : IsOpen[inst✝³] w
fzv : f z ∈ v
xw : x ∈ w
hvw : Disjoint v w
⊢ ∃ δ > 0, ball z δ ⊆ f ⁻¹' v

Tactic:
apply Metric.mem_nhds_iff.1
      exact f_cont.continuousAt.preimage_mem_nhds (v_open.mem_nhds fzv)

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 μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : ν t ≠ 0
⊢ NullMeasurableSet (t ×ˢ s) (ν.prod μ)

Tactic:
← preimage_swap_prod

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : ν t ≠ 0
⊢ NullMeasurableSet (Prod.swap ⁻¹' s ×ˢ t) (ν.prod μ)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
x : α
y : β
⊢ map (fun x ↦ (x, y)) (dirac x) = dirac (x, y)

Tactic:
map_dirac' measurable_prodMk_right

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
x : α
y : β
⊢ dirac (x, y) = dirac (x, y)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Mul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
c : ℝ≥0∞
g : G
⊢ Measure.map (fun x ↦ x * g) (c • μ) = c • μ

Tactic:
by rw [Measure.map_smul, map_mul_right_eq_self]

Goal state after:
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 ν
ρ : Measure (α × β)
inst✝ : IsProbabilityMeasure ρ
⊢ ρ.snd univ = 1

Tactic:
rw [snd_univ]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsProbabilityMeasure ρ
⊢ ρ univ = 1
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✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hμs : μ s = 0
hf : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹)
⊢ ∫⁻ (y : G), μ (HMul.hMul y ⁻¹' s⁻¹ ∩ s) ∂μ = 0

Tactic:
measure_mono_null inter_subset_right hμs,

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hμs : μ s = 0
hf : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹)
⊢ ∫⁻ (y : G), 0 ∂μ = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ.withDensity f) {a | ¬p a} = 0 ↔ μ {a | ¬(f a ≠ 0 → p a)} = 0

Tactic:
withDensity_apply_eq_zero' hf,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ μ ({x | f x ≠ 0} ∩ {a | ¬p a}) = 0 ↔ μ {a | ¬(f a ≠ 0 → p a)} = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.WeaklyRegular
x : ℝ≥0∞
hx : x ≠ ∞
⊢ (x • μ).WeaklyRegular

Tactic:
have := OuterRegular.smul μ hx
  exact ⟨WeaklyRegular.innerRegular.smul x⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n a) (g a) < ε)} = 0
x : α
⊢ (x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, (↑n)⁻¹ < edist (f k x) (g x)) →
    x ∈ {a | a ∈ s ∧ ∃ ε > 0, ∀ (N : ι), ∃ n ≥ N, ε ≤ edist (f n a) (g a)}

Tactic:
rintro ⟨hmem, hx⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n a) (g a) < ε)} = 0
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, (↑n)⁻¹ < edist (f k x) (g x)
⊢ x ∈ {a | a ∈ s ∧ ∃ ε > 0, ∀ (N : ι), ∃ n ≥ N, ε ≤ edist (f n a) (g a)}
Module: Mathlib.MeasureTheory.Measure.WithDensity

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

Tactic:
let f' := hf.mk f

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ≥0
⊢ 0 < sqrt x ↔ 0 < x

Tactic:
by simp [pos_iff_ne_zero]

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

Goal state before:
pp: x y : ℝ
h : x ^ 2 ≤ y
⊢ |x| ≤ √y

Tactic:
by
  rw [← sqrt_sq_eq_abs]; exact sqrt_le_sqrt h

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}ᶜ
x : α
hx : f' x = 0
⊢ (f' * g') x = (f' * g) x

Tactic:
simp only [hx, zero_mul, Pi.mul_apply]

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

Goal state before:
pp: ⊢ (√2 - 1)⁻¹ = √2 + 1

Tactic:
by
  grind

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

Goal state before:
pp: x : ℝ
⊢ x / √x = √x

Tactic:
by
  grind

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

Goal state before:
pp: x : ℝ
⊢ x / √x / x = 1 / (x / √x)

Tactic:
one_div_div,

Goal state after:
x : ℝ
⊢ x / √x / x = √x / x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ x < √y ↔ x ^ 2 < y

Tactic:
by
  rw [← sqrt_lt_sqrt_iff (sq_nonneg _), sqrt_sq hx]

Goal state after:
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∞
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
let f' := hf.mk f

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
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : HasFiniteIntegral f μ
x : α
⊢ ‖max (f x) 0‖ ≤ ‖f x‖

Tactic:
simp [abs_le, le_abs_self]

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

Goal state before:
pp: α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace ε''
inst✝³ : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst✝² : NormedAddGroup 𝕜
inst✝¹ : SMul 𝕜 ε''
inst✝ : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
⊢ ∫⁻ (a : α), ‖(c • f) a‖ₑ ∂μ < ∞

Tactic:
calc
    ∫⁻ a : α, ‖c • f a‖ₑ ∂μ = ∫⁻ a : α, ‖c‖ₑ * ‖f a‖ₑ ∂μ := lintegral_congr fun i ↦ enorm_smul _ _
    _ < ∞ := by
      rw [lintegral_const_mul']
      exacts [mul_lt_top coe_lt_top hf, coe_ne_top]

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

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

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

Tactic:
· intro hx
    obtain ⟨x₁, hx₁, hx₁'⟩ := hx
    simp [← hx₁', mem_preimage, mem_prod, hx₁]

Goal state after:
case mpr
a₁ a₂ b : ℝ
x : ℂ
⊢ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b} → x ∈ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]]
Module: Mathlib.Data.Complex.Basic

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

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

Tactic:
· intro hx
    obtain ⟨x₁, hx₁, hx₁'⟩ := hx
    simp [← hx₁', mem_preimage, mem_prod, hx₁]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : ℝ
n : ℕ
⊢ im ↑(a ^ n) = 0

Tactic:
@ofReal_im_ax

Goal state after:
K : Type u_1
inst✝ : RCLike K
a : ℝ
n : ℕ
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
F : ℂ →ₐ[ℝ] A
⊢ F (I * I) = -1

Tactic:
I_mul_I,

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
F : ℂ →ₐ[ℝ] A
⊢ F (-1) = -1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : ℝ
⊢ (algebraMap ℝ ℝ) ((AddMonoidHom.id ℝ) z) + (algebraMap ℝ ℝ) (0 z) * 0 = z

Tactic:
simp only [add_zero, mul_zero, Algebra.algebraMap_self, RingHom.id_apply, AddMonoidHom.id_apply]

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : { x // x ∈ e.source }
⊢ map Subtype.val (𝓝 x) = map Subtype.val (comap Subtype.val (comap (↑e) (𝓝 (↑e ↑x))))

Tactic:
e.toHomeomorphSourceTarget.nhds_eq_comap,

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : { x // x ∈ e.source }
⊢ map Subtype.val (comap (⇑e.toHomeomorphSourceTarget) (𝓝 (e.toHomeomorphSourceTarget x))) =
    map Subtype.val (comap Subtype.val (comap (↑e) (𝓝 (↑e ↑x))))
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
⊢ ∀ (r s : 𝕜), star (r + s) = star r + star s

Tactic:
by subst h''; exact h.star_add

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
c : ℝ
hc : 0 < c
x : α
⊢ x ∈ {x | (fun x ↦ ‖0‖ ≤ c * ‖g' x‖) x}

Tactic:
simpa using mul_nonneg hc.le (norm_nonneg <| g' x)

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

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * (y ^ (m - I) * ((↑I.factorial)⁻¹ * ((↑(m - I).factorial)⁻¹ * 1))) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
simp [div_eq_mul_inv, mul_assoc, mul_left_comm]

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

Goal state before:
pp: x : ℂ
x✝ : ℕ
⊢ ↑(exp' ((starRingEnd ℂ) x)) x✝ = ↑(cauSeqConj (exp' x)) x✝

Tactic:
dsimp [exp', Function.comp_def, cauSeqConj]

Goal state after:
x : ℂ
x✝ : ℕ
⊢ ∑ m ∈ range x✝, (starRingEnd ℂ) x ^ m / ↑m.factorial = (starRingEnd ℂ) (∑ m ∈ range x✝, x ^ m / ↑m.factorial)
Module: Mathlib.Analysis.Complex.Trigonometric

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

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

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

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

Tactic:
I_mul_I,

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

Goal state before:
pp: x y : ℂ
⊢ cos x * cos y + sin x * sin y * (I * I) = cos x * cos y - sin x * sin y

Tactic:
I_mul_I,

Goal state after:
x y : ℂ
⊢ cos x * cos y + sin x * sin y * -1 = cos x * cos y - sin x * sin y
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: G : Type u_5
G' : Type u_8
inst✝³ : Norm G
inst✝² : SeminormedAddCommGroup G'
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → G
g : α → G'
⊢ (∃ c > 0, ∀ᶠ (x : α) in atTop, c * ‖f x‖ ≤ ‖g x‖) ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖

Tactic:
← exists_prop,

Goal state after:
G : Type u_5
G' : Type u_8
inst✝³ : Norm G
inst✝² : SeminormedAddCommGroup G'
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → G
g : α → G'
⊢ (∃ c, ∃ (_ : c > 0), ∀ᶠ (x : α) in atTop, c * ‖f x‖ ≤ ‖g x‖) ↔
    ∀ᶠ (n₀ : α) in atTop, ∃ c, ∃ (_ : c > 0), ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
Module: Mathlib.Analysis.Complex.Trigonometric

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

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

Goal state after: