mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = -↑(π / 2 - ψ)
⊢ ↑θ + ↑ψ = ↑π

Tactic:
rw [coe_sub, coe_sub, eq_neg_iff_add_eq_zero, add_sub, sub_add_eq_add_sub, ← coe_add,
      add_halves, sub_sub, sub_eq_zero] at h

Goal state after:
case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑π = ↑θ + ↑ψ
⊢ ↑θ + ↑ψ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ -(π / 2) < z.arg ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
lt_iff_le_and_ne,

Goal state after:
z : ℂ
⊢ -(π / 2) ≤ z.arg ∧ -(π / 2) ≠ z.arg ↔ 0 < z.re ∨ 0 ≤ z.im
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
lt_iff_le_and_ne,

Goal state after:
z : ℂ
⊢ z.arg ≤ π / 2 ∧ z.arg ≠ π / 2 ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ toIocMod two_pi_pos (-π) θ.toReal = θ.toReal

Tactic:
by
  induction θ using Real.Angle.induction_on
  rw [toReal_coe]
  exact toIocMod_toIocMod _ _ _ _

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

Goal state before:
pp: θ : Angle
h : θ ≠ ↑π
⊢ θ.toReal ≠ π

Tactic:
simp [h]

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

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

Tactic:
lt_iff_le_and_ne,

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

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

Tactic:
lt_iff_le_and_ne,

Goal state after:
θ : Angle
⊢ 0 ≤ θ.cos ∧ 0 ≠ θ.cos ↔ |θ.toReal| ≤ π / 2 ∧ |θ.toReal| ≠ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
this : ContinuousAt (Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)

Tactic:
rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this

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

Goal state before:
pp: case inr.«0»
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
hk : θ.toReal + ψ.toReal = 2 * π * ↑((Nat.castEmbedding.trans (addLeftEmbedding (-1))) 0) + π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

Tactic:
simp at hk

Goal state after:
case inr.«0»
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
hk : θ.toReal + ψ.toReal = -(2 * π) + π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.«1»
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
hk : θ.toReal + ψ.toReal = 2 * π * ↑((Nat.castEmbedding.trans (addLeftEmbedding (-1))) 1) + π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

Tactic:
simp at hk

Goal state after:
case inr.«1»
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
hk : θ.toReal + ψ.toReal = π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
obtain ⟨hθ', hψ'⟩ : (-θ).sign = 1 ∧ (-ψ).sign = 1 := by grind [sign_neg, neg_neg]
    have hsa' : (-θ + -ψ).sign ≠ 1 := by
      rwa [← hθ', ne_comm, ← neg_add, sign_neg, sign_neg, neg_injective.ne_iff]
    convert! abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux hθ' hψ' hsa' using 1
    all_goals simp [-neg_add_rev, ← neg_add, abs_toReal_neg]

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

Goal state before:
pp: case neg
z w : ℂ
h : z = 0 ∧ w.re = 0 ∧ w ≠ 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
simp [h]

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

Goal state before:
pp: x : ℝ
⊢ x ^ (-1) = x⁻¹

Tactic:
rw [rpow_neg_eq_inv_rpow, rpow_one]

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

Goal state before:
pp: case pos
y : ℝ
h : y = 0
⊢ 0 ^ y = 1

Tactic:
simp [h]

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

Goal state before:
pp: case neg
y : ℝ
h : ¬y = 0
⊢ 0 ^ y = 0

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

Goal state before:
pp: z w : ℂ
h₁ : ¬(z, w).1 < 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (z, w)

Tactic:
lt_iff_le_and_ne,

Goal state after:
z w : ℂ
h₁ : ¬((z, w).1 ≤ 0 ∧ (z, w).1 ≠ 0)
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (z, w)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
simp [h]

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

Goal state before:
pp: y z : ℝ
x : ℝ≥0
hx : ↑x ≠ 0
h'x : ↑x ≠ ∞
h : x = 0
⊢ False

Tactic:
by simp [h] at hx

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

Goal state before:
pp: case refine_1
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p ↦ p.1 ^ p.2) = toNNReal ∘ (fun p ↦ p.1 ^ p.2) ∘ fun p ↦ (↑p.1, p.2)
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (↑(x, y).1, (x, y).2)

pp: case refine_2
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p ↦ p.1 ^ p.2) = toNNReal ∘ (fun p ↦ p.1 ^ p.2) ∘ fun p ↦ (↑p.1, p.2)
⊢ ContinuousAt (fun p ↦ (↑p.1, p.2)) (x, y)

Tactic:
· apply Real.continuousAt_rpow
    simpa using h

Goal state after:
case refine_2
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p ↦ p.1 ^ p.2) = toNNReal ∘ (fun p ↦ p.1 ^ p.2) ∘ fun p ↦ (↑p.1, p.2)
⊢ ContinuousAt (fun p ↦ (↑p.1, p.2)) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ x ^ y ≠ 0

Tactic:
simp [h]

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

Goal state before:
pp: y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ x ^ y ≠ 0

Tactic:
simp [h]

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

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ∞
⊢ ∞ ^ y = ∞

Tactic:
simp [h]

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

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
h : 0 < y
⊢ ContinuousAt (fun a ↦ a ^ y) x

Tactic:
by_cases hx : x = ⊤
  · rw [hx, ContinuousAt]
    convert! ENNReal.tendsto_rpow_at_top h
    simp [h]
  lift x to ℝ≥0 using hx
  rw [continuousAt_coe_iff]
  convert! continuous_coe.continuousAt.comp (NNReal.continuousAt_rpow_const (Or.inr h.le)) using 1
  ext1 x
  simp [← coe_rpow_of_nonneg _ h.le]

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

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

Tactic:
by
  cases x
  · simp [top_rpow_of_pos hz]
  · simp only [one_lt_coe_iff] at hx
    simp [← coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.one_lt_rpow hx hz]

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

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

Tactic:
by
  lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx2 le_top)
  simp only [coe_lt_one_iff, coe_pos] at hx1 hx2 ⊢
  simp [← coe_rpow_of_ne_zero (ne_of_gt hx1), NNReal.one_lt_rpow_of_pos_of_lt_one_of_neg hx1 hx2 hz]

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ ‖x ^ y‖ₑ = ‖x‖ₑ ^ y

Tactic:
by simp [enorm, nnnorm_rpow_of_nonneg hx, coe_rpow_of_nonneg _ hy]

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

Goal state before:
pp: b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ (↑r ^ d) ^ (↑d)⁻¹ = ↑r

pp: case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑m

Tactic:
Real.pow_rpow_inv_natCast

Goal state after:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑r = ↑r

case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑r

case hn
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ d ≠ 0

case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑m
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
p1 p2 : P1
⊢ f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2

Tactic:
by
  conv_rhs => rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]

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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 • x + b • y ∈ s

Tactic:
rwa [hab, zero_smul, one_smul, zero_add]

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

Goal state before:
pp: case inr.inr
𝕜 : 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
hca : c < a
hc : 0 < 1 - c
⊢ (lineMap x y) a ∈ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1

Tactic:
simp only [← lineMap_apply_one_sub y]

Goal state after:
case inr.inr
𝕜 : 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
hca : c < a
hc : 0 < 1 - c
⊢ (lineMap y x) (1 - a) ∈ (fun a ↦ (lineMap y ((lineMap y x) (1 - c))) (1 - a)) '' Ioo 0 1
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : y ≤ x
⊢ Icc y x = Icc (min x y) (max x y)

Tactic:
max_eq_left h,

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : y ≤ x
⊢ Icc y x = Icc (min x y) x
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ x + t • y ∈ s

Tactic:
have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> noncomm_ring

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ 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
v : V
p : P
direction : Submodule k V
hv : v ∈ direction
⊢ v +ᵥ p ∈ mk' p direction

Tactic:
by
  simpa

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

Goal state before:
pp: case a
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
p₁ p₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ p₁ -ᵥ p₃ ∈ vectorSpan k s

Tactic:
rw [hp₁, hp₃, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc]

Goal state after:
case a
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
p₁ p₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ v₁ + (p₂ -ᵥ p₄) - v₂ ∈ vectorSpan k s
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
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
hd : s.direction = ⊤.direction
⊢ (↑s ∩ ↑⊤).Nonempty

Tactic:
simp [h]

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✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Goal state after:
case 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
t : Set E
⊢ IsVonNBounded 𝕜 (∅ + t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 ∅ ∧ IsVonNBounded 𝕜 t

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
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✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
⊢ IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Goal state after:
case 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
⊢ IsVonNBounded 𝕜 (∅ + ∅) ↔ IsVonNBounded 𝕜 ∅

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 : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s
Module: Mathlib.Topology.MetricSpace.Equicontinuity

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
intro U hU
    rcases mem_uniformity_dist.mp hU with ⟨ε, hε, hεU⟩
    refine Exists.imp (fun V => And.imp_right fun h => ?_) (H _ hε)
    exact fun x hx x' hx' i => hεU (h _ hx _ hx' i)

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

Goal state before:
pp: case e_f.inl
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 ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
i : ι
h : i = j
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case e'_3
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✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
r : 𝕜
x : E
smul_le : f (r⁻¹ • r • x) ≤ ‖r‖⁻¹ * f (r • x)
h : ¬r = 0
⊢ x = r⁻¹ • r • x

Tactic:
simp [h]

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 ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
v : V
⊢ (s.weightedVSub (v +ᵥ p)) w = (s.weightedVSub p) w

Tactic:
by
  rw [weightedVSub, weightedVSubOfPoint_vadd,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]

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

Goal state before:
pp: case pos
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
i2 : ι
hi2 : i2 ∈ s
h : i2 = i
⊢ w i2 • (p i2 -ᵥ p i) = 0

Tactic:
simp [h]

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
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
⊢ ((map e s₂).weightedVSubOfPoint p (Classical.choice ⋯)) w +ᵥ Classical.choice ⋯ =
    (s₂.weightedVSubOfPoint (p ∘ ⇑e) (Classical.choice ⋯)) (w ∘ ⇑e) +ᵥ Classical.choice ⋯

Tactic:
weightedVSubOfPoint_map

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

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

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Goal state after:
case 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
t : Set Q
⊢ affineSpan k (∅ ×ˢ t) = (affineSpan k ∅).prod (affineSpan k t)

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

Goal state before:
pp: k : Type u_1
inst✝ : DivisionRing k
ι : Type u_4
s : Finset ι
h : ↑(#s) ≠ 0
⊢ ∑ i ∈ s, centroidWeights k s i = 1

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
this : Nonempty ↑s
⊢ ⨆ i, ↑i x ≤ p x

Tactic:
· exact ciSup_le fun q => hp q.2 x

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

Goal state before:
pp: case pos
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
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : i₁ = i₂
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x : E
⊢ (c • p).ball x r = p.ball x (r / ↑c)

Tactic:
ext
  rw [mem_ball, mem_ball, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    lt_div_iff₀ (NNReal.coe_pos.mpr hc)]

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

pp: case mp.inr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
⊢ v ∈ vectorSpan k (Set.range p) → ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w

Tactic:
swap

Goal state after:
case mp.inr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
⊢ v ∈ vectorSpan k (Set.range p) → ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w

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
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x₁ x₂ y : E
r : ℝ
⊢ p (x₁ - x₂ - y) < r ↔ p (x₁ - (x₂ + y)) < r

Tactic:
sub_sub

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

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

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x₁ x₂ y : E
r : ℝ
⊢ p (x₁ - x₂ - y) ≤ r ↔ p (x₁ - (x₂ + y)) ≤ r

Tactic:
sub_sub

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun x ↦ a • x) y = x
⊢ x ∈ p.ball 0 r

Tactic:
mem_ball_zero,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun x ↦ a • x) y = x
⊢ p x < r
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:
lift r to NNReal using hr

Goal state after:
𝕜 : 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 : ℝ≥0
⊢ (s.sup p).closedBall x ↑r = ⋂ i ∈ s, (p i).closedBall x ↑r
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: case inl
ι : 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✝ : DecidableEq ι
i j : ι
h : i = j
⊢ (b.coord i) (b j) = if i = j then 1 else 0

Tactic:
simp [h]

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

Goal state before:
pp: case inr
ι : 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✝ : DecidableEq ι
i j : ι
h : i ≠ j
⊢ (b.coord i) (b j) = if i = j then 1 else 0

Tactic:
simp [h]

Goal state after: