mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := ⋯
hj : j = n + k
⊢ -1 ≤ (‖x‖ / ↑n.succ) ^ k - 1

Tactic:
simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left]
        positivity

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x‖ ^ 2 * 1 = ‖x‖ ^ 2

Tactic:
by rw [mul_one]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 2
⊢ (∑ m ∈ range 3, (x / 2) ^ m / ↑m.factorial + (x / 2) ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3)) ^ 2 <
    (2 + x) / (2 - x)

Tactic:
by
    rw [lt_div_iff₀ (by linarith), ← sub_pos]
    simp only [Finset.sum_range_succ]
    ring_nf
    positivity

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

Goal state before:
pp: case hrec
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖

Tactic:
case hrec =>
    filter_upwards [eventually_forall_ge_atTop.mpr hg, eventually_forall_ge_atTop.mpr hf, hrec]
      with n₀ hn₀ hn₀' hnrec
    obtain ⟨C₀, hnrec⟩ := hnrec
    refine ⟨C₀, ?_⟩
    filter_upwards [hnrec, eventually_ge_atTop n₀]
    grind [Real.norm_eq_abs]

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

Goal state before:
pp: r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ (fun n ↦ r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n

Tactic:
refine (IsLittleO.of_norm_left ?_).of_norm_right

Goal state after:
r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ (fun x ↦ ‖r₁ ^ x‖) =o[atTop] fun x ↦ ‖r₂ ^ x‖
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case inr
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x ↦ (b * rexp x + c) / x ^ n) atTop atTop

Tactic:
simp only [add_div, mul_div_assoc]

Goal state after:
case inr
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x ↦ b * (rexp x / x ^ n) + c / x ^ n) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 0 < 2 * π

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: ⊢ 0 < 2 * π

Tactic:
by linarith [pi_pos]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
⊢ ‖S.normedMk‖ = 1

Tactic:
by
  refine le_antisymm (norm_normedMk_le S) ?_
  obtain ⟨x, hx⟩ : ∃ x : M, 0 < ‖(x : M ⧸ S)‖ := by
    refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_
    exact (norm_nonneg _).lt_of_ne' <| mt norm_mk_eq_zero_iff_mem_closure.1 hx
  refine (le_mul_iff_one_le_left hx).1 ?_
  exact norm_lift_apply_le S.normedMk (fun x ↦ (eq_zero_iff x).2) x

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

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 :
  (∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_8 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 : (∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
a : ℝ
ha : a < R
H : ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
⊢ ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x

Tactic:
refine ⟨a, A ⟨?_, ha⟩, .of_norm_eventuallyLE H⟩
    exact nonneg_of_eventually_pow_nonneg (H.mono fun n ↦ (abs_nonneg _).trans)

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

Goal state before:
pp: case refine_1
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ 0 ≤ π / 3

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: case refine_2
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ π / 3 < π

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: ⊢ 0 ≤ 2

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: case hx
⊢ 0 ≤ 3

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: ⊢ 2 ≠ 0

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: case hl
⊢ -π ≤ π / 3

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: case hr
⊢ π / 3 ≤ π

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: ⊢ cos (π / 6) = √3 / 2

Tactic:
rw [show (6 : ℝ) = 3 * 2 by norm_num, div_mul_eq_div_div, cos_half, cos_pi_div_three, one_add_div,
    ← div_mul_eq_div_div, two_add_one_eq_three, sqrt_div, sqrt_mul_self] <;> linarith [pi_pos]

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

Goal state before:
pp: α : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝⁷ : Field R✝
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
v w : AbsoluteValue R✝ S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
_i : OrderTopology S
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
hx : ‖x‖ < 1
⊢ Summable fun n ↦ x ^ n

Tactic:
have h1 : Summable fun n : ℕ ↦ ‖x‖ ^ n := summable_geometric_of_lt_one (norm_nonneg _) hx

Goal state after:
α : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝⁷ : Field R✝
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
v w : AbsoluteValue R✝ S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
_i : OrderTopology S
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
hx : ‖x‖ < 1
h1 : Summable fun n ↦ ‖x‖ ^ n
⊢ Summable fun n ↦ x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
⊢ -x < π / 2

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
⊢ -x < π / 2

Tactic:
by linarith [pi_pos]

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

Goal state before:
pp: ⊢ cos ↑π = -1

Tactic:
rw [← ofReal_cos, Real.cos_pi]; simp

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
⊢ ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s

pp: case refine_2
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s
⊢ s ∈ 𝓝 (const X c)

Tactic:
· rcases ContinuousMap.mem_nhds_iff.mp hs with ⟨S, hSf, hS, hSsub⟩
    choose hScompact hSopen hSmaps using hS
    have : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c := by
      simp only [biInter_mem hSf, Prod.forall, iInter_mem]
      rintro K U hKU ⟨x, hx⟩
      exact (hSopen K U hKU).mem_nhds <| hSmaps K U hKU hx
    rcases h.mem_iff.mp this with ⟨i, hpi, hi⟩
    refine ⟨(⋃ KU ∈ S, KU.1, i), ⟨hSf.isCompact_biUnion <| Prod.forall.2 hScompact, hpi⟩,
      Subset.trans ?_ hSsub⟩
    intro f hf K V hKV
    rcases K.eq_empty_or_nonempty with rfl | hKne
    · exact mapsTo_empty _ _
    · refine hf.out.mono (subset_biUnion_of_mem (u := Prod.fst) hKV) (hi.trans ?_)
      exact (biInter_subset_of_mem hKV).trans <| iInter_subset _ hKne

Goal state after:
case refine_2
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s
⊢ s ∈ 𝓝 (const X c)
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
r : X
f : C(Y, Z)
K : Set Y
hK : IsCompact K
U : Set (X × Z)
hU : IsOpen[instTopologicalSpaceProd] U
H : MapsTo (⇑((const Y (r, f).1).prodMk (r, f).2)) K U
V : Set X
W : Set Z
hV : IsOpen[inst✝²] V
hW : IsOpen[inst✝] W
hrV : {r} ⊆ V
hKW : ⇑f '' K ⊆ W
hVW : V ×ˢ W ⊆ U
⊢ r ∈ V

Tactic:
simpa using hrV

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

Goal state before:
pp: case refine_1
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ ∑ x ∈ Finset.range n, b * (f x.succ - f x)

Tactic:
← mul_sum

Goal state after:
case refine_1
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ b * ∑ i ∈ Finset.range n, (f i.succ - f i)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) +
      (-1) ^ (2 * n + 1 + 1) * f (2 * n + 1 + 1)

Tactic:
simp_rw [_root_.pow_succ', show (-1 : E) ^ (2 * n) = 1 by simp, neg_one_mul, neg_neg, one_mul,
      ← sub_eq_add_neg, sub_add_eq_add_sub, le_sub_iff_add_le]

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + f (2 * n + 1 + 1)
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ range ⇑(γ.reparam f hfcont hf₀ hf₁) = range ⇑γ

Tactic:
by
  change range (γ ∘ f) = range γ
  have : range f = univ := by
    rw [range_eq_univ]
    intro t
    have h₁ : Continuous (Set.IccExtend (zero_le_one' ℝ) f) := by fun_prop
    have := intermediate_value_Icc (zero_le_one' ℝ) h₁.continuousOn
    · rw [IccExtend_left, IccExtend_right, Icc.mk_zero, Icc.mk_one, hf₀, hf₁] at this
      rcases this t.2 with ⟨w, hw₁, hw₂⟩
      rw [IccExtend_of_mem _ _ hw₁] at hw₂
      exact ⟨_, hw₂⟩
  rw [range_comp, this, image_univ]

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

Goal state before:
pp: x : ℝ
⊢ arcsin x = π / 2 - arccos x

Tactic:
simp [arccos]

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

Goal state before:
pp: x : ℝ
⊢ 0 < arccos x ↔ x < 1

Tactic:
simp [arccos]

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

Goal state before:
pp: ⊢ arccos 0 = π / 2

Tactic:
simp [arccos]

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

Goal state before:
pp: ⊢ arccos 1 = 0

Tactic:
simp [arccos]

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

Goal state before:
pp: x : ℝ
⊢ arccos x = π / 2 ↔ x = 0

Tactic:
simp [arccos]

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

Goal state before:
pp: x : ℝ
⊢ arccos x ≤ π / 2 ↔ 0 ≤ x

Tactic:
simp [arccos]

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

Goal state before:
pp: x : ℝ
⊢ arccos x < π / 2 ↔ 0 < x

Tactic:
simp [arccos]

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

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

Tactic:
rcases hx.eq_or_lt with (rfl | hx)

Goal state after:
case inl
hx : 0 ≤ 0
⊢ 0 < log 0 ↔ 1 < 0

case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 0 < log x ↔ 1 < x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ log x ≤ 0 ↔ x ≤ 1

Tactic:
rcases hx.eq_or_lt with (rfl | hx)

Goal state after:
case inl
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ↔ 0 ≤ 1

case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 1 ≤ x⁻¹

Tactic:
rw [← le_inv_comm₀ h1 zero_lt_one, inv_one]

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ x ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case refine_2
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (fun x ↦ ↑x.arg * I) x

Tactic:
have h_cont_mul : Continuous fun x : ℂ => x * I := by fun_prop

Goal state after:
case refine_2
x : ℂ
h : x ∈ slitPlane
h_cont_mul : Continuous fun x ↦ x * I
⊢ ContinuousAt (fun x ↦ ↑x.arg * I) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
hx : x = 0
⊢ x ^ 1 = x

Tactic:
by simp [hx, cpow_def]

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

Goal state before:
pp: case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑π - ↑θ - ↑ψ = 0
⊢ ↑θ + ↑ψ = ↑π

Tactic:
sub_sub,

Goal state after:
case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑π - (↑θ + ↑ψ) = 0
⊢ ↑θ + ↑ψ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case left
⊢ -π < π / 2

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: case right
⊢ π / 2 ≤ π

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: case left
⊢ -π < -π / 2

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: case right
⊢ -π / 2 ≤ π

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: ⊢ -π / 2 ≠ 0

Tactic:
exact div_ne_zero (neg_ne_zero.2 Real.pi_ne_zero) two_ne_zero

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

Goal state before:
pp: θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
⊢ |(-↑θ).toReal| = θ

Tactic:
by_cases hnegpi : θ = π

Goal state after:
case pos
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : θ = π
⊢ |(-↑θ).toReal| = θ

case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ |(-↑θ).toReal| = θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ |θ.cos| = |ψ.sin|

Tactic:
by
  simp_rw [two_zsmul, ← two_nsmul] at h
  exact abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi h

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

Goal state before:
pp: y : ℝ
hy : 0 < y
b : ℝ
⊢ 0 ≤ b → ∀ᶠ (x : ℝ) in atTop, x ^ y ∈ Set.Ici b

Tactic:
hb

Goal state after:
y : ℝ
hy : 0 < y
b : ℝ
hb : 0 ≤ b
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ y ∈ Set.Ici b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 ≤ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
by
  rcases hy.eq_or_lt with (rfl | hy)
  · rw [zero_add, rpow_zero, one_mul]
  exact rpow_add' hx (ne_of_gt <| add_pos_of_pos_of_nonneg hy hz)

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

Goal state before:
pp: case refine_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 (0, z)) ((fun x ↦ ‖x‖) ∘ fun x ↦ rexp (-(x.1.arg * x.2.im)))

Tactic:
· simp only [Function.comp_def, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
    rcases exists_gt |im z| with ⟨C, hC⟩
    refine ⟨Real.exp (π * C), eventually_map.2 ?_⟩
    refine
      (((continuous_im.comp continuous_snd).abs.tendsto (_, z)).eventually (gt_mem_nhds hC)).mono
        fun z hz => Real.exp_le_exp.2 <| (neg_le_abs _).trans ?_
    rw [_root_.abs_mul]
    exact
      mul_le_mul (abs_le.2 ⟨(neg_pi_lt_arg _).le, arg_le_pi _⟩) hz.le (_root_.abs_nonneg _)
        Real.pi_pos.le

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Tactic:
rcases hx.eq_or_lt with (rfl | hx)

Goal state after:
case inl
y : ℝ
hx : 0 ≤ 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y

case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
y : ℝ
hx : 0 ≤ 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y

pp: case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Tactic:
· rcases _root_.em (y = 0) with (rfl | hy) <;> simp [*, zero_lt_one]

Goal state after:
case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0

Tactic:
rcases hx.eq_or_lt with (rfl | hx)

Goal state after:
case inl
y : ℝ
hx : 0 ≤ 0
⊢ 1 < 0 ^ y ↔ 1 < 0 ∧ 0 < y ∨ 0 < 0 ∧ 0 < 1 ∧ y < 0

case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case neg
x y : ℝ≥0
hy : 1 < ↑y
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ ↑y

Tactic:
have := NNReal.eventually_pow_one_div_le x (mod_cast hy : 1 < y)

Goal state after:
case neg
x y : ℝ≥0
hy : 1 < ↑y
this : ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ ↑y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
convert! this y x z hz (le_of_not_ge hxy) using 2 <;> simp only [mul_comm, and_comm, or_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inl
R : Type u_1
inst✝¹⁰ : CommSemiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_5
inst✝⁵ : CommSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : (algebraMap S R) a = 0
⊢ SameRay R v (a • v)

Tactic:
rw [← algebraMap_smul R a v, h, zero_smul]
    exact zero_right _

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : (fun x ↦ 2 • x) x = (fun x ↦ 2 • x) y
⊢ x = y

Tactic:
dsimp at h

Goal state after:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : 2 • x = 2 • y
⊢ x = y
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: case fst
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : AffineSpace V2 P2
inst✝⁷ : AddCommGroup V3
inst✝⁶ : AffineSpace V3 P3
inst✝⁵ : Module k V1
inst✝⁴ : Module k V2
inst✝³ : Module k V3
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
v : V2
f : V1 →ₗ[k] V2
⊢ ((fun f ↦ (f 0, f.linear)) ((fun p ↦ p.2.toAffineMap + const k V1 p.1) (v, f))).1 = (v, f).1

Tactic:
simp [const_linear]

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

Goal state before:
pp: case snd
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : AffineSpace V2 P2
inst✝⁷ : AddCommGroup V3
inst✝⁶ : AffineSpace V3 P3
inst✝⁵ : Module k V1
inst✝⁴ : Module k V2
inst✝³ : Module k V3
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
v : V2
f : V1 →ₗ[k] V2
x✝ : V1
⊢ ((fun f ↦ (f 0, f.linear)) ((fun p ↦ p.2.toAffineMap + const k V1 p.1) (v, f))).2 x✝ = (v, f).2 x✝

Tactic:
simp [const_linear]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)

Tactic:
refine
      ⟨r₂ / (r₁ + r₂), r₁ / (r₁ + r₂), div_nonneg h₂.le h₁₂.le, div_nonneg h₁.le h₁₂.le, ?_, ?_, ?_⟩

Goal state after:
case inr.inr.refine_1
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ r₂ / (r₁ + r₂) + r₁ / (r₁ + r₂) = 1

case inr.inr.refine_2
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)

case inr.inr.refine_3
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
⊢ openSegment 𝕜 x y = ⇑(AffineMap.lineMap x y) '' Ioo 0 1

Tactic:
convert openSegment_eq_image 𝕜 x y
  exact AffineMap.lineMap_apply_module _ _ _

Goal state after: