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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
dP : P.natDegree = k
A : (n + k).descFactorial k = Polynomial.eval n P
⊢ Polynomial.eval n (X ^ k + ∑ i ∈ Finset.range k, C (P.coeff i) * X ^ i) =
    n ^ k + ∑ i ∈ Finset.range k, (fun i ↦ P.coeff i) i * n ^ i

Tactic:
simp [eval_finsetSum]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U✝ : ι → Set Y
h : (𝓝 c).HasBasis p U✝
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
K : Set X
U : Set Y
hKU : (K, U) ∈ S
x : X
hx : x ∈ K
⊢ U ∈ 𝓝 c

Tactic:
exact (hSopen K U hKU).mem_nhds <| hSmaps K U hKU hx

Goal state after:
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
⊢ ∀ (x : X × C(Y, Z)) (K : Set Y),
    IsCompact K →
      ∀ (U : Set (X × Z)),
        IsOpen[instTopologicalSpaceProd] U →
          MapsTo (⇑((const Y x.1).prodMk x.2)) K U →
            ∀ᶠ (a : X × C(Y, Z)) in 𝓝 x, MapsTo (⇑((const Y a.1).prodMk a.2)) K U

Tactic:
rintro ⟨r, f⟩ K hK U hU H

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
r : X
f : C(Y, Z)
K : Set Y
hK : IsCompact K
U : Set (X × Z)
hU : IsOpen[instTopologicalSpaceProd] U
H : MapsTo (⇑((const Y (r, f).1).prodMk (r, f).2)) K U
⊢ ∀ᶠ (a : X × C(Y, Z)) in 𝓝 (r, f), MapsTo (⇑((const Y a.1).prodMk a.2)) K U
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: n : ℕ
⊢ ‖∑ i ∈ Finset.range n, (-1) ^ i‖ ≤ 1

Tactic:
rw [neg_one_geom_sum]

Goal state after:
n : ℕ
⊢ ‖if Even n then 0 else 1‖ ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∉ Icc (-(π / 2)) (π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
rw [Set.mem_Icc, not_and_or, not_le, not_le] at h₁
    rcases h₁ with h₁ | h₁
    · replace hθ := hθ.1
      have hcos : Real.cos θ < 0 := by
        rw [← neg_pos, ← Real.cos_add_pi]
        refine Real.cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith
      have hsin : Real.sin θ < 0 := Real.sin_neg_of_neg_of_neg_pi_lt (by linarith) hθ
      rw [if_neg, if_neg, ← Real.sin_add_pi, Real.arcsin_sin, add_sub_cancel_right] <;> [linarith;
        linarith; exact hsin.not_ge; exact hcos.not_ge]
    · replace hθ := hθ.2
      have hcos : Real.cos θ < 0 := Real.cos_neg_of_pi_div_two_lt_of_lt h₁ (by linarith)
      have hsin : 0 ≤ Real.sin θ := Real.sin_nonneg_of_mem_Icc ⟨by linarith, hθ⟩
      rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith;
        linarith; exact hsin; exact hcos.not_ge]

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

Goal state before:
pp: case pos
x : ℝ
h_zero : x = 0
⊢ x ≤ rexp (log x)

pp: case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ rexp (log x)

Tactic:
· rw [h_zero, log, dif_pos rfl, exp_zero]
    exact zero_le_one

Goal state after:
case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ rexp (log x)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
⊢ log (-x) = log x

Tactic:
rw [← log_abs x, ← log_abs (-x), abs_neg]

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

Goal state before:
pp: z : ℂ
hz : z.im < 0
⊢ z.arg = -Real.arccos (z.re / ‖z‖)

Tactic:
have h₀ : z ≠ 0 := mt (congr_arg im) hz.ne

Goal state after:
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ z.arg = -Real.arccos (z.re / ‖z‖)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case neg
x : ℂ
hx : ¬x.arg = π
⊢ ↑(Real.log ‖x‖) + -↑x.arg * I = ↑(Real.log ‖x‖) + ↑x.arg * (starRingEnd ℂ) I

Tactic:
conj_I,

Goal state after:
case neg
x : ℂ
hx : ¬x.arg = π
⊢ ↑(Real.log ‖x‖) + -↑x.arg * I = ↑(Real.log ‖x‖) + ↑x.arg * -I
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + ↑x.arg * (starRingEnd ℂ) I) -
      ↑(Real.log (normSq x)) =
    if x.arg = π then -(↑(Real.log ‖x‖) + ↑x.arg * (starRingEnd ℂ) I) else -(↑(Real.log ‖x‖) + ↑x.arg * I)

Tactic:
conj_I,

Goal state after:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + ↑x.arg * -I) - ↑(Real.log (normSq x)) =
    if x.arg = π then -(↑(Real.log ‖x‖) + ↑x.arg * -I) else -(↑(Real.log ‖x‖) + ↑x.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case neg.hr
x : ℂ
hx : ¬x = 0
⊢ 0 < (normSq x)⁻¹

Tactic:
rwa [inv_pos, Complex.normSq_pos]

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

Goal state before:
pp: z : ℂ
h : z ∈ slitPlane
⊢ log z ∈ {z | z.im ∈ Ioo (-π) π}

Tactic:
simp only [mem_ofPred, log_im, mem_Ioo, neg_pi_lt_arg, arg_lt_pi_iff, true_and]

Goal state after:
z : ℂ
h : z ∈ slitPlane
⊢ 0 ≤ z.re ∨ z.im ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
⊢ (↑r * (cos ↑θ + sin ↑θ * I)).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
rw [arg_mul_cos_add_sin_mul_I_eq_toIocMod hr, toIocMod_sub_self, toIocDiv_eq_neg_floor,
    zsmul_eq_mul]

Goal state after:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(- -⌊(-π + 2 * π - θ) / (2 * π)⌋) * (2 * π) = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ Real.cos θ.toReal = θ.cos

Tactic:
by
  conv_rhs => rw [← coe_toReal θ, cos_coe]

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

Goal state before:
pp: θ : Angle
⊢ 0 < θ.cos ↔ |θ.toReal| < π / 2

Tactic:
rw [lt_iff_le_and_ne, lt_iff_le_and_ne, cos_nonneg_iff_abs_toReal_le_pi_div_two, ←
    and_congr_right]

Goal state after:
θ : Angle
⊢ |θ.toReal| ≤ π / 2 → (|θ.toReal| ≠ π / 2 ↔ 0 ≠ θ.cos)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (2 • θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|

Tactic:
rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_neg_sign_iff]

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

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x ↦ |(g x).im|) l, (fun x1 x2 ↦ x1 ≤ x2) x b
⊢ (fun x ↦ rexp ((f x).arg * (g x).im)) =Θ[l] fun x ↦ 1

Tactic:
refine Real.isTheta_exp_comp_one.2 ⟨π * b, ?_⟩

Goal state after:
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x ↦ |(g x).im|) l, (fun x1 x2 ↦ x1 ≤ x2) x b
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun x ↦ |(f x).arg * (g x).im|) l, (fun x1 x2 ↦ x1 ≤ x2) x (π * b)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn

Goal state after:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ n) ^ (↑n)⁻¹ = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn

Goal state after:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
rpow_mul hx,

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℕ
z : ℝ
⊢ (x ^ ↑n) ^ z = (x ^ n) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
rpow_mul hx,

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
⊢ (x ^ y) ^ ↑n = (x ^ y) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℤ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
rpow_mul hx,

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℤ
z : ℝ
⊢ (x ^ ↑n) ^ z = (x ^ n) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
rpow_mul hx,

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

Goal state before:
pp: x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ rexp (log x * y) ≤ rexp (log x * z)

Tactic:
rw [exp_le_exp]

Goal state after:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ log x * y ≤ log x * z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ rexp (log x * y) ≤ rexp (log x * z)

Tactic:
rw [exp_le_exp]

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ log x * y ≤ log x * z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
have : x ^ y ≠ 0 := by simp [h]

Goal state after:
case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
this : x ^ y ≠ 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : 1 ≤ 1 / 2
⊢ False

Tactic:
norm_num at this

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

Goal state before:
pp: p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ 2 ^ p * max (a ^ p) (b ^ p) ≤ 2 ^ p * (a ^ p + b ^ p)

Tactic:
by gcongr; apply max_le_add_of_nonneg <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : SameRay R x (-x)
⊢ SameRay R x (-1 • x)

Tactic:
rwa [neg_one_smul]

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
inst✝¹ : IsDomain k
inst✝ : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ (c₁ - c₂) • (p₁ -ᵥ p₀) = 0 ↔ p₀ = p₁ ∨ c₁ = c₂

Tactic:
smul_eq_zero,

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
inst✝¹ : IsDomain k
inst✝ : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ c₁ - c₂ = 0 ∨ p₁ -ᵥ p₀ = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
⊢ ⇑f = ⇑f.linear + fun x ↦ f 0

Tactic:
by
  ext x
  calc
    f x = f.linear x +ᵥ f 0 := by rw [← f.map_vadd, vadd_eq_add, add_zero]
    _ = (f.linear + fun _ : V1 => f 0) x := rfl

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
⊢ x ∈ openSegment 𝕜 x y → x = y

Tactic:
rintro ⟨a, b, _, hb, hab, hx⟩
    refine smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 ?_)
    rw [hx, ← add_smul, hab, one_smul]

Goal state after:
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
⊢ (convexHull 𝕜) s = ∅ ↔ s = ∅

Tactic:
by
  constructor
  · intro h
    rw [← Set.subset_empty_iff, ← h]
    exact subset_convexHull 𝕜 _
  · rintro rfl
    exact convexHull_empty

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hsx : Convex 𝕜 (s \ {x})
hx : x ∈ (convexHull 𝕜) (s \ {x})
⊢ False

Tactic:
rw [hsx.convexHull_eq] at hx

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hsx : Convex 𝕜 (s \ {x})
hx : x ∈ s \ {x}
⊢ False
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ Convex 𝕜 (s \ {x}) → x ∉ (convexHull 𝕜) (s \ {x})

pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ x ∉ (convexHull 𝕜) (s \ {x}) → Convex 𝕜 (s \ {x})

Tactic:
· rintro hsx hx
    rw [hsx.convexHull_eq] at hx
    exact hx.2 (mem_singleton _)

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ x ∉ (convexHull 𝕜) (s \ {x}) → Convex 𝕜 (s \ {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
hs : Convex 𝕜 s
x : E
hx : x ∉ (convexHull 𝕜) (s \ {x})
h : s \ {x} = (convexHull 𝕜) (s \ {x})
⊢ Convex 𝕜 (s \ {x})

Tactic:
rw [h]
    exact convex_convexHull 𝕜 _

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
S : AffineSpace V P
Q : AffineSubspace k P
⊢ Q = ⊥ ∨ (↑Q).Nonempty

Tactic:
by
  rw [nonempty_iff_ne_bot]
  apply eq_or_ne

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
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
⊢ p ∈ iInf s ↔ ∀ (i : ι), p ∈ s i

Tactic:
by
  rw [iInf, mem_sInf_iff, Set.forall_mem_range]

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

Goal state before:
pp: case right
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₁ s₂ : AffineSubspace k P
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
⊢ v₁ +ᵥ p₁ ∈ ↑s₂

Tactic:
hv₁v₂

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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
⊢ -v₂ +ᵥ p₂ ∈ ↑s₂
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
inst✝ : Subsingleton P
⊢ affineSpan k s = ⊤ ↔ s.Nonempty

Tactic:
← bot_lt_affineSpan k,

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 : Set P
inst✝ : Subsingleton P
⊢ affineSpan k s = ⊤ ↔ ⊥ < affineSpan k s
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hxz : f x ≤ f z
⊢ f z ≤ f y

Tactic:
by
  obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
  exact hf.le_right_of_left_le' hx hy ha.le hb hab hxz

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
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ ∑ i ∈ s₁, w i • (p i -ᵥ b) = ∑ i ∈ s₂, (↑s₁).indicator w i • (p i -ᵥ b)

Tactic:
exact Eq.symm <|
    sum_indicator_subset_of_eq_zero w (fun i wi => wi • (p i -ᵥ b : V)) h fun i => zero_smul k _

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
⊢ BddAbove (range p) ↔ ∀ (x : E), BddAbove (range fun i ↦ (p i) x)

Tactic:
rw [Seminorm.bddAbove_iff, ← range_comp, bddAbove_range_pi]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
⊢ (∀ (a : E), BddAbove (range fun i ↦ (DFunLike.coe ∘ p) i a)) ↔ ∀ (x : E), BddAbove (range fun i ↦ (p i) x)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
⊢ Absorbent 𝕜 (p.ball x r)

Tactic:
by
  refine (p.absorbent_ball_zero <| sub_pos.2 hpr).mono fun y hy => ?_
  rw [p.mem_ball_zero] at hy
  exact p.mem_ball.2 ((map_sub_le_add p _ _).trans_lt <| add_lt_of_lt_sub_right hy)

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✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Nontrivial ι
i : ι
⊢ Function.Surjective ⇑(b.coord i)

Tactic:
by
  classical
    intro x
    obtain ⟨j, hij⟩ := exists_ne i
    let s : Finset ι := {i, j}
    have hi : i ∈ s := by simp [s]
    let w : ι → k := fun j' => if j' = i then x else 1 - x
    have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]
    use s.affineCombination k b w
    simp [w, b.coord_apply_combination_of_mem hi hw]

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
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓤 E = ⨅ r, ⨅ (_ : r > 0), 𝓟 {x | p (x.1 - x.2) < r}

Tactic:
rw [uniformSpace_eq_of_hasBasis p hb h₁ h₂]
  simp only [sub_eq_add_neg, ← map_neg_add p]
  rfl

Goal state after:
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₂
⊢ (affineCombination k fs₁ p) w₁ = (affineCombination k (fs₁ ∩ fs₂) p) w₁

Tactic:
rw [affineCombination_indicator_subset w₁ p Finset.inter_subset_left]
      refine affineCombination_congr (k := k) (P := P) _ ?_ (fun _ _ ↦ rfl)
      intro i hi
      rw [coe_inter, ← Set.indicator_indicator, Set.indicator_of_mem (by simpa using hi),
        Set.indicator_apply]
      simp only [mem_coe, left_eq_ite_iff]
      intro hi₂
      rw [← Set.indicator_of_mem (s := ↑fs₁) (by simpa using hi) w₁, ha]
      simp [hi₂]

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : IsOrderedRing 𝕜
⊢ stdSimplex 𝕜 (Fin 2) = [Pi.single 0 1 -[𝕜] Pi.single 1 1]

Tactic:
refine Subset.antisymm ?_ (segment_single_subset_stdSimplex 𝕜 (0 : Fin 2) 1)

Goal state after:
𝕜 : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : IsOrderedRing 𝕜
⊢ stdSimplex 𝕜 (Fin 2) ⊆ [Pi.single 0 1 -[𝕜] Pi.single 1 1]
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : ¬s₁.Subsingleton
⊢ vectorSpan k (p '' s₁) ≠ vectorSpan k (p '' s₂)

Tactic:
classical
  rw [Set.not_subsingleton_iff] at h₁
  obtain ⟨j, hj, hne⟩ := h₁.exists_ne i
  intro he
  have hs : p i -ᵥ p j ∈ vectorSpan k (p '' s₁) :=
    vsub_mem_vectorSpan k (Set.mem_image_of_mem _ his₁) (Set.mem_image_of_mem _ hj)
  rw [he, Set.image_eq_range, mem_vectorSpan_iff_eq_weightedVSub] at hs
  obtain ⟨fs, w, hw, hs⟩ := hs
  let w' : ι → k := Function.extend Subtype.val w 0
  have hw' : ∑ t ∈ fs.map (Embedding.subtype _), w' t = 0 := by
    simp only [sum_map, Embedding.subtype_apply, ← hw]
    exact sum_congr rfl fun t ht ↦ by simp [w']
  have hs' : p i -ᵥ p j = (fs.map (Embedding.subtype _)).weightedVSub p w' := by
    rw [hs, weightedVSub_map]
    simp [w', Function.comp_def]
  let fs' : Finset ι := insert i (insert j (fs.map (Embedding.subtype _)))
  have hfsfs' : fs.map (Embedding.subtype _) ⊆ fs' := by grind
  let w'' : ι → k := Set.indicator (fs.map (Embedding.subtype _)) w'
  have hs'' : p i -ᵥ p j = fs'.weightedVSub p w'' := by
    rw [hs']
    exact weightedVSubOfPoint_indicator_subset _ _ _ (by grind)
  have hw'' : ∑ t ∈ fs', w'' t = 0 := by
    rw [← hw']
    exact sum_indicator_subset _ (by grind)
  let w''' : ι → k := w'' - weightedVSubVSubWeights k i j
  have hi : i ∈ fs' := by grind
  have hj : j ∈ fs' := by grind
  have hw''' : ∑ t ∈ fs', w''' t = 0 := by
    simp [w''', sum_sub_distrib, hw'', hi, hj]
  have hs''' : fs'.weightedVSub p w''' = 0 := by
    simp [w''', ← hs'', hi, hj]
  have h0 := ha fs' w''' hw''' hs''' i hi
  simp [w''', w'', Pi.sub_apply, hne.symm, his₂] at h0

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

Goal state before:
pp: case neg.ha
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
⊢ p ∉ Simplex.setInterior I (s.map f hf)

pp: case neg.hb
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
⊢ ¬∃ x ∈ Simplex.setInterior I s, f x = p

Tactic:
· exact fun h ↦ hp (Set.mem_of_mem_of_subset h (s.map f hf).setInterior_subset_affineSpan)

Goal state after:
case neg.hb
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
⊢ ¬∃ x ∈ Simplex.setInterior I s, f x = p