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 γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsZeroOrProbabilityMeasure ρ
⊢ IsZeroOrProbabilityMeasure ρ.fst

Tactic:
rcases eq_zero_or_isProbabilityMeasure ρ with h | h

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsZeroOrProbabilityMeasure ρ
h : ρ = 0
⊢ IsZeroOrProbabilityMeasure ρ.fst

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsZeroOrProbabilityMeasure ρ
h : IsProbabilityMeasure ρ
⊢ IsZeroOrProbabilityMeasure ρ.fst
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsProbabilityMeasure ρ
⊢ ρ.snd univ = 1

Tactic:
rw [snd_univ]
    exact measure_univ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsZeroOrProbabilityMeasure ρ
⊢ IsZeroOrProbabilityMeasure ρ.snd

Tactic:
rcases eq_zero_or_isProbabilityMeasure ρ with h | h

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsZeroOrProbabilityMeasure ρ
h : ρ = 0
⊢ IsZeroOrProbabilityMeasure ρ.snd

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsZeroOrProbabilityMeasure ρ
h : IsProbabilityMeasure ρ
⊢ IsZeroOrProbabilityMeasure ρ.snd
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ∞ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
rw [← hμ, ← hν, this s' _ _ hm]

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ∞ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ ν' s' ≠ 0

G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ∞ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ ν' s' ≠ ∞
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
this : (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) = fun j ↦ 0
⊢ Tendsto (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Tactic:
rw [this]

Goal state after:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
this : (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) = fun j ↦ 0
⊢ Tendsto (fun j ↦ 0) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
⊢ Tendsto (fun j ↦ μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)

Tactic:
rcases isEmpty_or_nonempty ι with h | h
  · have : (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0 := by
      simp only [eq_iff_true_of_subsingleton]
    rw [this]
    exact tendsto_const_nhds
  rw [← measure_inter_notConvergentSeq_eq_zero hfg n, Set.inter_iInter]
  refine tendsto_measure_iInter_atTop
    (fun n ↦ (hsm.inter <| notConvergentSeq_measurableSet hf).nullMeasurableSet)
    (fun k l hkl => Set.inter_subset_inter_right _ <| notConvergentSeq_antitone hkl)
    ⟨h.some, ne_top_of_le_ne_top hs (measure_mono Set.inter_subset_left)⟩

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

Goal state before:
pp: case mp.inl
x : ℝ
hle : 0 ≤ x
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

pp: case mp.inr
x : ℝ
hlt : x < 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
· exact Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩

Goal state after:
case mp.inr
x : ℝ
hlt : x < 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0
Module: Mathlib.Analysis.Real.Sqrt

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

Tactic:
← abs_lt,

Goal state after:
x y : ℝ
⊢ x ^ 2 < y ↔ |x| < √y
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:

Tactic:
ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖ := by
        rw [← ENNReal.ofReal_add]
        · apply ofReal_le_ofReal
          apply norm_sub_le
        · exact norm_nonneg _
        · exact norm_nonneg _
      _ ≤ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) := add_le_add h₁ h₂
      _ = b a := by rw [← two_mul]

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
e₁ : A ≃⋆* B
e₂ : B ≃⋆* C
a : A
⊢ e₂.toFun (e₁.toFun (star a)) = star (e₂.toFun (e₁.toFun a))

Tactic:
e₁.map_star',

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
e₁ : A ≃⋆* B
e₂ : B ≃⋆* C
a : A
⊢ e₂.toFun (star (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))
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₂
K : ℝ≥0
hf : LipschitzWith K ⇑f
x : V₁
⊢ ‖f x‖ ≤ ↑K * ‖x‖

Tactic:
simpa only [dist_zero_right, map_zero] using hf.dist_le_mul x 0

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * (B * star B) * star U = 1

Tactic:
by rw [hB₂, mul_one, hA₂]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
⊢ f.NormNoninc ↔ ‖f‖ ≤ 1

Tactic:
refine ⟨fun h => ?_, fun h => fun v => ?_⟩
  · refine opNorm_le_bound _ zero_le_one fun v => ?_
    simpa [one_mul] using h v
  · simpa using le_of_opNorm_le f h v

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

Goal state before:
pp: case negSucc
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U : ↥(unitary R)
a✝ : ℕ
⊢ ↑(U ^ Int.negSucc a✝) = ↑U ^ Int.negSucc a✝

Tactic:
simp [coe_inv]

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 : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c l f g
⊢ ∃ c, IsBigOWith c l f g

Tactic:
exact ⟨c, h⟩

Goal state after:
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
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) i) < ε

Tactic:
obtain ⟨i, hi⟩ := hg (ε / 2) (div_pos ε0 (by simp))

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
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
⊢ ∃ i, ∀ j ≥ i, abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) i) < ε
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
f : E →ₛₗ[σ₁₂] E₂
hf : Isometry ⇑f
⊢ ∀ (x : E), ‖f x‖ = ‖x‖

Tactic:
simp_rw [← dist_zero_right]

Goal state after:
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
f : E →ₛₗ[σ₁₂] E₂
hf : Isometry ⇑f
⊢ ∀ (x : E), dist (f x) 0 = dist x 0
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
⊢ rexp |x| ≤ rexp x + rexp (-x)

Tactic:
cases le_total x 0 <;> simp [abs_of_nonpos, abs_of_nonneg, exp_nonneg, *]

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

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : n ≤ m ∧ m < j
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)

Tactic:
rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.1]

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

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
⊢ ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
intro x _ y hy hxy

Goal state after:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : dist x y < δ
⊢ dist (cexp x) (cexp y) < ε
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 ε : ℝ
x y : M ⧸ S
⊢ infDist 1 {m | ↑m = x * y} ≤ infDist 1 {m | ↑m = x} + infDist 1 {m | ↑m = y}

Tactic:
simp only [infDist_eq_iInf]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝ : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
⊢ ⨅ y_1, dist 1 ↑y_1 ≤ (⨅ y, dist 1 ↑y) + ⨅ y_1, dist 1 ↑y_1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
h : cos x = 1
n : ℤ
hn : ↑(2 * (n / 2)) * π + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
mul_comm (2 : ℤ),

Goal state after:
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑(n / 2 * 2) * π + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
y : X
⊢ JoinedIn {y} y y

Tactic:
exact JoinedIn.refl rfl

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

Goal state before:
pp: x : ℝ
⊢ ‖↑x‖ = |x - ↑(round x)|

Tactic:
simp [AddCircle.norm_eq]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
· replace hθ := hθ.2
      have hcos : Real.cos θ < 0 := Real.cos_neg_of_pi_div_two_lt_of_lt h₁ (by linarith)
      have hsin : 0 ≤ Real.sin θ := Real.sin_nonneg_of_mem_Icc ⟨by linarith, hθ⟩
      rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith;
        linarith; exact hsin; exact hcos.not_ge]

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

Goal state before:
pp: ψ θ : Angle
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π

Tactic:
have : Int.natAbs 2 = 2 := rfl

Goal state after:
ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ -θ ≠ θ ↔ ¬(θ = 0 ∨ θ = ↑π)

Tactic:
← neg_eq_self_iff.not

Goal state after:
θ : Angle
⊢ -θ ≠ θ ↔ ¬-θ = θ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case inr
x : ℂ
n : ℤ
y : ℂ
hx : x ≠ 0
⊢ cexp (↑n * (log x * y)) = cexp (log x * y) ^ n

Tactic:
exp_int_mul

Goal state after:
case inr
x : ℂ
n : ℤ
y : ℂ
hx : x ≠ 0
⊢ cexp (log x * y) ^ n = cexp (log x * y) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0

Tactic:
by
  rcases lt_trichotomy x.im 0 with (hi | hi | hi)
  · simp [hi, hi.ne, hi.not_gt, arg_neg_eq_arg_add_pi_of_im_neg, sub_eq_add_neg, ←
      add_eq_zero_iff_eq_neg, Real.pi_ne_zero]
  · rw [(ext rfl hi : x = x.re)]
    rcases lt_trichotomy x.re 0 with (hr | hr | hr)
    · rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]
      simp [hr]
    · simp [hr, Real.pi_ne_zero]
    · rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
      simp [hr.not_gt, ← add_eq_zero_iff_eq_neg, Real.pi_ne_zero]
  · simp [hi, arg_neg_eq_arg_sub_pi_of_im_pos]

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

Goal state before:
pp: ⊢ SignType.sign 0 = 0

Tactic:
_root_.sign_zero

Goal state after:
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x y : ℝ
hx : x < 0
⊢ |rexp (log x * y)| * |cos (y * π)| ≤ rexp (log x * y)

Tactic:
abs_of_pos (exp_pos _)

Goal state after:
case inr
x y : ℝ
hx : x < 0
⊢ rexp (log x * y) * |cos (y * π)| ≤ rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hy : 0 < y
⊢ Tendsto (fun x ↦ x ^ y) (𝓝 ∞) (𝓝 ∞)

Tactic:
rw [ENNReal.tendsto_nhds_top_iff_nnreal]

Goal state after:
y : ℝ
hy : 0 < y
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, ↑x < a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ |(g x).im|
⊢ (fun x ↦ rexp ((f x).arg * (g x).im)) =Θ[l] fun x ↦ 1

Tactic:
rcases hl with ⟨b, hb⟩
  refine Real.isTheta_exp_comp_one.2 ⟨π * b, ?_⟩
  rw [eventually_map] at hb ⊢
  refine hb.mono fun x hx => ?_
  rw [abs_mul]
  exact mul_le_mul (abs_arg_le_pi _) hx (abs_nonneg _) Real.pi_pos.le

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x ^ (-y) = (x ^ y)⁻¹

Tactic:
by
  simp only [rpow_def_of_nonneg hx]; split_ifs <;> simp_all [exp_neg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ x ^ ↑y = ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
rw [cpow_def_of_ne_zero hx, exp_eq_exp_re_mul_sin_add_cos, mul_comm (log x)]

Goal state after:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ cexp ↑(↑y * log x).re * (cos ↑(↑y * log x).im + sin ↑(↑y * log x).im * I) =
    ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
simpa using! rpow_add_intCast hx y (-n)

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Pointwise

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst✝³ : SMul M α
inst✝² : SMul N β
inst✝¹ : FunLike F α β
inst✝ : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective fun m ↦ c • m
hc' : Injective fun n ↦ σ c • n
⊢ ⇑f ⁻¹' (σ c • t) ⊆ c • ⇑f ⁻¹' t

Tactic:
rw [subset_def, hc.forall]

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst✝³ : SMul M α
inst✝² : SMul N β
inst✝¹ : FunLike F α β
inst✝ : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective fun m ↦ c • m
hc' : Injective fun n ↦ σ c • n
⊢ ∀ (x : α), c • x ∈ ⇑f ⁻¹' (σ c • t) → c • x ∈ c • ⇑f ⁻¹' t
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inl
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x ↦ rexp (log x.1 * x.2)) p

Tactic:
refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
      exact (continuousAt_log hp.ne).comp continuous_fst.continuousAt

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞

Tactic:
simp [H, asymm H, ne_of_lt, zero_rpow_of_neg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p ↦ p.1 ^ p.2) = toNNReal ∘ (fun p ↦ p.1 ^ p.2) ∘ fun p ↦ (↑p.1, p.2)
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (x, y)

Tactic:
rw [this]

Goal state after:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p ↦ p.1 ^ p.2) = toNNReal ∘ (fun p ↦ p.1 ^ p.2) ∘ fun p ↦ (↑p.1, p.2)
⊢ ContinuousAt (toNNReal ∘ (fun p ↦ p.1 ^ p.2) ∘ fun p ↦ (↑p.1, p.2)) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr
y z : ℝ
hy✝ : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ ∞ ^ (y + z) = ∞ ^ y * ∞ ^ z

Tactic:
rcases hz.eq_or_lt with rfl | hz

Goal state after:
case top.inr.inl
y : ℝ
hy✝ : 0 ≤ y
hy : 0 < y
hz : 0 ≤ 0
⊢ ∞ ^ (y + 0) = ∞ ^ y * ∞ ^ 0

case top.inr.inr
y z : ℝ
hy✝ : 0 ≤ y
hz✝ : 0 ≤ z
hy : 0 < y
hz : 0 < z
⊢ ∞ ^ (y + z) = ∞ ^ y * ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl.inr
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ 0 ≤ 0 ^ z

Tactic:
apply zero_rpow_nonneg

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
⊢ √‖x‖ * Real.sin (x.arg / 2) = √((‖x‖ - x.re) / 2)

Tactic:
sin_half_eq_sqrt,

Goal state after:
x : ℂ
hx : 0 ≤ x.im
⊢ √‖x‖ * √((1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)

case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.arg

case hr
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
⊢ a ^ b = (a ^ n)⁻¹

Tactic:
by
  rw [h.1, NNReal.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ midpoint R p₁ p₂ -ᵥ p = ⅟2 • (p₁ -ᵥ p₂) + (⅟2 • (p₂ -ᵥ p) + ⅟2 • (p₂ -ᵥ p))

Tactic:
invOf_two_smul_add_invOf_two_smul,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ midpoint R p₁ p₂ -ᵥ p = ⅟2 • (p₁ -ᵥ p₂) + (p₂ -ᵥ p)
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ midpoint R p₁ p₂ -ᵥ p = ⅟2 • (p₁ -ᵥ p) + ⅟2 • (p₂ -ᵥ p)

Tactic:
by
  rw [← vsub_sub_vsub_cancel_right p₁ p p₂, smul_sub, sub_eq_add_neg, ← smul_neg,
    neg_vsub_eq_vsub_rev, add_assoc, invOf_two_smul_add_invOf_two_smul, ← vadd_vsub_assoc,
    midpoint_comm, midpoint, lineMap_apply]

Goal state after: