mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1.inr
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
K : Set X
V : Set Y
hKV : (K, V) ∈ S
hKne : K.Nonempty
⊢ MapsTo (⇑f) K V

Tactic:
refine hf.out.mono (subset_biUnion_of_mem (u := Prod.fst) hKV) (hi.trans ?_)

Goal state after:
case refine_1.inr
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
K : Set X
V : Set Y
hKV : (K, V) ∈ S
hKne : K.Nonempty
⊢ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ⊆ V
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p (last n))
h₁ : range ⇑γ ⊆ s
h₂ : ∀ (i : Fin (n + 1)), ∃ y, γ y = p i
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
range_subset_iff

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p (last n))
h₁ : ∀ (y : ↑I), γ y ∈ s
h₂ : ∀ (i : Fin (n + 1)), ∃ y, γ y = p i
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ PathConnectedSpace X ↔ ∃ x, pathComponent x = univ

Tactic:
by
  simp [pathConnectedSpace_iff_univ, isPathConnected_iff_eq]

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 (γ'.map h) ⟨2 * ↑t - 1, ⋯⟩

Tactic:
map_coe

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

Goal state before:
pp: n : ℕ
⊢ ‖if Even n then 0 else 1‖ ≤ 1

Tactic:
split_ifs <;> norm_num

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

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))

Tactic:
let n := addOrderOf u
  change ∃ k : ℕ, ‖u‖ = p * (k / n)
  obtain ⟨m, -, -, hm⟩ := exists_gcd_eq_one_of_isOfFinAddOrder hu
  refine ⟨min (m % n) (n - m % n), ?_⟩
  rw [← hm, norm_div_natCast]

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

Goal state before:
pp: case neg
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ Real.cos (Real.arcsin ((-x).im / ‖x‖) - π) = x.re / ‖x‖

Tactic:
rw [Real.cos_sub_pi, Real.cos_arcsin]

Goal state after:
case neg
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ -√(1 - ((-x).im / ‖x‖) ^ 2) = x.re / ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≤] x)
⊢ Tendsto (fun x ↦ arcsin (f x)) l (𝓝[≤] arcsin x)

Tactic:
refine ((continuous_arcsin.tendsto _).inf <| MapsTo.tendsto fun y hy ↦ ?_).comp h
  exact monotone_arcsin hy

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

Goal state before:
pp: x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
| (↑r * x).arg

Tactic:
← norm_mul_cos_add_sin_mul_I x,

Goal state after:
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
| (↑r * (↑‖x‖ * (cos ↑x.arg + sin ↑x.arg * I))).arg
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
← not_lt,

Goal state after:
x : ℝ
hx : 0 < x
⊢ ¬log x < 0 ↔ 1 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1

Tactic:
← not_lt,

Goal state after:
case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ ¬0 < log x ↔ x ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inl
n : ℤ
hn : 0 < n
⊢ 0 ≤ log ↑n

Tactic:
have : (1 : ℝ) ≤ n := mod_cast hn
      exact log_nonneg this

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

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

Tactic:
cpow_add _ _ hx,

Goal state after:
x y z : ℂ
hx : x ≠ 0
⊢ x ^ y * x ^ (-z) = x ^ y / x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
z : ℂ
hz : z ≠ 0
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ z.im < 0 ↔ 0 < z.re

Tactic:
← not_lt,

Goal state after:
case inr
z : ℂ
hz : z ≠ 0
⊢ 0 < z.re ∨ ¬z.im < 0 ∧ z.im < 0 ↔ 0 < z.re
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ (x * y).arg = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π

Tactic:
rw [← arg_coe_angle_toReal_eq_arg, arg_mul_coe_angle hx₀ hy₀, ← Real.Angle.coe_add,
      Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]

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

Goal state before:
pp: ⊢ SignType.sign (Real.sin (-(π / 2))) = -1

Tactic:
Real.sin_neg,

Goal state after:
⊢ SignType.sign (-Real.sin (π / 2)) = -1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
rcases angle_eq_iff_two_pi_dvd_sub.mp h with ⟨k, hk⟩

Goal state after:
case inr
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
k : ℤ
hk : θ.toReal + ψ.toReal - π = 2 * π * ↑k
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
obtain (h | h | h) := ψ.sign.trichotomy
  all_goals grind [neg_neg, add_comm, toReal_add_of_sign_pos_sign_neg]

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

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℂ
⊢ ‖↑↑n ^ s‖ = ↑n ^ s.re

Tactic:
norm_cpow_eq_rpow_re_of_pos (Nat.cast_pos.mpr hn) _

Goal state after:
n : ℕ
hn : 0 < n
s : ℂ
⊢ ↑n ^ s.re = ↑n ^ s.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
log_rpow hx

Goal state after:
x y : ℝ
hx : 0 < x
hz : 0 < x ^ y
⊢ y * log x = y * log x
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

Goal state after:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p ↦ p.1 ^ p.2) = toNNReal ∘ (fun p ↦ p.1 ^ p.2) ∘ fun p ↦ (↑p.1, p.2)
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ log (x ^ z) ≤ log y ↔ z * log x ≤ log y

Tactic:
log_rpow hx

Goal state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ z * log x ≤ log y ↔ z * log x ≤ log y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ log (x ^ z) < log y ↔ z * log x < log y

Tactic:
log_rpow hx

Goal state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ z * log x < log y ↔ z * log x < log y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: n : ℕ
hn : 0 < n
w z : ℂ
h : w.re ≤ z.re
⊢ ‖↑n ^ w‖ ≤ ‖↑n ^ z‖

Tactic:
by
  simp_rw [norm_natCast_cpow_of_pos hn]
  exact Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast hn) h

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

Goal state before:
pp: case inr.inr.top
z : ℝ
H : 0 < z
⊢ (∞ ^ z).toNNReal = ∞.toNNReal ^ z

Tactic:
simp [H, ne_of_gt]

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

Goal state before:
pp: b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ (↑r ^ d) ^ (↑d)⁻¹ = ↑r

Tactic:
NNReal.pow_rpow_inv_natCast

Goal state after:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑r = ↑r

case hn
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ d ≠ 0
Module: Mathlib.Algebra.Order.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : Semiring β
inst✝³ : PartialOrder β
inst✝² : Algebra α β
inst✝¹ : ZeroLEOneClass β
inst✝ : SMulPosMono α β
a : α
ha : 0 ≤ a
⊢ 0 ≤ (algebraMap α β) a

Tactic:
simpa using algebraMap_mono β ha

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ ≠ 0
hc₂ : c₂ = 0
⊢ SameRay R (c₁ • v) (c₂ • v)

Tactic:
rw [hc₂, zero_smul]; exact SameRay.zero_right _

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
⊢ SameRay R (c₁ • v) (c₂ • v)

Tactic:
rcases eq_or_ne c₁ 0 with hc₁ | hc₁
  · rw [hc₁, zero_smul]; exact SameRay.zero_left _
  rcases eq_or_ne c₂ 0 with hc₂ | hc₂
  · rw [hc₂, zero_smul]; exact SameRay.zero_right _
  have hpos : 0 < c₁ * c₂ := h.lt_of_ne (mul_ne_zero hc₁ hc₂).symm
  rcases mul_pos_iff.mp hpos with ⟨h₁, h₂⟩ | ⟨h₁, h₂⟩
  · exact Or.inr (Or.inr ⟨c₂, c₁, h₂, h₁, by module⟩)
  · exact Or.inr (Or.inr ⟨-c₂, -c₁, neg_pos.2 h₂, neg_pos.2 h₁, by module⟩)

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

Goal state before:
pp: 𝕜 : 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
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
refine ⟨fun h y hy a b ha hb hab => h hy ha.le hb.le hab, ?_⟩

Goal state after:
𝕜 : 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
⊢ (∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) → StarConvex 𝕜 x s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
hz : z ∈ range ⇑(lineMap x y)
⊢ openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)

Tactic:
rcases hz with ⟨c, rfl⟩
  simp only [openSegment_eq_image_lineMap, ← mapsTo_iff_image_subset]
  rintro a ⟨h₀, h₁⟩
  rcases lt_trichotomy a c with (hac | rfl | hca)
  · right
    left
    have hc : 0 < c := h₀.trans hac
    refine ⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, ?_⟩
    simp only [← homothety_eq_lineMap, ← homothety_mul_apply, div_mul_cancel₀ _ hc.ne']
  · left
    rfl
  · right
    right
    have hc : 0 < 1 - c := sub_pos.2 (hca.trans h₁)
    simp only [← lineMap_apply_one_sub y]
    refine
      ⟨(a - c) / (1 - c), ⟨div_pos (sub_pos.2 hca) hc, (div_lt_one hc).2 <| sub_lt_sub_right h₁ _⟩,
        ?_⟩
    simp only [← homothety_eq_lineMap, ← homothety_mul_apply, sub_mul, one_mul,
      div_mul_cancel₀ _ hc.ne', sub_sub_sub_cancel_right]

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • 0 + b • x ∈ s
a : 𝕜
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ a • x ∈ s

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • 0 + b • x ∈ s

Tactic:
· simpa only [sub_add_cancel, eq_self_iff_true, forall_true_left, zero_add, smul_zero] using
      h (sub_nonneg_of_le ha₁) ha₀

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • 0 + b • x ∈ s
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
s : Set E
P : Prop
hs : Convex 𝕜 s
⊢ Convex 𝕜 {x | P → x ∈ s}

Tactic:
by
  by_cases hP : P <;> simp [hP, hs, convex_univ]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
hs : 0 ∈ s
⊢ ↑s -ᵥ ↑s = ↑s

Tactic:
ext x
  constructor
  · rintro ⟨a, ha, b, hb, rfl⟩
    simpa using s.smul_vsub_vadd_mem 1 ha hb hs
  · exact fun h => ⟨x, h, 0, hs, by simp⟩

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ s.direction ↔ v ∈ (fun x ↦ p -ᵥ x) '' ↑s

Tactic:
← Submodule.neg_mem_iff,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ -v ∈ s.direction ↔ v ∈ (fun x ↦ p -ᵥ x) '' ↑s
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≤ y
⊢ [x -[𝕜] y] ⊆ s

Tactic:
exact (segment_subset_Icc hxy).trans (hs.out hx hy)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set F
hs : Balanced 𝕜 s
f : E →ₑ[id] F
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
x✝ : x ∈ a • ⇑f ⁻¹' s
y : E
hy₁ : y ∈ ⇑f ⁻¹' s
hy₂ : (fun x ↦ a • x) y = x
⊢ x ∈ ⇑f ⁻¹' s

Tactic:
rw [mem_preimage, ← hy₂, map_smul]
  exact hs a ha (smul_mem_smul_set hy₁)

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

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ (a⁻¹ • b) • a • x ∈ s

Tactic:
by
        refine hs.smul_mem ?_ ha
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ hba (norm_nonneg _)

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝¹] s
hzero : 0 ∈ s
hr : ‖0‖ ≤ 1
⊢ ∃ i', ∃ (_ : ‖i'‖ ≤ 1 ∧ i' ≠ 0), 0 • s ⊆ i' • s

Tactic:
exact ⟨1, by simp, by simpa [Set.zero_smul_set ⟨0, hzero⟩]⟩

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
x✝ : Finite ↑I
⊢ IsVonNBounded 𝕜 (⋃ x, s ↑x) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)

Tactic:
isVonNBounded_iUnion,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
x✝ : Finite ↑I
⊢ (∀ (i : ↑I), IsVonNBounded 𝕜 (s ↑i)) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕜'
inst✝⁶ : NormedAlgebra 𝕜 𝕜'
inst✝⁵ : Nontrivial 𝕜'
inst✝⁴ : Zero E
inst✝³ : TopologicalSpace E
inst✝² : SMul 𝕜 E
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
⊢ IsVonNBounded 𝕜 s

Tactic:
intro V hV
  refine (h hV).restrict_scalars <| AntilipschitzWith.tendsto_cobounded (K := ‖(1 : 𝕜')‖₊⁻¹) ?_
  refine AntilipschitzWith.of_le_mul_nndist fun x y ↦ ?_
  rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← sub_smul, nnnorm_smul, ← div_eq_inv_mul,
    mul_div_cancel_right₀ _ (nnnorm_ne_zero_iff.2 one_ne_zero)]

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : IsDomain 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module.IsTorsionFree 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
hc : c ≠ 0
⊢ StrictConvex 𝕜 ((fun z ↦ c • z) ⁻¹' s)

Tactic:
refine hs.linear_preimage (LinearMap.lsmul _ _ c) ?_ (smul_right_injective E hc)

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : IsDomain 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module.IsTorsionFree 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
hc : c ≠ 0
⊢ Continuous ⇑((LinearMap.lsmul 𝕜 E) c)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p : P
⊢ ↑(affineSpan k {p}) = {p}

Tactic:
ext x
  rw [mem_coe, ← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_singleton p)) _,
    direction_affineSpan]
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ vectorSpan k {p₁, p₂} = k ∙ (p₁ -ᵥ p₂)

Tactic:
simp_rw [vectorSpan_eq_span_vsub_set_left k (mem_insert p₁ _), image_pair, vsub_self,
    Submodule.span_insert_zero]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
h : ¬r = 0
⊢ ‖r‖ * f x ≤ f (r • x)

Tactic:
rw [← mul_le_mul_iff_right₀ (inv_pos.mpr (norm_pos_iff.mpr h))]

Goal state after:
case neg
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
h : ¬r = 0
⊢ ‖r‖⁻¹ * (‖r‖ * f x) ≤ ‖r‖⁻¹ * f (r • x)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ (affineSpan k (↑s ∪ ↑(affineSpan k {p₂}))).direction = s.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
change (s ⊔ affineSpan k {p₂}).direction = _

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ (s ⊔ affineSpan k {p₂}).direction = s.direction ⊔ k ∙ (p₂ -ᵥ p₁)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
hs : s.Nonempty
x : E
i : ι
hi : i ∈ s
hix : (s.sup fun i ↦ ⟨(p i) x, ⋯⟩) = ⟨(p i) x, ⋯⟩
⊢ ∃ i ∈ s, (s.sup p) x = (p i) x

Tactic:
finset_sup_apply

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
hs : s.Nonempty
x : E
i : ι
hi : i ∈ s
hix : (s.sup fun i ↦ ⟨(p i) x, ⋯⟩) = ⟨(p i) x, ⋯⟩
⊢ ∃ i ∈ s, ↑(s.sup fun i ↦ NNReal.mk ((p i) x) ⋯) = (p i) x
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
⊢ ↑(s.sup fun i ↦ NNReal.mk (((C • p) i) x) ⋯) = C • (s.sup p) x

Tactic:
finset_sup_apply

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
⊢ ↑(s.sup fun i ↦ NNReal.mk (((C • p) i) x) ⋯) = C • ↑(s.sup fun i ↦ NNReal.mk ((p i) x) ⋯)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
⊢ (∀ ⦃x : E⦄,
      x ∈ s →
        ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y) →
    ∀ ⦃x : E⦄,
      x ∈ s →
        ∀ ⦃y : E⦄,
          y ∈ s →
            x ≠ y →
              ∀ ⦃a b : 𝕜⦄,
                0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y

Tactic:
by
    intro h x hx y hy hxy a b ha hb
    have hab := add_pos ha hb
    apply h hx hy hxy (div_pos ha hab) (div_pos hb hab)
    rw [← add_div, div_self hab.ne']

Goal state after: