mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (map f μa).prod (map g μc) = map (Prod.map f g) (μa.prod μc)

Tactic:
← sum_sfiniteSeq μa,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (map f (sum (sfiniteSeq μa))).prod (map g μc) = map (Prod.map f g) ((sum (sfiniteSeq μa)).prod μc)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁵ : T2Space β
s : Set γ
f : γ → β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set ↑s
⊢ MeasurableSet u → MeasurableSet (s.domRestrict f '' u)

Tactic:
hu

Goal state after:
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
tβ : TopologicalSpace β
inst✝⁵ : T2Space β
s : Set γ
f : γ → β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set ↑s
hu : MeasurableSet u
⊢ MeasurableSet (s.domRestrict f '' u)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
⊢ MeasurableSet (g '' t)

Tactic:
let u : Set β := {c | ∃ x, ∃ y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}

Goal state after:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
⊢ MeasurableSet (g '' t)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h ↦ h * g) ⁻¹' A) = μ A) ↔ μ.IsMulRightInvariant

Tactic:
trans ∀ g, map (· * g) μ = μ
  · simp_rw [Measure.ext_iff]
    refine forall_congr' fun g => forall_congr' fun A => forall_congr' fun hA => ?_
    rw [map_apply (measurable_mul_const g) hA]
  exact ⟨fun h => ⟨h⟩, fun h => h.1⟩

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✝ : IsProbabilityMeasure ν
s : Set α
hs : MeasurableSet s
⊢ (μ.prod ν) (Prod.fst ⁻¹' s) = μ s

Tactic:
← prod_univ,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure ν
s : Set α
hs : MeasurableSet s
⊢ (μ.prod ν) (s ×ˢ univ) = μ s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : AEMeasurable X μ
s : Set β
hs : MeasurableSet s
⊢ μ ((fun x ↦ (X x, Y x)) ⁻¹' Prod.fst ⁻¹' s) = μ (X ⁻¹' s)

Tactic:
← prod_univ,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : AEMeasurable X μ
s : Set β
hs : MeasurableSet s
⊢ μ ((fun x ↦ (X x, Y x)) ⁻¹' s ×ˢ univ) = μ (X ⁻¹' s)
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
⊢ ν' ≠ 0

Tactic:
refine mt ?_ h2s

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
⊢ ν' = 0 → ν' s = 0
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ μ' s * lintegral ν' g = ∫⁻ (x : G), f x ∂μ'

Tactic:
simp_rw [measure_mul_lintegral_eq μ' ν' sm g hg, g, inv_inv]

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * (f x / ν' ((fun z ↦ z * x) ⁻¹' s)) ∂μ' = ∫⁻ (x : G), f x ∂μ'
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

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

Tactic:
by
  simp only [ofReal_norm, edist_zero_right]

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

Goal state before:
pp: α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
simp only [HasFiniteIntegral]

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

Goal state before:
pp: x y : ℝ
⊢ x ^ 2 < y ↔ |x| < √y

Tactic:
← sq_abs,

Goal state after:
x y : ℝ
⊢ |x| ^ 2 < y ↔ |x| < √y
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ ‖z / w‖ = ‖z‖ / ‖w‖

Tactic:
by
  rw [norm_def, norm_def, norm_def, normSq_div, Real.sqrt_div (normSq_nonneg _)]

Goal state after:
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✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (c • f) μ

Tactic:
simp only [HasFiniteIntegral]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ ∫⁻ (a : α), ‖(c • f) a‖ₑ ∂μ < ∞
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 μ
⊢ HasFiniteIntegral (c • f) μ

Tactic:
simp only [HasFiniteIntegral]

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 μ
⊢ ∫⁻ (a : α), ‖(c • f) a‖ₑ ∂μ < ∞
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: q : ℚ
r : ℝ
⊢ ↑(q • r) = q • ↑r

Tactic:
simp [Rat.smul_def]

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

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ x⋆ * x = 0 ↔ x = 0

Tactic:
rw [← norm_eq_zero, norm_star_mul_self]
  exact mul_self_eq_zero.trans norm_eq_zero

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x✝ : (i : ι) → R i
x y : NNReal
h : x ≤ y
⊢ (fun x ↦ x ^ 2) x ≤ (fun x ↦ x ^ 2) y

Tactic:
by simpa only [sq] using mul_le_mul' h h

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

Goal state before:
pp: z : ℂ
hz : 0 ≤ z
⊢ z = ↑‖z‖

Tactic:
by
  lift z to ℝ using hz.2.symm
  rw [norm_real, Real.norm_of_nonneg (id hz.1 : 0 ≤ z)]

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

Goal state before:
pp: 𝕜 : Type u_3
W : Type u_5
G : Type u_6
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup W
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : G ≃ₗᵢ[𝕜] W
α : ↥(unitary 𝕜)
⊢ (α • e).symm = α⁻¹ • e.symm

Tactic:
ext; simp [symm_smul_apply]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖
x : α
x✝ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖ ∧ 0 < ‖g x‖
hx₁ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖
hx₂ : 0 < ‖g x‖
⊢ 2⁻¹ * ‖g x‖ < ‖g x‖

Tactic:
rw [mul_lt_iff_lt_one_left hx₂]

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖
x : α
x✝ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖ ∧ 0 < ‖g x‖
hx₁ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖
hx₂ : 0 < ‖g x‖
⊢ 2⁻¹ < 1
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (c : ℝ) in atTop, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g' x‖

Tactic:
simp only [IsBigOWith_def]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
ι : Sort u_18
p : ι → Prop
s : ι → Set α
h✝ : f =O[l] g'
hb : l.HasBasis p s
c : ℝ
h : c > 0 ∧ IsBigOWith c l f g'
⊢ c > 0 ∧ ∃ i, p i ∧ ∀ x ∈ s i, ‖f x‖ ≤ c * ‖g' x‖

Tactic:
by
    simpa only [isBigOWith_iff, hb.eventually_iff, exists_prop] using h

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hc : c₁ = c₂
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ IsBigOWith c₁ l f₁ g₁ ↔ IsBigOWith c₂ l f₂ g₂

Tactic:
simp only [IsBigOWith_def]

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hc : c₁ = c₂
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ IsBigOWith c (map k l) f g ↔ IsBigOWith c l (f ∘ k) (g ∘ k)

Tactic:
simp only [IsBigOWith_def]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ (∀ᶠ (x : α) in map k l, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (x : β) in l, ‖(f ∘ k) x‖ ≤ c * ‖(g ∘ k) x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
⊢ IsBigOWith (‖c‖ / ‖c'‖) l (fun _x ↦ c) fun _x ↦ c'

Tactic:
simp only [IsBigOWith_def]

Goal state after:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
⊢ ∀ᶠ (x : α) in l, ‖c‖ ≤ ‖c‖ / ‖c'‖ * ‖c'‖
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
c : ℝ
l : Filter α
inst✝ : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
this : Nontrivial S
⊢ IsBigOWith (Nat.casesOn 0 ‖1‖ fun n ↦ c ^ (n + 1)) l (fun x ↦ f x ^ 0) fun x ↦ g x ^ 0

Tactic:
simpa using isBigOWith_const_const (1 : R) (one_ne_zero' S) l

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

Tactic:
have h₁ : (m.choose I : ℂ) ≠ 0 :=
      Nat.cast_ne_zero.2 (pos_iff_ne_zero.1 (Nat.choose_pos (Nat.le_of_lt_succ (mem_range.1 hi))))

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑m.factorial)⁻¹ = x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case hgf
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h✝ : Tendsto (fun x ↦ g x / f x) l atTop
x : α
h : 1 ≤ g x / f x
h0 : g x = 0
⊢ f x = 0

Tactic:
simp only [h0, zero_div] at h

Goal state after:
case hgf
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h✝ : Tendsto (fun x ↦ g x / f x) l atTop
x : α
h0 : g x = 0
h : 1 ≤ 0
⊢ f x = 0
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ IsBigOWith c l u v

Tactic:
simp only [IsBigOWith_def]

Goal state after:
α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cosh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (cosh x)

Tactic:
cosh,

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

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

Tactic:
cosh,

Goal state after:
x : ℂ
⊢ (starRingEnd ℂ) (cexp x + cexp (-x)) / 2 = (starRingEnd ℂ) ((cexp x + cexp (-x)) / 2)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case neg
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ * ‖f x‖ ≤ ‖g x‖
hf : ¬f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
field_simp at hx

Goal state after:
case neg
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hf : ¬f x = 0
hx : ‖f x‖ ≤ C * ‖g x‖
⊢ ‖f x‖ ≤ C * ‖g x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos (2 * x) = cos x ^ 2 - sin x ^ 2

Tactic:
rw [two_mul, cos_add, ← sq, ← sq]

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

Goal state before:
pp: x : ℂ
h : cos x ≠ 0
⊢ (1 + tan x ^ 2) * cos x ^ 2 = 1

Tactic:
conv_rhs => rw [← sin_sq_add_cos_sq x, ← tan_mul_cos h]

Goal state after:
x : ℂ
h : cos x ≠ 0
⊢ (1 + tan x ^ 2) * cos x ^ 2 = (tan x * cos x) ^ 2 + cos x ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
h : cos x ≠ 0
⊢ (1 + tan x ^ 2) * cos x ^ 2 = 1

Tactic:
conv_rhs => rw [← sin_sq_add_cos_sq x, ← tan_mul_cos h]
  ring

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

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ (i : ι), IsBigOWith c l (fun x ↦ f x i) g') ↔
    ∀ (i : ι) ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x ↦ f x i) g'

Tactic:
exact ⟨fun h i c hc => h hc i, fun h c hc i => h i hc⟩

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

Goal state before:
pp: x : ℝ
⊢ cosh x * 2 = rexp x + rexp (-x)

Tactic:
cosh,

Goal state after:
x : ℝ
⊢ (Complex.cosh ↑x).re * 2 = rexp x + rexp (-x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖1 - cexp (↑x * I)‖

Tactic:
← norm_neg,

Goal state after:
x : ℝ
⊢ ‖-(cexp (I * ↑x) - 1)‖ = ‖1 - cexp (↑x * I)‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂
⊢ |rexp x - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

Tactic:
by
  grw [abs_sub_le, h]
  subst e₁; rw [expNear_succ, expNear_sub, abs_mul]
  convert!
    mul_le_mul_of_nonneg_left (a := |x| ^ n / ↑(Nat.factorial n)) (le_sub_iff_add_le'.1 e) ?_
      using 1
  · simp [mul_add, pow_succ', div_eq_mul_inv, abs_mul, abs_inv, Nat.factorial]
    ac_rfl
  · simp [div_nonneg, abs_nonneg]

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

Goal state before:
pp: case inr
n : ℕ
hn : 0 < n
⊢ ∃ i,
    0 < i ∧
      ∀ ⦃x : ℂ⦄, x ∈ {y | ‖y‖ < i} → ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !‖ ≤ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖

Tactic:
refine ⟨1, one_pos, fun x hx ↦ ?_⟩

Goal state after:
case inr
n : ℕ
hn : 0 < n
x : ℂ
hx : x ∈ {y | ‖y‖ < 1}
⊢ ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !‖ ≤ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
⊢ Subtype.val '' Set.Iic (expOrderIso a) = Set.Ioc 0 ((Subtype.val ∘ ⇑expOrderIso) a)

Tactic:
image_subtype_val_Ioi_Iic,

Goal state after:
a : ℝ
⊢ Set.Ioc 0 ↑(expOrderIso a) = Set.Ioc 0 ((Subtype.val ∘ ⇑expOrderIso) a)
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝ : M ⧸ S
m : M
r✝ ε : ℝ
h : S ≤ T
x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T
r : ℝ
h₁ : ∀ (m : M), ↑m = (quotientQuotientEquivQuotient S T h) x → r ≤ ‖m‖
y : M ⧸ S
h₂ : ↑y = x
z : M
h₃ : ↑z = y
⊢ ↑z = (quotientQuotientEquivQuotient S T h) x

Tactic:
subst_vars; rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ‖S.normedMk m‖ = sInf ((fun m_1 ↦ ‖m + m_1‖) '' ↑S.normedMk.ker)

Tactic:
simpa [S.ker_normedMk] using quotient_norm_mk_eq _ m

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
n i : ℕ
hi : i < n + 1
⊢ ↑((i + k).choose k) * r ^ (i + (n - i)) = ↑((i + k).choose k) * r ^ n

Tactic:
show i + (n - i) = n by lia

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
n i : ℕ
hi : i < n + 1
⊢ ↑((i + k).choose k) * r ^ n = ↑((i + k).choose k) * r ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
⊢ ‖cexp (↑a * (cexp z + cexp (-z)))‖ ≤ rexp (a * Real.cos b * rexp |z.re|)

Tactic:
by
  simp only [norm_exp, Real.exp_le_exp, re_ofReal_mul, add_re, exp_re, neg_im, Real.cos_neg, ←
    add_mul, mul_assoc, mul_comm (Real.cos b), neg_re, ← Real.cos_abs z.im]
  have : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re) :=
    apply_abs_le_add_of_nonneg (fun x => (Real.exp_pos x).le) z.re
  refine mul_le_mul_of_nonpos_left (mul_le_mul this ?_ ?_ ((Real.exp_pos _).le.trans this)) ha
  · exact
      Real.cos_le_cos_of_nonneg_of_le_pi (_root_.abs_nonneg _)
        (hb.trans <| half_le_self <| Real.pi_pos.le) hz
  · refine Real.cos_nonneg_of_mem_Icc ⟨?_, hb⟩
    exact (neg_nonpos.2 <| Real.pi_div_two_pos.le).trans ((_root_.abs_nonneg _).trans hz)

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ ‖∑ i ∈ Finset.range n, f i - (∑ x ∈ Finset.range n, f x + f n)‖ ≤ C * r ^ n

Tactic:
← norm_neg,

Goal state after:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ ‖-(∑ i ∈ Finset.range n, f i - (∑ x ∈ Finset.range n, f x + f n))‖ ≤ C * r ^ 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 : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn (f '' F) (f x) (f y) ↔ JoinedIn F x y

Tactic:
refine ⟨?_, (.map · hf.continuous)⟩
  rintro ⟨γ, hγ⟩
  choose γ' hγ'F hγ' using hγ
  have h₀ : x ⤳ γ' 0 := by rw [← hf.specializes_iff, hγ', γ.source]
  have h₁ : γ' 1 ⤳ y := by rw [← hf.specializes_iff, hγ', γ.target]
  have h : JoinedIn F (γ' 0) (γ' 1) := by
    refine ⟨⟨⟨γ', ?_⟩, rfl, rfl⟩, hγ'F⟩
    simpa only [hf.continuous_iff, comp_def, hγ'] using map_continuous γ
  exact (h₀.joinedIn hx (hγ'F _)).trans <| h.trans <| h₁.joinedIn (hγ'F _) hy

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U W : Set X
hW : IsPathConnected W
hWU : W ⊆ U
⊢ IsPathConnected (Subtype.val '' Subtype.val ⁻¹' W)

Tactic:
Subtype.image_preimage_val,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U W : Set X
hW : IsPathConnected W
hWU : W ⊆ U
⊢ IsPathConnected (U ∩ W)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
⊢ z.arg ∈ Ioc (-π) π

Tactic:
rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos (arg z) (-π) with ⟨N, hN, -⟩

Goal state after:
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + N • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ z.arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
x✝ : x ∈ univ
⊢ log (rexp x) = x

Tactic:
log_exp

Goal state after:
x : ℝ
x✝ : x ∈ univ
⊢ x = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ |x * y| = |x| * rexp (log y)

Tactic:
exp_log_eq_abs hy,

Goal state after:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ |x * y| = |x| * |y|