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

Goal state before:
pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ↑x = 0
h✝¹ : ¬↑y = 0
h✝ : ¬x = 0
⊢ Complex.re 0 = rexp (log x * y)

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

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

Goal state before:
pp: case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ¬↑x = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = 1

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

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

Goal state before:
pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ¬↑x = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = 0

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

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

Goal state before:
pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : ¬↑x = 0
h✝ : ¬x = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y)

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ (↑(x.toNNReal ^ y)).toNNReal = x.toNNReal ^ y

Tactic:
Real.toNNReal_coe

Goal state after:
x y : ℝ
hx : 0 ≤ x
⊢ x.toNNReal ^ y = x.toNNReal ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
← coe_one,

Goal state after:
x : ℝ
⊢ ↑1 ^ x = ↑1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
rw [← coe_one, ← coe_rpow_of_ne_zero one_ne_zero]
  simp

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

Goal state before:
pp: x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = √x ^ r

Tactic:
rw [sqrt_eq_rpow, ← rpow_mul hx]
  congr
  ring

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

Goal state before:
pp: x : ℂ
hx : x.im < 0
⊢ (x ^ 2⁻¹).im = -√((‖x‖ - x.re) / 2)

Tactic:
rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, sin_half_eq_neg_sqrt, mul_neg, ← sqrt_mul (norm_nonneg _),
    ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
  · linarith [pi_pos, neg_pi_lt_arg x]
  · exact (arg_neg_iff.2 hx).le

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ midpoint R x y = y ↔ x = y

Tactic:
by
  rw [midpoint_comm, midpoint_eq_left_iff, eq_comm]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x y : E
⊢ [x -[𝕜] y] = (fun p ↦ p.1 • x + p.2 • y) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

Tactic:
by
  simp only [segment, image, Prod.exists, mem_ofPred_eq, and_assoc]

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c d : k
⊢ (lineMap ((lineMap p₀ p₁) c) p₁) d = (lineMap p₁ p₀) ((1 - d) * (1 - c))

Tactic:
← lineMap_apply_one_sub p₁,

Goal state after:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c d : k
⊢ (lineMap p₁ ((lineMap p₁ p₀) (1 - c))) (1 - d) = (lineMap p₁ p₀) ((1 - d) * (1 - c))
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
h : SameRay R v₁ v₂
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)

Tactic:
by
  rcases h with (rfl | rfl | ⟨r₁, r₂, h₁, h₂, H⟩)
  · use 0, 1
    simp
  · use 1, 0
    simp
  · have h₁₂ : 0 < r₁ + r₂ := add_pos h₁ h₂
    refine
      ⟨r₂ / (r₁ + r₂), r₁ / (r₁ + r₂), div_nonneg h₂.le h₁₂.le, div_nonneg h₁.le h₁₂.le, ?_, ?_, ?_⟩
    · rw [← add_div, add_comm, div_self h₁₂.ne']
    · rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']
    · rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']

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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (lineMap x y) a ∈ ⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1

Tactic:
left

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (lineMap x y) a ∈ ⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) a) (⇑(lineMap x ((lineMap x y) a)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) a) y) '' Ioo 0 1)

Tactic:
left

Goal state after:
case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (lineMap x y) a = (lineMap x y) a
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
⊢ ¬s.Nonempty → ¬(spanPoints k s).Nonempty

Tactic:
rw [Set.not_nonempty_iff_eq_empty, Set.not_nonempty_iff_eq_empty]

Goal state after:
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
⊢ s = ∅ → spanPoints k s = ∅
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : Semiring 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : PartialOrder 𝕜
𝕜' : Type u_5
inst✝⁵ : Semiring 𝕜'
inst✝⁴ : PartialOrder 𝕜'
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomSurjective σ
F' : Type u_6
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜' F'
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
hσ : ∀ {s t : 𝕜}, σ s ≤ σ t ↔ s ≤ t
f : E →ₛₗ[σ] F'
x : E
hx : x ∈ s
y : E
hy : y ∈ s
r : 𝕜
ha : 0 ≤ σ r
t : 𝕜
hb : 0 ≤ σ t
hab : σ r + σ t = 1
⊢ 0 ≤ t

Tactic:
simp_all [(@hσ 0 t).mp]

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 : Set P
⊢ (affineSpan k s).direction = vectorSpan k s

Tactic:
by
  apply le_antisymm
  · refine Submodule.span_le.2 ?_
    rintro v ⟨p₁, ⟨p₂, hp₂, v₁, hv₁, hp₁⟩, p₃, ⟨p₄, hp₄, v₂, hv₂, hp₃⟩, rfl⟩
    simp only [SetLike.mem_coe]
    rw [hp₁, hp₃, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc]
    exact
      (vectorSpan k s).sub_mem ((vectorSpan k s).add_mem hv₁ (vsub_mem_vectorSpan k hp₂ hp₄)) hv₂
  · exact vectorSpan_mono k (subset_spanPoints k s)

Goal state after:
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
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
⊢ balancedCore 𝕜 U ∈ 𝓝 0

Tactic:
by
  -- Getting neighborhoods of the origin for `0 : 𝕜` and `0 : E`
  obtain ⟨r, V, hr, hV, hrVU⟩ : ∃ (r : ℝ) (V : Set E),
      0 < r ∧ V ∈ 𝓝 (0 : E) ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U := by
    have h : Filter.Tendsto (fun x : 𝕜 × E => x.fst • x.snd) (𝓝 (0, 0)) (𝓝 0) :=
      continuous_smul.tendsto' (0, 0) _ (smul_zero _)
    simpa only [← Prod.exists', ← Prod.forall', ← and_imp, ← and_assoc, exists_prop] using!
      h.basis_left (NormedAddGroup.nhds_zero_basis_norm_lt.prod_nhds (𝓝 _).basis_sets) U hU
  obtain ⟨y, hyr, hy₀⟩ : ∃ y : 𝕜, ‖y‖ < r ∧ y ≠ 0 :=
    Filter.nonempty_of_mem <|
      (nhdsWithin_hasBasis NormedAddGroup.nhds_zero_basis_norm_lt {0}ᶜ).mem_of_mem hr
  have : y • V ∈ 𝓝 (0 : E) := (set_smul_mem_nhds_zero_iff hy₀).mpr hV
  -- It remains to show that `y • V ⊆ balancedCore 𝕜 U`
  refine Filter.mem_of_superset this (subset_balancedCore (mem_of_mem_nhds hU) fun a ha => ?_)
  rw [smul_smul]
  rintro _ ⟨z, hz, rfl⟩
  refine hrVU _ _ ?_ hz
  rw [norm_mul, ← one_mul r]
  exact mul_lt_mul' ha hyr (norm_nonneg y) one_pos

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht

Goal state after:
case inr.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 ∅

case inr.inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : (fun x1 x2 ↦ x1 + x2) v w ≠ (fun x1 x2 ↦ x1 + x2) v y
⊢ a • v + b • v + (a • w + b • y) ∈ interior (s + t)

Tactic:
refine interior_mono (add_subset_add (singleton_subset_iff.2 hv) Subset.rfl) ?_
    rw [Convex.combo_self hab, singleton_add]
    exact
      (isOpenMap_add_left _).image_interior_subset _
        (mem_image_of_mem _ <| ht hw hy (ne_of_apply_ne _ h) ha hb hab)

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
ι : Type u_4
p : ι → P
i0 : ι
⊢ vectorSpan k (range p) = Submodule.span k (range fun i ↦ p i0 -ᵥ p i)

Tactic:
vectorSpan_eq_span_vsub_set_left k (Set.mem_range_self i0),

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
ι : Type u_4
p : ι → P
i0 : ι
⊢ Submodule.span k ((fun x ↦ p i0 -ᵥ x) '' range p) = Submodule.span k (range fun i ↦ p i0 -ᵥ p i)
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
ι : Type u_4
p : ι → P
i₀ : ι
⊢ vectorSpan k (p '' univ) = Submodule.span k (range fun i ↦ p i₀ -ᵥ p ↑i)

Tactic:
vectorSpan_image_eq_span_vsub_set_left_ne k _ (Set.mem_univ i₀)

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
ι : Type u_4
p : ι → P
i₀ : ι
⊢ Submodule.span k ((fun x ↦ p i₀ -ᵥ x) '' p '' (univ \ {i₀})) = Submodule.span k (range fun i ↦ p i₀ -ᵥ p ↑i)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 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

Tactic:
left

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
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ∑ x ∈ s, Pi.single i 1 x - ∑ x ∈ s, Pi.single j 1 x = 0

Tactic:
simp [hi, hj]

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

Goal state before:
pp: case inr
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
⊢ affineSpan k (s ×ˢ t) = (affineSpan k s).prod (affineSpan k t)

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht

Goal state after:
case inr.inl
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
hs : s.Nonempty
⊢ affineSpan k (s ×ˢ ∅) = (affineSpan k s).prod (affineSpan k ∅)

case inr.inr
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
⊢ affineSpan k (s ×ˢ t) = (affineSpan k s).prod (affineSpan k t)
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
r : ℝ
hr : 0 ≤ r
⊢ (s.sup p).closedBall x r = ⋂ i ∈ s, (p i).closedBall x r

Tactic:
by
  lift r to NNReal using hr
  simp_rw [closedBall, iInter_ofPred, finset_sup_apply, NNReal.coe_le_coe, Finset.sup_le_iff, ←
    NNReal.coe_le_coe, NNReal.coe_mk]

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
p₁ : P
p : ι → P
s : Set ι
h : p₁ ∈ affineSpan k (p '' s)
⊢ ∃ fs w, ↑fs ⊆ s ∧ ∑ i ∈ fs, w i = 1 ∧ p₁ = (Finset.affineCombination k fs p) w

Tactic:
Set.image_eq_range

Goal state after:
ι : 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
p₁ : P
p : ι → P
s : Set ι
h : p₁ ∈ affineSpan k (Set.range fun x ↦ p ↑x)
⊢ ∃ fs w, ↑fs ⊆ s ∧ ∑ i ∈ fs, w i = 1 ∧ p₁ = (Finset.affineCombination k fs p) w
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
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (p '' s')

Tactic:
Set.image_eq_range

Goal state after:
ι : 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
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range fun x ↦ p ↑x)
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁹ : AddCommGroup V
inst✝⁸ : AffineSpace V P
inst✝⁷ : Ring k
inst✝⁶ : Module k V
b✝ : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : DistribMulAction G V
inst✝² : DistribMulAction G' V
inst✝¹ : SMulCommClass G k V
inst✝ : SMulCommClass G' k V
a : G
b : AffineBasis ι k V
⊢ affineSpan k (range (a • ⇑b)) = ⊤

Tactic:
rw [Pi.smul_def, ← smul_set_range, ← AffineSubspace.smul_span, b.tot,
          AffineSubspace.smul_top (Group.isUnit a)]

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

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
ι : Type u_4
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : ι → k := fun i ↦ if h : ∃ i2, f i2 = i then w h.choose else 0
hw' : ∀ (i2 : ι2), w' (f i2) = w i2
hw's : ∑ i ∈ fs', w' i = 0
hs' : (fs'.weightedVSub p) w' = 0
⊢ w i0 = 0

Tactic:
← ha fs' w' hw's hs' (f i0) ((Finset.mem_map' _).2 hi0),

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
ι : Type u_4
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : ι → k := fun i ↦ if h : ∃ i2, f i2 = i then w h.choose else 0
hw' : ∀ (i2 : ι2), w' (f i2) = w i2
hw's : ∑ i ∈ fs', w' i = 0
hs' : (fs'.weightedVSub p) w' = 0
⊢ w i0 = w' (f i0)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mp.refine_2
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
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : ↑fs₁ ⊆ s₁
w₁ : ι → k
hw₁ : ∑ i ∈ fs₁, w₁ i = 1
fs₂ : Finset ι
hfs₂ : ↑fs₂ ⊆ s₂
w₂ : ι → k
hw₂ : ∑ i ∈ fs₂, w₂ i = 1
hw₁₂ : (affineCombination k fs₁ p) w₁ = (affineCombination k fs₂ p) w₂
ha : (↑fs₁).indicator w₁ = (↑fs₂).indicator w₂
i : ι
hi : i ∈ fs₁
⊢ w₁ i = if i ∈ ↑fs₂ then w₁ i else 0

Tactic:
simp only [mem_coe, left_eq_ite_iff]

Goal state after:
case mp.refine_2
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
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : ↑fs₁ ⊆ s₁
w₁ : ι → k
hw₁ : ∑ i ∈ fs₁, w₁ i = 1
fs₂ : Finset ι
hfs₂ : ↑fs₂ ⊆ s₂
w₂ : ι → k
hw₂ : ∑ i ∈ fs₂, w₂ i = 1
hw₁₂ : (affineCombination k fs₁ p) w₁ = (affineCombination k fs₂ p) w₂
ha : (↑fs₁).indicator w₁ = (↑fs₂).indicator w₂
i : ι
hi : i ∈ fs₁
⊢ i ∉ fs₂ → w₁ i = 0
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: 𝕜 : Type u_2
ι : Type u_1
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : ZeroLEOneClass 𝕜
i : ι
⊢ (fun x ↦ if i = x then 1 else 0) ∈ stdSimplex 𝕜 ι

Tactic:
by
  simpa only [@eq_comm _ i, ← Pi.single_apply] using single_mem_stdSimplex 𝕜 i

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
⊢ Metric.diam (stdSimplex ℝ ι) = 1

Tactic:
by
  refine le_antisymm diam_stdSimplex_le ?_
  obtain ⟨i, j, hij⟩ := exists_pair_ne ι
  classical
  rw [show (1 : ℝ) = dist (Pi.single i 1 : ι → ℝ) (Pi.single j 1) by
    simp [dist_single_single i j (1 : ℝ) 1 hij, Real.dist_eq]]
  exact Metric.dist_le_diam_of_mem (bounded_stdSimplex _)
    (single_mem_stdSimplex _ _) (single_mem_stdSimplex _ _)

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

Goal state before:
pp: case neg
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ a • x + b • y ∈ s

Tactic:
convert! h { x, y } (fun z => if z = y then b else a) _ _ _
    · simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial]
    · grind
    · simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial, hab]
    · intro i hi
      simp only [Finset.mem_singleton, Finset.mem_insert] at hi
      cases hi <;> subst i <;> assumption

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

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
⊢ LocallyPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen[inst✝] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x

Tactic:
rw [locallyPathConnectedSpace_iff_isOpen_pathComponentIn]
  simp_rw [forall_comm (β := Set X), ← imp_forall_iff]
  refine forall_congr' fun u ↦ imp_congr_right fun _ ↦ ?_
  exact ⟨fun h x hxu ↦ (h x).mem_nhds (mem_pathComponentIn_self hxu),
    fun h x ↦ isOpen_iff_mem_nhds.mpr fun y hy ↦
      pathComponentIn_congr hy ▸ h y <| pathComponentIn_subset hy⟩

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

Goal state before:
pp: case inr
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x

Tactic:
rw [nhdsWithin_union, eventually_sup]

Goal state after:
case inr
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
⊢ (∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x) ∧ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case refine_1.inr
ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
h : LocallyPathConnectedSpace ((i : ι) → Z i)
x : (i : ι) → Z i
this : ∀ (i : ι), Nonempty (Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htV : J.pi t ⊆ pathComponent x
i : ι
hi : i ∈ {i | ¬PathConnectedSpace (Z i)}
hiJ : i ∉ J
⊢ PathConnectedSpace (Z i)

Tactic:
suffices himg : eval i '' pathComponent x = univ from pathConnectedSpace_iff_univ.mpr
      (himg ▸ isPathConnected_pathComponent.image (continuous_apply i))

Goal state after:
case refine_1.inr
ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
h : LocallyPathConnectedSpace ((i : ι) → Z i)
x : (i : ι) → Z i
this : ∀ (i : ι), Nonempty (Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htV : J.pi t ⊆ pathComponent x
i : ι
hi : i ∈ {i | ¬PathConnectedSpace (Z i)}
hiJ : i ∉ J
⊢ eval i '' pathComponent x = univ
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: case coe
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
r : NNReal
⊢ Convex ℝ (eball a ↑r)

Tactic:
| coe r =>

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

Goal state before:
pp: case coe
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
r : NNReal
⊢ Convex ℝ (closedEBall a ↑r)

Tactic:
| coe r =>

Goal state after: