mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: z : ℂ
⊢ ∃ n, log (cexp z) = z + ↑n * (2 * ↑π * I)

Tactic:
← exp_eq_exp_iff_exists_int,

Goal state after:
z : ℂ
⊢ cexp (log (cexp z)) = cexp z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x n : ℂ
⊢ (if x⁻¹ = 0 then if n = 0 then 1 else 0 else cexp (log x⁻¹ * n)) =
    if x.arg = π then
      (starRingEnd ℂ) (if x = 0 then if (starRingEnd ℂ) n = 0 then 1 else 0 else cexp (log x * (starRingEnd ℂ) n))⁻¹
    else (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n))⁻¹

Tactic:
log_inv_eq_ite,

Goal state after:
x n : ℂ
⊢ (if x⁻¹ = 0 then if n = 0 then 1 else 0 else cexp ((if x.arg = π then -(starRingEnd ℂ) (log x) else -log x) * n)) =
    if x.arg = π then
      (starRingEnd ℂ) (if x = 0 then if (starRingEnd ℂ) n = 0 then 1 else 0 else cexp (log x * (starRingEnd ℂ) n))⁻¹
    else (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
arg_lt_pi_div_two_iff,

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

Goal state before:
pp: ⊢ Function.Injective toReal

Tactic:
intro θ ψ h

Goal state after:
θ ψ : Angle
h : θ.toReal = ψ.toReal
⊢ θ = ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
rcases lt_trichotomy θ.toReal 0 with (ht | ht | ht)

Goal state after:
case inl
θ : Angle
h : θ ≠ ↑π
ht : θ.toReal < 0
⊢ SignType.sign θ.toReal = θ.sign

case inr.inl
θ : Angle
h : θ ≠ ↑π
ht : θ.toReal = 0
⊢ SignType.sign θ.toReal = θ.sign

case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < θ.toReal
⊢ SignType.sign θ.toReal = θ.sign
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ : Angle
h : θ.sign = -1
⊢ -↑(-θ.toReal) = θ

Tactic:
coe_neg,

Goal state after:
case inl
θ : Angle
h : θ.sign = -1
⊢ - -↑θ.toReal = θ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hr : y < 0
⊢ Tendsto (fun x ↦ x ^ y) (𝓝[>] 0) atTop

Tactic:
simp_rw +singlePass [← neg_neg y, Real.rpow_neg_eq_inv_rpow]
  exact (tendsto_rpow_atTop <| neg_pos.mpr hr).comp tendsto_inv_nhdsGT_zero

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

Goal state before:
pp: x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ log x ≠ 0

Tactic:
exact log_ne_zero.2 ⟨hx₀.ne', hx₁, by bound⟩

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

Goal state before:
pp: case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ 0 < ‖x‖

Tactic:
rwa [norm_pos_iff]

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

Goal state before:
pp: case inl
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_pos : 0 < p
⊢ 0 < x ^ p

Tactic:
exact rpow_pos_of_nonneg hp_pos

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

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

Tactic:
convert! rpow_lt_rpow_of_exponent_lt hx hz

Goal state after:
x z : ℝ
hx : 1 < x
hz : z < 0
⊢ 1 = x ^ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
by
  lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx le_top)
  simp only [coe_lt_one_iff] at hx
  simp [← coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.rpow_lt_one hx hz]

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

Goal state before:
pp: x p : ℝ
hx_pos : 0 < x
⊢ x.toNNReal ^ p = (x ^ p).toNNReal

pp: case h
x p : ℝ
hx_pos : 0 < x
⊢ x.toNNReal ≠ 0

Tactic:
Real.toNNReal_rpow_of_nonneg hx_pos.le

Goal state after:
x p : ℝ
hx_pos : 0 < x
⊢ x.toNNReal ^ p = x.toNNReal ^ p

case h
x p : ℝ
hx_pos : 0 < x
⊢ x.toNNReal ≠ 0
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.inr.refine_2
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 z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (rx * ry) • (x + y) = (ry * rz₁ + rx * rz₂) • z

Tactic:
convert! congr(ry • $Hx + rx • $Hy) using 1

Goal state after:
case e'_2
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 z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (rx * ry) • (x + y) = ry • rx • x + rx • ry • y

case e'_3
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 z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (ry * rz₁ + rx * rz₂) • z = ry • rz₁ • z + rx • rz₂ • z
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
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ M
inst✝ : Module R✝ N
x y : M
R : Type u_4
v : RayVector R M
⊢ ↑((equiv R M) (- -v)) = ↑((equiv R M) v)

Tactic:
coe_neg,

