mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
⊢ ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
have H := this 0 (ε / (2 * Real.exp a)) ha

Goal state after:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
H : ∀ᶠ (x : ℂ) in 𝓝 0, dist (cexp x) (cexp 0) < ε / (2 * Real.exp a)
⊢ ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε
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
⊢ [∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x, ∃ 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 ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x,
      ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE

Tactic:
tfae_have 1 → 3 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩

Goal state after:
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
⊢ [∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x, ∃ 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 ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x,
      ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
⊢ Subtype.val '' ⇑expOrderIso '' Set.Iic a = Set.Ioc 0 ((Subtype.val ∘ ⇑expOrderIso) a)

Tactic:
expOrderIso.image_Iic,

Goal state after:
a : ℝ
⊢ Subtype.val '' Set.Iic (expOrderIso a) = Set.Ioc 0 ((Subtype.val ∘ ⇑expOrderIso) a)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℤ
⊢ cos (↑n * (2 * π) - π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.int_mul n).sub_antiperiod_eq cos_antiperiodic

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
this : ∀ (ε : ℝ), mk '' ball 1 ε = {x | ‖x‖ < ε}
⊢ (𝓝 1).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {x | ‖x‖ < ε}

Tactic:
← mk_one,

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
this : ∀ (ε : ℝ), mk '' ball 1 ε = {x | ‖x‖ < ε}
⊢ (𝓝 ↑1).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {x | ‖x‖ < ε}
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
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ f (m + x) = f m

Tactic:
rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero]

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

Goal state before:
pp: n : ℕ
A : 1 < 2 ^ (n + 1)
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2

Tactic:
have B : π / 2 ^ (n + 1) < π := div_lt_self pi_pos A

Goal state after:
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ (1 - r) * dist y x ≤ (1 - 0) * dist y x

Tactic:
by gcongr; exact h.1

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

Goal state before:
pp: n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ √((1 + sqrtTwoAddSeries 0 n / 2) / 2) = √(2 + sqrtTwoAddSeries 0 n) / 2

pp: case hl
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ -π ≤ π / 2 ^ (n + 1)

pp: case hr
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ π / 2 ^ (n + 1) ≤ π

Tactic:
add_div_eq_mul_add_div,

Goal state after:
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ √((1 * 2 + sqrtTwoAddSeries 0 n) / 2 / 2) = √(2 + sqrtTwoAddSeries 0 n) / 2

case hc
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ 2 ≠ 0

case hl
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ -π ≤ π / 2 ^ (n + 1)

case hr
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ π / 2 ^ (n + 1) ≤ π
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (sphere x r) = sphere x r

Tactic:
rw [isClosed_sphere.frontier_eq, interior_sphere x hr, sdiff_empty]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x ↦ c • x
⊢ ⨅ y ∈ s, ‖c‖₊ • edist x y = ‖c‖₊ • ⨅ y ∈ s, edist x y

Tactic:
· have : (‖c‖₊ : ENNReal) ≠ 0 := by simp [hc]
    simp_rw [ENNReal.smul_def, smul_eq_mul, ENNReal.mul_iInf_of_ne this ENNReal.coe_ne_top]

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

Goal state before:
pp: n : ℤ
⊢ cos (↑n * (2 * ↑π) - ↑π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.int_mul n).sub_antiperiod_eq cos_antiperiodic

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Tactic:
by
  rcases eq_or_ne c 0 with (rfl | hc)
  · simp [hr, zero_smul_set, Set.singleton_zero, nonempty_closedBall]
  · exact smul_closedBall' hc x r

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
h : CauchySeq fun n ↦ ∑ k ∈ Finset.range n, f k
b : ℕ → ℝ
left✝ : ∀ (n : ℕ), 0 ≤ b n
key : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (∑ k ∈ Finset.range n, f k) (∑ k ∈ Finset.range m, f k) ≤ b N
right✝ : Tendsto b atTop (𝓝 0)
n : ℕ
⊢ ‖f n‖ ≤ b 0

Tactic:
simpa only [dist_partial_sum'] using key n (n + 1) 0 zero_le zero_le

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:
simpa using! hm₁.mul hm₂

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

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
⊢ ∀ (a b : ZerothHomotopy X), a = b

Tactic:
rintro ⟨x⟩ ⟨y⟩

Goal state after:
case mp.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
a✝ : ZerothHomotopy X
x : X
b✝ : ZerothHomotopy X
y : X
⊢ Quot.mk (⇑(pathSetoid X)) x = Quot.mk (⇑(pathSetoid X)) y
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ PathConnectedSpace ↑F

Tactic:
pathConnectedSpace_iff_univ,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ IsPathConnected univ
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
⊢ PathConnectedSpace Y

Tactic:
pathConnectedSpace_iff_univ,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
⊢ IsPathConnected univ
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 s : Set X
t : Set Y
inst✝¹ : PathConnectedSpace X
inst✝ : PathConnectedSpace Y
⊢ PathConnectedSpace (X × Y)

Tactic:
pathConnectedSpace_iff_univ,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y z : X
ι : Type u_3
F s : Set X
t : Set Y
inst✝¹ : PathConnectedSpace X
inst✝ : PathConnectedSpace Y
⊢ IsPathConnected univ
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)
⊢ PathConnectedSpace ((i : ι) → Z i)

Tactic:
pathConnectedSpace_iff_univ,

Goal state after:
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 univ
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
⊢ Summable fun n ↦ f n * z ^ n

Tactic:
have hw : 0 < ‖w‖ := (norm_nonneg z).trans_lt hz
  obtain ⟨C, hC⟩ := exists_norm_le_of_cauchySeq h
  rw [summable_iff_cauchySeq_finset]
  refine cauchySeq_finset_of_geometric_bound (r := ‖z‖ / ‖w‖) (C := C) ((div_lt_one hw).mpr hz)
    (fun n ↦ ?_)
  rw [norm_mul, norm_pow, div_pow, ← mul_comm_div]
  conv at hC => enter [n]; rw [norm_mul, norm_pow, ← _root_.le_div_iff₀ (by positivity)]
  gcongr
  exact hC n

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

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
m n : ℕ
⊢ p⁻¹ * (p * (↑m / ↑n)) = ↑m / ↑n

Tactic:
inv_mul_cancel_left₀ hp.out.ne.symm

Goal state after:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
⊢ ↑m / ↑n = ↑m / ↑n
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
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
n : ℕ
h : Odd (2 * n + 1)
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i| ≤ f (2 * n + 1)

Tactic:
specialize upper (n + 1)

Goal state after:
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
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (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
n : ℕ
upper : ∑ i ∈ Finset.range (2 * (n + 1)), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Odd (2 * n + 1)
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i| ≤ f (2 * n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ 2 • ↑π = 0

Tactic:
by simp [← intCast_mul_eq_zsmul]

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

Goal state before:
pp: ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ ψ = θ + 0 ∨ ψ = θ + 1 • ↑(2 * π / ↑2) ↔ ψ = θ ∨ ψ = θ + ↑π

Tactic:
add_zero,

Goal state after:
ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ ψ = θ ∨ ψ = θ + 1 • ↑(2 * π / ↑2) ↔ ψ = θ ∨ ψ = θ + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (fun x ↦ log (x + y) - log x) atTop (𝓝 0)

Tactic:
rw [← comap_exp_nhds_exp, exp_zero, tendsto_comap_iff, ← add_zero (1 : ℝ)]

Goal state after:
y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (rexp ∘ fun x ↦ log (x + y) - log x) atTop (𝓝 (1 + 0))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case mpr.inl
x : ℂ
h : x ≠ 0
⊢ 0 ^ x = 0

pp: case mpr.inr
⊢ 0 ^ 0 = 1

Tactic:
· exact zero_cpow h

Goal state after:
case mpr.inr
⊢ 0 ^ 0 = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

Tactic:
rw [cpow_def]

Goal state after:
x : ℂ
⊢ (if 1 = 0 then if x = 0 then 1 else 0 else cexp (log 1 * x)) = 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d n : ℕ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 0 < Real.log e

Tactic:
by
    rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have : 1 < (n : ℝ) / d := by
      simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h)
    exact Real.log_pos this

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

Goal state before:
pp: x y z : ℂ
hx : x ≠ 0
⊢ x ^ y * x ^ (-z) = x ^ y / x ^ z

Tactic:
cpow_neg,

Goal state after:
x y z : ℂ
hx : x ≠ 0
⊢ x ^ y * (x ^ z)⁻¹ = x ^ y / x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

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

Tactic:
· left
      rw [coe_sub, coe_sub] at h
      exact sub_right_inj.1 h

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

Goal state before:
pp: case mp
θ ψ : ℝ
⊢ sin θ = sin ψ → ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π

Tactic:
intro Hsin
    rw [← cos_pi_div_two_sub, ← cos_pi_div_two_sub] at Hsin
    rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hsin with h | h
    · left
      rw [coe_sub, coe_sub] at h
      exact sub_right_inj.1 h
    right
    rw [coe_sub, coe_sub, eq_neg_iff_add_eq_zero, add_sub, sub_add_eq_add_sub, ← coe_add,
      add_halves, sub_sub, sub_eq_zero] at h
    exact h.symm

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

Goal state before:
pp: case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n • (2 * π) = -1 * π + 0
⊢ ↑θ = ↑ψ

Tactic:
add_zero,

Goal state after:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n • (2 * π) = -1 * π
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

Tactic:
rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]
      simp [hr.not_gt, ← two_mul, Real.pi_ne_zero]

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

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

Tactic:
by
  rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_sign_iff]

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

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

