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

Goal state before:
pp: x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
← rpow_le_rpow_iff hz,

Goal state after:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ z ≤ (y ^ z⁻¹) ^ z ↔ x ^ z ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Tactic:
← rpow_le_rpow_iff hz,

Goal state after:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ (x ^ z⁻¹) ^ z ≤ y ^ z ↔ x ≤ y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
⊢ x ^ (-y) = (x ^ y)⁻¹

Tactic:
by
  cases x with
  | top =>
    rcases lt_trichotomy y 0 with (H | H | H) <;>
      simp [top_rpow_of_pos, top_rpow_of_neg, H, neg_pos.mpr]
  | coe x =>
    by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]
    · have A : x ^ y ≠ 0 := by simp [h]
      simp [← coe_rpow_of_ne_zero h, ← coe_inv A, NNReal.rpow_neg]

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

Goal state before:
pp: x y : ℝ
h₁ : 1 ≤ x
h₂ : 1 ≤ y
⊢ x ≤ x ^ y

Tactic:
simpa only [rpow_one] using rpow_le_rpow_of_exponent_le h₁ h₂

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

Goal state before:
pp: x y : ℝ
h₁ : 1 ≤ x
h₂ : y ≤ 1
⊢ x ^ y ≤ x

Tactic:
simpa only [rpow_one] using rpow_le_rpow_of_exponent_le h₁ h₂

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

Goal state before:
pp: case inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹

Tactic:
cases hy

Goal state after:
case inr.inl.inl
y : ℝ
h✝ : y < 0
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹

case inr.inl.inr
y : ℝ
h✝ : 0 < y
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : ∞ ≠ 0
⊢ ∞⁻¹ ^ y = (∞ ^ y)⁻¹

Tactic:
cases hy

Goal state after:
case inr.inr.inl.inl
y : ℝ
h0 : ∞ ≠ 0
h✝ : y < 0
⊢ ∞⁻¹ ^ y = (∞ ^ y)⁻¹

case inr.inr.inl.inr
y : ℝ
h0 : ∞ ≠ 0
h✝ : 0 < y
⊢ ∞⁻¹ ^ y = (∞ ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ ‖x‖ ^ 2⁻¹ * Real.cos (x.arg * 2⁻¹) = √((‖x‖ + x.re) / 2)

Tactic:
← div_eq_mul_inv,

Goal state after:
x : ℂ
⊢ ‖x‖ ^ 2⁻¹ * Real.cos (x.arg / 2) = √((‖x‖ + x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
⊢ ‖x‖ ^ 2⁻¹ * Real.sin (x.arg * 2⁻¹) = √((‖x‖ - x.re) / 2)

Tactic:
← div_eq_mul_inv,

Goal state after:
x : ℂ
hx : 0 ≤ x.im
⊢ ‖x‖ ^ 2⁻¹ * Real.sin (x.arg / 2) = √((‖x‖ - x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : x.im < 0
⊢ ‖x‖ ^ 2⁻¹ * Real.sin (x.arg * 2⁻¹) = -√((‖x‖ - x.re) / 2)

Tactic:
← div_eq_mul_inv,

Goal state after:
x : ℂ
hx : x.im < 0
⊢ ‖x‖ ^ 2⁻¹ * Real.sin (x.arg / 2) = -√((‖x‖ - x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ |‖x‖ ^ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)

Tactic:
← div_eq_mul_inv,

Goal state after:
x : ℂ
⊢ |‖x‖ ^ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
by_cases hp0 : p = 0
  · simp [hp0]
  by_cases hx0 : x = 0
  · rw [← Ne] at hp0
    have hp_pos : 0 < p := lt_of_le_of_ne hp_nonneg hp0.symm
    simp [hx0, hp_pos, hp_pos.ne.symm]
  rw [← Ne] at hx0
  exact ofReal_rpow_of_pos (hx_nonneg.lt_of_ne hx0.symm)

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
⊢ midpoint R x y = x ↔ x = y

Tactic:
by
  rw [midpoint_eq_iff, pointReflection_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
h₀ : r • x = 0
⊢ x = 0

pp: case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • r • x
⊢ x = 0

Tactic:
· simpa [hr.ne] using h₀

Goal state after:
case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • r • x
⊢ x = 0
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v : Ray R M
this : 0 < ↑u * ↑u
⊢ (u * u) • u⁻¹ • v = u • v

Tactic:
by rw [mul_smul, smul_inv_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case h
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
u : Rˣ
v : M
hv : v ≠ 0
⊢ u • rayOfNeZero R v hv = rayOfNeZero R v hv ↔ 0 < ↑u

Tactic:
| h v hv =>

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

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

Tactic:
rw [decomp]
  simp only [map_zero, Pi.add_apply, add_sub_cancel_right, zero_add]

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

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V1
inst✝⁵ : AffineSpace V1 P1
inst✝⁴ : AddCommGroup V2
inst✝³ : AffineSpace V2 P2
inst✝² : Module k V1
inst✝¹ : Module k V2
inst✝ : SMulCommClass k k V2
f g : P1 →ᵃ[k] P2
c : k
p : P1
⊢ ((lineMap f g) c) p = (lineMap (f p) (g p)) c

Tactic:
simp [AffineMap.lineMap_apply]

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✝ : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t

pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t

Tactic:
· exact Or.inl (hs hy ha hb hab)

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t
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
r : k
⊢ (homothety c r).linear = r • LinearMap.id

Tactic:
simp [homothety]

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]

Goal state after:
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
⊢ [y -[𝕜] x] ⊆ Icc y x
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case a
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
← add_div

Goal state after:
case a
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ (a + b) / (a + b) = 1
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
⊢ StarConvex 𝕜 x s ↔ s.OrdConnected

Tactic:
by
  simp_rw [ordConnected_iff_uIcc_subset_left hx, starConvex_iff_segment_subset, segment_eq_uIcc]

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

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

Tactic:
by simp [hs]

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

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

Tactic:
rintro (rfl : y = x)

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
y : E
hx : y ∉ (convexHull 𝕜) (s \ {y})
hy : y ∈ (convexHull 𝕜) (s \ {y})
⊢ False
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: case h₁
𝕜 : 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:
rw [Set.image_subset_iff]

Goal state after:
case h₁
𝕜 : 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
⊢ (convexHull 𝕜) s ⊆ ⇑f ⁻¹' (convexHull 𝕜) (⇑f '' s)
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : PartialOrder 𝕜
hs : Balanced 𝕜 s
this : Convex 𝕜 {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
⊢ Balanced 𝕜 ((convexHull 𝕜) s)

Tactic:
rw [balanced_iff_smul_mem] at hs ⊢

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : PartialOrder 𝕜
hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this : Convex 𝕜 {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
⊢ ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ (convexHull 𝕜) s → a • x ∈ (convexHull 𝕜) s
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ -((1 - a) / 2) • x + ((a - -1) / 2) • x ∈ s

Tactic:
neg_smul,

Goal state after:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ -(((1 - a) / 2) • x) + ((a - -1) / 2) • x ∈ s
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
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
x✝ : Finite ↑I
⊢ IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)

Tactic:
rw [biUnion_eq_iUnion, isVonNBounded_iUnion, Subtype.forall]

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
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
c : P
hc : c ∈ s
r : k
p : P
hp : p ∈ s
⊢ (homothety c r) p ∈ s

Tactic:
rw [AffineMap.homothety_eq_lineMap]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
c : P
hc : c ∈ s
r : k
p : P
hp : p ∈ s
⊢ (lineMap c p) r ∈ s
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 ι
C : ℝ≥0
x : E
⊢ C • ↑(s.sup fun i ↦ NNReal.mk ((p i) x) ⋯) = ↑(s.sup fun i ↦ NNReal.mk (((C • p) i) x) ⋯)

Tactic:
exact congr_arg ((↑) : ℝ≥0 → ℝ) (NNReal.mul_finset_sup C s (fun i ↦ ⟨p i x, apply_nonneg _ _⟩))

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr.refine_2
𝕜 : 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
hx : p x < ‖k‖ * r
⊢ (k * k⁻¹) • x = x

Tactic:
← div_eq_mul_inv,

Goal state after:
case inr.refine_2
𝕜 : 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
hx : p x < ‖k‖ * r
⊢ (k / k) • x = x
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ (k * k⁻¹) • x = x

Tactic:
← div_eq_mul_inv,

Goal state after:
case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ (k / k) • x = x
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
q : P
hq : q ∈ affineSpan k (range ⇑b)
⊢ ∑ i, (b.coord i) q = 1

Tactic:
obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq

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
b : AffineBasis ι k P
inst✝ : Fintype ι
w : ι → k
hw : ∑ i, w i = 1
hq : (Finset.affineCombination k Finset.univ ⇑b) w ∈ affineSpan k (range ⇑b)
⊢ ∑ i, (b.coord i) ((Finset.affineCombination k Finset.univ ⇑b) w) = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
q : P
hq : q ∈ affineSpan k (range ⇑b)
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) q) = q

Tactic:
obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq

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
b : AffineBasis ι k P
inst✝ : Fintype ι
w : ι → k
hw : ∑ i, w i = 1
hq : (Finset.affineCombination k Finset.univ ⇑b) w ∈ affineSpan k (range ⇑b)
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) ((Finset.affineCombination k Finset.univ ⇑b) w)) =
    (Finset.affineCombination k Finset.univ ⇑b) w
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : p.closedBall 0 r ∈ 𝓝 0
⊢ ContinuousAt (⇑p) 0

Tactic:
refine continuousAt_zero_of_forall' fun ε hε ↦ ?_

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : p.closedBall 0 r ∈ 𝓝 0
ε : ℝ
hε : ε > 0
⊢ p.closedBall 0 ε ∈ 𝓝 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
ι : Sort u_12
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓤 E = ⨅ r, ⨅ (_ : r > 0), 𝓟 {x | p (x.1 - x.2) < r}

Tactic:
simp only [sub_eq_add_neg, ← map_neg_add p]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
ι : Sort u_12
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓤 E = ⨅ r, ⨅ (_ : r > 0), 𝓟 {x | p (-x.1 + x.2) < r}
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
j : Fin (n - 1 + 1)
⊢ (s.faceOpposite i).points j = s.points (i.succAbove (Fin.cast ⋯ j))

Tactic:
by
  simp_rw [faceOpposite, face, comp_apply, Finset.orderEmbOfFin_compl_singleton_apply]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Subsingleton ι
⊢ Metric.diam (stdSimplex ℝ ι) = 0

Tactic:
cases isEmpty_or_nonempty ι with
  | inl h => rw [stdSimplex_of_isEmpty_index, Metric.diam_empty]
  | inr h => rw [stdSimplex_unique, Metric.diam_singleton]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.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
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ (affineCombination k univ s.points) (Pi.single i 1) ∈ s.closedInterior

Tactic:
affineCombination_mem_closedInterior_iff (Fintype.sum_pi_single' _ _)

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
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin (n + 1)), Pi.single i 1 i_1 ∈ Set.Icc 0 1
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case e_a
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ (∑ i ∈ t with w i ≠ 0, w i)⁻¹ = (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹

Tactic:
congr 1
    exact sum_congr (by grind) (by grind)

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.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
inst✝² : PartialOrder k
inst✝¹ : Nontrivial k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
⊢ (s.face h).closedInterior ⊂ s.closedInterior

Tactic:
by
  obtain ⟨a, ha⟩ := Classical.not_forall.mp <| Finset.eq_univ_iff_forall.not.mp hfs
  apply (Set.ssubset_iff_of_subset (s.closedInterior_face_subset_closedInterior h)).mpr
  exact ⟨s.points a, s.point_mem_closedInterior a, fun hs ↦ ha (by simpa using hs)⟩

Goal state after:
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
p : ι → P
ha : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
c : k
⊢ (∀ i ∈ s, w i = (AffineMap.lineMap w₁ w₂) c i) ↔ ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i)) c

Tactic:
simp [AffineMap.lineMap_apply]

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

Goal state before:
pp: case inr.refine_1
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
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
h : LinearIndepOn k id ((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : AffineIndependent k fun p ↦ ↑p
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
h0 : ∀ v ∈ h.extend ⋯, v ≠ 0
⊢ s ⊆ {p₁} ∪ (fun v ↦ v +ᵥ p₁) '' (fun p ↦ p -ᵥ p₁) '' (s \ {p₁})

Tactic:
simp [Set.image_image]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
⊢ interior (closure s) = interior s

Tactic:
refine subset_antisymm ?_ (interior_mono subset_closure)

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
⊢ interior (closure s) ⊆ interior s
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
| 𝓝[s ∩ (Iio a ∪ Ioi a)] a

Tactic:
inter_union_distrib_left

Goal state after:
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
| 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
⊢ AffineIndependent k fun x ↦ ![p₁, p₂, p₃] ↑x

Tactic:
← affineIndependent_equiv (finSuccAboveEquiv (2 : Fin 3))

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
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
⊢ AffineIndependent k ((fun x ↦ ![p₁, p₂, p₃] ↑x) ∘ ⇑(finSuccAboveEquiv 2))
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (Metric.cthickening δ s)

Tactic:
by
  obtain hδ | hδ := le_total 0 δ
  · rw [cthickening_eq_iInter_thickening hδ]
    exact convex_iInter₂ fun _ _ => hs.thickening _
  · rw [cthickening_of_nonpos hδ]
    exact hs.closure

Goal state after: