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

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
⊢ y ∈ ball x r

Tactic:
rcases (mem_closedBall.1 <| interior_subset hy).lt_or_eq with (hr | rfl)

Goal state after:
case inr.inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝¹ : r ≠ 0
hr✝ : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
hr : dist y x < r
⊢ y ∈ ball x r

case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
⊢ y ∈ ball x (dist y x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 6) = √3 / 2

Tactic:
show (6 : ℝ) = 3 * 2 by norm_num,

Goal state after:
⊢ cos (π / (3 * 2)) = √3 / 2
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n ↦ x ^ n
a✝ : Nontrivial R
this : 1 ≤ ‖1‖
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
have : 0 ≤ (1 - ‖x‖)⁻¹ := inv_nonneg.2 (by linarith)

Goal state after:
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n ↦ x ^ n
a✝ : Nontrivial R
this✝ : 1 ≤ ‖1‖
this : 0 ≤ (1 - ‖x‖)⁻¹
⊢ 0 ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case neg
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable fun n ↦ x ^ n
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
· simp only [tsum_eq_zero_of_not_summable hx, norm_zero]
    nontriviality R
    have : 1 ≤ ‖(1 : R)‖ := one_le_norm_one R
    have : 0 ≤ (1 - ‖x‖)⁻¹ := inv_nonneg.2 (by linarith)
    linarith

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
u : ℕ → α
n : ℕ
⊢ dist (∑ k ∈ Finset.range n, u k) (∑ k ∈ Finset.range (n + 1), u k) = ‖u n‖

Tactic:
simp [dist_eq_norm', sum_range_succ]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ (γ₁.trans γ₂).extend (1 - (1 - t)) = γ₂.extend (2 * t - 1)

Tactic:
rw [← extend_symm_apply, trans_symm, extend_trans_of_le_half _ _ (by linarith), extend_symm_apply]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ γ₂.extend (1 - 2 * (1 - t)) = γ₂.extend (2 * t - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: x : ℝ
n : ℤ
⊢ ↑(↑n * x) = n • ↑x

Tactic:
by
  simpa only [zsmul_eq_mul] using! coeHom.map_zsmul n x

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

Goal state before:
pp: case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ x + ↑n * (2 * ↑π * I) = 0

Tactic:
have : (x + n * (2 * π * I)).im ∈ Set.Ioc (-π) π := by simpa [two_mul, mul_add] using hn

Goal state after:
case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
this : (x + ↑n * (2 * ↑π * I)).im ∈ Ioc (-π) π
⊢ x + ↑n * (2 * ↑π * I) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
⊢ θ.cos = ψ.cos ↔ θ = ψ ∨ θ = -ψ

Tactic:
by
  induction ψ using Real.Angle.induction_on
  exact cos_eq_real_cos_iff_eq_or_eq_neg

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

Goal state before:
pp: θ : Angle
⊢ (↑(π / 2) - θ).sin = θ.cos

Tactic:
induction θ using Real.Angle.induction_on
  exact Real.sin_pi_div_two_sub _

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

Goal state before:
pp: θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.sin| = |ψ.sin|

Tactic:
simp_rw [two_zsmul, ← two_nsmul] at h

Goal state after:
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.sin| = |ψ.sin|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.cos| = |ψ.cos|

Tactic:
simp_rw [two_zsmul, ← two_nsmul] at h

Goal state after:
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.cos| = |ψ.cos|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ |θ.cos| = |ψ.sin|

Tactic:
simp_rw [two_zsmul, ← two_nsmul] at h

Goal state after:
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ |θ.cos| = |ψ.sin|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt arg x

Tactic:
have h₀ : ‖x‖ ≠ 0 := by
    rw [norm_ne_zero_iff]
    exact slitPlane_ne_zero h
  rw [mem_slitPlane_iff, ← lt_or_lt_iff_ne] at h
  rcases h with (hx_re | hx_im | hx_im)
  exacts [(Real.continuousAt_arcsin.comp
          (continuous_im.continuousAt.div continuous_norm.continuousAt h₀)).congr
      (arg_eq_nhds_of_re_pos hx_re).symm,
    (Real.continuous_arccos.continuousAt.comp
            (continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).neg.congr
      (arg_eq_nhds_of_im_neg hx_im).symm,
    (Real.continuous_arccos.continuousAt.comp
          (continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).congr
      (arg_eq_nhds_of_im_pos hx_im).symm]

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

Goal state before:
pp: θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ θ.tan = ψ.tan

Tactic:
simp_rw [two_zsmul, ← two_nsmul] at h

Goal state after:
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ θ.tan = ψ.tan
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ ψ.tan = θ.tan⁻¹

Tactic:
simp_rw [two_zsmul, ← two_nsmul] at h

Goal state after:
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ ψ.tan = θ.tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1

Tactic:
by
  rcases eq_or_ne θ π with rfl | h
  · simp
  · simp only [Set.mem_Ioo, ← sign_toReal h, sign_eq_one_iff, and_iff_left_iff_imp]
    exact fun _ ↦ (toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)

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

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x ↦ rexp (log b * x)) =o[atTop] fun _x ↦ 1

Tactic:
rw [isLittleO_const_iff one_ne_zero]
      refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
      rw [← log_neg_eq_log, log_neg_iff (by linarith)]
      linarith

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

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

Tactic:
have := toReal_add_of_sign_eq_neg_sign (.inr <| by simpa [neg_eq_iff_eq_neg]) hs.symm

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

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

Tactic:
grind [sign_eq_zero_iff, toReal_eq_zero_iff, toReal_neg_iff_sign_neg]

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

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

Tactic:
simp only [Real.rpow_def_of_nonneg hx, Complex.cpow_def, ofReal_eq_zero]; split_ifs <;>
    simp [Complex.ofReal_log hx]

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ InjOn (fun y ↦ y ^ x) {y | 0 ≤ y}

Tactic:
by
  rintro y hy z hz (hyz : y ^ x = z ^ x)
  rw [← rpow_one y, ← rpow_one z, ← mul_inv_cancel₀ hx, rpow_mul hy, rpow_mul hz, hyz]

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

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx : x < 1
hz : 0 < z
⊢ x ^ z < 1

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx le_top)
  simp only [coe_lt_one_iff] at hx
  simp [← coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.rpow_lt_one hx hz]

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

Goal state before:
pp: a : ℝ≥0
b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ b = a⁻¹ ^ (↑n / ↑d)

Tactic:
by
  rw [NNReal.inv_rpow, ← NNReal.rpow_neg, hb.neg_to_eq rfl rfl]

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

Goal state before:
pp: case mpr
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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
⊢ p ∈ s₂ → p ∈ s₁

Tactic:
intro hp
    rw [← vsub_vadd p hn.some]
    refine vadd_mem_of_mem_direction ?_ hq1
    rw [hd]
    exact vsub_mem_direction hp hq2

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • balancedHull 𝕜 s ⊆ balancedHull 𝕜 s

Tactic:
simp_rw [balancedHull, smul_set_iUnion₂, subset_def, mem_iUnion₂]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ ∀ (x : E), (∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ a • i • s) → ∃ i, ∃ (_ : ‖i‖ ≤ 1), x ∈ i • s
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 𝕜 (insert 0 (interior A))

Tactic:
exact hA.zero_insert_interior

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a : Set E
ha : IsVonNBounded 𝕜 a
V : Set E
⊢ V ∈ 𝓝 0 → Absorbs 𝕜 V (closure[inst✝³] a)

Tactic:
hV

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a : Set E
ha : IsVonNBounded 𝕜 a
V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V (closure[inst✝³] a)
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
V : Set E
⊢ V ∈ 𝓝 0 → Absorbs 𝕜 V s

Tactic:
hV

Goal state after:
𝕜 : 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
V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V s
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
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ (((Finset.subtype pred s).weightedVSubOfPoint (fun i ↦ p ↑i) b) fun i ↦ w ↑i) =
    ({x ∈ s | pred x}.weightedVSubOfPoint p b) w

Tactic:
by
  rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_subtype_eq_sum_filter]

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

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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : r • (p₂ -ᵥ p₁) + v₂ = p -ᵥ p₁
⊢ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
use r, v₂ +ᵥ p₁, vadd_mem_of_mem_direction hv₂ hp₁

Goal state after:
case right
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
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : r • (p₂ -ᵥ p₁) + v₂ = p -ᵥ p₁
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ 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 ι
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.le
  rw [finset_sup_apply, NNReal.coe_lt_coe, Finset.sup_lt_iff]
  · exact h
  · exact NNReal.coe_pos.mpr ha

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
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
hs : p1 -ᵥ p i0 = (s.weightedVSub p) w
s' : Finset ι := insert i0 s
w' : ι → k := (↑s).indicator w
⊢ ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w

Tactic:
have h' : ∑ i ∈ s', w' i = 0 := by
      rw [← h, Finset.sum_indicator_subset _ (Finset.subset_insert i0 s)]

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
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
hs : p1 -ᵥ p i0 = (s.weightedVSub p) w
s' : Finset ι := insert i0 s
w' : ι → k := (↑s).indicator w
h' : ∑ i ∈ s', w' i = 0
⊢ ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w
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✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
i j : ι
h : i ≠ j
⊢ 1 - (b.basisOf i).sumCoords (b j -ᵥ b i) = 0

Tactic:
← Subtype.coe_mk (p := (· ≠ i)) j h.symm,

Goal state after:
ι : Type u_1
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
i j : ι
h : i ≠ j
⊢ 1 - (b.basisOf i).sumCoords (b ↑⟨j, ⋯⟩ -ᵥ b i) = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: case intro
ι : Type u_1
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
inst✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂
val✝ : Fintype ι
⊢ q₁ = q₂

Tactic:
rw [← b.affineCombination_coord_eq_self q₁, ← b.affineCombination_coord_eq_self q₂]

Goal state after:
case intro
ι : Type u_1
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
inst✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂
val✝ : Fintype ι
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) q₁) =
    (Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) q₂
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_2.inl
k : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
i : Fin (n + 1)
h : w i = 0
hk : Subsingleton k
⊢ (affineCombination k univ s.points) w ∈ affineSpan k (s.points '' {i}ᶜ)

Tactic:
have : Subsingleton V := Module.subsingleton k _

Goal state after:
case refine_2.inl
k : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
i : Fin (n + 1)
h : w i = 0
hk : Subsingleton k
this : Subsingleton V
⊢ (affineCombination k univ s.points) w ∈ affineSpan k (s.points '' {i}ᶜ)
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
⊢ Continuous (stdSimplexEquivIcc ℝ).invFun

Tactic:
apply Continuous.subtype_mk

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
⊢ Continuous fun x ↦ ![1 - ↑x, ↑x]
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case h₂
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
inst✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
⊢ s.interior ∪ ⋃ i, (s.faceOpposite i).closedInterior ⊆ s.closedInterior

Tactic:
refine Set.union_subset s.interior_subset_closedInterior (Set.iUnion_subset fun i ↦ ?_)
    exact s.closedInterior_faceOpposite_subset_closedInterior i

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ nhdsKer s ⊆ nhdsKer t ↔ 𝓝ˢ s ≤ 𝓝ˢ t

Tactic:
simp +contextual only [subset_nhdsKer_iff, (hasBasis_nhdsSet _).ge_iff,
    and_imp, IsOpen.mem_nhdsSet, IsOpen.nhdsKer_subset]

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

Goal state before:
pp: case neg
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ∃ c, (lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∉ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
by_cases hy' : y ∈ interior s

Goal state after:
case pos
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ∃ c, (lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∉ interior s
hy' : y ∈ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

case neg
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ∃ c, (lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∉ interior s
hy' : y ∉ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
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
| 𝓝[s \ {a}] a

Tactic:
rw [sdiff_eq, ← Iio_union_Ioi, inter_union_distrib_left]

Goal state after:
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
| 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a
Module: Mathlib.Analysis.Convex.Jensen

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj✝ : j ∈ t
k : ι
hk✝ : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι
hj : j ∉ u
hk : k ∉ u
ht : t = cons j (cons k u hk) ⋯
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)

Tactic:
subst ht

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this : k ∈ (cons j (cons k u hk✝) ⋯).erase j
⊢ f (∑ i ∈ cons j (cons k u hk✝) ⋯, w i • p i) < ∑ i ∈ cons j (cons k u hk✝) ⋯, w i • f (p i)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
x : E
w : E → R
hw : ∑ y ∈ s, w y = 1
⊢ s.centerMass w id = x ↔ ∑ y ∈ s, w y • y = x

Tactic:
centerMass_eq_of_sum_1 _ _ hw,

Goal state after:
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
x : E
w : E → R
hw : ∑ y ∈ s, w y = 1
⊢ ∑ i ∈ s, w i • id i = x ↔ ∑ y ∈ s, w y • y = x
Module: Mathlib.Analysis.Convex.Jensen

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i

Tactic:
by
  refine ⟨?_, fun h ↦ ?_⟩
  · obtain rfl | ⟨i₀, hi₀⟩ := t.eq_empty_or_nonempty
    · simp
    intro h_eq i hi
    have H (j) (hj : j ∈ t) : p j = p i₀ := hf.eq_of_le_map_sum h₀ h₁ hmem h_eq.ge hj hi₀
    calc p i = p i₀ := by rw [H _ hi]
      _ = (1 : 𝕜) • p i₀ := by simp
      _ = (∑ j ∈ t, w j) • p i₀ := by rw [h₁]
      _ = ∑ j ∈ t, (w j • p i₀) := by rw [sum_smul]
      _ = ∑ j ∈ t, (w j • p j) := by congr! 2 with j hj; rw [← H _ hj]
  · grind [hf.map_sum_eq_iff_of_pos h₀ h₁ hmem]

Goal state after: