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

Goal state before:
pp: case e'_5
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
B : HasSum (fun n ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ (fun n ↦ ↑n * x ^ n) = fun b ↦ (↑b + 1) * x ^ b - x ^ b

Tactic:
ext n

Goal state after:
case e'_5
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
B : HasSum (fun n ↦ x ^ n) (1 - x)⁻¹ʳ
n : ℕ
⊢ ↑n * x ^ n = (↑n + 1) * x ^ n - x ^ n
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ Surjective mk

Tactic:
rintro ⟨x⟩
  exact ⟨x, rfl⟩

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ Continuous[_, inst✝] ({1}.piecewise (const (↑I) y) (const (↑I) x))

pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : ↑I
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ?refine_1, source' := ⋯, target' := ⋯ }
      t ∈
    F

Tactic:
· exact isClosed_singleton.continuous_piecewise_of_specializes continuous_const continuous_const
      fun _ ↦ h

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : ↑I
⊢ { toFun := {1}.piecewise (const (↑I) y) (const (↑I) x), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } t ∈ F
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace (X × Y)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] (Function.uncurry fun x y ↦ (Function.uncurry (fun x y ↦ x.curry y) x) y)

Tactic:
← (Homeomorph.prodAssoc _ _ _).symm.comp_continuous_iff'

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace (X × Y)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹]
    ((Function.uncurry fun x y ↦ (Function.uncurry (fun x y ↦ x.curry y) x) y) ∘
      ⇑(Homeomorph.prodAssoc C(X × Y, Z) X Y).symm)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
s : (i : ι) → Set (Z i)
h : ∀ (i : ι), IsPathConnected (s i)
⊢ IsPathConnected (univ.pi s)

Tactic:
by
  choose x hx hjoin using h
  exact ⟨x, by simpa, fun y hy ↦ .pi fun i ↦ hjoin i (by grind)⟩

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

Goal state before:
pp: ⊢ Tendsto Int.cast Filter.cofinite (cocompact ℝ)

Tactic:
apply (castAddHom ℝ).tendsto_coe_cofinite_of_discrete cast_injective
  rw [range_castAddHom, SetLike.isDiscrete_iff_discreteTopology]
  infer_instance

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

Goal state before:
pp: case pos
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ -(‖x‖ * √((‖x‖ ^ 2 - (-x).im ^ 2) / ‖x‖ ^ 2)) = x.re

Tactic:
simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]

Goal state after:
case pos
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ -(‖x‖ * (-x.re / ‖x‖)) = x.re
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ -(‖x‖ * √((‖x‖ ^ 2 - (-x).im ^ 2) / ‖x‖ ^ 2)) = x.re

Tactic:
simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]

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

Goal state before:
pp: x : ℝ
⊢ arccos x = 0 ↔ 1 ≤ x

Tactic:
simp [arccos, sub_eq_zero]

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

Goal state before:
pp: case neg.mpr
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ { re := x, im := y }.im < 0 → { re := x, im := y }.arg = -(π / 2)

Tactic:
rintro ⟨rfl : x = 0, hy : y < 0⟩

Goal state after:
case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ { re := 0, im := y }.arg = -(π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).im = (log ↑x).im

Tactic:
rw [ofReal_im, log_im, arg_ofReal_of_nonneg hx]

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

Goal state before:
pp: x : ℝ
n : ℕ
⊢ log (x ^ n) = ↑n * log x

Tactic:
induction n with

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

Goal state before:
pp: case refine_2
s : Set ℂ
hs : s.Countable
⊢ (cexp ⁻¹' s).Countable

Tactic:
· rw [← Set.biUnion_preimage_singleton]
    refine hs.biUnion fun z hz => ?_
    by_cases! h : ∃ w, exp w = z
    · rcases h with ⟨w, rfl⟩
      simp only [Set.preimage, Set.mem_singleton_iff, exp_eq_exp_iff_exists_int, Set.ofPred_exists]
      exact Set.countable_iUnion fun m => Set.countable_singleton _
    · simp [Set.preimage, h]

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

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
⊢ (fun x ↦ 1 + y / x) =ᶠ[atTop] rexp ∘ fun x ↦ log (x + y) - log x

Tactic:
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_gt_atTop (-y)] with x hx₀ hxy

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

Goal state before:
pp: z : ℂ
⊢ |z.arg| < π / 2 ↔ 0 < z.re ∨ z = 0

Tactic:
by
  rw [abs_lt, arg_lt_pi_div_two_iff, neg_pi_div_two_lt_arg_iff, ← or_and_left]
  rcases eq_or_ne z 0 with hz | hz
  · simp [hz]
  · simp_rw [hz, or_false, ← not_lt, not_and_self_iff, or_false]

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

Goal state before:
pp: x n : ℂ
⊢ x⁻¹ ^ n = if x.arg = π then (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else (x ^ n)⁻¹

Tactic:
by
  simp_rw [Complex.cpow_def, log_inv_eq_ite, inv_eq_zero, map_eq_zero, ite_mul, neg_mul,
    RCLike.conj_inv, apply_ite conj, apply_ite exp, apply_ite Inv.inv, map_zero, map_one, exp_neg,
    inv_one, inv_zero, ← exp_conj, map_mul, conj_conj]
  split_ifs with hx hn ha ha <;> rfl

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

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

Tactic:
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
      simp [hr]

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

Goal state before:
pp: θ : ℝ
⊢ (↑θ).toReal = θ + 2 * π ↔ θ ∈ Set.Ioc (-3 * π) (-π)

Tactic:
convert! @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ (-1) using 2 <;> norm_num

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

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

Tactic:
induction n with

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

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

Tactic:
induction n with
    | zero => simp
    | succ n ih => rw [pow_succ, arg_mul_coe_angle (pow_ne_zero n x0) x0, ih, succ_nsmul]

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

Goal state before:
pp: z : ℂ
θ : Real.Angle
⊢ ↑z.arg = θ ↔ z.arg = θ.toReal

Tactic:
rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]

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

Goal state before:
pp: θ : Angle
h : θ.sign = -1 ∨ θ.sign = 0
⊢ -↑|θ.toReal| = θ

Tactic:
rcases h with (h | h)

Goal state after:
case inl
θ : Angle
h : θ.sign = -1
⊢ -↑|θ.toReal| = θ

case inr
θ : Angle
h : θ.sign = 0
⊢ -↑|θ.toReal| = θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
rwa [← hθ', ne_comm, ← neg_add, sign_neg, sign_neg, neg_injective.ne_iff]

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

Goal state before:
pp: h : Tendsto (fun x ↦ log x * x) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (fun x ↦ log x * x) (𝓝[<] 0) (𝓝 0)

Tactic:
have h_eq : ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ (fun x ↦ |x|)) x = log x * x := by
    simp only [Set.mem_Iio, Pi.neg_apply, Function.comp_apply, log_abs]
    intro x hx
    simp only [abs_of_nonpos hx.le, mul_neg, neg_neg]

Goal state after:
h : Tendsto (fun x ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ fun x ↦ |x|) x = log x * x
⊢ Tendsto (fun x ↦ log x * x) (𝓝[<] 0) (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x

Tactic:
rcases eq_bot_or_bot_lt x with (rfl | (h : 0 < x))

Goal state after:
case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
⊢ ⊥ ^ z ≤ ⊥

case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
h : 0 < y
⊢ (if 0 = 0 ∧ y < 0 then ∞ else ↑(NNReal.rpow 0 y)) = some 0

Tactic:
simp [asymm h, ne_of_gt h]

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

Goal state before:
pp: x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
⊢ x ^ n ≤ y ↔ ↑n * log x ≤ log y

Tactic:
rw [← rpow_le_iff_le_log hx hy, rpow_intCast]

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
hf : ∀ i ∈ s, f i ≠ ∞
r : ℝ
⊢ ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih =>
    have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
    rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
    apply prod_ne_top h2f

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

Goal state before:
pp: case insert
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
ih : ∏ i ∈ s✝, f i ^ r = (∏ i ∈ s✝, f i) ^ r
⊢ f a✝ ^ r * (∏ i ∈ s✝, f i) ^ r = (f a✝ * ∏ i ∈ s✝, f i) ^ r

Tactic:
← mul_rpow_of_nonneg _ _ hr

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

Goal state before:
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:
lift y to ℝ≥0 using hy
    simp only [← coe_rpow_of_nonneg _ h.le, NNReal.rpow_lt_rpow (coe_lt_coe.1 hxy) h, coe_lt_coe]

Goal state after:
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 : P1 → P2
f' : V1 →ₗ[k] V2
p : P1
h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p
p' : P1
v : V1
⊢ f' ((v +ᵥ p') -ᵥ p) +ᵥ f p = f' v +ᵥ f p'

Tactic:
h p',

Goal state after:
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 : P1 → P2
f' : V1 →ₗ[k] V2
p : P1
h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p
p' : P1
v : V1
⊢ f' ((v +ᵥ p') -ᵥ p) +ᵥ f p = f' v +ᵥ f' (p' -ᵥ p) +ᵥ f p
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ SameRay R x y ∧ y ≠ 0 → ∃ r, 0 < r ∧ r • x = y

Tactic:
· rintro ⟨hxy, hy⟩
    exact (exists_pos_left_iff_sameRay hx hy).2 hxy

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

Goal state before:
pp: k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝⁴ : (i : ι) → AddCommGroup (φv i)
inst✝³ : (i : ι) → Module k (φv i)
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst✝ : Nonempty ι
h : ∀ (i : ι), f.comp (LinearMap.single k φv i).toAffineMap = g.comp (LinearMap.single k φv i).toAffineMap
i : ι
x : φv i
⊢ f (Pi.single i x) = g (Pi.single i x)

Tactic:
convert! AffineMap.congr_fun (h i) x

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

Goal state before:
pp: case mp
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 : Set P
⊢ (spanPoints k s).Nonempty → s.Nonempty

Tactic:
contrapose
    rw [Set.not_nonempty_iff_eq_empty, Set.not_nonempty_iff_eq_empty]
    intro h
    simp [h, spanPoints]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : IsStrictOrderedModule 𝕜 E
inst✝ : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
hz : z ∉ Iic x
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • y + b • z ∉ Iic x

Tactic:
mem_Iic

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : IsStrictOrderedModule 𝕜 E
inst✝ : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
hz : ¬z ≤ x
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ¬a • y + b • z ≤ x
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ x ∈ (convexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t

Tactic:
convexHull_eq_iInter,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ x ∈ ⋂ t, ⋂ (_ : s ⊆ t), ⋂ (_ : Convex 𝕜 t), t ↔ ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t
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
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ s.direction = ⊤ ↔ s = ⊤

Tactic:
by
  constructor
  · intro hd
    rw [← direction_top k V P] at hd
    refine ext_of_direction_eq hd ?_
    simp [h]
  · rintro rfl
    simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ interior A
⊢ Balanced 𝕜 (interior A)

Tactic:
rw [← insert_eq_self.2 h]

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ interior A
⊢ Balanced 𝕜 (insert 0 (interior A))
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.ball 0 1

Tactic:
rw [← isVonNBounded_iff 𝕜]
  constructor
  · intro h
    rcases (h (Metric.ball_mem_nhds 0 zero_lt_one)).exists_pos with ⟨ρ, _, hρball⟩
    rcases NormedField.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩
    exact ⟨a, hρball a ha.le⟩
  · rintro ⟨a, ha⟩
    exact ((isVonNBounded_ball 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

Goal state after:
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 ι
x : E
⊢ (s.sup p) x = 0 ∨ ∃ i ∈ s, (s.sup p) x = (p i) x

Tactic:
rcases Finset.eq_empty_or_nonempty s with (rfl | hs)

Goal state after:
case inl
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ (∅.sup p) x = 0 ∨ ∃ i ∈ ∅, (∅.sup p) x = (p i) x

case inr
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
hs : s.Nonempty
⊢ (s.sup p) x = 0 ∨ ∃ i ∈ s, (s.sup p) x = (p i) x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : AffineSpace W Q
s : Set P
t : Set Q
hs : s.Nonempty
ht : t.Nonempty
⊢ vectorSpan k (s ×ˢ t) = (vectorSpan k s).prod (vectorSpan k t)

Tactic:
rw [vectorSpan_def, Set.prod_vsub_prod_comm]
  exact Submodule.span_prod_eq k hs.zero_mem_vsub_self ht.zero_mem_vsub_self

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ p.closedBall x r = ⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ

Tactic:
by
  ext y; simp_rw [mem_closedBall, mem_iInter₂, mem_ball, ← forall_gt_iff_le]

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

Goal state before:
pp: case right
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hw : ∑ i ∈ insert i0 l.support, w i = 0
hz : (fun i ↦ w i • (p i -ᵥ p i0)) i0 = 0
⊢ v = ((insert i0 l.support).weightedVSub p) w

Tactic:
rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w p hw (p i0),
          Finset.weightedVSubOfPoint_apply, ← hv, Finsupp.linearCombination_apply,
          @Finset.sum_insert_zero _ _ l.support i0 _ _ _ hz]

Goal state after:
case right
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hw : ∑ i ∈ insert i0 l.support, w i = 0
hz : (fun i ↦ w i • (p i -ᵥ p i0)) i0 = 0
⊢ (l.sum fun i a ↦ a • (p i -ᵥ p i0)) = ∑ x ∈ l.support, w x • (p x -ᵥ p i0)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕝 : Type u_6
E : Type u_7
ι : Type u_11
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : ι → Seminorm 𝕝 E
s : Finset ι
hp : ∀ i ∈ s, Continuous[inst✝, _] ⇑(p i)
⊢ Continuous[inst✝, _] ⇑(∑ i ∈ s, p i)

Tactic:
change Continuous (fun x ↦ FunLike.coeAddMonoidHom _ _ _ (∑ i ∈ s, p i) x)
  simp_rw [map_sum, Finset.sum_apply]
  exact _root_.continuous_finsetSum s hp

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_4
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
xεpos : 0 < p x / ε
n : ℤ
hn : p x / ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ ‖c ^ (-(n + 1))‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x

Tactic:
· show ‖(c ^ (-(n + 1)))‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x
    have : ε⁻¹ * ‖c‖ * p x = ε⁻¹ * p x * ‖c‖ := by ring
    rw [zpow_neg, norm_inv, inv_inv, norm_zpow, zpow_add₀ (ne_of_gt cpos), zpow_one, this,
        ← div_eq_inv_mul]
    gcongr; exact hn.1

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (range fun x_1 ↦ (p x_1) x)
⊢ BddAbove (range p)

Tactic:
rw [Seminorm.bddAbove_range_iff]
  intro x
  obtain ⟨c, hc₀, hc⟩ : ∃ c ≠ 0, (c : 𝕜) • x ∈ s :=
    (eventually_mem_nhdsWithin.and (hs.eventually_nhdsNE_zero x)).exists
  rcases h _ hc with ⟨M, hM⟩
  refine ⟨M / ‖c‖, forall_mem_range.mpr fun i ↦ (le_div_iff₀' (norm_pos_iff.2 hc₀)).2 ?_⟩
  exact hM ⟨i, map_smul_eq_mul ..⟩

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

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → V
hp : AffineIndependent k p
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (w₁ - w₂) i = 0

Tactic:
simpa [sub_mul, sub_smul, sub_eq_zero]

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

Goal state before:
pp: case refine_2
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → V
hp : AffineIndependent k p
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (w₁ - w₂) i • p i = 0

Tactic:
simpa [sub_mul, sub_smul, sub_eq_zero]

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

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w₁ w₂ : V → k
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i
i : V
hi : i ∈ s
⊢ ∑ x ∈ s, (w₁ - w₂) x = 0

Tactic:
simpa [sub_mul, sub_smul, sub_eq_zero]

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

Goal state before:
pp: case refine_2
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w₁ w₂ : V → k
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i
i : V
hi : i ∈ s
⊢ ∑ x ∈ s, (w₁ - w₂) x • x = 0

Tactic:
simpa [sub_mul, sub_smul, sub_eq_zero]

Goal state after: