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

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

pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → z.arg = π / 2

Tactic:
· intro h
    rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [h₀]

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

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

Tactic:
← log_one

Goal state after:
x : ℝ
h : 0 < x
⊢ log x < log 1 ↔ x < 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

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

Tactic:
· intro h
    rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [h₀]

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

Goal state before:
pp: x : ℂ
⊢ log (cexp x) = x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)

Tactic:
log_exp_eq_re_add_toIocMod,

Goal state after:
x : ℂ
⊢ ↑x.re + ↑(toIocMod Real.two_pi_pos (-π) x.im) * I = x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
obtain ⟨x, y⟩ := z
    rintro ⟨rfl : x = 0, hy : y < 0⟩
    rw [← arg_neg_I, ← arg_real_mul (-I) (neg_pos.2 hy), mk_eq_add_mul_I]
    simp

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

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

Tactic:
by
  by_cases hx : x = 0
  · simp [hx]
  rw [inv_def, log_mul_ofReal, Real.log_inv, ofReal_neg, ← sub_eq_neg_add, log_conj_eq_ite]
  · simp_rw [log, map_add, map_mul, conj_ofReal, conj_I, normSq_eq_norm_sq, Real.log_pow,
      Nat.cast_two, ofReal_mul, neg_add, mul_neg, neg_neg]
    norm_num
    grind
  · rwa [inv_pos, Complex.normSq_pos]
  · rwa [map_ne_zero]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)

Tactic:
have H : (fun i ↦ log (f i)).support = f.mulSupport := by
    grind [mem_mulSupport, mem_support, log_eq_zero]

Goal state after:
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support fun i ↦ log (f i)) = mulSupport f
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
rcases le_or_gt 0 x with hx | hx
  · rw [abs_rpow_of_nonneg hx]
  · rw [abs_of_neg hx, rpow_def_of_neg hx, rpow_def_of_pos (neg_pos.2 hx), log_neg_eq_log, abs_mul,
      abs_of_pos (exp_pos _)]
    exact mul_le_of_le_one_right (exp_pos _).le (abs_cos_le_one _)

Goal state after:
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
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
have : ((θ + ψ).toReal : Angle) = ↑(θ.toReal + ψ.toReal) := by simp

Goal state after:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
Complex.ofReal_add,

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

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

Tactic:
rcases le_total x y with hxy | hxy

Goal state after:
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)

case inr
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : y ≤ x
⊢ max x y ^ p = max (x ^ p) (y ^ p)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
rcases le_total x y with hxy | hxy

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

case inr
x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
hxy : y ≤ x
⊢ max x y ^ p = max (x ^ p) (y ^ p)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x y z : ℝ
x1 : 1 ≤ x
yz : y ≤ z
⊢ x ^ y ≤ x ^ z

Tactic:
exact Real.rpow_le_rpow_of_exponent_le x1 yz

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

Goal state before:
pp: case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
· rw [coe_le_one_iff] at hx1
    simp [← coe_rpow_of_ne_zero h,
      NNReal.rpow_le_rpow_of_exponent_ge (bot_lt_iff_ne_bot.mpr h) hx1 hyz]

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

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

Tactic:
by
  nth_rw 1 [← ENNReal.rpow_one x]
  exact ENNReal.rpow_le_rpow_of_exponent_le hx h_one_le

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

Goal state before:
pp: case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_nonpos : p ≤ 0
⊢ 0 < x ^ p

Tactic:
rw [← neg_neg p, rpow_neg, ENNReal.inv_pos]
    exact rpow_ne_top_of_nonneg (Right.nonneg_neg_iff.mpr hp_nonpos) hx_ne_top

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < (↑n ^ ↑x)⁻¹

Tactic:
refine RCLike.inv_pos_of_pos ?_
  rw [show (n : ℂ) ^ (x : ℂ) = (n : ℝ) ^ (x : ℂ) from rfl, ← ofReal_cpow n.cast_nonneg']
  positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
⊢ (1 - p) • c + p • x ∈ {c}

Tactic:
have Hx : x = (x - c) + c := by abel

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
⊢ (1 - p) • c + p • x ∈ {c}
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ [x -[𝕜] x]

Tactic:
rw [segment_same]
    exact hyz.antisymm hxz

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ (fun θ ↦ x + θ • (y - x)) '' Icc 0 1

Tactic:
exact mem_image_of_mem _ ⟨ht₀, ht₁⟩

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
h : (↑s).Nonempty
c : k
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
hp₂ : p₂ ∈ ↑s
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ ↑s

Tactic:
exact s.smul_vsub_vadd_mem c hp₁ hp₂ hp₂

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 ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Tactic:
coe_direction_eq_vsub_set_left hp

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 ∈ (fun x ↦ p -ᵥ x) '' ↑s ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst✝¹] U
h : 0 ∈ U
⊢ IsClosed[inst✝¹] (balancedCore 𝕜 U)

Tactic:
rw [balancedCore_eq_iInter h]

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst✝¹] U
h : 0 ∈ U
⊢ IsClosed[inst✝¹] (⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • U)
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NormedDivisionRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : RegularSpace E
s : Set E
hs : s ∈ 𝓝 0 ∧ IsClosed[inst✝³] s
⊢ ∃ i', (i' ∈ 𝓝 0 ∧ IsClosed[inst✝³] i' ∧ Balanced 𝕜 i') ∧ id i' ⊆ id s

Tactic:
refine ⟨balancedCore 𝕜 s, ⟨balancedCore_mem_nhds_zero hs.1, ?_⟩, balancedCore_subset s⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NormedDivisionRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : RegularSpace E
s : Set E
hs : s ∈ 𝓝 0 ∧ IsClosed[inst✝³] s
⊢ IsClosed[inst✝³] (balancedCore 𝕜 s) ∧ Balanced 𝕜 (balancedCore 𝕜 s)
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_6
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
𝕝 : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : NormedAlgebra 𝕜 𝕝
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
⊢ ∃ ε, Tendsto ε atTop (𝓝 0) ∧ ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0

Tactic:
simpa only [tendsto_nhdsWithin_iff] using! exists_seq_tendsto (𝓝[≠] (0 : 𝕜))

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Metric.ball 0 r
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Metric.ball 0 i) s

Tactic:
rw [← ball_normSeminorm 𝕜 E] at hr ⊢

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ (normSeminorm 𝕜 E).ball 0 r
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 ((normSeminorm 𝕜 E).ball 0 i) s
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: case inr
𝕜 : Type u_1
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : TopologicalSpace β
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : OrderTopology β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
hlt : y < x
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
openSegment_symm

Goal state after:
case inr
𝕜 : Type u_1
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : TopologicalSpace β
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : OrderTopology β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
hlt : y < x
⊢ openSegment 𝕜 y x ⊆ interior s
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightMono 𝕜
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ (fun θ ↦ x + θ • (y - x)) '' Ioo 0 1

Tactic:
exact mem_image_of_mem _ ⟨ht₀, ht₁⟩

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

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
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ ((s \ s₂).weightedVSubOfPoint p b) w + (s₂.weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w

Tactic:
s.weightedVSubOfPoint_sdiff h

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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ (s.weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 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✝² : SeminormedRing 𝕜
inst✝¹ : AddGroup E
inst✝ : SMul 𝕜 E
f g : Seminorm 𝕜 E
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
rcases f with ⟨⟨_⟩⟩

Goal state after:
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✝² : SeminormedRing 𝕜
inst✝¹ : AddGroup E
inst✝ : SMul 𝕜 E
g : Seminorm 𝕜 E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le'✝ : ∀ (r s : E), toFun✝ (r + s) ≤ toFun✝ r + toFun✝ s
neg'✝ : ∀ (r : E), toFun✝ (-r) = toFun✝ r
smul'✝ :
  ∀ (a : 𝕜) (x : E),
    { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝ }.toFun (a • x) =
      ‖a‖ * { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝ }.toFun x
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝, smul' := smul'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝, smul' := smul'✝ } = g
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

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
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : ∑ i ∈ s, w i = 1
⊢ ∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i) = 0

Tactic:
refine sum_eq_zero ?_

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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : ∑ i ∈ s, w i = 1
⊢ ∀ x ∈ s, w x • (p x -ᵥ p i) = 0
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
a : ℝ
ha : 0 ≤ a
h : ∀ i ∈ s, (p i) x ≤ a
⊢ (s.sup p) x ≤ a

Tactic:
lift a to ℝ≥0 using ha
  rw [finset_sup_apply, NNReal.coe_le_coe]
  exact Finset.sup_le h

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k univ p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0

Tactic:
by
  rw [univ_fin2]
  convert! centroid_pair k p 0 1

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

Goal state before:
pp: ι : 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
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
p : ι → P
hnz : ∑ i ∈ s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (Finset.affineCombination k s p) w1 = p i1
hv : (Finset.affineCombination k s p) w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction
⊢ ((Finset.affineCombination k s p) w -ᵥ p i1) +ᵥ p i1 ∈ affineSpan k (Set.range p)

Tactic:
exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_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 q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ (p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r

Tactic:
by
  simp_rw [closedBall, ← Set.ofPred_and, coe_sup, Pi.sup_apply, sup_le_iff]

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

Goal state before:
pp: case mp.inl
ι : 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
hι : IsEmpty ι
⊢ v ∈ vectorSpan k (Set.range p) → ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w

Tactic:
rw [Set.range_eq_empty, vectorSpan_empty, Submodule.mem_bot]
        rintro rfl
        use ∅
        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✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ p₄ = ((1 - r₁) * (r₂ - r₁)⁻¹) • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
simp [mul_smul, ← hr, sub_smul, hp₁]

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

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : DivisionRing k
inst✝¹ : Module k V
inst✝ : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
⊢ (b.coord i) (Finset.centroid k s ⇑b) = (↑s.card)⁻¹

Tactic:
rw [Finset.centroid,
    b.coord_apply_combination_of_mem hi (s.sum_centroidWeights_eq_one_of_nonempty _ ⟨i, hi⟩),
    Finset.centroidWeights, Function.const_apply]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 ((normSeminorm 𝕜 E).ball 0 r)

Tactic:
exact (normSeminorm _ _).balanced_ball_zero r

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (Metric.ball 0 r)

Tactic:
rw [← ball_normSeminorm 𝕜]
  exact (normSeminorm _ _).balanced_ball_zero r

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

Goal state before:
pp: S : Type u_1
inst✝³ : Semiring S
inst✝² : PartialOrder S
X : Type u_2
inst✝¹ : Fintype X
inst✝ : IsOrderedRing S
s : ↑(stdSimplex S X)
x : X
⊢ s x ≤ 1

Tactic:
by
  rw [← sum_eq_one s]
  exact Finset.single_le_sum (by simp) (by simp)

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

Goal state before:
pp: case refine_2
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
x✝ : (affineCombination k univ s.points) w ∈ Simplex.setInterior I s
⊢ (affineCombination k univ s.points) w ∈ Simplex.setInterior I (s.reindex e)

Tactic:
rw [← Function.comp_id w, ← Function.comp_id s.points, ← e.symm_comp_self,
      ← Function.comp_assoc, ← Function.comp_assoc, ← e.coe_toEmbedding,
      ← Finset.univ.affineCombination_map e.toEmbedding, map_univ_equiv]

Goal state after:
case refine_2
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
x✝ : (affineCombination k univ s.points) w ∈ Simplex.setInterior I s
⊢ (affineCombination k univ (s.points ∘ ⇑e.symm)) (w ∘ ⇑e.symm) ∈ Simplex.setInterior I (s.reindex e)
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
⊢ (⋃ x ∈ s, nhdsKer {x}) ×ˢ ⋃ y ∈ t, nhdsKer {y} = nhdsKer s ×ˢ nhdsKer t

Tactic:
by
    simp_rw [← nhdsKer_biUnion, biUnion_of_singleton]

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ (univ.pi fun i ↦ ⋃ x ∈ s i, nhdsKer {x}) = univ.pi fun i ↦ nhdsKer (s i)

Tactic:
by
    simp_rw [← nhdsKer_biUnion, biUnion_of_singleton]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
⊢ AlexandrovDiscrete α

Tactic:
by
    simp only [alexandrovDiscrete_iff_isClosed, isClosed_iff_clusterPt, ClusterPt, funext hα,
      inf_principal, principal_neBot_iff]
    intro S hS a ha
    rw [sUnion_eq_biUnion, inter_iUnion₂, nonempty_biUnion] at ha
    obtain ⟨s, hs, has⟩ := ha
    specialize hS s hs a has
    exact mem_sUnion_of_mem hS hs

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous[inst✝¹, x✝] f
y : Y
u : Set Y
hu : IsOpen[TopologicalSpace.coinduced f inst✝¹] u
x : X
hx : x ∈ f ⁻¹' pathComponentIn u y
hx' : x ∈ f ⁻¹' u
⊢ pathComponentIn (f ⁻¹' u) x ⊆ f ⁻¹' pathComponentIn u y

Tactic:
← image_subset_iff,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
Y : Type u_4
f : X → Y
x✝ : TopologicalSpace Y := TopologicalSpace.coinduced f inst✝¹
hf : Continuous[inst✝¹, x✝] f
y : Y
u : Set Y
hu : IsOpen[TopologicalSpace.coinduced f inst✝¹] u
x : X
hx : x ∈ f ⁻¹' pathComponentIn u y
hx' : x ∈ f ⁻¹' u
⊢ f '' pathComponentIn (f ⁻¹' u) x ⊆ pathComponentIn u y
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : s ∩ Ioi a = ∅
⊢ 𝓝[s \ {a}] a = 𝓝[<] a

Tactic:
rw [sdiff_eq, ← Iio_union_Ioi, inter_union_distrib_left, nhdsWithin_union]
  simp [h_Ioi, hs.nhdsWithin_inter_Iio_eq_nhdsLT has h_Iio]

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

Goal state before:
pp: F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
⊢ (convexHull ℝ) (sphere x r) = closedBall x r

Tactic:
suffices convexHull ℝ (sphere (0 : F) r) = closedBall 0 r by
    rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]

Goal state after:
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
⊢ (convexHull ℝ) (sphere 0 r) = closedBall 0 r
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (Metric.thickening δ s)

Tactic:
by
  rw [← add_ball_zero]
  exact hs.add (convex_ball 0 _)

Goal state after: