mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
⊢ Injective fun f ↦ ⇑f

Tactic:
rintro ⟨_⟩ ⟨_⟩
  simp

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
⊢ IsBigOWith (∑ i ∈ s, C i) l (∑ i ∈ s, A i) g

Tactic:
induction s using Finset.cons_induction with
  | empty =>
      rw [Finset.sum_empty]
      apply isBigOWith_zero'
  | cons i s is IH =>
    simp only [Finset.sum_cons, Finset.forall_mem_cons] at h ⊢
    exact h.1.add (IH h.2)

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ ↑n.factorial * ↑n * (↑n * ↑n.factorial)⁻¹ * (↑n.succ - (↑n.succ)⁻¹ ^ (j - n) * ↑n.succ) =
    ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)

Tactic:
mul_comm (n : α) n.factorial,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ ↑n.factorial * ↑n * (↑n.factorial * ↑n)⁻¹ * (↑n.succ - (↑n.succ)⁻¹ ^ (j - n) * ↑n.succ) =
    ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖

Tactic:
rw [mul_comm, one_div, ← div_eq_mul_inv, le_div_iff₀, mul_sub, mul_one, mul_comm]

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ - c * ‖f₂ x‖ ≤ ‖f₂ x - f₁ x‖

α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ 0 < 1 - c
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (Complex.cosh ↑x).re * 2 = (cexp ↑x).re + (cexp ↑(-x)).re

Tactic:
Complex.ofReal_neg,

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

Goal state before:
pp: n : ℕ
⊢ (fun x ↦ cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x ↦ x ^ n

Tactic:
by
  rcases eq_zero_or_pos n with rfl | hn
  · simpa using continuous_exp.continuousAt.norm.isBoundedUnder_le
  · refine .of_bound (n.succ / (n ! * n)) ?_
    rw [NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff]
    refine ⟨1, one_pos, fun x hx ↦ ?_⟩
    convert! exp_bound hx.out.le hn using 1
    simp [field]

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
a : ℝ
ha : a ∈ Set.Ioo (-R) R
H : f =O[atTop] fun x ↦ a ^ x
⊢ ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x

Tactic:
by
    rcases exists_between (abs_lt.2 ha) with ⟨b, hab, hbR⟩
    exact ⟨b, ⟨(abs_nonneg a).trans_lt hab, hbR⟩,
      H.trans_isLittleO (isLittleO_pow_pow_of_abs_lt_left (hab.trans_le (le_abs_self b)))⟩

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

Goal state before:
pp: ⊢ Tendsto rexp (𝓝 0) (𝓝 1)

Tactic:
by
  convert! continuous_exp.tendsto 0
  simp

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

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ rexp (x + 1) / (rexp 1 * C) = rexp x / C

Tactic:
rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']

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

Goal state before:
pp: x : ℝ
⊢ sin (x - π / 2) = -cos x

Tactic:
simp [sub_eq_add_neg, sin_add]

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

Goal state before:
pp: x : ℝ
⊢ sin (π / 2 - x) = cos x

Tactic:
simp [sub_eq_add_neg, sin_add]

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ ball x δ * s = x • thickening δ s

Tactic:
by rw [mul_comm, mul_ball]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : 1 < v a
⊢ Tendsto (fun n ↦ v (1 / (1 + a ^ n))) atTop (𝓝 0)

Tactic:
simp_rw [div_eq_mul_inv, one_mul, map_inv₀, fun n ↦ add_comm 1 (a ^ n)]
  refine (tendsto_atTop_mono (fun n ↦ v.le_add _ _) ?_).inv_tendsto_atTop
  simpa using (tendsto_atTop_add_right_of_le _ _ (tendsto_pow_atTop_atTop_of_one_lt ha)
    (fun _ ↦ le_rfl)).congr fun n ↦ (sub_eq_add_neg (v a ^ n) 1).symm

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
hr : 0 < ↑r - δ
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < ↑r

Tactic:
rw [edist_lt_coe, ← dist_lt_coe, ← add_sub_cancel δ ↑r] at h

Goal state after:
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 : dist x z < δ + (↑r - δ)
hr : 0 < ↑r - δ
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < ↑r
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℂ
⊢ sin (x - ↑π / 2) = -cos x

Tactic:
simp [sub_eq_add_neg, sin_add]

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

Goal state before:
pp: x : ℂ
⊢ sin (↑π / 2 - x) = cos x

Tactic:
simp [sub_eq_add_neg, sin_add]

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

Goal state before:
pp: ⊢ Function.Antiperiodic cexp (↑π * I)

Tactic:
by simp [exp_add, exp_mul_I]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: 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
⊢ (𝓝 (const X c)).HasBasis (fun Ki ↦ IsCompact Ki.1 ∧ p Ki.2) fun Ki ↦ {f | MapsTo (⇑f) Ki.1 (U Ki.2)}

Tactic:
by
  refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun hs ↦ ?_⟩⟩
  · 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
  · rcases hs with ⟨⟨K, i⟩, ⟨hK, hpi⟩, hi⟩
    filter_upwards [eventually_mapsTo hK isOpen_interior fun x _ ↦
      mem_interior_iff_mem_nhds.mpr <| h.mem_of_mem hpi] with f hf
    exact hi <| hf.mono_right interior_subset

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
⊢ ∀ (x : C(X, Y) × C(Y, Z)) (K : Set X),
    IsCompact K →
      ∀ (U : Set Z),
        IsOpen[inst✝¹] U →
          MapsTo (⇑(x.2.comp x.1)) K U → ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 x, MapsTo (⇑(a.2.comp a.1)) K U

Tactic:
intro ⟨f, g⟩ K hK U hU (hKU : MapsTo (g ∘ f) K U)

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
⊢ ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), PathConnectedSpace (Z i)
⊢ IsPathConnected (Set.pi ?m.12 fun i ↦ univ)

pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), PathConnectedSpace (Z i)
⊢ Set ι

Tactic:
exact .pi fun _ ↦ isPathConnected_univ

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑0
h₂ : ¬↑0 ≤ t₁
h₄ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

pp: case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑0
h✝ : t₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend t₀

pp: case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑0
h✝ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

Tactic:
all_goals rfl

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

Goal state before:
pp: x : ℂ
⊢ Real.sin x.arg = x.im / ‖x‖

Tactic:
by
  unfold arg; split_ifs <;>
    simp [sub_eq_add_neg, Real.sin_arcsin (abs_le.1 (abs_im_div_norm_le_one x)).1
      (abs_le.1 (abs_im_div_norm_le_one x)).2, Real.sin_add, neg_div, Real.arcsin_neg, Real.sin_neg]

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

Goal state before:
pp: case inr
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n : ℕ
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
upper : ∀ (k : ℕ), ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
lower : ∀ (k : ℕ), ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i
I : ∀ (n : ℕ), 0 ≤ f n
h : Odd n
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range n, (-1) ^ i * f i| ≤ f n

Tactic:
obtain ⟨n, rfl⟩ := odd_iff_exists_bit1.mp h
    specialize upper (n + 1)
    specialize lower n
    rw [Nat.mul_add, Finset.sum_range_succ] at upper
    rw [abs_sub_le_iff]
    constructor
    · rw [sub_le_iff_le_add, add_comm]
      exact lower.trans (le_add_of_nonneg_right (I (2 * n + 1)))
    · simpa [Finset.sum_range_succ, add_comm, pow_add] using upper

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

Goal state before:
pp: n : ℤ
hn : 0 < -n
⊢ 1 ≤ -↑n

Tactic:
exact mod_cast hn

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

Goal state before:
pp: θ : Angle
⊢ -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
rw [← not_or, ← neg_eq_self_iff.not]

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

Goal state before:
pp: n : ℕ
⊢ (fun x ↦ log x ^ n) =o[atTop] id

Tactic:
by
  rw [Asymptotics.isLittleO_iff_tendsto']
  · simpa using tendsto_pow_log_div_mul_add_atTop 1 0 n one_ne_zero
  filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim

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

Goal state before:
pp: case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0

Tactic:
lift z to ℝ using him

Goal state after:
case convert_1
z : ℝ
hre : (↑z).re < 0
⊢ ‖↑z‖ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ ↑(-x).arg = ↑x.arg + ↑π

Tactic:
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
  · rw [arg_neg_eq_arg_add_pi_of_im_neg hi, Real.Angle.coe_add]
  · 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, ←
        Real.Angle.coe_add, ← two_mul, Real.Angle.coe_two_pi, Real.Angle.coe_zero]
    · exact False.elim (hx (ext hr hi))
    · rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr),
        Real.Angle.coe_zero, zero_add]
  · rw [arg_neg_eq_arg_sub_pi_of_im_pos hi, Real.Angle.coe_sub, Real.Angle.sub_coe_pi_eq_add_coe_pi]

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

Goal state before:
pp: θ : ℝ
⊢ (cos ↑θ + sin ↑θ * I).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
by
  rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_eq_toIocMod zero_lt_one]

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

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(x / y).arg = ↑x.arg - ↑y.arg

Tactic:
by
  rw [div_eq_mul_inv, arg_mul_coe_angle hx (inv_ne_zero hy), arg_inv_coe_angle, sub_eq_add_neg]

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

Goal state before:
pp: case convert_3
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0

Tactic:
lift z to ℝ using him

Goal state after:
case convert_3
z : ℝ
hre : (↑z).re < 0
⊢ ‖↑z‖ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case refine_1
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ‖z‖ ≠ 0

Tactic:
lift z to ℝ using him

Goal state after:
case refine_1
z : ℝ
hre : (↑z).re < 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] ↑z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ‖↑z‖ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: α : Type u_1
f : α → ℝ
⊢ f ^ 0 = 1

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
⊢ f ^ 1 = f

Tactic:
ext; simp

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

Goal state before:
pp: a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ ((rexp ∘ fun x ↦ a * (x / (b * rexp x + c))) ∘ log) x = (fun x ↦ x ^ (a / (b * x + c))) x

Tactic:
simp only [Set.mem_Ioi, Function.comp_apply] at hx ⊢

Goal state after:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * rexp (log x) + c))) = x ^ (a / (b * x + c))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
⊢ False

Tactic:
have := norm_prime_cpow_le_one_half ⟨p, hp⟩ hs

Goal state after:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : ‖↑↑⟨p, hp⟩ ^ (-s)‖ ≤ 1 / 2
⊢ False
Module: Mathlib.Algebra.Order.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : CommSemiring α
inst✝⁶ : PartialOrder α
inst✝⁵ : Semiring β
inst✝⁴ : PartialOrder β
inst✝³ : Algebra α β
inst✝² : ZeroLEOneClass β
inst✝¹ : Nontrivial β
inst✝ : SMulPosStrictMono α β
⊢ StrictMono ⇑(algebraMap α β)

Tactic:
simpa [Algebra.smul_def] using smul_one_strictMono (α := α) β

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
⊢ SameRay R x z

Tactic:
by
  rcases eq_or_ne x 0 with (rfl | hx); · exact zero_left z
  rcases eq_or_ne z 0 with (rfl | hz); · exact zero_right x
  rcases eq_or_ne y 0 with (rfl | hy)
  · exact (hy rfl).elim (fun h => (hx h).elim) fun h => (hz h).elim
  rcases hxy.exists_pos hx hy with ⟨r₁, r₂, hr₁, hr₂, h₁⟩
  rcases hyz.exists_pos hy hz with ⟨r₃, r₄, hr₃, hr₄, h₂⟩
  refine Or.inr (Or.inr <| ⟨r₃ * r₁, r₂ * r₄, mul_pos hr₃ hr₁, mul_pos hr₂ hr₄, ?_⟩)
  rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr
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 : 0 < (algebraMap S R) a
⊢ (algebraMap S R) a • v = 1 • a • v

Tactic:
module

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case e'_2
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (rx * ry) • (x + y) = ry • rx • x + rx • ry • y

Tactic:
module

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case e'_3
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (ry * rz₁ + rx * rz₂) • z = ry • rz₁ • z + rx • rz₂ • z

Tactic:
module

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ ≠ 0
hc₂ : c₂ ≠ 0
hpos : 0 < c₁ * c₂
h₁ : 0 < c₁
h₂ : 0 < c₂
⊢ c₂ • c₁ • v = c₁ • c₂ • v

Tactic:
module

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ ≠ 0
hc₂ : c₂ ≠ 0
hpos : 0 < c₁ * c₂
h₁ : c₁ < 0
h₂ : c₂ < 0
⊢ -c₂ • c₁ • v = -c₁ • c₂ • v

Tactic:
module

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 → P2
f' : V1 →ₗ[k] V2
p : P1
h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p
p' : P1
v : V1
⊢ f' (v + (p' -ᵥ p)) +ᵥ f p = f' v +ᵥ f' (p' -ᵥ p) +ᵥ f p

Tactic:
f'.map_add,

Goal state after:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 → P2
f' : V1 →ₗ[k] V2
p : P1
h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p
p' : P1
v : V1
⊢ (f' v + f' (p' -ᵥ p)) +ᵥ f p = f' v +ᵥ f' (p' -ᵥ p) +ᵥ f p
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case a
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 < 0
⊢ -m 0 • x + m 0 • x - (-m 1 • -y + -(m 1 • y)) = 0

Tactic:
module

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case a
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : 0 < m 1
⊢ -m 0 • x + m 0 • x - (m 1 • y + -(m 1 • y)) = 0

Tactic:
module

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.inl.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
rw [Fin.exists_fin_two] at hmne

Goal state after:
case neg.refine_2.inr.inl.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : m 0 ≠ 0 ∨ m 1 ≠ 0
hm0 : m 0 = 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : AddCommGroup V₃
inst✝⁸ : AddCommGroup V₄
inst✝⁷ : Module k V₁
inst✝⁶ : Module k V₂
inst✝⁵ : Module k V₃
inst✝⁴ : Module k V₄
inst✝³ : AffineSpace V₁ P₁
inst✝² : AffineSpace V₂ P₂
inst✝¹ : AffineSpace V₃ P₃
inst✝ : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
x✝ : P₁ →ᵃ[k] P₃
⊢ (fun f ↦ (↑e₂.symm).comp (f.comp ↑e₁)) ((fun f ↦ (↑e₂).comp (f.comp ↑e₁.symm)) x✝) = x✝

Tactic:
ext; simp

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : AddCommGroup V₃
inst✝⁸ : AddCommGroup V₄
inst✝⁷ : Module k V₁
inst✝⁶ : Module k V₂
inst✝⁵ : Module k V₃
inst✝⁴ : Module k V₄
inst✝³ : AffineSpace V₁ P₁
inst✝² : AffineSpace V₂ P₂
inst✝¹ : AffineSpace V₃ P₃
inst✝ : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
x✝ : P₂ →ᵃ[k] P₄
⊢ (fun f ↦ (↑e₂).comp (f.comp ↑e₁.symm)) ((fun f ↦ (↑e₂.symm).comp (f.comp ↑e₁)) x✝) = x✝

Tactic:
ext; simp

Goal state after: