mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
__spread✝⁻⁰ : M ⧸ S ≃ M ⧸ S := Subgroup.quotientEquivOfEq ⋯
x1✝ : M ⧸ S
a✝¹ : M
x2✝ : M ⧸ S
a✝ : M
⊢ edist ((Subgroup.quotientEquivOfEq ⋯).toFun (Quot.mk (⇑(leftRel S)) a✝¹))
      ((Subgroup.quotientEquivOfEq ⋯).toFun (Quot.mk (⇑(leftRel S)) a✝)) =
    edist (Quot.mk (⇑(leftRel S)) a✝¹) (Quot.mk (⇑(leftRel S)) a✝)

Tactic:
rfl

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

Goal state before:
pp: x : ℝ
hx₁ : -(2 * π) < x
hx₂ : x < 2 * π
h : cos x = 1
⊢ x = 0

Tactic:
by
    rcases (cos_eq_one_iff _).1 h with ⟨n, rfl⟩
    rw [mul_lt_iff_lt_one_left two_pi_pos] at hx₂
    rw [neg_lt, neg_mul_eq_neg_mul, mul_lt_iff_lt_one_left two_pi_pos] at hx₁
    norm_cast at hx₁ hx₂
    obtain rfl : n = 0 := le_antisymm (by lia) (by lia)
    simp

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

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

Tactic:
rfl

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‖ = 0

Tactic:
by
  refine le_antisymm (opNorm_le_bound _ le_rfl fun x => ?_) (norm_nonneg _)
  have hker : x ∈ S.normedMk.ker.topologicalClosure := by
    rw [S.ker_normedMk, ← SetLike.mem_coe, h]
    trivial
  rw [ker_normedMk] at hker
  simp [norm_mk_eq_zero_iff_mem_closure.mpr hker]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
x : M
⊢ f x = (lift S f hf) (S.normedMk x)

Tactic:
rfl

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

Goal state before:
pp: ⊢ SurjOn sin (Icc (-(π / 2)) (π / 2)) (Icc (-1) 1)

Tactic:
simpa only [sin_neg, sin_pi_div_two] using!
    intermediate_value_Icc (neg_le_self pi_div_two_pos.le) continuous_sin.continuousOn

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

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R M
S : Submodule R M
__spread✝⁻⁰ : (M ⧸ S) ≃ₗ[R] M ⧸ S := S.quotEquivOfEq S ⋯
x✝ : M ⧸ S
a✝ : M
⊢ ‖(S.quotEquivOfEq S ⋯) (Quot.mk (⇑S.quotientRel) a✝)‖ = ‖Quot.mk (⇑S.quotientRel) a✝‖

Tactic:
rfl

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ (↑(Units.oneSub x h))⁻¹ʳ = (1 - x)⁻¹ʳ

Tactic:
rfl

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

Goal state before:
pp: x : ℝ
h0x : 0 ≤ x
hxp : x ≤ π / 2
hx0 : 0 = x
x✝ : x < π / 2 ∨ x = π / 2
⊢ 0 ≤ tan x

Tactic:
simp [hx0.symm]

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

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n) * r ^ n‖ ≤ ‖1‖ * (↑(u n) * ‖r‖ ^ n)

Tactic:
apply (norm_mul_le _ _).trans

Goal state after:
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n)‖ * ‖r ^ n‖ ≤ ‖1‖ * (↑(u n) * ‖r‖ ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ StrictMonoOn tan (Ioo (-(π / 2)) (π / 2))

Tactic:
by
  rintro x hx y hy hlt
  rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos,
    div_lt_div_iff₀ (cos_pos_of_mem_Ioo hx) (cos_pos_of_mem_Ioo hy), mul_comm, ← sub_pos, ← sin_sub]
  exact sin_pos_of_pos_of_lt_pi (sub_pos.2 hlt) <| by linarith [hx.1, hy.2]

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

Goal state before:
pp: case nil
M : Type u_4
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l l' : List M
⊢ Joined [].prod [].prod

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x✝ y : X
x : ↑I → X
h11 : Continuous[_, inst✝] x
h12 : { toFun := x, continuous_toFun := h11 }.toFun 0 = x✝
h13 : { toFun := x, continuous_toFun := h11 }.toFun 1 = y
h21 : Continuous[_, inst✝] ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }
h22 :
  { toFun := ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }, continuous_toFun := h21 }.toFun
      0 =
    x✝
h23 :
  { toFun := ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }, continuous_toFun := h21 }.toFun
      1 =
    y
⊢ { toFun := x, continuous_toFun := h11, source' := h12, target' := h13 } =
    { toFun := ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }, continuous_toFun := h21,
      source' := h22, target' := h23 }

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.symm.symm = γ

Tactic:
grind

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

Goal state before:
pp: case convert_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), N₀ ≤ b → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n ↦ f (n + N)) atTop (𝓝 0)
⊢ ∀ (n : ℕ), r * ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) n ≤ ((fun a ↦ ‖a‖) ∘ fun n ↦ f (n + N)) (n + 1)

Tactic:
grind

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

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
s : (i : ι) → Set (Z i)
x : (i : ι) → Z i
hx : ∀ (i : ι), x i ∈ s i
hjoin : ∀ (i : ι) ⦃y : Z i⦄, y ∈ s i → JoinedIn (s i) (x i) y
y : (i : ι) → Z i
hy : y ∈ univ.pi s
i : ι
⊢ y i ∈ s i

Tactic:
grind

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 : X
γ : Path x y
f : X → Y
h : Continuous[inst✝¹, inst✝] f
t : ↑I
⊢ (γ.map h) t = (f ∘ ⇑γ) t

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
x✝ : C(X × Y, Z)
a✝ : X × Y
⊢ x✝.curry.uncurry a✝ = x✝ a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
x✝ : C(X, C(Y, Z))
a✝¹ : X
a✝ : Y
⊢ (x✝.uncurry.curry a✝¹) a✝ = (x✝ a✝¹) a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Instances.ZMultiples

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ IsOpen {0}

Tactic:
isOpen_induced_iff

Goal state after:
case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ ∃ t, IsOpen t ∧ Subtype.val ⁻¹' t = {0}
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : Unique X
f : C(X, Y)
x : X
⊢ (const X ((fun f ↦ f default) f)) default = f default

Tactic:
rfl

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
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous[inst✝¹, inst✝] f
t : ↑I
⊢ f (if h : ↑t ≤ 1 / 2 then γ ⟨2 * ↑t, ⋯⟩ else γ' ⟨2 * ↑t - 1, ⋯⟩) =
    if h : ↑t ≤ 1 / 2 then (f ∘ ⇑γ) ⟨2 * ↑t, ⋯⟩ else (f ∘ ⇑γ') ⟨2 * ↑t - 1, ⋯⟩

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
x✝ : ↑I
⊢ (γ.map ⋯) x✝ = γ x✝

Tactic:
rfl

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 : X
γ : Path x y
Z : Type u_4
inst✝ : TopologicalSpace Z
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
g : Y → Z
hg : Continuous[inst✝¹, inst✝] g
x✝ : ↑I
⊢ ((γ.map hf).map hg) x✝ = (γ.map ⋯) x✝

Tactic:
rfl

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

Goal state before:
pp: case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Tactic:
have hx := norm_coe_mul p x p⁻¹

Goal state after:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : ‖↑(p⁻¹ * x)‖ = |p⁻¹| * ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
a₁ a₂ a₃ : X
b₁ b₂ b₃ : Y
γ₁ : Path a₁ a₂
δ₁ : Path a₂ a₃
γ₂ : Path b₁ b₂
δ₂ : Path b₂ b₃
⊢ (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
h✝ : ↑t ≤ 1 / 2
⊢ (Path.pi γ₀).extend (2 * ↑t) i = (γ₀ i).extend (2 * ↑t)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case neg
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
h✝ : ¬↑t ≤ 1 / 2
⊢ (Path.pi γ₁).extend (2 * ↑t - 1) i = (γ₁ i).extend (2 * ↑t - 1)

Tactic:
rfl

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₁

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
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₀

Tactic:
rfl

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✝ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

Tactic:
rfl

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₀ ≤ ↑1
h₂ : ¬↑1 ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

Tactic:
rfl

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₀ ≤ ↑1
h₃ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
x✝ : ↑I
⊢ (γ.reparam id ⋯ ⋯ ⋯) x✝ = γ x✝

Tactic:
rfl

Goal state after:
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)
hfa : Antitone f
k : ℕ
⊢ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ l

Tactic:
by
  have hm : Monotone (fun n ↦ ∑ i ∈ range (2 * n), (-1) ^ i * f i) := by
    refine monotone_nat_of_le_succ (fun n ↦ ?_)
    rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring, sum_range_succ, sum_range_succ]
    simp_rw [_root_.pow_succ', show (-1 : E) ^ (2 * n) = 1 by simp, neg_one_mul, one_mul,
      ← sub_eq_add_neg, le_sub_iff_add_le]
    gcongr
    exact hfa (by lia)
  exact hm.ge_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; lia) tendsto_id)) _

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

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
⊢ p ≤ addOrderOf u • ‖u‖

Tactic:
by
  obtain ⟨n, hn⟩ := exists_norm_eq_of_isOfFinAddOrder hu
  replace hu : (addOrderOf u : ℝ) ≠ 0 := by
    norm_cast
    exact (addOrderOf_pos_iff.mpr hu).ne'
  conv_lhs => rw [← mul_one p]
  rw [hn, nsmul_eq_mul, ← mul_assoc, mul_comm _ p, mul_assoc, mul_div_cancel₀ _ hu,
    mul_le_mul_iff_right₀ hp.out, Nat.one_le_cast, Nat.one_le_iff_ne_zero]
  contrapose hu'
  simpa only [hu', Nat.cast_zero, zero_div, mul_zero, norm_eq_zero] using hn

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

Goal state before:
pp: α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (fun x ↦ f₂ x • g x) l (𝓝 t)

Tactic:
apply hmul.congr_dist

Goal state after:
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (fun x ↦ dist (f₁ x • g x) (f₂ x • g x)) l (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case refine_2
x : ℝ
h : 0 ≤ { re := x, im := 0 }.re
⊢ { re := x, im := 0 }.arg = 0

Tactic:
exact arg_ofReal_of_nonneg h

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

Goal state before:
pp: case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

Tactic:
simp [h₀, Real.pi_ne_zero.symm]

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

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π → z.re < 0 ∧ z.im = 0

Tactic:
intro h
    rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [h₀]

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

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 → z.re = 0 ∧ 0 < z.im

Tactic:
intro h
    rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [h₀]

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

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = -(π / 2) → z.re = 0 ∧ z.im < 0

Tactic:
intro h
    rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [h₀]

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

Goal state before:
pp: ψ θ : ℝ
⊢ -ψ + θ ∈ AddSubgroup.zmultiples (2 * π) ↔ ∃ k, θ - ψ = 2 * π * ↑k

Tactic:
simp only [AddSubgroup.zmultiples_eq_closure,
    AddSubgroup.mem_closure_singleton, zsmul_eq_mul', (sub_eq_neg_add _ _).symm, eq_comm]

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

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

Tactic:
grind

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ (1 + x) * (x + 2 - x) = x + 2 + x

Tactic:
grind

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ x < x + 2

Tactic:
grind

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 0 < 1 + x

Tactic:
grind

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ (1 + x) * (x + 2 - x) = x + 2 + x

Tactic:
grind

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ x < x + 2

Tactic:
grind

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

Goal state before:
pp: case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + -(↑x.arg * I)) - 2 * ↑(Real.log ‖x‖) =
    if x.arg = π then -↑(Real.log ‖x‖) + ↑x.arg * I else -↑(Real.log ‖x‖) + -(↑x.arg * I)

Tactic:
grind

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

Goal state before:
pp: θ : Angle
⊢ θ = -θ ↔ θ = 0 ∨ θ = ↑π

Tactic:
← add_eq_zero_iff_eq_neg,

Goal state after:
θ : Angle
⊢ θ + θ = 0 ↔ θ = 0 ∨ θ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case mp
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
grind

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

Goal state before:
pp: x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else (cexp (log x * n))⁻¹) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0⁻¹ else ((starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1 else 0⁻¹ else (cexp (log x * n))⁻¹

Tactic:
inv_zero,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else (cexp (log x * n))⁻¹) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else ((starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case pos
x n : ℂ
hx : x = 0
hn : n = 0
ha : x.arg = π
⊢ 1 = 1

Tactic:
rfl

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

Goal state before:
pp: case neg
x n : ℂ
hx : x = 0
hn : n = 0
ha : ¬x.arg = π
⊢ 1 = 1

Tactic:
rfl

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

Goal state before:
pp: case pos
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : x.arg = π
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case neg
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : ¬x.arg = π
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case pos
x n : ℂ
hx : ¬x = 0
h✝ : x.arg = π
⊢ (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ = (cexp ((starRingEnd ℂ) (log x) * n))⁻¹

Tactic:
rfl

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

Goal state before:
pp: case neg
x n : ℂ
hx : ¬x = 0
h✝ : ¬x.arg = π
⊢ (cexp (log x * n))⁻¹ = (cexp (log x * n))⁻¹

Tactic:
rfl

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

Goal state before:
pp: case pos
x n : ℂ
h : x.arg = π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹

Tactic:
rfl

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

Goal state before:
pp: case inl
θ : Angle
⊢ |θ.sin| = |θ.sin|

Tactic:
rfl

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

Goal state before:
pp: case inl
θ : Angle
⊢ |θ.cos| = |θ.cos|

Tactic:
rfl

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

Goal state before:
pp: θ : ℝ
⊢ θ ∈ Set.Ioc (-π) π ↔ -π < θ ∧ θ ≤ π

Tactic:
rfl

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

Goal state before:
pp: θ : Angle
⊢ θ.toReal = π ↔ θ = ↑π

Tactic:
by rw [← toReal_inj, toReal_pi]

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

Goal state before:
pp: case pos
x n : ℂ
hcx : x = 0
hn : n = 0
hx : x.arg = π
⊢ 1 = 1

Tactic:
rfl

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

Goal state before:
pp: case neg
x n : ℂ
hcx : x = 0
hn : n = 0
hx : ¬x.arg = π
⊢ 1 = 1

Tactic:
rfl

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

Goal state before:
pp: case pos
x n : ℂ
hcx : x = 0
hn : ¬n = 0
h✝ : x.arg = π
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case neg
x n : ℂ
hcx : x = 0
hn : ¬n = 0
h✝ : ¬x.arg = π
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case pos
x n : ℂ
hcx : ¬x = 0
h✝ : x.arg = π
⊢ cexp (log x * n) = cexp (log x * n)

Tactic:
rfl

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

Goal state before:
pp: case neg
x n : ℂ
hcx : ¬x = 0
h✝ : ¬x.arg = π
⊢ cexp ((starRingEnd ℂ) (log x) * n) = cexp ((starRingEnd ℂ) (log x) * n)

Tactic:
rfl

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

Goal state before:
pp: case inr.succ
x : ℂ
x0 : x ≠ 0
n : ℕ
ih : ↑(x ^ n).arg = n • ↑x.arg
⊢ ↑(x ^ n * x).arg = (n + 1) • ↑x.arg

Tactic:
arg_mul_coe_angle (pow_ne_zero n x0) x0,

Goal state after:
case inr.succ
x : ℂ
x0 : x ≠ 0
n : ℕ
ih : ↑(x ^ n).arg = n • ↑x.arg
⊢ ↑(x ^ n).arg + ↑x.arg = (n + 1) • ↑x.arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ψ : Angle
hθ : 0 < -ψ.cos
hψ : 0 < ψ.cos
⊢ False

Tactic:
grind

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

Goal state before:
pp: case inl
θ : Angle
⊢ θ.tan = θ.tan

Tactic:
rfl

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

Goal state before:
pp: θ : Angle
this : 0 < π / 2
⊢ |θ.toReal| < π / 2 ∨ θ = 0 ∨ θ = ↑π ↔ θ = ↑π ∨ |θ.toReal| < π / 2

Tactic:
grind

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

Goal state before:
pp: case inr.«0»
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
hk : θ.toReal + ψ.toReal = -(2 * π) + π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

Tactic:
grind

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

Goal state before:
pp: case inr.«1»
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
hk : θ.toReal + ψ.toReal = π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

Tactic:
grind

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

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x ↦ b ^ x) atTop (𝓝 0)

Tactic:
simp_rw [Real.rpow_def_of_pos hb]

Goal state after:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x ↦ rexp (log b * x)) atTop (𝓝 0)
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]
  intro x
  obtain ⟨c, _, hc⟩ :=
    (atTop_basis_Ioi.tendsto_iff atTop_basis_Ioi).mp (NNReal.tendsto_rpow_atTop hy) x trivial
  have hc' : Set.Ioi ↑c ∈ 𝓝 (⊤ : ℝ≥0∞) := Ioi_mem_nhds ENNReal.coe_lt_top
  filter_upwards [hc'] with a ha
  by_cases ha' : a = ⊤
  · simp [ha', hy]
  lift a to ℝ≥0 using ha'
  simp only [Set.mem_Ioi, coe_lt_coe] at ha hc
  rw [← ENNReal.coe_rpow_of_nonneg _ hy.le]
  exact mod_cast hc a ha

Goal state after: