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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
⊢ ∃ C, ∀ (n : ℕ), 1 / infDist (↑(u n)) (↑s)ᶜ < C

Tactic:
by
    refine ⟨(1 / 2) ^ 0 + 1 / infDist (u 0).1 sᶜ, fun n ↦ ?_⟩
    rw [← sub_lt_iff_lt_add]
    calc
      _ ≤ |1 / infDist (u n).1 sᶜ - 1 / infDist (u 0).1 sᶜ| := le_abs_self _
      _ = |1 / infDist (u 0).1 sᶜ - 1 / infDist (u n).1 sᶜ| := abs_sub_comm _ _
      _ ≤ dist (u 0) (u n) := le_add_of_nonneg_left dist_nonneg
      _ < (1 / 2) ^ 0 := hu 0 0 n le_rfl n.zero_le

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μa : Measure α
μb : Measure β
h : MeasurePreserving (⇑e) μa μb
⊢ map (⇑e.symm) μb = μa

Tactic:
by
    rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : β → ℝ≥0∞
g : α ≃ᵐ β
hg : MeasurePreserving (⇑g) μ ν
⊢ ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : β), f a ∂Measure.map (⇑g) μ

Tactic:
hg.map_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : β → ℝ≥0∞
g : α ≃ᵐ β
hg : MeasurePreserving (⇑g) μ ν
⊢ ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : β), f a ∂ν
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → t.indicator 1 a = 1
⊢ (dirac a) s ≤ univ.indicator 1 a

Tactic:
← dirac_apply' a MeasurableSet.univ

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → t.indicator 1 a = 1
⊢ (dirac a) s ≤ (dirac a) univ
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
⊢ (sum fun a ↦ μ {a} • dirac a) = μ

Tactic:
by simpa using (map_eq_sum μ id measurable_id).symm

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

Goal state before:
pp: case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s = (sᶜ ∩ h.nullSetᶜᶜ ∪ sᶜ ∩ h.nullSetᶜ)ᶜ

Tactic:
compl_compl,

Goal state after:
case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s = (sᶜ ∩ h.nullSet ∪ sᶜ ∩ h.nullSetᶜ)ᶜ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case refine_1
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
m : ι
⊢ s m ⊆ ⋂ n, u m n

Tactic:
exact subset_iInter fun n => hsu m n

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → ℝ≥0∞
c : ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x = c
⊢ ∫⁻ (x : α), f x ∂μ = c

Tactic:
simp [lintegral_congr_ae hf]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
t : Set α
hst : sᶜ ⊆ t
htm : MeasurableSet t
ht : (fun μ ↦ μ t) =ᵐ[m] 0
⊢ s ∈ (ae m).bind ae

Tactic:
mem_bind'

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
t : Set α
hst : sᶜ ⊆ t
htm : MeasurableSet t
ht : (fun μ ↦ μ t) =ᵐ[m] 0
⊢ {a | s ∈ ae a} ∈ ae m
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
⊢ ∃ n, ∀ (x : α), ψ x ≤ ↑n

Tactic:
rcases ψ.range.bddAbove with ⟨C, hC⟩
    exact ⟨⌈C⌉₊, fun x ↦ (hC <| ψ.mem_range_self x).trans (Nat.le_ceil _)⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
L : Tendsto (fun n ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
N : ℕ
y : ℕ → ℕ
hxy : y ∈ ball x ((1 / 2) ^ N)
ys : y ∈ s
E : ⋂ n, ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n) = ⋂ n, ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
⊢ (⋂ n, ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty

Tactic:
rw [E]

Goal state after:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
L : Tendsto (fun n ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
N : ℕ
y : ℕ → ℕ
hxy : y ∈ ball x ((1 / 2) ^ N)
ys : y ∈ s
E : ⋂ n, ⋂ (_ : n ≤ N), closedBall (u (x n)) ((1 / 2) ^ n) = ⋂ n, ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)
⊢ (⋂ n, ⋂ (_ : n ≤ N), closedBall (u (y n)) ((1 / 2) ^ n)).Nonempty
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m

Tactic:
lintegral_finsetSum (s n)

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∑ b ∈ s n, ∫⁻ (a : Measure α), b * f n b a ∂m

α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hfm : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∀ b ∈ s n, Measurable fun a ↦ b * f n b a
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
n : ℕ
hn : ∀ (x : α), ψ x ≤ ↑n
⊢ ∫⁻ (a : α) in s, min (f a) ↑n ∂μ ≤ ∫⁻ (a : α) in s, g n a ∂μ

Tactic:
by
      have : ∫⁻ a in (toMeasurable μ s)ᶜ, min (f a) n ∂μ ≠ ∞ :=
        IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal _ ⟨n, fun _ ↦ min_le_right ..⟩ |>.ne
      have hsm : MeasurableSet (toMeasurable μ s) := measurableSet_toMeasurable ..
      apply ENNReal.le_of_add_le_add_right this
      rw [← μ.restrict_toMeasurable_of_sFinite, lintegral_add_compl _ hsm, hgint,
        ← lintegral_add_compl _ hsm]
      gcongr with x
      exact le_min (hgf n x) (hgle n x)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : L < ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ ↑(f x)), (SimpleFunc.map ofNNReal φ).lintegral μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
lt_iSup_iff

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
L : ℝ≥0∞
hL : ∃ i, ∃ (_ : ∀ (x : α), ↑(i x) ≤ ↑(f x)), L < (SimpleFunc.map ofNNReal i).lintegral μ
⊢ ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
ϕ : ↥H × ↥K ≃ ↥K × ↥H :=
  { toFun := fun x ↦ (x.2⁻¹, x.1⁻¹), invFun := fun x ↦ (x.2⁻¹, x.1⁻¹), left_inv := ⋯, right_inv := ⋯ }
ψ : G ≃ G := { toFun := fun g ↦ g⁻¹, invFun := fun g ↦ g⁻¹, left_inv := ⋯, right_inv := ⋯ }
hf : (⇑ψ ∘ fun x ↦ ↑x.1 * ↑x.2) = (fun x ↦ ↑x.1 * ↑x.2) ∘ ⇑ϕ
⊢ K.IsComplement' H

Tactic:
rwa [isComplement'_def, isComplement_iff_bijective, ← Equiv.bijective_comp ϕ, ← hf,
      ψ.comp_bijective]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case e'_2.mpr
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x ↦ ↑x.1 * ↑x.2 = g) y → y = x
⊢ ∃! s, (↑s)⁻¹ * g ∈ T

Tactic:
· exact ⟨x.1, by simp [← hx], fun y hy ↦ (Prod.ext_iff.1 <| by simpa using hx' (y, ⟨_, hy⟩)).1⟩

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 ∈ S
⊢ g * (↑(hST.equiv g).2)⁻¹ = 1 ↔ g ∈ T

Tactic:
mul_inv_eq_one,

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
⊢ g = ↑(hST.equiv g).2 ↔ g ∈ T
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map (fun x ↦ (x, y)) (sfiniteSeq μ i)) (s ×ˢ t) = (sfiniteSeq μ i) s * (dirac y) t

Tactic:
simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, mul_one]

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

Goal state before:
pp: case pos.refine_1
α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
e : α ≃ β
h : Countable α
this : Countable β := Countable.of_equiv α e
⊢ Measurable ⇑e

Tactic:
apply measurable_of_countable

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

Goal state before:
pp: case pos.refine_2
α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
e : α ≃ β
h : Countable α
this : Countable β := Countable.of_equiv α e
⊢ Measurable ⇑e.symm

Tactic:
apply measurable_of_countable

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : Measurable g
⊢ μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g

Tactic:
by
  simpa only [add_comm] using withDensity_add_left hg f

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ ?m.55 t ≠ ∞

Tactic:
rwa [← measure_congr hst]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ] g
a : α
ha : f a = g a
⊢ {x | g x ≠ 0} a = {x | f x ≠ 0} a

Tactic:
simp only [eq_iff_iff]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ] g
a : α
ha : f a = g a
⊢ {x | g x ≠ 0} a ↔ {x | f x ≠ 0} a
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ
⊢ ∫⁻ (a : α), (fun x ↦ ⨆ n, g n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, g n x) a ∂μ

Tactic:
have : Monotone fun n a => f a * g n a := fun m n hmn x => by dsimp; grw [h_mono_g hmn x]

Goal state after:
case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ
this : Monotone fun n a ↦ f a * g n a
⊢ ∫⁻ (a : α), (fun x ↦ ⨆ n, g n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, g n x) a ∂μ
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: x : ℂ
⊢ (fun z ↦ { re := z.re, im := -z.im }) ((fun z ↦ { re := z.re, im := -z.im }) x) = x

Tactic:
by simp only [eta, neg_neg]

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

Goal state before:
pp: r : ℝ
n : ℕ
⊢ ↑(r ^ n) = ↑r ^ n

Tactic:
induction n

Goal state after:
case zero
r : ℝ
⊢ ↑(r ^ 0) = ↑r ^ 0

case succ
r : ℝ
n✝ : ℕ
a✝ : ↑(r ^ n✝) = ↑r ^ n✝
⊢ ↑(r ^ (n✝ + 1)) = ↑r ^ (n✝ + 1)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: m : ℤ
| I ^ m

Tactic:
rw [← Int.mul_ediv_add_emod m 4]

Goal state after:
m : ℤ
| I ^ (4 * (m / 4) + m % 4)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
x✝ : V₁
⊢ ‖0 x✝‖ = 0

Tactic:
exact norm_zero

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
⊢ 1 ∈ {U | star U * U = 1 ∧ U * star U = 1}

Tactic:
simp only [mul_one, and_self_iff, Set.mem_ofPred_eq, star_one]

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
    ext
    rw [coe_star, coe_star, star_star]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
x✝ : (starRingEnd K) z = z
h : (starRingEnd K) z = z := x✝
⊢ 0 / 2 = ↑0

Tactic:
zero_div,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
x✝ : (starRingEnd K) z = z
h : (starRingEnd K) z = z := x✝
⊢ 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 * F I = -1

Tactic:
rw [← map_mul, I_mul_I, map_neg, map_one]

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

Goal state before:
pp: n : ℕ
⊢ ↑n ∈ slitPlane ↔ n ≠ 0

Tactic:
by
  simpa [pos_iff_ne_zero] using @ofReal_mem_slitPlane n

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'
e : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ ContinuousOn f.invFun f.target

Tactic:
by
    rw [continuousOn_iff_continuous_domRestrict,
      ← continuous_codRestrict_iff (s := f.source) (by simp)]
    exact ((Equiv.isHomeomorph_iff _).1 h).2

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Opens X
hs : Nonempty ↥s
⊢ (s.openPartialHomeomorphSubtypeCoe hs).target = ↑s

Tactic:
simp [openPartialHomeomorphSubtypeCoe]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : 0 ≤ x
⊢ x = ↑‖x‖

Tactic:
← norm_le_re_iff_eq_norm,

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
hx : 0 ≤ x
⊢ ‖x‖ ≤ re 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
⊢ 𝕜 →+ ℝ

Tactic:
subst h''; exact h.im

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³⁶ : Semiring R
inst✝³⁵ : Semiring R₂
inst✝³⁴ : Semiring R₃
inst✝³³ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝³² : RingHomInvPair σ₁₂ σ₂₁
inst✝³¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝³⁰ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁹ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁸ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁷ : RingHomInvPair σ₃₂ σ₂₃
inst✝²⁶ : RingHomInvPair σ₁₄ σ₄₁
inst✝²⁵ : RingHomInvPair σ₄₁ σ₁₄
inst✝²⁴ : RingHomInvPair σ₂₄ σ₄₂
inst✝²³ : RingHomInvPair σ₄₂ σ₂₄
inst✝²² : RingHomInvPair σ₃₄ σ₄₃
inst✝²¹ : RingHomInvPair σ₄₃ σ₃₄
inst✝²⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁸ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁷ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹⁵ : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹⁴ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹³ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝¹² : SeminormedAddCommGroup E
inst✝¹¹ : SeminormedAddCommGroup E₂
inst✝¹⁰ : SeminormedAddCommGroup E₃
inst✝⁹ : SeminormedAddCommGroup E₄
inst✝⁸ : Module R E
inst✝⁷ : Module R₂ E₂
inst✝⁶ : Module R₃ E₃
inst✝⁵ : Module R₄ E₄
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module R F
e✝ : E ≃ₛₗᵢ[σ₁₂] E₂
α : Type u_11
inst✝² : TopologicalSpace α
inst✝¹ : Module R E₂
inst✝ : Module R E₃
g : E₃
e : E
f : E₂
⊢ ‖(LinearEquiv.prodAssoc R E E₂ E₃) ((e, f), g)‖ = ‖((e, f), g)‖

