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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • sphere x r = sphere (0 • x) (‖0‖ * r)

Tactic:
simp [zero_smul_set, Set.singleton_zero, hr]

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
⊢ CauchySeq fun n ↦ ∑ k ∈ Finset.range (n + 1), u k

Tactic:
set v : ℕ → α := fun n ↦ if n < N then 0 else u n

Goal state after:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
⊢ CauchySeq fun n ↦ ∑ k ∈ Finset.range (n + 1), u k
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
inst✝ : LocallyCompactPair Y Z
f : C(X, Y)
g : C(Y, Z)
K : Set X
hK : IsCompact K
U : Set Z
hU : IsOpen[inst✝¹] U
hKU : MapsTo (⇑g ∘ ⇑f) K U
L : Set Y
hKL : MapsTo (⇑f) K (interior L)
hLc : IsCompact L
hLU : MapsTo (⇑g) L U
⊢ ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U

Tactic:
exact ((eventually_mapsTo hK isOpen_interior hKL).prod_nhds
    (eventually_mapsTo hLc hU hLU)).mono fun ⟨f', g'⟩ ⟨hf', hg'⟩ ↦
      hg'.comp <| hf'.mono_right interior_subset

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U : Set Y
inst✝ : RegularSpace Y
f : C(X, Y)
⊢ (𝓝 f).lift' closure ≤ 𝓝 f

Tactic:
rw [← tendsto_id', tendsto_nhds_compactOpen]

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U : Set Y
inst✝ : RegularSpace Y
f : C(X, Y)
⊢ ∀ (K : Set X),
    IsCompact K →
      ∀ (U : Set Y), IsOpen[inst✝³] U → MapsTo (⇑f) K U → ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a)) K U
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case snoc.snoc
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y : X
hp₂ : ∀ (x : X), (∀ (i : Fin n), p i ∈ s) → x ∈ s → ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin n), p i ∈ range ⇑γ
x : X
hp : ∀ (i : Fin (n + 1)), snoc p y i ∈ s
hx : x ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), snoc p y i ∈ range ⇑γ

Tactic:
simp only [forall_fin_succ', snoc_castSucc, snoc_last, snoc_apply_zero, Path.cast_coe] at hp ⊢

Goal state after:
case snoc.snoc
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y : X
hp₂ : ∀ (x : X), (∀ (i : Fin n), p i ∈ s) → x ∈ s → ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin n), p i ∈ range ⇑γ
x : X
hx : x ∈ s
hp : (∀ (i : Fin n), p i ∈ s) ∧ y ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ (∀ (i : Fin n), p i ∈ range ⇑γ) ∧ y ∈ range ⇑γ
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
s₁ : Set X
hs₁ : IsCompact s₁
s₂ : Set X
hs₂ : IsCompact s₂
x : X
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
h₁ : Tendsto ((fun f ↦ f ⟨x, hxs₁⟩) ∘ fun i ↦ restrict s₁ (F i)) l (𝓝 ((f s₁ hs₁) ⟨x, hxs₁⟩))
h₂ : Tendsto ((fun f ↦ f ⟨x, hxs₂⟩) ∘ fun i ↦ restrict s₂ (F i)) l (𝓝 ((f s₂ hs₂) ⟨x, hxs₂⟩))
⊢ (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩

Tactic:
exact tendsto_nhds_unique h₁ h₂

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

Goal state before:
pp: case pos
x : ℂ
h : x = 0
⊢ Real.tan x.arg = x.im / x.re

Tactic:
simp only [h, zero_div, Complex.zero_im, Complex.arg_zero, Real.tan_zero, Complex.zero_re]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ rexp (2 * x / (x + 2)) < 1 + x

Tactic:
convert exp_lt_two_add_div_two_sub (x := 2 * x / (x + 2)) (by positivity) _ using 1

Goal state after:
x : ℝ
hx : 0 < x
⊢ 1 + x = (2 + 2 * x / (x + 2)) / (2 - 2 * x / (x + 2))

x : ℝ
hx : 0 < x
⊢ 2 * x / (x + 2) < 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s.Countable

Tactic:
refine ((hs.image exp).insert 0).mono ?_
    rw [Set.image_preimage_eq_inter_range, range_exp, ← Set.sdiff_eq, ← Set.union_singleton,
        Set.sdiff_union_self]
    exact Set.subset_union_left

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

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

Tactic:
rw [two_nsmul_eq_iff] at h
  rcases h with (rfl | rfl)
  · rfl
  · exact tan_add_pi _

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

Goal state before:
pp: x : ℝ
n : ℕ
⊢ x ^ (-↑n) = x ^ (-↑n)

Tactic:
by
  rw [← rpow_intCast, Int.cast_neg, Int.cast_natCast]

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

Goal state before:
pp: k a b : ℝ
ha' : a < b
⊢ Tendsto (fun x ↦ x ^ k * rexp (-(b - a) * x)) atTop (𝓝 0)

Tactic:
exact tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero _ _ (sub_pos.mpr ha')

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ≥0
⊢ (fun y ↦ y ^ x) (y ^ x⁻¹) = y

Tactic:
by simp_rw [← rpow_mul, inv_mul_cancel₀ hx, rpow_one]

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

Goal state before:
pp: case inl.inl
hx : 0 ≤ 0
⊢ 1 < 0 ^ 0 ↔ 1 < 0 ∧ 0 < 0 ∨ 0 < 0 ∧ 0 < 1 ∧ 0 < 0

Tactic:
simp [*, (zero_lt_one' ℝ).not_gt]

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

Goal state before:
pp: case inl.inr
y : ℝ
hx : 0 ≤ 0
hy : ¬y = 0
⊢ 1 < 0 ^ y ↔ 1 < 0 ∧ 0 < y ∨ 0 < 0 ∧ 0 < 1 ∧ y < 0

Tactic:
simp [*, (zero_lt_one' ℝ).not_gt]

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

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

Tactic:
rw [hx, ContinuousAt]

Goal state after:
case pos
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ∞
⊢ Tendsto (fun a ↦ a ^ y) (𝓝 ∞) (𝓝 (∞ ^ y))
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < x
hx1 : x < 1
⊢ ↑x ^ y < ↑x ^ z

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt hx0), NNReal.rpow_lt_rpow_of_exponent_gt hx0 hx1 hyz]

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

Goal state before:
pp: case inr
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ √x = x ^ (1 / 2)

Tactic:
sqrt_eq_zero_of_nonpos h.le,

Goal state after:
case inr
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ 0 = x ^ (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 < x✝
⊢ ↑x✝ ^ z < 1

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_trans zero_lt_one hx)),
      NNReal.rpow_lt_one_of_one_lt_of_neg hx hz]

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

Goal state before:
pp: case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 < ↑x✝
⊢ 1 < ↑x✝ ^ z

Tactic:
· 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.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 (midpoint R x y)) x = y

Tactic:
rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
    mul_invOf_self, one_smul, vsub_vadd]

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 (midpoint R x y)) x = y

Tactic:
rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
    mul_invOf_self, one_smul, vsub_vadd]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.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
x y : M
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hx : SameRay R x 0
hy : SameRay R y 0
⊢ SameRay R (x + y) 0

Tactic:
apply zero_right

Goal state after:
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
u : Rˣ
hu : 0 < ↑u
v : Ray R M
⊢ u • v = v

Tactic:
induction v using Module.Ray.ind

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ u • rayOfNeZero R v✝ hv✝ = rayOfNeZero R v✝ hv✝
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
u : Rˣ
v : Ray R M
⊢ -u • v = -(u • v)

Tactic:
induction v using Module.Ray.ind

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v✝ : M
hv✝ : v✝ ≠ 0
⊢ -u • rayOfNeZero R v✝ hv✝ = -(u • rayOfNeZero R v✝ hv✝)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : SameRay R x y
hx : x ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y

Tactic:
obtain rfl | hy := eq_or_ne y 0

Goal state after:
case inl
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
h : SameRay R x 0
⊢ ∃ r, 0 ≤ r ∧ r • x = 0

case inr
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y -[𝕜] z] ↔ SameRay 𝕜 (x - y) (z - x)

Tactic:
refine ⟨sameRay_of_mem_segment, fun h => ?_⟩
  rcases h.exists_eq_smul_add with ⟨a, b, ha, hb, hab, hxy, hzx⟩
  rw [add_comm, sub_add_sub_cancel] at hxy hzx
  rw [← mem_segment_translate _ (-x), neg_add_cancel]
  refine ⟨b, a, hb, ha, add_comm a b ▸ hab, ?_⟩
  rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_cancel]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (x + z) s
⊢ StarConvex 𝕜 x ((fun x ↦ x + z) ⁻¹' s)

Tactic:
rw [add_comm] at hs
  simpa only [add_comm] using hs.preimage_add_right

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x y : E
h : y ≤ x
⊢ [x -[𝕜] y] ⊆ uIcc x y

Tactic:
rw [uIcc_of_ge h, segment_symm]
    exact segment_subset_Icc h

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

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
z : E
⊢ Convex 𝕜 (z +ᵥ s)

Tactic:
simp_rw [← image_vadd, vadd_eq_add, ← singleton_add]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ({z} + s)
Module: Mathlib.Analysis.Convex.Star

Goal state before:

Tactic:
b • z ≤ (a + b) • x - a • y := by rwa [le_sub_iff_add_le', hab, one_smul]
    _ < b • x := by
      rw [add_smul, sub_lt_iff_lt_add']
      gcongr

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ affineSpan k s ≠ ⊥ ↔ s ≠ ∅

Tactic:
exact (affineSpan_eq_bot _).not

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

Goal state before:
pp: 𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedDivisionRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
S : Set E
⊢ IsVonNBounded 𝕜 S ↔ ∀ t ∈ 𝓝 0, ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ t

Tactic:
refine forall₂_congr fun V hV ↦ ?_

Goal state after:
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedDivisionRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
S V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V S ↔ ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ V
Module: Mathlib.Analysis.LocallyConvex.Bounded

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

Tactic:
simp [isVonNBounded_add_of_nonempty, *]

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

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

Tactic:
simp [isVonNBounded_add_of_nonempty, *]

Goal state after:
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
a b : G
x✝ : ι
⊢ swap (DFunLike.coe ∘ F) (a * b) x✝ = (swap (DFunLike.coe ∘ F) a * swap (DFunLike.coe ∘ F) b) x✝

Tactic:
exact map_mul _ _ _

Goal state after:
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : UniformSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsUniformGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
a b : G
x✝ : ι
⊢ swap (DFunLike.coe ∘ F) (a * b) x✝ = (swap (DFunLike.coe ∘ F) a * swap (DFunLike.coe ∘ F) b) x✝

Tactic:
exact map_mul _ _ _

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 ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ (s.weightedVSubOfPoint p (p j)) w₁ = (s.weightedVSubOfPoint p (p j)) w₂

Tactic:
simp only [Finset.weightedVSubOfPoint_apply]
  congr
  ext i
  rcases eq_or_ne i j with h | h
  · simp [h]
  · simp [hw i h]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 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✝⁸ : SeminormedRing 𝕜
inst✝⁷ : AddGroup E
inst✝⁶ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x✝ : E
r : ℝ
inst✝⁵ : SMul R ℝ
inst✝⁴ : SMul R ℝ≥0
inst✝³ : IsScalarTower R ℝ≥0 ℝ
inst✝² : Preorder R
inst✝¹ : Zero R
inst✝ : IsOrderedModule R ℝ
p q : Seminorm 𝕜 E
hpq : p ≤ q
c : R
x : E
⊢ (c • 1) • p x ≤ (c • q) x

Tactic:
hpq x

Goal state after:
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✝⁸ : SeminormedRing 𝕜
inst✝⁷ : AddGroup E
inst✝⁶ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x✝ : E
r : ℝ
inst✝⁵ : SMul R ℝ
inst✝⁴ : SMul R ℝ≥0
inst✝³ : IsScalarTower R ℝ≥0 ℝ
inst✝² : Preorder R
inst✝¹ : Zero R
inst✝ : IsOrderedModule R ℝ
p q : Seminorm 𝕜 E
hpq : p ≤ q
c : R
x : E
⊢ (c • 1) • q x ≤ (c • q) x
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ f.symm (a • x + b • y) < a • f.symm x + b • f.symm y

Tactic:
simp only [hx'', hy'', OrderIso.symm_apply_apply, gt_iff_lt]

Goal state after:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ f.symm (a • f x' + b • f y') < a • x' + b • y'
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ a • f.symm x + b • f.symm y < f.symm (a • x + b • y)

Tactic:
simp only [hx'', hy'', OrderIso.symm_apply_apply, gt_iff_lt]

Goal state after:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ a • x' + b • y' < f.symm (a • f x' + b • f y')
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
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
⊢ (s.weightedVSub p) w ∈ vectorSpan k (Set.range p)

Tactic:
rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)

Goal state after:
case 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
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
hι : IsEmpty ι
⊢ (s.weightedVSub p) w ∈ vectorSpan k (Set.range p)

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 : ι
⊢ (s.weightedVSub p) w ∈ vectorSpan k (Set.range p)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
p : ι → P
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)

Tactic:
by
  classical
    have hnz : ∑ i ∈ s, w i ≠ 0 := h.symm ▸ one_ne_zero
    have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
    obtain ⟨i1, hi1⟩ := hn
    let w1 : ι → k := Function.update (Function.const ι 0) i1 1
    have hw1 : ∑ i ∈ s, w1 i = 1 := by
      simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
          Finset.sum_const_zero, add_zero]
    have hw1s : s.affineCombination k p w1 = p i1 :=
      s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_self ..) fun _ _ hne =>
        Function.update_of_ne hne ..
    have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction := by
      rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
      apply weightedVSub_mem_vectorSpan
      simp [Pi.sub_apply, h, hw1]
    rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
    exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))

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

Goal state before:
pp: case mp
ι : 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
⊢ v ∈ vectorSpan k (Set.range p) → ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w

Tactic:
rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)

Goal state after:
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

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

Goal state before:
pp: 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
p₁ p₂ : P
⊢ line[k, p₁, p₂] = line[k, p₂, p₁]

Tactic:
Set.pair_comm

Goal state after:
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
p₁ p₂ : P
⊢ line[k, p₂, p₁] = line[k, p₂, p₁]
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: 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₃]
h₁₂₄₅ : ∃ z, z • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
h₂₃₅₆ : ∃ z, z • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
h₃₁₆₄ : ∃ z, z • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
⊢ ∃ r, r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)

Tactic:
obtain ⟨r₁, hr₁⟩ := h₁₂₄₅

Goal state after:
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₃]
h₂₃₅₆ : ∃ z, z • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
h₃₁₆₄ : ∃ z, z • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
r₁ : kˣ
hr₁ : r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
⊢ ∃ r, r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)