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

Goal state before:
pp: b : ℝ
n : ℕ
h : IsNat b n
a : ℝ
⊢ a ^ b = a ^ n

Tactic:
by
  rw [h.1, Real.rpow_natCast]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case 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
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ = 0
⊢ SameRay R (c₁ • v) (c₂ • v)

Tactic:
hc₁,

Goal state after:
case 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
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ = 0
⊢ SameRay R (0 • v) (c₂ • v)
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
      simp [hm0, hy, hm1.ne.symm] at hm

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
⊢ (1 - p) • c + p • x ∈ {c}

Tactic:
have : c + q • (y - c) = c + p • (x - c) := by
    convert! H using 1 <;> simp [sub_smul]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
this : c + q • (y - c) = c + p • (x - c)
⊢ (1 - p) • c + p • x ∈ {c}
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝⁴ : (i : ι) → AddCommGroup (φv i)
inst✝³ : (i : ι) → Module k (φv i)
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst✝ : Nonempty ι
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
inhabited_h : Inhabited ι
⊢ f 0 = g 0

Tactic:
rw [← Pi.single_zero default]

Goal state after:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝⁴ : (i : ι) → AddCommGroup (φv i)
inst✝³ : (i : ι) → Module k (φv i)
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst✝ : Nonempty ι
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
inhabited_h : Inhabited ι
⊢ f (Pi.single default 0) = g (Pi.single default 0)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : 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
⊢ [x -[𝕜] y] ⊆ uIcc x y

Tactic:
rcases le_total x y with h | h
  · rw [uIcc_of_le h]
    exact segment_subset_Icc h
  · rw [uIcc_of_ge h, segment_symm]
    exact segment_subset_Icc h

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
p₁ p₂ p₁a : P
hp₁a : p₁a ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hv₁p : p₁ = v₁ +ᵥ p₁a
p₂a : P
hp₂a : p₂a ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p₂ = v₂ +ᵥ p₂a
⊢ (v₁ +ᵥ p₁a) -ᵥ (v₂ +ᵥ p₂a) ∈ vectorSpan k s

Tactic:
vsub_vadd_eq_vsub_sub (v₁ +ᵥ p₁a),

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
p₁ p₂ p₁a : P
hp₁a : p₁a ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hv₁p : p₁ = v₁ +ᵥ p₁a
p₂a : P
hp₂a : p₂a ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p₂ = v₂ +ᵥ p₂a
⊢ (v₁ +ᵥ p₁a) -ᵥ p₂a - v₂ ∈ vectorSpan k 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 : AffineSubspace k P
h : (↑s).Nonempty
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
hp₂ : p₂ ∈ ↑s
p₃ : P
hp₃ : p₃ ∈ ↑s
p₄ : P
hp₄ : p₄ ∈ ↑s
⊢ (fun x1 x2 ↦ x1 -ᵥ x2) p₁ p₂ +ᵥ p₃ ∈ ↑s

Tactic:
mem_coe

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 : AffineSubspace k P
h : (↑s).Nonempty
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
hp₂ : p₂ ∈ ↑s
p₃ : P
hp₃ : p₃ ∈ ↑s
p₄ : P
hp₄ : p₄ ∈ ↑s
⊢ (fun x1 x2 ↦ x1 -ᵥ x2) p₁ p₂ +ᵥ p₃ ∈ s
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : ZeroLEOneClass 𝕜
inst✝⁶ : Module 𝕜 E
R : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : Module R E
inst✝² : Module R 𝕜
inst✝¹ : IsScalarTower R 𝕜 E
inst✝ : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a • 1) • x + (b • 1) • y ∈ s

Tactic:
refine hs hx hy ?_ ?_ (by simpa [add_smul] using congr($(hab) • (1 : 𝕜)))

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : ZeroLEOneClass 𝕜
inst✝⁶ : Module 𝕜 E
R : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : Module R E
inst✝² : Module R 𝕜
inst✝¹ : IsScalarTower R 𝕜 E
inst✝ : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 ≤ a • 1

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : ZeroLEOneClass 𝕜
inst✝⁶ : Module 𝕜 E
R : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : Module R E
inst✝² : Module R 𝕜
inst✝¹ : IsScalarTower R 𝕜 E
inst✝ : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 ≤ b • 1
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 : Set V
⊢ ↑(vectorSpan k s) + s = ↑(affineSpan k s)