Tactic:
rw [rpow_def_of_nonneg (le_of_lt hx), if_neg (ne_of_gt hx)]

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

Goal state before:
pp: case inr
x y : ℝ
hx : x < 0
⊢ |rexp (log x * y) * cos (y * π)| ≤ (-x) ^ y

Tactic:
rpow_def_of_pos (neg_pos.2 hx),

Goal state after:
case inr
x y : ℝ
hx : x < 0
⊢ |rexp (log x * y) * cos (y * π)| ≤ rexp (log (-x) * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y + ↑n ≠ 0
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
rpow_add' hx h,

Goal state after:
x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y + ↑n ≠ 0
⊢ x ^ y * x ^ ↑n = x ^ y * x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y + ↑n ≠ 0
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
rpow_add' hx h,

Goal state after:
x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y + ↑n ≠ 0
⊢ x ^ y * x ^ ↑n = x ^ y * x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : y + 1 ≠ 0
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
rpow_add' hx h,

Goal state after:
x y : ℝ
hx : 0 ≤ x
h : y + 1 ≠ 0
⊢ x ^ y * x ^ 1 = x ^ y * x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : 1 + y ≠ 0
⊢ x ^ (1 + y) = x * x ^ y

Tactic:
rpow_add' hx h,

Goal state after:
x y : ℝ
hx : 0 ≤ x
h : 1 + y ≠ 0
⊢ x ^ 1 * x ^ y = x * x ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: M : ℝ≥0
P : ℝ
hP : 0 ≤ P
⊢ ↑M ^ P = ↑(M ^ P)

Tactic:
by
  rw [ENNReal.coe_rpow_of_nonneg _ hP, ← ENNReal.rpow_eq_pow]

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

Goal state before:
pp: case inl
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : x ≤ y
⊢ max x y ^ p = max (x ^ p) (y ^ p)

Tactic:
rw [max_eq_right hxy, max_eq_right (by gcongr)]

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

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

pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ 0 ≤ x ^ z⁻¹

Tactic:
rpow_inv_rpow hx hz

Goal state after:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ x = y ^ z ↔ x = y ^ z

x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ 0 ≤ x ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
z : ℝ
h : 0 < z
x : ℝ≥0
hxy : ↑x < ∞
⊢ (fun x ↦ x ^ z) ↑x < (fun x ↦ x ^ z) ∞

pp: case inr
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : ↑x < y
hy : y ≠ ∞
⊢ (fun x ↦ x ^ z) ↑x < (fun x ↦ x ^ z) y

Tactic:
· simp only [top_rpow_of_pos h, ← coe_rpow_of_nonneg _ h.le, coe_lt_top]

Goal state after:
case inr
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : ↑x < y
hy : y ≠ ∞
⊢ (fun x ↦ x ^ z) ↑x < (fun x ↦ x ^ z) y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr
x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
hxy : y ≤ x
⊢ max x y ^ p = max (x ^ p) (y ^ p)

Tactic:
· rw [max_eq_left hxy, max_eq_left (rpow_le_rpow hxy hp)]

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

Goal state before:
pp: case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.arg

Tactic:
arg_nonneg_iff

Goal state after:
case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.im
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

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

Tactic:
· simp [top_rpow_of_neg hz, zero_lt_one]

Goal state after:
case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 < ↑x✝
⊢ ↑x✝ ^ z < 1
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
⊢ -(x -ᵥ x') + 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y

Tactic:
add_zero,

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
⊢ -(x -ᵥ x') = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
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 g : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ f (v +ᵥ p) -ᵥ g (v +ᵥ p) = (f.linear - g.linear) v +ᵥ f p -ᵥ g p

Tactic:
by
      simp [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, sub_add_eq_add_sub]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2
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
h : ∃ g, ∑ i, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
· rcases h with ⟨m, hm, hmne⟩
    rw [Fin.sum_univ_two, add_eq_zero_iff_eq_neg] at hm
    dsimp only [Matrix.cons_val] at hm
    rcases lt_trichotomy (m 0) 0 with (hm0 | hm0 | hm0) <;>
      rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
    · refine
        Or.inr (Or.inr (Or.inr ⟨-m 0, -m 1, Left.neg_pos_iff.2 hm0, Left.neg_pos_iff.2 hm1, ?_⟩))
      linear_combination (norm := module) -hm
    · exfalso
      simp [hm1, hx, hm0.ne] at hm
    · refine Or.inl (Or.inr (Or.inr ⟨-m 0, m 1, Left.neg_pos_iff.2 hm0, hm1, ?_⟩))
      linear_combination (norm := module) -hm
    · exfalso
      simp [hm0, hy, hm1.ne] at hm
    · rw [Fin.exists_fin_two] at hmne
      exact False.elim (not_and_or.2 hmne ⟨hm0, hm1⟩)
    · exfalso
      simp [hm0, hy, hm1.ne.symm] at hm
    · refine Or.inl (Or.inr (Or.inr ⟨m 0, -m 1, hm0, Left.neg_pos_iff.2 hm1, ?_⟩))
      rwa [neg_smul]
    · exfalso
      simp [hm1, hx, hm0.ne.symm] at hm
    · refine Or.inr (Or.inr (Or.inr ⟨m 0, m 1, hm0, hm1, ?_⟩))
      rwa [smul_neg]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x : E
hx : x ∈ ⋃ i, s i
y : E
hy : y ∈ ⋃ i, s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⋃ i, s i

Tactic:
rw [mem_iUnion] at hx hy ⊢

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x : E
hx : ∃ i, x ∈ s i
y : E
hy : ∃ i, y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ i, a • x + b • y ∈ s i
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inr.refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ (y - z) / (y - x) + (z - x) / (y - x) = 1

pp: case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z

Tactic:
· rw [← add_div, sub_add_sub_cancel, div_self h.ne']

Goal state after:
case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z