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

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
ψ : NormedAddGroupHom V₁ ↥(f.equalizer g)
⊢ f.comp ((ι f g).comp ψ) = g.comp ((ι f g).comp ψ)

Tactic:
rw [← comp_assoc, ← comp_assoc, comp_ι_eq]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case pos
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

Tactic:
by_cases hL : L.NeBot
    · exact ⟨fun h ↦ (e.hasSum.mp ((e.summable.mpr hf).hasSum_iff.mpr h)).tsum_eq, fun h ↦
        (e.hasSum.mpr (hf.hasSum_iff.mpr h)).tsum_eq⟩
    · simp only [tsum_bot hL, eq_symm_apply]
      constructor <;> rintro rfl
      exacts [e.map_finsum f, (e.map_finsum f).symm]

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: i j : Fin 2
⊢ (basisOneI.repr (![1, I] i)) j = (Finsupp.single i 1) j

Tactic:
by
        fin_cases i <;> fin_cases j <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Star E
inst✝¹ : Module ℂ E
inst✝ : StarModule ℂ E
r : ℝ
a : E
⊢ star (r • a) = star r • star a

Tactic:
← smul_one_smul ℂ r a,

Goal state after:
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Star E
inst✝¹ : Module ℂ E
inst✝ : StarModule ℂ E
r : ℝ
a : E
⊢ star ((r • 1) • a) = star r • star a
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) + ↑(im z) * I + (↑(re z) - ↑(im z) * I) = 2 * ↑(re z)

Tactic:
rw [add_add_sub_cancel, two_mul]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
x : Y
h : x ∈ e.target
⊢ ContinuousWithinAt (f ∘ ↑e) univ (↑e.symm x) ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x)

Tactic:
continuousWithinAt_univ

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
x : Y
h : x ∈ e.target
⊢ ContinuousAt (f ∘ ↑e) (↑e.symm x) ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x)
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k : ℕ
⊢ abv (∑ i ∈ range (k + max n i), f i - ∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (k + max n i), a k - ∑ k ∈ range (max n i), a k

Tactic:
induction k with

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : Function.uncurry A =o[⊤ ×ˢ l] Function.uncurry B
⊢ (fun H ↦ ∑ j ∈ i H, A j H) =o[l] fun H ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
isLittleO_iff_forall_isBigOWith

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (⊤ ×ˢ l) (Function.uncurry A) (Function.uncurry B)
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun H ↦ ∑ j ∈ i H, A j H) fun H ↦ ∑ j ∈ i H, ‖B j H‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
g'' : α → F''
h : ∀ (x : α), g'' x = 0 → f'' x = 0
⊢ f'' =O[cofinite] g'' ↔ ∃ C, ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖

Tactic:
classical
  exact ⟨fun h' =>
    let ⟨C, _C₀, hC⟩ := bound_of_isBigO_cofinite h'
    ⟨C, fun x => if hx : g'' x = 0 then by simp [h _ hx, hx] else hC hx⟩,
    fun h => (isBigO_top.2 h).mono le_top⟩

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖-x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 +
      ‖x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 ≤
    ‖x‖ ^ 4 * (5 / 96)

Tactic:
by norm_num

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x ↦ f x * g x) h) ↔ g =o[l] fun x ↦ h x / f x

Tactic:
isLittleO_iff_forall_isBigOWith

Goal state after:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x ↦ f x * g x) h) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g fun x ↦ h x / f x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ 1 * (5 / 96) + 1 / 2 < 1

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ |1| ^ 4 * (5 / 96) + (1 - 1 ^ 2 / 2) ≤ 5 / 9

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ 2 * (5 / 9) ^ 2 - 1 < 0

Tactic:
by norm_num

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

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

Tactic:
hn₀'

Goal state after:
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₀ : ℕ
hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y
hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y
⊢ (∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n) →
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 2 = 4 / 2

Tactic:
by norm_num

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

Goal state before:
pp: x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ 0 ≤ sin (x / 2)

Tactic:
apply sin_nonneg_of_nonneg_of_le_pi <;> linarith

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

Goal state before:
pp: x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : sin x = 0
⊢ x = 0

Tactic:
contrapose! h

Goal state after:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
⊢ sin x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
by norm_num

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty

Tactic:
rw [Set.image_nonempty]

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ (↑f.ker).Nonempty
Module: Mathlib.Analysis.Normed.Group.Pointwise

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

Tactic:
rw [← smul_ball_one, mul_smul_comm, mul_ball_one]

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

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
⊢ ξ ≠ 1

Tactic:
contrapose! h

Goal state after:
K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ξ = 1
⊢ 1 ≤ ‖ξ‖
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
rw [← closure_thickening hδ, infEDist_closure, infEDist_thickening hδ]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))

Tactic:
induction k with

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ ‖∑ x ∈ Finset.range n, f x - a‖ ≤ C * r ^ n / (1 - r)

Tactic:
by
  rw [← dist_eq_norm]
  apply dist_le_of_le_geometric_of_tendsto r C hr (dist_partial_sum_le_of_le_geometric hf)
  exact ha.tendsto_sum_nat

Goal state after:
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
M : Type u_4
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m₁ m₂ : M
hm₁ : m₁ ∈ pathComponent 1
hm₂ : m₂ ∈ pathComponent 1
⊢ m₁ * m₂ ∈ pathComponent 1

Tactic:
by simpa using! hm₁.mul hm₂

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
γ' : Path y z
⊢ ((fun t ↦ if t ≤ 1 / 2 then γ.extend (2 * t) else γ'.extend (2 * t - 1)) ∘ Subtype.val) 1 = z

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑x.val / ↑N < 0 + 1

Tactic:
simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑y.val / ↑N < 0 + 1

Tactic:
simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _

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

Goal state before:
pp: case inr
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ |p| / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : p < 0
⊢ ‖↑x‖ = |x|

Tactic:
abs_eq_neg_self.mpr hp.le

Goal state after:
case inr
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ -p / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : p < 0
⊢ ‖↑x‖ = |x|
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 : ℕ
⊢ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i ≤ l

Tactic:
by
  have hm : Monotone (fun n ↦ ∑ i ∈ range (2 * n + 1), (-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 _ (2 * n + 1 + 1), sum_range_succ _ (2 * n + 1)]
    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]
    gcongr
    exact hfm (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' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ p * ↑n

Tactic:
mul_le_mul_iff_right₀ hp.out,

Goal state after:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ 1 ≤ ↑n
Module: Mathlib.Analysis.Normed.Group.AddCircle

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

Tactic:
by simp [AddCircle.norm_eq]

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

Goal state before:
pp: x y : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
hy : y ∈ Icc (-1) 1
⊢ x ≤ arcsin y ↔ sin x ≤ y

Tactic:
rw [← neg_le_neg_iff, ← arcsin_neg,
    arcsin_le_iff_le_sin ⟨neg_le_neg hy.2, neg_le.2 hy.1⟩ ⟨neg_le_neg hx.2, neg_le.2 hx.1⟩, sin_neg,
    neg_le_neg_iff]

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

Goal state before:
pp: θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (↑1 * (cos ↑θ + sin ↑θ * I)).arg = θ

Tactic:
arg_mul_cos_add_sin_mul_I zero_lt_one hθ

Goal state after:
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ θ = θ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

pp: case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

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

Goal state after:
case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ 2 * π - 0 = 2 * π * ↑1

Tactic:
rw [sub_zero, Int.cast_one, mul_one]

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

Goal state before:
pp: case mp
x : ℂ
h : cexp x = 1
⊢ ∃ n, x = ↑n * (2 * ↑π * I)

Tactic:
rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos x.im (-π) with ⟨n, hn, -⟩

Goal state after:
case mp
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ ∃ n, x = ↑n * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
⊢ (if 1 = 0 then if x = 0 then 1 else 0 else cexp (log 1 * x)) = 1

Tactic:
split_ifs <;> simp_all [one_ne_zero]

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

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

Tactic:
rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hsin with h | h

Goal state after:
case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = ↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π

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

Goal state before:
pp: case inr
θ : Angle
h : θ ≠ ↑π
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1

Tactic:
· simp only [Set.mem_Ioo, ← sign_toReal h, sign_eq_one_iff, and_iff_left_iff_imp]
    exact fun _ ↦ (toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)

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

Goal state before:
pp: θ : Angle
⊢ (2 • θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|

Tactic:
by
  simpa [← cos_pos_iff_abs_toReal_lt_pi_div_two, ← cos_neg_iff_pi_div_two_lt_abs_toReal]
    using sign_two_nsmul_eq_sign_iff (θ := θ + π)

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

Goal state before:
pp: a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = ↑π
⊢ a = b + ↑π

Tactic:
simp [← h]

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

Goal state before:
pp: case inr
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
pos : 0 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
exact rpow_add pos _ _

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

Goal state before:
pp: case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : -y = 0
h✝ : y = 0
⊢ 1 = 1⁻¹

Tactic:
simp_all [exp_neg]

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

Goal state before:
pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : -y = 0
h✝ : ¬y = 0
⊢ 1 = 0⁻¹

Tactic:
simp_all [exp_neg]

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

Goal state before:
pp: case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : ¬-y = 0
h✝ : y = 0
⊢ 0 = 1⁻¹

Tactic:
simp_all [exp_neg]

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

Goal state before:
pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : ¬-y = 0
h✝ : ¬y = 0
⊢ 0 = 0⁻¹

Tactic:
simp_all [exp_neg]

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

Goal state before:
pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ rexp (log x * -y) = (rexp (log x * y))⁻¹

Tactic:
simp_all [exp_neg]

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

Goal state before:
pp: case e'_2
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
hsa' : (-θ + -ψ).sign ≠ 1
⊢ |(θ + ψ).toReal| = |(-θ + -ψ).toReal|

pp: case e'_3
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
hsa' : (-θ + -ψ).sign ≠ 1
⊢ 2 * π - (|θ.toReal| + |ψ.toReal|) = 2 * π - (|(-θ).toReal| + |(-ψ).toReal|)

Tactic:
all_goals simp [-neg_add_rev, ← neg_add, abs_toReal_neg]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℂ
⊢ ‖↑x‖ ^ y.re / rexp 0 = x ^ y.re

Tactic:
Real.exp_zero,

Goal state after:
x : ℝ
hx : 0 < x
y : ℂ
⊢ ‖↑x‖ ^ y.re / 1 = x ^ y.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
by
  rw [← rpow_mul hx, inv_mul_cancel₀ hy, rpow_one]

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

Goal state before:
pp: x : ℝ≥0
n : ℤ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
by
  rw [rpow_mul, rpow_intCast]

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

Goal state before:
pp: x : ℝ≥0
y : ℝ
n : ℤ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
by
  rw [rpow_mul, rpow_intCast]

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

Goal state before:
pp: ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map f l).prod ^ r

Tactic:
rw [← list_prod_map_rpow, List.map_map]

Goal state after:
ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map ((fun x ↦ x ^ r) ∘ f) l).prod
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

Tactic:
have :
    (fun p : ℝ≥0 × ℝ => p.1 ^ p.2) =
      Real.toNNReal ∘ (fun p : ℝ × ℝ => p.1 ^ p.2) ∘ fun p : ℝ≥0 × ℝ => (p.1.1, p.2) := by
    ext p
    simp only [coe_rpow, val_eq_coe, Function.comp_apply, coe_toNNReal', left_eq_sup]
    positivity
  rw [this]
  refine continuous_real_toNNReal.continuousAt.comp (ContinuousAt.comp ?_ ?_)
  · apply Real.continuousAt_rpow
    simpa using h
  · fun_prop

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ InjOn (fun y ↦ y ^ x) {y | 0 ≤ y}

Tactic:
rintro y hy z hz (hyz : y ^ x = z ^ x)

Goal state after:
x : ℝ
hx : x ≠ 0
y : ℝ
hy : y ∈ {y | 0 ≤ y}
z : ℝ
hz : z ∈ {y | 0 ≤ y}
hyz : y ^ x = z ^ x
⊢ y = z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

Tactic:
by
  convert! ENNReal.Tendsto.const_mul (ENNReal.continuous_rpow_const.tendsto 0) _
  · simp [hy]
  · exact Or.inr hc

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

Goal state before:
pp: case inl
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_pos : 0 < p
⊢ 0 < x ^ p

Tactic:
exact rpow_pos_of_nonneg hx_pos (le_of_lt hp_pos)

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

Goal state before:
pp: x : ℝ≥0∞
n : ℤ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
by
  rw [rpow_mul, rpow_intCast]

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

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
n : ℤ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
by
  rw [rpow_mul, rpow_intCast]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ midpoint R x y = x ↔ x = y

Tactic:
midpoint_eq_iff,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (pointReflection R x) x = y ↔ x = y
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x x' y y' : P
⊢ midpoint R (x -ᵥ x') (y -ᵥ y') = 0 ↔ x -ᵥ x' = y' -ᵥ y

Tactic:
midpoint_eq_iff,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x x' y y' : P
⊢ (pointReflection R 0) (x -ᵥ x') = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R x y = ⅟2 • (x + y)

Tactic:
midpoint_eq_iff,

Goal state after:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ (pointReflection R (⅟2 • (x + y))) x = y
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
inst✝ : IsTorsionFree R M
v : M
r : R
⊢ SameRay R v (-(r • v)) ↔ r ≤ 0 ∨ v = 0

Tactic:
← neg_smul,

Goal state after:
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
v : M
r : R
⊢ SameRay R v (-r • v) ↔ r ≤ 0 ∨ v = 0
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
ha' : 0 < a
⊢ a • x + b • y ∈ openSegment 𝕜 x y

Tactic:
· exact ⟨a, b, ha', hb', hab, rfl⟩

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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y ∈ s

Tactic:
rw [zero_add] at hab
    rwa [hab, one_smul, zero_smul, zero_add]

Goal state after: