mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
x✝ : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F)) ∧ Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
hi : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F))
right✝ : Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
x : F
h : Filter.Tendsto (fun n ↦ WithAbs.toAbs v x ^ n) Filter.atTop (𝓝 0)
⊢ Filter.Tendsto (fun n ↦ WithAbs.toAbs w x ^ n) Filter.atTop (𝓝 0)

Tactic:
simpa [Function.comp_def] using (hi.continuous.tendsto 0).comp h

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
n : ℕ
IH :
  dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
    dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
Ign :
  dist (g (u n)) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n.succ) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ ↑c * ↑f'symm.nnnorm * dist (f (u n)) y ≤ ↑c * ↑f'symm.nnnorm * ((↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y)

Tactic:
by
        gcongr
        apply IH.1

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case refine_2.succ.succ
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
H :
  ∀ (x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })) (y : Y.obj (op { obj := ⦋2⦌, property := _proof_14 })),
    f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x) =
        (ConcreteCategory.hom (Y.map (δ₂ 2 _proof_12 _proof_15).op)) y →
      f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_12 _proof_15).op)) y →
        f₁ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_12 _proof_15).op)) y
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
n : ℕ
hn : n + 1 + 1 < 2
i : Fin (n + 1 + 1 + 1)
⊢ naturalityProperty f₀ f₁ hδ₁ hδ₀ hY (σ 2 i ⋯ ⋯)

Tactic:
· lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝ : SmallCategory C
F : X.HomotopyCategory ⥤ C
x y : X.obj (op { obj := ⦋0⦌, property := _proof_11 })
e : Edge x y
⊢ ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))

Tactic:
exact ComposableArrows.arrowEquiv.injective
    (congr_arg F.mapArrow.obj (congr_arrowMk_homMk (Edge.mk' e.edge) e rfl))

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case convert_5.hf
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
⊢ Tendsto (fun x ↦ (c + ↑x) / (a + ↑x)) atTop (𝓝 1)

Tactic:
convert! tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero

Goal state after:
case e'_3.e'_5.e'_6
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
x✝ : ℕ
⊢ ↑x✝ = 1 * ↑x✝

case e'_3.e'_6.e'_6
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
x✝ : ℕ
⊢ ↑x✝ = 1 * ↑x✝

case e'_5
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
⊢ 1 = 1 / 1
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case convert_5.hg
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
⊢ Tendsto (fun x ↦ (1 + ↑x) / (b + ↑x)) atTop (𝓝 1)

Tactic:
convert! tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero

Goal state after:
case e'_3.e'_5.e'_6
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
x✝ : ℕ
⊢ ↑x✝ = 1 * ↑x✝

case e'_3.e'_6.e'_6
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
x✝ : ℕ
⊢ ↑x✝ = 1 * ↑x✝

case e'_5
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
habc : ∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
this : ∀ (k : ℕ), (a + ↑k)⁻¹ * (b + ↑k)⁻¹ * (c + ↑k) * (1 + ↑k) = (c + ↑k) / (a + ↑k) * ((1 + ↑k) / (b + ↑k))
⊢ 1 = 1 / 1
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
s : Finset ι
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ σ ∈ s, MeromorphicAt (F σ) x
⊢ MeromorphicAt (∏ i ∈ s, F i) x

Tactic:
induction s using Finset.induction with

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
ι : Type u_5
s : Finset ι
G : ι → 𝕜 → E
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (G σ) x
⊢ MeromorphicAt (∑ n ∈ s, G n) x

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: ⊢ logDeriv sin = cot

Tactic:
ext
  rw [logDeriv, Real.deriv_sin, Pi.div_apply, Real.cot_eq_cos_div_sin]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
⊢ (descPochhammer ℤ (k + 1)).smeval ↑n = ↑(n.descFactorial (k + 1))

Tactic:
rw [descPochhammer_succ_right, Nat.descFactorial_succ, smeval_mul, ih, mul_comm, Nat.cast_mul,
      smeval_sub, smeval_X, smeval_natCast, npow_one, npow_zero, nsmul_one]

Goal state after:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
ih : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)
⊢ ↑(n.descFactorial k) * (↑n - ↑k) = ↑(n.descFactorial k) * ↑(n - k)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f x = g x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
⊢ a ∈ U → a ∈ (U \ {x | f x = g x})ᶜ → f a = g a

Tactic:
h₁a

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f x = g x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
h₁a : a ∈ U
⊢ a ∈ (U \ {x | f x = g x})ᶜ → f a = g a
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
U : Set 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
⊢ {x | AnalyticAt 𝕜 f x} ∈ codiscreteWithin U

Tactic:
mem_codiscreteWithin

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
U : Set 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
h : MeromorphicOn f U
⊢ ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ {x | AnalyticAt 𝕜 f x}))
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : y = a
⊢ ContinuousWithinAt f t a

Tactic:
exact f_lim.mono ts

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
y : ℝ
hy : y ∈ Icc b a
h : y = a
⊢ ContinuousWithinAt f t a

Tactic:
exact f_lim.mono ts

Goal state after:
Module: Mathlib.Analysis.Analytic.Polynomial

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
inst✝² : NormedCommRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x ↦ f x i) z
p : MvPolynomial σ A
k : A
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) (C k)) z

pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
inst✝² : NormedCommRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x ↦ f x i) z
p✝ p q : MvPolynomial σ A
hp : AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p) z
hq : AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) q) z
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) (p + q)) z

pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
inst✝² : NormedCommRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x ↦ f x i) z
p✝ p : MvPolynomial σ A
i : σ
hp : AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p) z
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) (p * X i)) z

Tactic:
· simp_rw [aeval_C]; apply analyticAt_const

Goal state after:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
inst✝² : NormedCommRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x ↦ f x i) z
p✝ p q : MvPolynomial σ A
hp : AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p) z
hq : AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) q) z
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) (p + q)) z

𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
inst✝² : NormedCommRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt 𝕜 (fun x ↦ f x i) z
p✝ p : MvPolynomial σ A
i : σ
hp : AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p) z
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) (p * X i)) z
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inl.inr.inr
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
⊢ (x ^ y).log = ↑y * x.log

Tactic:
have x_ne_top := (ENNReal.toReal_pos_iff.1 x_real).2.ne

Goal state after:
case inl.inr.inr
x : ℝ≥0∞
y : ℝ
y_neg : y < 0
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
⊢ (x ^ y).log = ↑y * x.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inr.inr
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
⊢ (x ^ y).log = ↑y * x.log

Tactic:
have x_ne_top := (ENNReal.toReal_pos_iff.1 x_real).2.ne

Goal state after:
case inr.inr.inr.inr
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
x_real : 0 < x.toReal
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
⊢ (x ^ y).log = ↑y * x.log
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
x✝¹ : a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n))
b : EReal
x✝ : b ∈ Set.Ioo 0 (linearGrowthInf u)
left✝ : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * ↑(v a) ≤ u (v a)
n : ℕ
b_uvn : b * ↑(v n) ≤ u (v n)
a_vn : a < ↑(v n) / ↑n
⊢ 0 < n → a * b * ↑n ≤ (u ∘ v) n

Tactic:
n_0

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
x✝¹ : a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n))
b : EReal
x✝ : b ∈ Set.Ioo 0 (linearGrowthInf u)
left✝ : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * ↑(v a) ≤ u (v a)
n : ℕ
b_uvn : b * ↑(v n) ≤ u (v n)
a_vn : a < ↑(v n) / ↑n
n_0 : 0 < n
⊢ a * b * ↑n ≤ (u ∘ v) n
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthSup u
b_0 : 0 ≤ b
uv_b : ∀ᶠ (n : ℕ) in atTop, u (v n) ≤ b * ↑(v n)
n : ℕ
uvn_b : u (v n) ≤ b * ↑(v n)
vn_a : ↑(v n) / ↑n < a
⊢ 0 < n → (u ∘ v) n ≤ a * b * ↑n

Tactic:
n_0

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthSup u
b_0 : 0 ≤ b
uv_b : ∀ᶠ (n : ℕ) in atTop, u (v n) ≤ b * ↑(v n)
n : ℕ
uvn_b : u (v n) ≤ b * ↑(v n)
vn_a : ↑(v n) / ↑n < a
n_0 : 0 < n
⊢ (u ∘ v) n ≤ a * b * ↑n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
⊢ expGrowthSup v + expGrowthInf u ≤ expGrowthSup (v * u)

Tactic:
exact le_expGrowthSup_mul

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

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
v_a' : (linearGrowthSup fun n ↦ ↑(v n)) < a'
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
n : ℕ
vn_a' : ↑(v n) / ↑n < a'
⊢ 0 < n → ↑(v n) ≤ a' * ↑n

Tactic:
n_0

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
v_a' : (linearGrowthSup fun n ↦ ↑(v n)) < a'
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
n : ℕ
vn_a' : ↑(v n) / ↑n < a'
n_0 : 0 < n
⊢ ↑(v n) ≤ a' * ↑n
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun n ↦ ↑(v n)
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
n : ℕ
a_vn' : a' < ↑(v n) / ↑n
⊢ 0 < n → a' * ↑n ≤ ↑(v n)

Tactic:
n_0

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun n ↦ ↑(v n)
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
n : ℕ
a_vn' : a' < ↑(v n) / ↑n
n_0 : 0 < n
⊢ a' * ↑n ≤ ↑(v n)
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
s : Set (α × β)
hs : MeasurableSet s
x✝ : μ s < ∞
⊢ ∀ t ∈ Set.image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t},
    ∫⁻ (x : α × β) in t, f x ∂μ = ∫⁻ (x : α × β) in t, g x ∂μ

Tactic:
rintro _ ⟨s, hs, t, ht, rfl⟩
    exact h hs ht

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ (μ - ν).restrict s = μ.restrict s - ν.restrict s

Tactic:
repeat rw [sub_def]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
⊢ (sInf {d | μ ≤ d + ν}).restrict s = sInf {d | μ.restrict s ≤ d + ν.restrict s}
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ (ν.restrict s).rnDeriv ν =ᵐ[ν] s.indicator 1

Tactic:
by
  rw [← withDensity_indicator_one hs]
  exact rnDeriv_withDensity _ (measurable_one.indicator hs)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case e_f
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
i : ℕ
⊢ edist (f (↑p.2 (i + 1))) (f (↑p.2 i)) = edist (f' (↑p.2 (i + 1))) (f' (↑p.2 i))

Tactic:
edist_congr_right (h <| p.snd.prop.2 (i + 1)),

Goal state after:
case e_f
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
i : ℕ
⊢ edist (f' (↑p.2 (i + 1))) (f (↑p.2 i)) = edist (f' (↑p.2 (i + 1))) (f' (↑p.2 i))
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: case inr
α : Type u_2
inst✝⁶ : LinearOrder α
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set α
f : α → E
g : α → F
hf : BoundedVariationOn f s
hg : BoundedVariationOn g s
B : E →L[ℝ] F →L[ℝ] G
x : α
hx : x ∈ s
A : ∀ y ∈ s, ‖f y‖ₑ ≤ ‖f x‖ₑ + eVariationOn f s
A' : ∀ y ∈ s, ‖g y‖ₑ ≤ ‖g x‖ₑ + eVariationOn g s
⊢ ‖B‖ₑ * ((‖f x‖ₑ + eVariationOn f s) * eVariationOn g s + (‖g x‖ₑ + eVariationOn g s) * eVariationOn f s) < ∞

Tactic:
simp [mul_add, ENNReal.mul_lt_top_iff, hf.lt_top, hg.lt_top]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StarOrdered

Goal state before:
pp: case mp
α : Type u_1
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : Zero α
R : Type u_2
inst✝⁸ : TopologicalSpace R
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : IsTopologicalSemiring R
inst✝¹ : ContinuousStar R
inst✝ : StarOrderedRing C(α, R)
f g : C(α, R)₀
⊢ (∀ (x : α), ↑f x ≤ ↑g x) → ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p

Tactic:
← ContinuousMap.le_def,

Goal state after:
case mp
α : Type u_1
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : Zero α
R : Type u_2
inst✝⁸ : TopologicalSpace R
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : IsTopologicalSemiring R
inst✝¹ : ContinuousStar R
inst✝ : StarOrderedRing C(α, R)
f g : C(α, R)₀
⊢ ↑f ≤ ↑g → ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p