Tactic:
simp only [LinearEquiv.prodAssoc_apply, AddEquiv.toEquiv_eq_coe,
        Equiv.toFun_as_coe, EquivLike.coe_coe, AddEquiv.coe_prodAssoc,
        Equiv.prodAssoc_apply, Prod.norm_def, max_assoc]

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

Goal state before:
pp: case inl
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
c : E''
l : Filter α
inst✝ : l.NeBot
⊢ ((fun _x ↦ c) =O[l] fun _x ↦ 0) ↔ 0 = 0 → c = 0

pp: case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
c : E''
c' : F''
l : Filter α
inst✝ : l.NeBot
hc' : c' ≠ 0
⊢ ((fun _x ↦ c) =O[l] fun _x ↦ c') ↔ c' = 0 → c = 0

Tactic:
· simp [EventuallyEq]

Goal state after:
case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
c : E''
c' : F''
l : Filter α
inst✝ : l.NeBot
hc' : c' ≠ 0
⊢ ((fun _x ↦ c) =O[l] fun _x ↦ c') ↔ c' = 0 → c = 0
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j = k + max n i
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) (k + max n i) - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) ≤
    ∑ k ∈ range (k + max n i), a k - ∑ k ∈ range (max n i), a k

Tactic:
dsimp only

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j = k + max n i
⊢ abv (∑ i ∈ range (k + max n i), f i - ∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (k + max n i), a k - ∑ k ∈ range (max n i), a k
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case inr
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
hx : f x ≠ 0
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖

Tactic:
· have hc : 0 < c := pos_of_mul_pos_left ((norm_pos_iff.2 hx).trans_le hle) (norm_nonneg _)
    replace hle := inv_anti₀ (norm_pos_iff.2 hx) hle
    simpa only [norm_inv, mul_inv, ← div_eq_inv_mul, div_le_iff₀ hc] using! hle

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

Goal state before:
pp: α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → 𝕜
g : α → R
n : ℕ
hn : n ≠ 0
h : (f ^ n) =O[l] (g ^ n)
⊢ f =O[l] g

Tactic:
by
  rcases h.exists_pos with ⟨C, _hC₀, hC⟩
  obtain ⟨c : ℝ, hc₀ : 0 ≤ c, hc : C ≤ c ^ n⟩ :=
    ((eventually_ge_atTop _).and <| (tendsto_pow_atTop hn).eventually_ge_atTop C).exists
  exact (hC.of_pow hn hc hc₀).isBigO

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z‖ / ‖↑m.succ‖ * ‖z ^ m / ↑m.factorial‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖

Tactic:
norm_natCast

Goal state after:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z‖ / ↑m.succ * ‖z ^ m / ↑m.factorial‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖
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'
B : ι → α → ℝ
i : α → Finset ι
hAB : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (⊤ ×ˢ l) (Function.uncurry A) (Function.uncurry B)
c : ℝ
hc : 0 < c
⊢ IsBigOWith c l (fun H ↦ ∑ j ∈ i H, A j H) fun H ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
exact (hAB hc).sum_congr'

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) * ↑(m.choose I) * (↑m.factorial)⁻¹ = x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
rw [← h₂, Nat.cast_mul, Nat.cast_mul, mul_inv, mul_inv]

Goal state after:
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) * ↑(m.choose I) * ((↑(m.choose I))⁻¹ * (↑I.factorial)⁻¹ * (↑(m - I).factorial)⁻¹) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)