Goal state after:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
inst✝⁵ : PartialOrder R✝
inst✝⁴ : IsStrictOrderedRing R✝
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ M
inst✝ : Module R✝ N
x y : M
R : Type u_4
v : RayVector R M
⊢ -↑((equiv R M) (-v)) = ↑((equiv R M) v)
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
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ M
inst✝ : Module R✝ N
x y : M
R : Type u_4
v : RayVector R M
⊢ -↑((equiv R M) (-v)) = ↑((equiv R M) v)

Tactic:
coe_neg,

Goal state after:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
inst✝⁵ : PartialOrder R✝
inst✝⁴ : IsStrictOrderedRing R✝
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ M
inst✝ : Module R✝ N
x y : M
R : Type u_4
v : RayVector R M
⊢ - -↑((equiv R M) v) = ↑((equiv R M) v)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
b : 𝕜
hb : 0 ≤ b
hb' : 0 < b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y = y

Tactic:
← zero_add b,

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
b : 𝕜
hb : 0 ≤ b
hb' : 0 < b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + (0 + b) • y = y
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
x y : E
⊢ [x -[𝕜] y] = (fun θ ↦ x + θ • (y - x)) '' Icc 0 1

Tactic:
convert! segment_eq_image 𝕜 x y using 2

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y
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
hx : x ≠ 0
⊢ (∃ r, 0 ≤ r ∧ r • x = y) ↔ SameRay R x y

Tactic:
by
  refine ⟨fun h => ?_, fun h => h.exists_nonneg_left hx⟩
  rcases h with ⟨r, hr, rfl⟩
  exact SameRay.sameRay_nonneg_smul_right x hr

Goal state after:
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
inst✝¹ : IsTorsionFree k V1
inst✝ : IsCancelMulZero k
c : P1
r : k
hr : r ≠ 0
x✝¹ x✝ : P1
h : (homothety c r) x✝¹ = (homothety c r) x✝
⊢ x✝¹ = x✝

Tactic:
by simpa [homothety_def, hr] using h

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : IsOrderedRing 𝕜
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1

Tactic:
rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]

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 : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Tactic:
rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_left hp]

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
p : P
hp : p ∈ s
v : V
⊢ v ∈ (fun x ↦ p -ᵥ x) '' ↑s ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case refine_1.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
hz : 0 * x + b * y ∈ Ico x y
⊢ ∃ a b_1, 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y

Tactic:
rw [zero_add] at hab
      rw [hab, one_mul, zero_mul, zero_add] at hz
      exact (hz.2.ne rfl).elim

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : Semiring 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : PartialOrder 𝕜
𝕜' : Type u_5
inst✝⁵ : Semiring 𝕜'
inst✝⁴ : PartialOrder 𝕜'
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomSurjective σ
F' : Type u_6
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜' F'
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
hσ : ∀ {s t : 𝕜}, σ s ≤ σ t ↔ s ≤ t
f : E →ₛₗ[σ] F'
⊢ Convex 𝕜' (⇑f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ a b ha hb hab
  obtain ⟨r, rfl⟩ : ∃ r : 𝕜, σ r = a := RingHomSurjective.is_surjective ..
  obtain ⟨t, rfl⟩ : ∃ t : 𝕜, σ t = b := RingHomSurjective.is_surjective ..
  refine ⟨r • x + t • y, hs hx hy (by simp_all [(@hσ 0 r).mp]) (by simp_all [(@hσ 0 t).mp])
    ?_, by simp⟩
  apply_fun σ using Function.Injective.of_eq_imp_le (hσ.mp ·.le)
  simpa

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).direction = vectorSpan k s

Tactic:
apply le_antisymm

Goal state after:
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ (affineSpan k s).direction ≤ vectorSpan k s

case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ vectorSpan k s ≤ (affineSpan k s).direction
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : { t // 0 ≤ t }
h : x ≤ y
⊢ [x -[{ t // 0 ≤ t }] y] = uIcc x y

Tactic:
simp [h, Nonneg.segment_eq_Icc]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Balanced 𝕜 s
hs_nonempty : s.Nonempty
⊢ 0 ∈ s

Tactic:
rw [← hs.balancedCore_eq] at hs_nonempty
  exact balancedCore_nonempty_iff.mp hs_nonempty

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a : Set E
ha : IsVonNBounded 𝕜 a
⊢ IsVonNBounded 𝕜 (closure[inst✝³] a)

Tactic:
intro V hV
  rcases exists_mem_nhds_isClosed_subset hV with ⟨W, hW₁, hW₂, hW₃⟩
  specialize ha hW₁
  filter_upwards [ha] with b ha'
  grw [ha', closure_smul₀ b, closure_subset_iff_isClosed.mpr hW₂, hW₃]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
s : Set E
x y : E
inst✝² : IsOrderedRing 𝕜
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
⊢ x = y

Tactic:
obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
  classical
    by_contra hxy
    exact
      (h ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, rfl⟩).2
        (hs hx hy hxy ha₀ (sub_pos_of_lt ha₁) <| add_sub_cancel _ _)

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✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ p -ᵥ p₂ ∈ s.direction ↔ p₂ ∈ s

Tactic:
rw [mem_direction_iff_eq_vsub_left hp]
  simp

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✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
⊢ affineSpan k (Subtype.val ⁻¹' A) = ⊤

Tactic:
eq_top_iff

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
A : Set P
inst✝ : Nonempty ↑A
⊢ ⊤ ≤ affineSpan k (Subtype.val ⁻¹' A)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
h :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (-f) (a • x + b • y) ≤ a • (-f) x + b • (-f) y
⊢ ConcaveOn 𝕜 s f

Tactic:
refine ⟨hconv, fun x hx y hy a b ha hb hab => ?_⟩

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
h :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (-f) (a • x + b • y) ≤ a • (-f) x + b • (-f) y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ f (a • x + b • y)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)
⊢ ConvexOn 𝕜 s (-f)

Tactic:
refine ⟨hconv, fun x hx y hy a b ha hb hab => ?_⟩

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (-f) (a • x + b • y) ≤ a • (-f) x + b • (-f) y
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
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ (s₁.weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint p b) ((↑s₁).indicator w)

Tactic:
by
  rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
  exact Eq.symm <|
    sum_indicator_subset_of_eq_zero w (fun i wi => wi • (p i -ᵥ b : V)) h fun i => zero_smul k _

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

Goal state before:
pp: case mpr
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
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs w, ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p ↑i -ᵥ b)) →
    ∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)

Tactic:
· rintro ⟨fs, w, rfl, rfl⟩
      refine ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i =>
        if h : i ∈ s then w ⟨i, h⟩ else 0, ?_, ?_⟩ <;> simp

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
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs,
      ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (fs.weightedVSubOfPoint p (Classical.choice ⋯)) w +ᵥ Classical.choice ⋯) ↔
    ∃ fs w,
      ∑ i ∈ fs, w i = 1 ∧ p0 = (fs.weightedVSubOfPoint (fun i ↦ p ↑i) (Classical.choice ⋯)) w +ᵥ Classical.choice ⋯

Tactic:
eq_vadd_iff_vsub_eq

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
ι : Type u_4
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs,
      ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 -ᵥ Classical.choice ⋯ = (fs.weightedVSubOfPoint p (Classical.choice ⋯)) w) ↔
    ∃ fs w,
      ∑ i ∈ fs, w i = 1 ∧ p0 -ᵥ Classical.choice ⋯ = (fs.weightedVSubOfPoint (fun i ↦ p ↑i) (Classical.choice ⋯)) w
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✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
⊢ ⨆ i, ↑i 0 = ⨆ x, 0

Tactic:
congr!

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✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
x✝ : ↑s
⊢ ↑x✝ 0 = 0
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✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
a : 𝕜
x : E
⊢ ⨆ i, ↑i (a • x) = ⨆ i, ‖a‖ • ↑i x

Tactic:
congr!

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✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝¹ : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
a : 𝕜
x : E
x✝ : ↑s
⊢ ↑x✝ (a • x) = ‖a‖ • ↑x✝ x
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₂
⊢ comap f ⊤ = ⊤

Tactic:
by
  rw [AffineSubspace.ext_iff]
  exact preimage_univ (f := f)

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 : ι
⊢ ∃ 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:
let w' := Set.indicator (↑s) w

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
⊢ ∃ 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: 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₁ : AffineSubspace k P
v : V
⊢ s₁ = map (↑(constVAdd k P (-v))) (map (↑(constVAdd k P v)) s₁)

Tactic:
rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add, neg_add_cancel, constVAdd_zero,
    coe_refl_to_affineMap, map_id]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ x✝ ∈ {y | p (f (y - x)) < r} ↔ f x✝ ∈ {y | p (y - f x) < r}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ p (f (x✝ - x)) < r ↔ p (f x✝ - f x) < r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ x✝ ∈ {y | p (f (y - x)) ≤ r} ↔ f x✝ ∈ {y | p (y - f x) ≤ r}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ p (f (x✝ - x)) ≤ r ↔ p (f x✝ - f x) ≤ r