mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case ind
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, n₁ ≤ m → ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
⊢ ‖f n‖ ≤ max C₀ C₁ * ‖g n‖

Tactic:
| ind n h_ind =>

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
⊢ f i - f j < ε

Tactic:
sub_lt_iff_lt_add'

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
⊢ f i < f j + ε
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
| a - (l.pred • ε + ε) + ε

Tactic:
sub_add,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
| a - (l.pred • ε + ε - ε)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: x y : ℂ
⊢ dist y x < 1 → dist (cexp y) (cexp x) ≤ 2 * ‖cexp x‖ * dist y x

Tactic:
simpa [dist_eq_norm, one_add_one_eq_two] using locally_lipschitz_exp zero_le_one le_rfl x y

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)
⊢ ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
refine ⟨δ, hδ.1, ?_⟩

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 ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto f l (comap rexp atTop) ↔ Tendsto f l atTop

Tactic:
comap_exp_atTop

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

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

Tactic:
rw [← abs_cos_eq_sqrt_one_sub_sin_sq, abs_of_nonneg (cos_nonneg_of_mem_Icc ⟨hl, hu⟩)]

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s / closedBall 1 δ = cthickening δ s

Tactic:
by simp [div_eq_mul_inv, hs.mul_closedBall_one hδ]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam s ≤ ‖c⁻¹‖₊ • ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)

Tactic:
nnnorm_inv,

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam s ≤ ‖c‖₊⁻¹ • ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
⊢ ⋃ c ∈ s, sphere 0 (‖c‖ * r) = (fun x ↦ ‖x‖) ⁻¹' (fun x ↦ ‖x‖ * r) '' s

Tactic:
ext; simp [eq_comm]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr.coe
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < ↑r
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < ↑r

Tactic:
have hr : 0 < ↑r - δ := by
      refine sub_pos_of_lt ?_
      have := hs.trans_lt ((infEDist_le_edist_of_mem hz).trans_lt h)
      rw [ofReal_eq_coe_nnreal hδ.le] at this
      exact mod_cast this
    rw [edist_lt_coe, ← dist_lt_coe, ← add_sub_cancel δ ↑r] at h
    obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hr hδ h
    refine (ENNReal.add_lt_add_right ofReal_ne_top <|
      infEDist_lt_iff.2 ⟨_, mem_thickening_iff.2 ⟨_, hz, hyz⟩, edist_lt_ofReal.2 hxy⟩).trans_le ?_
    rw [← ofReal_add hr.le hδ.le, sub_add_cancel, ofReal_coe_nnreal]

Goal state after:
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 ≤ δ
x : E
⊢ cthickening ε (Metric.closedBall x δ) = Metric.closedBall x (ε + δ)

Tactic:
by
  rw [← cthickening_singleton _ hδ, cthickening_cthickening hε hδ,
      cthickening_singleton _ (add_nonneg hε hδ)]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
⊢ x +ᵥ r • ball 0 1 = ball x r

Tactic:
by
  rw [smul_unitBall_of_pos hr, vadd_ball_zero]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ Surjective mk

Tactic:
by
  rintro ⟨x⟩
  exact ⟨x, rfl⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ ∀ (x_1 : X), (∃ i, ∃ (_ : i ∈ connectedComponent x), x_1 ∈ pathComponent i) ↔ x_1 ∈ connectedComponent x

Tactic:
exact fun z ↦ ⟨fun ⟨y, hy, hz⟩ ↦ connectedComponent_eq hy ▸ pathComponent_subset_component _ hz,
    (⟨z, ·, mem_pathComponent_self z⟩)⟩

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactPair Y Z
f : C(X, Y)
g : C(Y, Z)
K : Set X
hK : IsCompact K
U : Set Z
hU : IsOpen[inst✝¹] U
hKU : MapsTo (⇑g ∘ ⇑f) K U
L : Set Y
hKL : ⇑f '' K ⊆ interior L
hLc : IsCompact L
hLU : MapsTo (⇑g) L U
⊢ ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U

Tactic:
← mapsTo_iff_image_subset

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactPair Y Z
f : C(X, Y)
g : C(Y, Z)
K : Set X
hK : IsCompact K
U : Set Z
hU : IsOpen[inst✝¹] U
hKU : MapsTo (⇑g ∘ ⇑f) K U
L : Set Y
hKL : MapsTo (⇑f) K (interior L)
hLc : IsCompact L
hLU : MapsTo (⇑g) L U
⊢ ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
⊢ ContinuousOn (fun x ↦ mkD (f x) g) s

Tactic:
have (x) (hx : x ∈ s) : Continuous (f x) := f_cont.comp_continuous
    (Continuous.prodMk_right x) fun _ ↦ ⟨hx, trivial⟩
  simp_rw [continuousOn_iff_continuous_domRestrict, s.domRestrict_def]
  refine continuous_of_continuous_uncurry _ ?_
  conv in mkD _ _ => rw [mkD_of_continuous (this x x.2)]
  exact f_cont.comp_continuous (.prodMap continuous_subtype_val continuous_id)
    fun xz ↦ ⟨xz.1.2, trivial⟩

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‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n * z ^ n‖ ≤ C * (‖z‖ / ‖w‖) ^ n

Tactic:
rw [norm_mul, norm_pow, div_pow, ← mul_comm_div]

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‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a : X
x✝ : ↑I
⊢ ((refl a).trans (refl a)) x✝ = (refl a) x✝

Tactic:
simp [Path.trans]

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
a b : X
γ : Path a b
t : ℝ
⊢ γ.extend (min t t) = γ.extend t

Tactic:
rw [min_self]

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

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ arccos x = 0

Tactic:
rw [arccos, arcsin_of_one_le hx, sub_self]

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

Goal state before:
pp: x y : ℝ
⊢ ∀ ⦃x : ℝ⦄, x ∈ Ioo 0 π → cos x ∈ Ioo (-1) 1

Tactic:
grind [arccos_pos, arccos_lt_pi, arccos_cos]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ rexp (log x) = x

Tactic:
exp_log_eq_abs hx.ne'

Goal state after:
x : ℝ
hx : 0 < x
⊢ |x| = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ log x ≤ y ↔ x ≤ rexp y

Tactic:
by rw [← exp_le_exp, exp_log hx]

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

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = log ↑(n.factorization.prod HPow.hPow)

pp: case inr.hg
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ n.factorization a) = 0 → n.factorization a = 0

Tactic:
Nat.prod_factorization_pow_eq_self hn

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = log ↑n

case inr.hg
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ n.factorization a) = 0 → n.factorization a = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
θ : Angle
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π → θ ≠ ↑π

Tactic:
rintro ⟨h, h'⟩ rfl

Goal state after:
case mp
h : -π < -(↑π).toReal
h' : -(↑π).toReal ≤ π
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x n : ℂ
hx : x.arg ≠ π
⊢ x ^ (starRingEnd ℂ) n = (starRingEnd ℂ) ((starRingEnd ℂ) x ^ n)

Tactic:
conj_cpow _ _ hx,

Goal state after:
x n : ℂ
hx : x.arg ≠ π
⊢ x ^ (starRingEnd ℂ) n = (starRingEnd ℂ) ((starRingEnd ℂ) (x ^ (starRingEnd ℂ) n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
x✝ : ℝ
⊢ (↑x✝ + ↑π).tan = (↑x✝).tan

Tactic:
rw [← coe_add, tan_coe, tan_coe]

Goal state after:
case h
x✝ : ℝ
⊢ Real.tan (x✝ + π) = Real.tan x✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

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

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

Goal state before:
pp: y : ℝ
h : y - 1 ≠ 0
x : ℝ≥0
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
by
  rw [rpow_sub' h, rpow_one]

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

Goal state before:
pp: y : ℝ
h : 1 - y ≠ 0
x : ℝ≥0
⊢ x ^ (1 - y) = x / x ^ y

Tactic:
by
  rw [rpow_sub' h, rpow_one]

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

Goal state before:
pp: case inl
y z : ℝ
⊢ 0 ^ y = 0 ^ z ↔ y = z ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
obtain rfl | hz := eq_or_ne z 0
    · simp [zero_rpow_def]
    · simp +contextual [hz]

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z

Tactic:
← rpow_le_rpow_iff_of_neg _ hx hz,

Goal state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ (y ^ z⁻¹) ^ z ≤ x ^ z ↔ y ≤ x ^ z

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < y ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z⁻¹ < y ↔ y ^ z < x

Tactic:
rw [← rpow_lt_rpow_iff_of_neg hy _ hz, rpow_inv_rpow _ hz.ne] <;> positivity

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

Goal state before:
pp: case coe
y : ℝ
x : ℝ≥0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

Tactic:
| coe x =>

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

Goal state before:
pp: case coe
y : ℝ
x : ℝ≥0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

Tactic:
| coe x =>

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

Goal state before:
pp: case coe
y z : ℝ
x : ℝ≥0
hx : ↑x ≠ 0
h'x : ↑x ≠ ∞
⊢ ↑x ^ (y + z) = ↑x ^ y * ↑x ^ z

Tactic:
| coe x =>

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

Goal state before:
pp: case coe
y : ℝ
x : ℝ≥0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
| coe x =>

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

Goal state before:
pp: case coe
y z : ℝ
x : ℝ≥0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
| coe x =>

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

Goal state before:
pp: case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a ↦ a ^ 0) x

Tactic:
simp only [rpow_zero]
    exact continuousAt_const

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

Goal state before:
pp: case top
z : ℝ
hz : z < 0
hx : 1 ≤ ∞
⊢ ∞ ^ z ≤ 1

pp: case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 ≤ ↑x✝
⊢ ↑x✝ ^ z ≤ 1

Tactic:
· simp [top_rpow_of_neg hz]

Goal state after:
case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 ≤ ↑x✝
⊢ ↑x✝ ^ z ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl.coe
z : ℝ
H : z < 0
x : ℝ≥0
⊢ (↑x ^ z).toNNReal = (↑x).toNNReal ^ z

Tactic:
| coe x =>

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : Module k V1
inst✝² : AffineSpace V1 P1
inst✝¹ : IsDomain k
inst✝ : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ c₁ = c₂ ∨ p₁ = p₀ ↔ p₀ = p₁ ∨ c₁ = c₂

Tactic:
or_comm,

Goal state after:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : Module k V1
inst✝² : AffineSpace V1 P1
inst✝¹ : IsDomain k
inst✝ : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ p₁ = p₀ ∨ c₁ = c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ [x -[𝕜] y]
⊢ z ∈ openSegment 𝕜 x y

Tactic:
rw [← insert_endpoints_openSegment] at hz
  exact (hz.resolve_left hx.symm).resolve_left hy.symm

Goal state after:
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
x : E
s : Set E
inst✝ : ZeroLEOneClass 𝕜
hs : StarConvex 𝕜 x s
h : s.Nonempty
⊢ x ∈ s

Tactic:
by
  obtain ⟨y, hy⟩ := h
  convert! hs hy zero_le_one le_rfl (add_zero 1)
  rw [one_smul, zero_smul, add_zero]

Goal state after:
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ ⇑f '' s

Tactic:
exact ⟨a • x + b • y, hs hy ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ vectorSpan k ∅ = ⊥

Tactic:
vectorSpan_def,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Submodule.span k (∅ -ᵥ ∅) = ⊥
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
hz : z ∈ range ⇑(lineMap x y)
⊢ openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)

Tactic:
by
  rcases hz with ⟨c, rfl⟩
  simp only [openSegment_eq_image_lineMap, ← mapsTo_iff_image_subset]
  rintro a ⟨h₀, h₁⟩
  rcases lt_trichotomy a c with (hac | rfl | hca)
  · right
    left
    have hc : 0 < c := h₀.trans hac
    refine ⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, ?_⟩
    simp only [← homothety_eq_lineMap, ← homothety_mul_apply, div_mul_cancel₀ _ hc.ne']
  · left
    rfl
  · right
    right
    have hc : 0 < 1 - c := sub_pos.2 (hca.trans h₁)
    simp only [← lineMap_apply_one_sub y]
    refine
      ⟨(a - c) / (1 - c), ⟨div_pos (sub_pos.2 hca) hc, (div_lt_one hc).2 <| sub_lt_sub_right h₁ _⟩,
        ?_⟩
    simp only [← homothety_eq_lineMap, ← homothety_mul_apply, sub_mul, one_mul,
      div_mul_cancel₀ _ hc.ne', sub_sub_sub_cancel_right]

Goal state after:
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
c : 𝕜
⊢ StarConvex 𝕜 (z + c • x) ((fun x ↦ z + c • x) '' s)

Tactic:
by
  have h := (hs.smul c).add_left z
  rwa [← image_smul, image_image] at h

Goal state after:
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : IsStrictOrderedModule 𝕜 E
inst✝ : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ a • x + b • x - a • y < b • x

Tactic:
sub_lt_iff_lt_add'

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : IsStrictOrderedModule 𝕜 E
inst✝ : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ a • x + b • x < a • y + b • x
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ x ∈ t • s

Tactic:
by
  rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']
  exact hs.smul_mem hx (by positivity) (inv_le_one_of_one_le₀ ht)

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
h : ↑s.direction = s
⊢ 0 ∈ s

Tactic:
rw [← h]; simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
⊢ vectorSpan k ∅ = ⊥

Tactic:
vectorSpan_def,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
⊢ Submodule.span k (∅ -ᵥ ∅) = ⊥
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : Set ι
x y : (i : ι) → M i
⊢ [x -[𝕜] y] ⊆ s.pi fun i ↦ [x i -[𝕜] y i]

Tactic:
by
  rintro z ⟨a, b, ha, hb, hab, hz⟩ i -
  exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩

Goal state after:
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : Set ι
x y : (i : ι) → M i
⊢ openSegment 𝕜 x y ⊆ s.pi fun i ↦ openSegment 𝕜 (x i) (y i)

Tactic:
by
  rintro z ⟨a, b, ha, hb, hab, hz⟩ i -
  exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩

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

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ ‖b‖ / ‖a‖ ≤ 1

Tactic:
exact div_le_one_of_le₀ hba (norm_nonneg _)

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕜 (id V) S
hV : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
⊢ False

Tactic:
have : ∀ᶠ n in l, ∃ x : S, ε n • (x : E) ∉ V := by
    filter_upwards [hε] with n hn
    rw [absorbs_iff_norm] at hVS
    push Not at hVS
    rcases hVS ‖(ε n)⁻¹‖ with ⟨a, haε, haS⟩
    rcases Set.not_subset.mp haS with ⟨x, hxS, hx⟩
    refine ⟨⟨x, hxS⟩, fun hnx => ?_⟩
    rw [← Set.mem_inv_smul_set_iff₀ hn] at hnx
    exact hx (hVb.smul_mono haε hnx)

Goal state after:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕜 (id V) S
hV : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
this : ∀ᶠ (n : ι) in l, ∃ x, ε n • ↑x ∉ V
⊢ False