mathlib-initiative/mathlib-tactics huggingface dataset:
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:
lintegral_const_mul'

Goal state after:
α : 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 μ
⊢ ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

case hr
α : 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 μ
⊢ ‖c‖ₑ ≠ ∞
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
hc : IsUnit c
f : α → β
⊢ HasFiniteIntegral (c • f) μ ↔ HasFiniteIntegral f μ

Tactic:
obtain ⟨c, rfl⟩ := hc

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral (↑c • f) μ ↔ HasFiniteIntegral f μ
Module: Mathlib.Analysis.Complex.Order

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

Tactic:
by
  rw [le_def, not_and_or, not_le]

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

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

Tactic:
simp [← hx₁', mem_preimage, mem_prod, hx₁]

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

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

Tactic:
simp [← hx₁', mem_preimage, mem_prod, hx₁]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ AEMeasurable (fun y ↦ φ (x, y)) ν

Tactic:
by fun_prop

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ AEMeasurable (fun y ↦ φ (x, y)) ν

Tactic:
by fun_prop

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

Goal state before:
pp: G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
a : G
⊢ AEMeasurable (fun y ↦ f y * g (y⁻¹ * a)) μ

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x y : V₁
⊢ dist (f x) (f y) ≤ ↑⟨‖f‖, ⋯⟩ * dist x y

Tactic:
by
    rw [dist_eq_norm, dist_eq_norm, ← map_sub]
    apply le_opNorm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U : R
hU : U ∈ unitary R
⊢ star (star U) * star U = 1

Tactic:
rw [star_star, mul_star_self_of_mem hU]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R✝ : Type u_7
R₂ : Type u_8
M✝ : Type u_9
M₂ : Type u_10
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
x✝ : α
⊢ f (x✝ • a • b₂) = f ((x✝ * a) • b₂)

Tactic:
congr 1

Goal state after:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R✝ : Type u_7
R₂ : Type u_8
M✝ : Type u_9
M₂ : Type u_10
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
x✝ : α
⊢ x✝ • a • b₂ = (x✝ * a) • b₂
Module: Mathlib.Topology.Instances.RealVectorSpace

Goal state before:
pp: E : Type u_1
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_2
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousSMul ℝ F
inst✝² : T2Space F
G : Type u_3
inst✝¹ : FunLike G E F
inst✝ : AddMonoidHomClass G E F
f : G
hf : Continuous ⇑f
c : ℝ
x : E
⊢ Continuous fun c ↦ f (c • x)

Tactic:
by fun_prop

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
⊢ 1 + 0 = 1

Tactic:
add_zero

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
⊢ 1 = 1
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
    (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I' +
      ((algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * (algebraMap ℝ A) x₂)

Tactic:
congr 1

Goal state after:
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I'

case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (x₁ * y₂ + y₁ * x₂) • I' = (algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * (algebraMap ℝ A) x₂
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
x✝ : im z = 0
h : im z = 0 := x✝
| ↑(re z) + 0

Tactic:
add_zero

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
x✝ : im z = 0
h : im z = 0 := x✝
| ↑(re z)
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: ⊢ ∀ (x y : ℤ), dist ↑↑x ↑↑y = dist x y

Tactic:
Complex.isometry_ofReal.dist_eq,

Goal state after:
⊢ ∀ (x y : ℤ), dist ↑x ↑y = dist x y
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ℜ (z • a) = z.re • ℜ a - z.im • ℑ a

Tactic:
have := by congrm (ℜ ($((re_add_im z).symm) • a))
  simpa [-re_add_im, add_smul, ← smul_smul, sub_eq_add_neg]

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

Goal state before:
pp: r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
z : ℂ
hzs : z ∈ s
hz : z ≤ 0
this : ‖z‖ = r
⊢ -↑r ∈ s

Tactic:
simpa [← this, ← norm_neg z ▸ eq_coe_norm_of_nonneg (neg_nonneg.mpr hz)]

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

Goal state before:
pp: z : ℂ
| ↑(ℜ z)

Tactic:
← re_add_im z

Goal state after:
z : ℂ
| ↑(ℜ (↑z.re + ↑z.im * I))
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
h : ↑a' * b ≤ ↑a' * c
ha1 : a' > 0
ha2 : ↑a' = ↑a
⊢ 0 ≤ c - b

Tactic:
← sub_nonneg,

Goal state after:
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
h : 0 ≤ ↑a' * c - ↑a' * b
ha1 : a' > 0
ha2 : ↑a' = ↑a
⊢ 0 ≤ c - b
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : 0 < ↑a' * (c - b)
⊢ 0 ≤ c - b

Tactic:
ofReal_mul_pos_iff

Goal state after:
case inl
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : a' < 0 ∧ c - b < 0 ∨ 0 < a' ∧ 0 < c - b
⊢ 0 ≤ c - b
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
z : K
⊢ ‖{ toFun := (realRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (realRingEquiv h).invFun, left_inv := ⋯,
          right_inv := ⋯ }
        z‖ =
    ‖z‖

Tactic:
← re_add_im z

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
z : K
⊢ ‖{ toFun := (realRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (realRingEquiv h).invFun, left_inv := ⋯,
          right_inv := ⋯ }
        (↑(re z) + ↑(im z) * I)‖ =
    ‖↑(re z) + ↑(im z) * I‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
⊢ 0 < c → IsBigOWith c l (fun x ↦ f₁ x * f₂ x) fun x ↦ g₁ x * g₂ x

Tactic:
cpos

Goal state after:
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x ↦ f₁ x * f₂ x) fun x ↦ g₁ x * g₂ x
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
c : ℝ
⊢ 0 < c → IsBigOWith c l (fun x ↦ f₁ x * f₂ x) fun x ↦ g₁ x * g₂ x

Tactic:
cpos

Goal state after:
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x ↦ f₁ x * f₂ x) fun x ↦ g₁ x * g₂ x
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁✝ : k₁ =O[l] k₂
h₂✝ : f' =O[l] g'
c₁ : ℝ
h₁ : IsBigOWith c₁ l k₁ k₂
c₂ : ℝ
h₂ : IsBigOWith c₂ l f' g'
⊢ (fun x ↦ k₁ x • f' x) =O[l] fun x ↦ k₂ x • g' x

Tactic:
exact (h₁.smul h₂).isBigO

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'
c : ℝ
⊢ 0 < c → IsBigOWith c l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x

Tactic:
cpos

Goal state after:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
c : ℝ
⊢ 0 < c → IsBigOWith c l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x

Tactic:
cpos

Goal state after:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x
Module: Mathlib.Analysis.Asymptotics.Lemmas

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

Tactic:
have : ¬Tendsto (Function.const α ‖c‖) l atTop :=
    not_tendsto_atTop_of_tendsto_nhds tendsto_const_nhds
  simp only [isLittleO_const_left, or_iff_left_iff_imp]
  exact fun h => (this h).elim

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ x ^ m / ↑m.factorial = x ^ (n + (m - n)) / ↑m.factorial

Tactic:
add_tsub_cancel_of_le hm.2

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ x ^ m / ↑m.factorial = x ^ m / ↑m.factorial
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case inr
x : ℝ
h1✝ : 0 ≤ x
h2 : x < 1
h1 : 0 < x
⊢ rexp x ≤ 1 / (1 - x)

Tactic:
exact (exp_bound_div_one_sub_of_interval' h1 h2).le

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

Goal state before:
pp: a : ℝ
⊢ Continuous cexp

Tactic:
by fun_prop

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

Goal state before:
pp: s : Set ℝ
⊢ ContinuousOn rexp s

Tactic:
by fun_prop

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

Goal state before:
pp: ⊢ Tendsto rexp atTop atTop

Tactic:
by
  have A : Tendsto (fun x : ℝ => x + 1) atTop atTop :=
    tendsto_atTop_add_const_right atTop 1 tendsto_id
  have B : ∀ᶠ x in atTop, x + 1 ≤ exp x := eventually_atTop.2 ⟨0, fun x _ => add_one_le_exp x⟩
  exact tendsto_atTop_mono' atTop B A

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

Goal state before:
pp: case inl
x : ℝ
hx : |x| ≤ π
h : x < 0
⊢ |sin x| = sin (-x)

Tactic:
sin_neg,

Goal state after:
case inl
x : ℝ
hx : |x| ≤ π
h : x < 0
⊢ |sin x| = -sin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
hl : 0 ≤ x
hu : x ≤ π
⊢ sin x = √(1 - cos x ^ 2)

Tactic:
rw [← abs_sin_eq_sqrt_one_sub_cos_sq, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi hl hu)]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
r : ℝ
⊢ r ≤ ‖x‖ ↔ ∀ (m : M), ↑m = x → r ≤ ‖m‖

Tactic:
by
  simp [norm_eq_infDist, le_infDist (norm_aux _)]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ f m + 0 = f m

Tactic:
add_zero

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ f m = f m
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ (1 - 0) * dist y x = dist y x

Tactic:
sub_zero,

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ 1 * dist y x = dist y x
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
inst✝ : NormedRing R
r : ℝ
hr : 1 < r
⊢ Nat.cast =o[atTop] fun n ↦ r ^ n

Tactic:
by
  simpa only [pow_one] using @isLittleO_pow_const_const_pow_of_one_lt R _ 1 _ hr

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

Goal state before:
pp: ⊢ cos (3 * (π / 3)) = cos π

Tactic:
congr 1

Goal state after:
⊢ 3 * (π / 3) = π
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
ε : ℝ
hε : 0 < ε
s : Set E
hδ : 0 ≤ 0
⊢ thickening ε s = thickening (ε + 0) s

Tactic:
add_zero

Goal state after:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
ε : ℝ
hε : 0 < ε
s : Set E
hδ : 0 ≤ 0
⊢ thickening ε s = thickening ε s
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 0 + sin (-(↑π / 2)) * I = -I

Tactic:
sin_neg,

Goal state after:
⊢ 0 + -sin (↑π / 2) * I = -I
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:
rw [ball_add, thickening_ball hε hδ b, Metric.vadd_ball, vadd_eq_add]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
dP : P.natDegree = k
⊢ (n + k).descFactorial k = Polynomial.eval n P

Tactic:
have : n + 1 + k - 1 = n + k := by lia

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
dP : P.natDegree = k
this : n + 1 + k - 1 = n + k
⊢ (n + k).descFactorial k = Polynomial.eval n P
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ Continuous[_, instTopologicalSpaceSubtype] fun t ↦ ⟨h.somePath t, ⋯⟩

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x✝¹ : G
x✝ : x✝¹ ∈ Subgroup.pathComponentOne G
g : G
γ : Path 1 x✝¹
⊢ Continuous[_, inst✝¹] fun x ↦ g * γ x * g⁻¹

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ γ : Path x y
⊢ Continuous[_, inst✝¹] (⇑γ ∘ σ)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ γ : Path x y
⊢ ContinuousOn ⇑γ.extend I

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace T
K : Set X
U : Set Y
f : C(X × Y, Z)
a : X
⊢ Continuous[inst✝², instTopologicalSpaceProd] (Prod.mk a)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
⊢ Summable fun n ↦ f n * z ^ n

Tactic:
have hw : 0 < ‖w‖ := (norm_nonneg z).trans_lt hz

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
⊢ Summable fun n ↦ f n * z ^ n
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type u_3
F : Set X
x y : ℝ
⊢ Continuous fun t ↦ (1 - ↑t) * x + ↑t * y

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case inr
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ (if h : ↑⟨t, ⋯⟩ ≤ 1 / 2 then γ₁ ⟨2 * ↑⟨t, ⋯⟩, ⋯⟩ else γ₂ ⟨2 * ↑⟨t, ⋯⟩ - 1, ⋯⟩) = γ₁.extend (2 * t)

Tactic:
dif_pos,

Goal state after:
case inr
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ γ₁ ⟨2 * ↑⟨t, ⋯⟩, ⋯⟩ = γ₁.extend (2 * t)

case inr.hc
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
ht₀ : 0 ≤ t
⊢ ↑⟨t, ⋯⟩ ≤ 1 / 2
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ γ₂.extend (1 - 2 * (1 - t)) = γ₂.extend (2 * t - 1)

Tactic:
congr 1

Goal state after:
case e_6
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ 1 - 2 * (1 - t) = 2 * t - 1
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Function.LeftInverse uncurry ContinuousMap.curry

Tactic:
by intro; ext; rfl

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Function.RightInverse uncurry ContinuousMap.curry

Tactic:
by intro; ext; rfl

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ Continuous[_, inst✝] ↿fun t ↦ t

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b : ι → X
γ : (t : ι) → Path (a t) (b t)
h : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ t).extend

Tactic:
apply h.comp (continuous_id.prodMap continuous_projIcc)

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b : ι → X
γ : (t : ι) → Path (a t) (b t)
h : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ
⊢ 0 ≤ 1