Tactic:
by
  ext
  simp [mem_add, coe_affineSpan, spanPoints]
  grind

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ ⇑f '' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f '' s)

Tactic:
by
  apply Set.Subset.antisymm
  · rw [Set.image_subset_iff]
    refine convexHull_min ?_ ((convex_convexHull 𝕜 (f '' s)).affine_preimage f)
    rw [← Set.image_subset_iff]
    exact subset_convexHull 𝕜 (f '' s)
  · exact convexHull_min (Set.image_mono (subset_convexHull 𝕜 s))
      ((convex_convexHull 𝕜 s).affine_image f)

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
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
he : ↑s₁ ∩ ↑s₂ = ∅
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction

Tactic:
obtain ⟨p₁, hp₁⟩ := h1

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
h2 : (↑s₂).Nonempty
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : NormedDivisionRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
s : Set E
inst✝⁴ : NormedRing 𝕝
inst✝³ : Module 𝕜 𝕝
inst✝² : NormSMulClass 𝕜 𝕝
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ ‖b⁻¹ • a‖ ≤ 1

Tactic:
rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ h (norm_nonneg _)

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
h'' : 1 ≤ ‖a⁻¹ • r‖
h' : y ∈ (a⁻¹ • r) • s
⊢ (fun x ↦ a • x) y ∈ r • s

Tactic:
rwa [smul_assoc, mem_inv_smul_set_iff₀ h] at h'

Goal state after:
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✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hfg : EqOn f g s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ g (a • x + b • y) < a • g x + b • g y

Tactic:
simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha.le hb.le hab)] using
      hf.2 hx hy hxy ha hb hab

Goal state after:
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✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f g : E → β
hf : StrictConcaveOn 𝕜 s f
hfg : EqOn f g s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • g x + b • g y < g (a • x + b • y)

Tactic:
simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha.le hb.le hab)] using
      hf.2 hx hy hxy ha hb hab

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 = 0
b₁ b₂ : P
⊢ (s.weightedVSubOfPoint p b₁) w = (s.weightedVSubOfPoint p b₂) w

Tactic:
by
  apply eq_of_sub_eq_zero
  rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_sub_distrib]
  conv_lhs =>
    congr
    · skip
    · ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]
  rw [← sum_smul, h, zero_smul]

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
⊢ p y < r

Tactic:
rwa [mem_ball_zero] at hy

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 : ℝ
⊢ Balanced 𝕜 (p.closedBall 0 r)

Tactic:
rintro a ha x ⟨y, hy, hx⟩
  rw [mem_closedBall_zero, ← hx, map_smul_eq_mul]
  calc
    _ ≤ p y := mul_le_of_le_one_left (apply_nonneg p _) ha
    _ ≤ r := by rwa [mem_closedBall_zero] at 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
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ ((v +ᵥ b).coord i) p = ((b.coord i).comp ↑(AffineEquiv.constVAdd k P v).symm) p

Tactic:
simp only [coord, ne_eq, basisOf_vadd, coe_vadd, Pi.vadd_apply, Basis.coe_sumCoords,
    AffineMap.coe_mk, AffineEquiv.constVAdd_symm, AffineMap.coe_comp, AffineEquiv.coe_toAffineMap,
    Function.comp_apply, AffineEquiv.constVAdd_apply, sub_right_inj]

Goal state after:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ (((b.basisOf i).repr (p -ᵥ (v +ᵥ b i))).sum fun x ↦ id) = ((b.basisOf i).repr ((-v +ᵥ p) -ᵥ b i)).sum fun x ↦ id
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 ι
hs₁₂ : affineSpan k (p '' s₁) = affineSpan k (p '' s₂)
hne : s₁ ≠ s₂
⊢ False

Tactic:
apply hne

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
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
hs₁₂ : affineSpan k (p '' s₁) = affineSpan k (p '' s₂)
hne : s₁ ≠ s₂
⊢ s₁ = s₂
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 ↑x ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
refine ⟨(↑) ⁻¹' t', ⟨?_, ?_⟩, (preimage_mono ht'.2).trans ht.2⟩

Goal state after:
case refine_1
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 ↑x ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ Subtype.val ⁻¹' t' ∈ 𝓝 x

case refine_2
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : ↑S
s : Set ↑S
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 ↑x ∧ Subtype.val ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 ↑x ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ IsPathConnected (Subtype.val ⁻¹' t')
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case pos
R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : 0 < (s.sup p) v
⊢ {x | ‖x‖ * (s.sup p) v < r} ∈ 𝓝 0

pp: case neg
R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : (s.sup p) v ≤ 0
⊢ {x | ‖x‖ * (s.sup p) v < r} ∈ 𝓝 0

Tactic:
· simp_rw [(lt_div_iff₀ h).symm]
    rw [← _root_.ball_zero_eq]
    exact Metric.ball_mem_nhds 0 (div_pos hr h)

Goal state after:
case neg
R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : (s.sup p) v ≤ 0
⊢ {x | ‖x‖ * (s.sup p) v < r} ∈ 𝓝 0
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_2
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
⊢ ⨅ i, comap (⇑(p i)) (𝓝 0) ≤ p.moduleFilterBasis.filter

Tactic:
rw [p.moduleFilterBasis.toFilterBasis.hasBasis.ge_iff]
    rintro U (hU : U ∈ p.basisSets)
    rcases p.basisSets_iff.mp hU with ⟨s, r, hr, rfl⟩
    rw [id, Seminorm.ball_finset_sup_eq_iInter _ _ _ hr, s.iInter_mem_sets]
    exact fun i _ =>
      Filter.mem_iInf_of_mem i
        ⟨Metric.ball 0 r, Metric.ball_mem_nhds 0 hr,
          Eq.subset (p i).ball_zero_eq_preimage_ball.symm⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι : Type u_6
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ (comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (𝓝 ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) 0))).HasBasis
    (fun Si ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun Si ↦ {f | ∀ x ∈ Si.1, f x ∈ b Si.2}

Tactic:
exact (UniformOnFun.hasBasis_nhds_zero_of_basis 𝔖 h𝔖₁ h𝔖₂ h).comap DFunLike.coe

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : FunLike 𝓕 E F
inst✝¹ : SemilinearMapClass 𝓕 σ₁₂ E F
inst✝ : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
⊢ ball x r ⊆ Set.range ⇑f ↔ Function.Surjective ⇑f

Tactic:
refine ⟨fun h ↦ ?_, by simp_all⟩
  rw [← ball_zero_subset_range_iff_surjective hr, ← LinearMap.coe_coe]
  simp_rw [← LinearMap.coe_range, Set.subset_def, SetLike.mem_coe] at h ⊢
  intro _ _
  rw [← Submodule.add_mem_iff_left (f : E →ₛₗ[σ₁₂] F).range (h _ <| mem_ball_self hr)]
  apply h
  simp_all

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

Goal state before:
pp: E : Type u_6
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
f : E →ₗ[ℝ] ℝ
hfp : ∀ (x : E), f x ≤ p x
x : E
⊢ -f x ≤ p x

Tactic:
simpa using hfp (-x)

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

Goal state before:
pp: case hconvex
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedSpace ℝ 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
s : Set E
hs : ∃ i i_1, ∃ (_ : 0 < i_1), s = (i.sup p).ball 0 i_1
⊢ Convex ℝ (id s)

Tactic:
rcases hs with ⟨I, r, _, rfl⟩

Goal state after:
case hconvex
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedSpace ℝ 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
I : Finset ι
r : ℝ
w✝ : 0 < r
⊢ Convex ℝ (id ((I.sup p).ball 0 r))
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → 𝐤Y
inst✝ : CompactSpace X
⊢ ContinuousOn f univ ↔ Continuous[inst✝², inst✝¹] (⇑(CompactCoherentification.mk Y).symm ∘ f)

Tactic:
continuousOn_rng_of_isCompact isCompact_univ,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → 𝐤Y
inst✝ : CompactSpace X
⊢ ContinuousOn (⇑(CompactCoherentification.mk Y).symm ∘ f) univ ↔
    Continuous[inst✝², inst✝¹] (⇑(CompactCoherentification.mk Y).symm ∘ f)
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:

Tactic:
‖c x • f‖ = ‖c x‖ * ‖f‖ := norm_smul _ _
      _ ≤ ‖c‖ * ‖x‖ * ‖f‖ := by gcongr; apply le_opNorm
      _ = ‖c‖ * ‖f‖ * ‖x‖ := by ring

Goal state after:
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case mpr
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst✝ : f.NeBot
⊢ (∃ x,
      ∃ (hx : 0 ≤ x),
        ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
          (∀ᶠ (a : ι) in f, ↑(u a) ≤ ↑(NNReal.mk x_1 hx_1)) → ↑(NNReal.mk x hx) ≤ ↑(NNReal.mk x_1 hx_1)) →
    ∃ b, ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, ↑(u a_1) ≤ a) → b ≤ a

Tactic:
· rintro ⟨b, hb₀, hb⟩
    exact ⟨b, fun x hx ↦ hb _ (hx.exists.choose_spec.trans' (by simp)) hx⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ∃ b, f = mk (const α b) ⋯
⊢ StronglyMeasurable (const α (Classical.choose h))

Tactic:
exact stronglyMeasurable_const

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ (∀ (i_1 : ι), x✝ i_1 ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) i_1) ↔
    ∀ (i_1 : ι), x✝ i_1 ∈ ⋃ j, update (fun i' ↦ t i' j) i s i_1

Tactic:
apply forall_congr'

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ ∀ (a : ι), x✝ a ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) a ↔ x✝ a ∈ ⋃ j, update (fun i' ↦ t i' j) i s a
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁹ : MeasurableSpace α
μ : Measure α
inst✝⁸ : TopologicalSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : MeasurableSpace γ
inst✝² : PseudoMetrizableSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : SecondCountableTopology γ
g : β → γ
hg : Measurable g
f : α →ₘ[μ] β
⊢ ↑(compMeasurable g hg f) =ᵐ[μ] g ∘ ↑f

Tactic:
rw [compMeasurable_eq_mk]
  apply coeFn_mk

Goal state after:
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLinearOrder β
f : α → β
h : ∀ ⦃x : α⦄ ⦃a : β⦄, a < f x → μ {y | a < f y} ≠ 0
i : α
⊢ ∀ b ∈ {a | μ {x | a < f x} = 0}, f i ≤ b

Tactic:
intro b

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLinearOrder β
f : α → β
h : ∀ ⦃x : α⦄ ⦃a : β⦄, a < f x → μ {y | a < f y} ≠ 0
i : α
b : β
⊢ b ∈ {a | μ {x | a < f x} = 0} → f i ≤ b
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
⊢ (uniformOn (s ∩ u)) t * (uniformOn s) u + (uniformOn (s ∩ uᶜ)) t * (uniformOn s) uᶜ =
    (uniformOn (s ∩ u)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      (uniformOn (s ∩ uᶜ)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)

Tactic:
simp [uniformOn_inter_self hs]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
c : ε
⊢ eLpNormEssSup (s.indicator fun x ↦ c) μ ≤ ‖c‖ₑ

Tactic:
obtain rfl | hμ0 := eq_or_ne μ 0
  · simp
  · exact (eLpNormEssSup_indicator_le s fun _ => c).trans (eLpNormEssSup_const c hμ0).le

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∉ s
⊢ ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖

Tactic:
· simp [Set.indicator_of_notMem hx]

Goal state after: