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

Goal state before:
pp: z : ℂ
hz : 0 < z.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (0, z)

Tactic:
by
  have hz₀ : z ≠ 0 := ne_of_apply_ne re hz.ne'
  rw [ContinuousAt, zero_cpow hz₀, tendsto_zero_iff_norm_tendsto_zero]
  refine squeeze_zero (fun _ => norm_nonneg _) (fun _ => norm_cpow_le _ _) ?_
  simp only [div_eq_mul_inv, ← Real.exp_neg]
  refine Tendsto.zero_mul_isBoundedUnder_le ?_ ?_
  · convert!
    (continuous_fst.norm.tendsto ((0 : ℂ), z)).rpow ((continuous_re.comp continuous_snd).tendsto _)
      _ <;>
      simp [hz, Real.zero_rpow hz.ne']
  · simp only [Function.comp_def, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
    rcases exists_gt |im z| with ⟨C, hC⟩
    refine ⟨Real.exp (π * C), eventually_map.2 ?_⟩
    refine
      (((continuous_im.comp continuous_snd).abs.tendsto (_, z)).eventually (gt_mem_nhds hC)).mono
        fun z hz => Real.exp_le_exp.2 <| (neg_le_abs _).trans ?_
    rw [_root_.abs_mul]
    exact
      mul_le_mul (abs_le.2 ⟨(neg_pi_lt_arg _).le, arg_le_pi _⟩) hz.le (_root_.abs_nonneg _)
        Real.pi_pos.le

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

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ x ^ y ≤ x ^ z ↔ z ≤ y

Tactic:
by
  rw [← log_le_log_iff (rpow_pos_of_pos hx0 y) (rpow_pos_of_pos hx0 z), log_rpow hx0, log_rpow hx0,
    mul_le_mul_right_of_neg (log_neg hx0 hx1)]

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

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

Tactic:
ext p

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

Goal state before:
pp: x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
⊢ x ^ n < y ↔ ↑n * log x < log y

Tactic:
by
  rw [← rpow_lt_iff_lt_log hx hy, rpow_natCast]

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
⊢ (pointReflection R ((lineMap x y) ⅟2)) x = y

Tactic:
pointReflection_apply,

Goal state after:
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
⊢ ((lineMap x y) ⅟2 -ᵥ x) +ᵥ (lineMap x y) ⅟2 = y
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
⊢ (pointReflection ((lineMap x y) ⅟2)) x = y

Tactic:
pointReflection_apply,

Goal state after:
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
⊢ ((lineMap x y) ⅟2 -ᵥ x) +ᵥ (lineMap x y) ⅟2 = y
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R x y

Tactic:
rw [Subsingleton.elim x 0]
  exact zero_left _

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inl
R : Type u_1
inst✝¹⁰ : CommSemiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_5
inst✝⁵ : CommSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : (algebraMap S R) a = 0
⊢ SameRay R v (a • v)

Tactic:
rw [← algebraMap_smul R a v, h, zero_smul]

Goal state after:
case inl
R : Type u_1
inst✝¹⁰ : CommSemiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_5
inst✝⁵ : CommSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : (algebraMap S R) a = 0
⊢ SameRay R v 0
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 x' y y' : P
⊢ (pointReflection R 0) (x -ᵥ x') = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y

Tactic:
pointReflection_apply,

Goal state after:
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 x' y y' : P
⊢ (0 -ᵥ (x -ᵥ x')) +ᵥ 0 = y -ᵥ y' ↔ x -ᵥ x' = y' -ᵥ y
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ (pointReflection R (⅟2 • (x + y))) x = y

Tactic:
pointReflection_apply,

Goal state after:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ (⅟2 • (x + y) -ᵥ x) +ᵥ ⅟2 • (x + y) = y
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x : V
⊢ midpoint R x (-x) = 0

Tactic:
by
  rw [midpoint_eq_smul_add, add_neg_cancel, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inl.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
exfalso

Goal state after:
case neg.refine_2.inl.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 = 0
⊢ False
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.inl.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
exfalso

Goal state after:
case neg.refine_2.inr.inl.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 < 0
⊢ False
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.inl.inr.inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
exfalso

Goal state after:
case neg.refine_2.inr.inl.inr.inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : 0 < m 1
⊢ False
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : MulActionWithZero 𝕜 E
x y : E
⊢ 1 • x + 0 • y = x

Tactic:
by rw [zero_smul, one_smul, add_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.inr.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
exfalso

Goal state after:
case neg.refine_2.inr.inr.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 = 0
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c : P1
⊢ homothety c 1 = id k P1

Tactic:
ext p

Goal state after:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p : P1
⊢ (homothety c 1) p = (id k P1) p
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c : P1
⊢ homothety c 0 = const k P1 c

Tactic:
ext p

Goal state after:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p : P1
⊢ (homothety c 0) p = (const k P1 c) p
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
hs : 0 ∈ s
⊢ ↑s -ᵥ ↑s = ↑s

Tactic:
by
  ext x
  constructor
  · rintro ⟨a, ha, b, hb, rfl⟩
    simpa using s.smul_vsub_vadd_mem 1 ha hb hs
  · exact fun h => ⟨x, h, 0, hs, by simp⟩

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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
⊢ s₁ = s₂

Tactic:
ext p

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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
⊢ p ∈ s₁ ↔ p ∈ s₂
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 𝕜
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ t • (y - x) + x ∈ s

Tactic:
exact h.lineMap_mem hx hy ht

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
⊢ (convexHull 𝕜) s = ∅ → s = ∅

pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ s = ∅ → (convexHull 𝕜) s = ∅

Tactic:
· intro h
    rw [← Set.subset_empty_iff, ← h]
    exact subset_convexHull 𝕜 _

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
⊢ s = ∅ → (convexHull 𝕜) 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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h2 : (↑s₂).Nonempty
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction

Tactic:
obtain ⟨p₂, hp₂⟩ := h2

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case mem
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 : (x : P) → x ∈ affineSpan k s → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : x ∈ affineSpan k s
⊢ ∀ x ∈ s, ∃ (hx : x ∈ affineSpan k s), p x hx

pp: case smul_vsub_vadd
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 : (x : P) → x ∈ affineSpan k s → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : x ∈ affineSpan k s
⊢ ∀ (c : k) (u v w : P),
    (∃ (hx : u ∈ affineSpan k s), p u hx) →
      (∃ (hx : v ∈ affineSpan k s), p v hx) →
        (∃ (hx : w ∈ affineSpan k s), p w hx) → ∃ (hx : c • (u -ᵥ v) +ᵥ w ∈ affineSpan k s), p (c • (u -ᵥ v) +ᵥ w) hx

Tactic:
· exact fun y hy ↦ ⟨subset_affineSpan _ _ hy, mem y hy⟩

Goal state after:
case smul_vsub_vadd
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 : (x : P) → x ∈ affineSpan k s → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : x ∈ affineSpan k s
⊢ ∀ (c : k) (u v w : P),
    (∃ (hx : u ∈ affineSpan k s), p u hx) →
      (∃ (hx : v ∈ affineSpan k s), p v hx) →
        (∃ (hx : w ∈ affineSpan k s), p w hx) → ∃ (hx : c • (u -ᵥ v) +ᵥ w ∈ affineSpan k s), p (c • (u -ᵥ v) +ᵥ w) hx
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : SMul 𝕜 E
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ι : Sort u_6
inst✝ : Finite ι
s : ι → Set E
⊢ IsVonNBounded 𝕜 (⋃ i, s i) ↔ ∀ (i : ι), IsVonNBounded 𝕜 (s i)

Tactic:
by
  simp only [IsVonNBounded, absorbs_iUnion, @forall_comm ι]

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

Goal state before:
pp: 𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ Tendsto (fun x ↦ x • S) (𝓝 0) (⨅ i, comap (eval i) (𝓝 (0 i))).smallSets ↔
    ∀ (i : ι), Tendsto (fun x ↦ x • eval i '' S) (𝓝 0) (𝓝 0).smallSets

Tactic:
smallSets_iInf,

Goal state after:
𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ Tendsto (fun x ↦ x • S) (𝓝 0) (⨅ i, (comap (eval i) (𝓝 (0 i))).smallSets) ↔
    ∀ (i : ι), Tendsto (fun x ↦ x • eval i '' S) (𝓝 0) (𝓝 0).smallSets
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕜 (id V) S
hV : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
this : ∀ᶠ (n : ι) in l, ∃ x, ε n • ↑x ∉ V
x : ι → ↑S
hx : ∀ᶠ (x_1 : ι) in l, ε x_1 • ↑(x x_1) ∉ V
⊢ ∀ᶠ (x : ι) in l, False

Tactic:
filter_upwards [hx,
    (H (_ ∘ x) fun n => (x n).2).eventually (eventually_mem_set.mpr hV)] using fun n => id

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
p : P
h : ∑ i ∈ s, w i = 1
⊢ (affineCombination k s fun x ↦ p) w = p

Tactic:
rw [affineCombination_apply, s.weightedVSubOfPoint_apply_const, h, one_smul, vsub_vadd]

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
V₂ : 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₂
f : P₁ →ᵃ[k] P₂
hf : Function.Injective ⇑f
s₁ s₂ : AffineSubspace k P₁
⊢ map f (s₁ ⊓ s₂) = map f s₁ ⊓ map f s₂

Tactic:
ext p

Goal state after:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : 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₂
f : P₁ →ᵃ[k] P₂
hf : Function.Injective ⇑f
s₁ s₂ : AffineSubspace k P₁
p : P₂
⊢ p ∈ map f (s₁ ⊓ s₂) ↔ p ∈ map f s₁ ⊓ map f s₂
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₁
V₂ : Type u_8
P₂ : Type u_9
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
s : Set P₁
f g : P₁ →ᵃ[k] P₂
h_agree : EqOn (⇑f) (⇑g) s
x : P₁
hx : x ∈ s
y : P₁
hy : y ∈ s
⊢ f.linear ((fun x1 x2 ↦ x1 -ᵥ x2) x y) = g.linear ((fun x1 x2 ↦ x1 -ᵥ x2) x y)

Tactic:
simp [h_agree hx, h_agree hy]

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

Goal state before:
pp: case 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
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := (↑s).indicator w
⊢ ∃ l ∈ Finsupp.supported k k Set.univ,
    (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = ∑ i ∈ s, w i • (p i -ᵥ p i0)

Tactic:
have hwx : ∀ i, w' i ≠ 0 → i ∈ s := fun i => Set.mem_of_indicator_ne_zero

Goal state after:
case 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
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := (↑s).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∃ l ∈ Finsupp.supported k k Set.univ,
    (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = ∑ i ∈ s, w i • (p i -ᵥ p i0)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case neg
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
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ s₁ ∥ s₂

Tactic:
refine ⟨p₂ -ᵥ p₁, (eq_iff_direction_eq_of_mem hp₂ ?_).2 ?_⟩

Goal state after:
case neg.refine_1
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
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ p₂ ∈ map (↑(constVAdd k P (p₂ -ᵥ p₁))) s₁

case neg.refine_2
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ s₂.direction = (map (↑(constVAdd k P (p₂ -ᵥ p₁))) s₁).direction
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 x✝ : E
⊢ p (x✝ - x) * ↑c ≤ r ↔ p (x✝ - x) ≤ r / ↑c

Tactic:
le_div_iff₀ (NNReal.coe_pos.mpr hc)

Goal state after:
𝕜 : 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 x✝ : E
⊢ p (x✝ - x) * ↑c ≤ r ↔ p (x✝ - x) * ↑c ≤ r
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬↑r₁ = r₂
⊢ ∃ r, r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)

Tactic:
exfalso

Goal state after:
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬↑r₁ = r₂
⊢ False
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 (Set.range fun x ↦ p ↑x)
⊢ ∃ fs w, ↑fs ⊆ s ∧ ∑ i ∈ fs, w i = 1 ∧ p₁ = (Finset.affineCombination k fs p) w

Tactic:
obtain ⟨fs', w', hw', rfl⟩ := eq_affineCombination_of_mem_affineSpan h

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
s : Set ι
fs' : Finset ↑s
w' : ↑s → k
hw' : ∑ i ∈ fs', w' i = 1
h : (Finset.affineCombination k fs' fun x ↦ p ↑x) w' ∈ affineSpan k (Set.range fun x ↦ p ↑x)
⊢ ∃ fs w,
    ↑fs ⊆ s ∧ ∑ i ∈ fs, w i = 1 ∧ (Finset.affineCombination k fs' fun x ↦ p ↑x) w' = (Finset.affineCombination k fs p) w
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
k : 𝕜
r : ℝ
hk : k ≠ 0
x✝ : E
⊢ k⁻¹ • x✝ ∈ p.ball 0 r ↔ x✝ ∈ p.ball 0 (‖k‖ * r)

Tactic:
p.mem_ball_zero,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x✝ : E
⊢ p (k⁻¹ • x✝) < r ↔ x✝ ∈ p.ball 0 (‖k‖ * r)
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
k : 𝕜
r : ℝ
hk : k ≠ 0
x✝ : E
⊢ p (k⁻¹ • x✝) < r ↔ x✝ ∈ p.ball 0 (‖k‖ * r)

Tactic:
p.mem_ball_zero,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x✝ : E
⊢ p (k⁻¹ • x✝) < r ↔ p x✝ < ‖k‖ * r