mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
⊢ False

Tactic:
obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_le hδ hε hxy

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y ≤ ε
⊢ False
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
⊢ γ 0 ∈ F ∧ γ 1 ∈ F

Tactic:
constructor

Goal state after:
case left
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
⊢ γ 0 ∈ F

case right
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
⊢ γ 1 ∈ F
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x ↔ z ∈ pathComponent y

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x → z ∈ pathComponent y

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent y → z ∈ pathComponent x
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn F y
⊢ pathComponentIn F x = pathComponentIn F y

Tactic:
ext

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn F y
x✝ : X
⊢ x✝ ∈ pathComponentIn F x ↔ x✝ ∈ pathComponentIn F y
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn F x = F

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F → ∃ x ∈ F, pathComponentIn F x = F

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ (∃ x ∈ F, pathComponentIn F x = F) → IsPathConnected F
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case snoc.elim0
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
x : X
hp : ∀ (i : Fin 0), i.elim0 ∈ s
hx : x ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin 0), i.elim0 ∈ range ⇑γ

Tactic:
simp only [snoc_zero]
    use Path.refl x
    simp [hx]

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
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∃ f, Tendsto F l (𝓝 f)) ↔ ∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)

Tactic:
constructor

Goal state after:
case mp
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∃ f, Tendsto F l (𝓝 f)) → ∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)

case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)) → ∃ f, Tendsto F l (𝓝 f)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
⊢ PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := ⋯
⊢ PathConnectedSpace X → Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := ⋯
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X) → PathConnectedSpace X
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst✝¹] (Function.uncurry f)
⊢ Continuous[inst✝, _] fun x ↦ mkD (f x) g

Tactic:
have (x : _) : Continuous (f x) := f_cont.comp (Continuous.prodMk_right x)

Goal state after:
X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst✝¹] (Function.uncurry f)
this : ∀ (x : T), Continuous[inst✝², inst✝¹] (f x)
⊢ Continuous[inst✝, _] fun x ↦ mkD (f x) g
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a : X
⊢ (refl a).trans (refl a) = refl a

Tactic:
ext

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a : X
x✝ : ↑I
⊢ ((refl a).trans (refl a)) x✝ = (refl a) x✝
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)
⊢ x✝.curry.uncurry = x✝

Tactic:
ext

Goal state after:
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✝
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))
⊢ x✝.uncurry.curry = x✝

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Topology.Instances.ZMultiples

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
k : ℤ
hx : k • a ∈ AddSubgroup.zmultiples a
⊢ |↑k| < 1 ↔ |k| < 1

Tactic:
by norm_cast

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

Goal state before:
pp: a : ℝ
ha : a ≠ 0
⊢ IsDiscrete ↑((zmultiplesHom ℝ) a).range

Tactic:
rw [AddSubgroup.range_zmultiplesHom, SetLike.isDiscrete_iff_discreteTopology]

Goal state after:
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)
Module: Mathlib.Topology.Path

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

Tactic:
ext

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
x✝ : ↑I
⊢ (γ.map ⋯) x✝ = γ x✝
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
⊢ (γ.map hf).map hg = γ.map ⋯

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case refine_1
x r : ℝ
hr : ∀ (m : ℝ), ↑m = ↑x → r ≤ ‖m‖
⊢ r ≤ fract x ∧ r ≤ 1 - fract x

Tactic:
constructor

Goal state after:
case refine_1.left
x r : ℝ
hr : ∀ (m : ℝ), ↑m = ↑x → r ≤ ‖m‖
⊢ r ≤ fract x

case refine_1.right
x r : ℝ
hr : ∀ (m : ℝ), ↑m = ↑x → r ≤ ‖m‖
⊢ r ≤ 1 - fract x
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case refine_2
x : ℝ
⊢ ∀ (m : ℝ), ↑m = ↑x → |x - ↑(round x)| ≤ |m|

Tactic:
simpa [zmultiples, QuotientAddGroup.eq, zsmul_eq_mul, mul_one, mem_mk, mem_range, and_imp,
      forall_exists_index, eq_neg_add_iff_add_eq, ← eq_sub_iff_add_eq, forall_comm (α := ℕ)]
      using round_le _

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

Goal state before:
pp: case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)

Tactic:
constructor

Goal state after:
case inr.left
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ -(1 / 2) ≤ p⁻¹ * x

case inr.right
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p⁻¹ * x < 1 / 2
Module: Mathlib.Topology.Path

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

Tactic:
ext

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
x✝ : ↑I
⊢ (γ.reparam id ⋯ ⋯ ⋯) x✝ = γ x✝
Module: Mathlib.Topology.Path

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

Tactic:
ext

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x✝ : ↑I
⊢ ((refl x).reparam f hfcont hf₀ hf₁) x✝ = (refl x) x✝
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case inl
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))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)
⊢ ∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ f (2 * n) ∧
    ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i - ∑' (i : ℕ), (-1) ^ i * f i ≤ f (2 * n)

Tactic:
constructor

Goal state after:
case inl.left
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))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)
⊢ ∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ f (2 * n)

case inl.right
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))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i - ∑' (i : ℕ), (-1) ^ i * f i ≤ f (2 * n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: ⊢ Subtype.val '' range (IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) = Icc (-(π / 2)) (π / 2)

Tactic:
ext

Goal state after:
x✝ : ℝ
⊢ x✝ ∈ Subtype.val '' range (IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) ↔ x✝ ∈ Icc (-(π / 2)) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
this : 0 < π
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)

Tactic:
constructor

Goal state after:
case left
x : ℝ
this : 0 < π
⊢ -(π / 2) < π / 4

case right
x : ℝ
this : 0 < π
⊢ π / 4 ≤ π / 2
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))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
upper : ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤ ∑' (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) ∧
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i - ∑' (i : ℕ), (-1) ^ i * f i ≤ f (2 * n + 1)

Tactic:
constructor

Goal state after:
case inr.left
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))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
upper : ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤ ∑' (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)

case inr.right
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))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
upper : ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Odd (2 * n + 1)
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i - ∑' (i : ℕ), (-1) ^ i * f i ≤ f (2 * n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x

Tactic:
constructor

Goal state after:
case mp
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 → π / 4 ≤ arcsin x

case mpr
x : ℝ
⊢ π / 4 ≤ arcsin x → π / 2 - arcsin x ≤ π / 4
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
hx : ¬x = 0
⊢ |x⁻¹| = |x|⁻¹

Tactic:
abs_inv

Goal state after:
case neg
x : ℝ
hx : ¬x = 0
⊢ |x|⁻¹ = |x|⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
constructor

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

case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
h : log x ≤ y
⊢ x ≤ rexp y

Tactic:
rcases le_or_gt x 0 with hx | hx
  · exact hx.trans <| exp_nonneg y
  · exact (log_le_iff_le_exp hx).mp h

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

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

Tactic:
simp [h₀, Real.pi_div_two_pos.ne]

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

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

Tactic:
constructor

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

case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → z.arg = π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
constructor

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

case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ z.im < 0 → z.arg = -(π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: n : ℕ
⊢ 0 ≤ log ↑n

Tactic:
if hn : n = 0 then
    simp [hn]
  else
    have : (1 : ℝ) ≤ n := mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
    exact log_nonneg this

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

Goal state before:
pp: x : ℝ
⊢ log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
constructor

Goal state after:
case mp
x : ℝ
⊢ log x = 0 → x = 0 ∨ x = 1 ∨ x = -1

case mpr
x : ℝ
⊢ x = 0 ∨ x = 1 ∨ x = -1 → log x = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case cons
a : ℝ
l : List ℝ
ih : log l.prod = (List.map (fun x ↦ log x) l).sum
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
this : l.prod ≠ 0
⊢ log a + log l.prod = log a + (List.map (fun x ↦ log x) l).sum

Tactic:
add_right_inj,

Goal state after:
case cons
a : ℝ
l : List ℝ
ih : log l.prod = (List.map (fun x ↦ log x) l).sum
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
this : l.prod ≠ 0
⊢ log l.prod = (List.map (fun x ↦ log x) l).sum
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

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

Tactic:
constructor

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

case mpr
x : ℂ
⊢ (∃ n, x = ↑n * (2 * ↑π * I)) → cexp x = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : ℝ
⊢ cos θ = cos ψ ↔ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

Tactic:
constructor

Goal state after:
case mp
θ ψ : ℝ
⊢ cos θ = cos ψ → ↑θ = ↑ψ ∨ ↑θ = -↑ψ

case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ → cos θ = cos ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: ⊢ 𝓝 0 ⊓ 𝓟 {0}ᶜ = 𝓝[≠] 0

Tactic:
nhdsWithin

Goal state after:
⊢ 𝓝 0 ⊓ 𝓟 {0}ᶜ = 𝓝 0 ⊓ 𝓟 {0}ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x a : ℂ
⊢ 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
constructor

Goal state after:
case mp
x a : ℂ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

case mpr
x a : ℂ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : ℝ
⊢ sin θ = sin ψ ↔ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π

Tactic:
constructor

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

case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π → sin θ = sin ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ ((starRingEnd ℂ) x).arg = if x.arg = π then π else -x.arg

Tactic:
simp_rw [arg_eq_pi_iff, arg, neg_im, conj_im, conj_re, norm_conj, neg_div, neg_neg,
    Real.arcsin_neg]
  rcases lt_trichotomy x.re 0 with (hr | hr | hr) <;>
    rcases lt_trichotomy x.im 0 with (hi | hi | hi)
  · simp [hr, hr.not_ge, hi.le, hi.ne, not_le.2 hi, add_comm]
  · simp [hr, hr.not_ge, hi]
  · simp [hr, hr.not_ge, hi.ne.symm, hi.le, not_le.2 hi, sub_eq_neg_add]
  · simp [hr]
  · simp [hr]
  · simp [hr]
  · simp [hr.le, hi.ne]
  · simp [hr.le, hr.le.not_gt]
  · simp [hr.le, hr.le.not_gt]

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

Goal state before:
pp: x : ℂ
⊢ (∃ θ, cexp (↑θ * I) = x) ↔ ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

Tactic:
constructor

Goal state after:
case mp
x : ℂ
⊢ (∃ θ, cexp (↑θ * I) = x) → ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

case mpr
x : ℂ
⊢ (∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x) → ∃ θ, cexp (↑θ * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: ⊢ (fun θ ↦ cexp (↑θ * I)) '' Ioc (-π) π = sphere 0 1

Tactic:
ext

Goal state after:
x✝ : ℂ
⊢ x✝ ∈ (fun θ ↦ cexp (↑θ * I)) '' Ioc (-π) π ↔ x✝ ∈ sphere 0 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π ↔ θ ≠ ↑π

Tactic:
constructor

Goal state after:
case mp
θ : Angle
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π → θ ≠ ↑π

case mpr
θ : Angle
⊢ θ ≠ ↑π → -π < -θ.toReal ∧ -θ.toReal ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ -π < π / 2 ∧ π / 2 ≤ π

Tactic:
constructor

Goal state after:
case left
⊢ -π < π / 2

case right
⊢ π / 2 ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ -π < -π / 2 ∧ -π / 2 ≤ π

Tactic:
constructor

Goal state after:
case left
⊢ -π < -π / 2

case right
⊢ -π / 2 ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ -π < ↑n * θ.toReal ∧ ↑n * θ.toReal ≤ π ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)

Tactic:
Set.mem_Ioc,

Goal state after:
n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ -π < ↑n * θ.toReal ∧ ↑n * θ.toReal ≤ π ↔ -π / ↑n < θ.toReal ∧ θ.toReal ≤ π / ↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
⊢ (cexp (↑θ * I)).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
arg_exp_mul_I

Goal state after:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ toIocMod Real.two_pi_pos (-π) θ = toIocMod Real.two_pi_pos (-π) θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b ∨ a = b + ↑π ↔ a = b

Tactic:
constructor

Goal state after:
case mp
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b ∨ a = b + ↑π → a = b

case mpr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b → a = b ∨ a = b + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : θ + ψ = 0
⊢ |θ.toReal| + |ψ.toReal| = π

pp: case inr
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : θ + ψ = ↑π
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
· simp_all [add_eq_zero_iff_eq_neg.mp h]

Goal state after:
case inr
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : θ + ψ = ↑π
⊢ |θ.toReal| + |ψ.toReal| = π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
ext

Goal state after:
α : Type u_1
f : α → ℝ
x✝ : α
⊢ (f ^ 0) x✝ = 1 x✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x a : ℝ
⊢ 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
constructor

Goal state after:
case mp
x a : ℝ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

case mpr
x a : ℝ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
ext

Goal state after:
α : Type u_1
f : α → ℝ
x✝ : α
⊢ (f ^ 1) x✝ = f x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : - -θ.sign = (θ + ψ).sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
← sign_neg

Goal state after:
case inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : -(-θ).sign = (θ + ψ).sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
⊢ (θ + ψ).toReal ≤ 0 ∨ θ + ψ = ↑π

Tactic:
have := (θ + ψ).sign.trichotomy
    grind [sign_eq_zero_iff, toReal_eq_zero_iff, toReal_neg_iff_sign_neg]

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

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

Tactic:
ext

Goal state after:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)