mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝¹ : Field α
inst✝ : LinearOrder α
p : ℤ
hp : Even p
a : α
⊢ |a| ^ p = a ^ p

Tactic:
rcases abs_choice a with h | h

Goal state after:
case inl
α : Type u_1
inst✝¹ : Field α
inst✝ : LinearOrder α
p : ℤ
hp : Even p
a : α
h : |a| = a
⊢ |a| ^ p = a ^ p

case inr
α : Type u_1
inst✝¹ : Field α
inst✝ : LinearOrder α
p : ℤ
hp : Even p
a : α
h : |a| = -a
⊢ |a| ^ p = a ^ p
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
this : Continuous (cexp - 1)
⊢ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
Metric.continuous_iff'

Goal state after:
a : ℝ
this : ∀ (a : ℂ), ∀ ε > 0, ∀ᶠ (x : ℂ) in 𝓝 a, dist ((cexp - 1) x) ((cexp - 1) a) < ε
⊢ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝ : M ⧸ S
m : M
r✝ ε : ℝ
x : M ⧸ S
r : ℝ
⊢ r ≤ infDist 1 {m | ↑m = x⁻¹} ↔ r ≤ infDist 1 {m | ↑m = x}

Tactic:
simp only [le_infDist (norm_aux _)]
    exact (Equiv.inv _).forall_congr (by simp [← inv_eq_iff_eq_inv])

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ ‖↑x‖ ≤ ‖S.normedMk‖ * ‖↑x‖

Tactic:
exact norm_lift_apply_le S.normedMk (fun x ↦ (eq_zero_iff x).2) x

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ‖S.normedMk m‖ = sInf ((fun m_1 ↦ ‖m + m_1‖) '' ↑S.normedMk.ker)

Tactic:
by simpa [S.ker_normedMk] using quotient_norm_mk_eq _ m

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam ((fun x ↦ c⁻¹ • x) '' (c • s)) ≤ ↑‖c⁻¹‖₊ • ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)

Tactic:
← ENNReal.smul_def,

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam ((fun x ↦ c⁻¹ • x) '' (c • s)) ≤ ‖c⁻¹‖₊ • ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
⊢ diam (c • x) = ‖c‖ * diam x

Tactic:
by
  simp_rw [diam, ediam_smul₀, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm, smul_eq_mul]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ⨅ y ∈ c • s, edist (c • x) y = ‖c‖₊ • ⨅ y ∈ s, edist x y

Tactic:
have : Function.Surjective ((c • ·) : E → E) :=
    Function.RightInverse.surjective (smul_inv_smul₀ hc)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x ↦ c • x
⊢ ⨅ y ∈ c • s, edist (c • x) y = ‖c‖₊ • ⨅ y ∈ s, edist x y
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
⊢ (fun n ↦ ↑n ^ k * r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n

Tactic:
by_cases h0 : r₁ = 0
  · refine (isLittleO_zero _ _).congr' (mem_atTop_sets.2 <| ⟨1, fun n hn ↦ ?_⟩) EventuallyEq.rfl
    simp [zero_pow (one_le_iff_ne_zero.1 hn), h0]
  rw [← Ne, ← norm_pos_iff] at h0
  have A : (fun n ↦ (n : R) ^ k : ℕ → R) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n :=
    isLittleO_pow_const_const_pow_of_one_lt k ((one_lt_div h0).2 h)
  suffices (fun n ↦ r₁ ^ n) =O[atTop] fun n ↦ ‖r₁‖ ^ n by
    simpa [div_mul_cancel₀ _ (pow_pos h0 _).ne', div_pow] using A.mul_isBigO this
  exact .of_norm_eventuallyLE <| eventually_norm_pow_le r₁

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ s * (2 * c) = 2 * s * c

Tactic:
by rw [← mul_assoc, mul_comm 2]

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

Goal state before:
pp: ⊢ 0 + sin (↑π / 2) * I = I

Tactic:
sin_pi_div_two,

Goal state after:
⊢ 0 + 1 * I = I
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 0 + -sin (↑π / 2) * I = -I

Tactic:
sin_pi_div_two,

Goal state after:
⊢ 0 + -1 * I = -I
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hS : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen[inst✝] U ∧ MapsTo (⇑(const X c)) K U
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
⊢ ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s

Tactic:
choose hScompact hSopen hSmaps using hS

Goal state after:
case refine_1
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
⊢ ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case left
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
⊢ γ 0 ∈ F

Tactic:
apply γ_in

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case right
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
⊢ γ 1 ∈ F

Tactic:
apply γ_in

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
a₁ a₂ a₃ : X
b₁ b₂ b₃ : Y
γ₁ : Path a₁ a₂
δ₁ : Path a₂ a₃
γ₂ : Path b₁ b₂
δ₂ : Path b₂ b₃
⊢ (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ x : ℝ
_hx : x ∈ I
⊢ (γ.truncate t₀ t₁) ⟨x, _hx⟩ ∈ range ⇑γ.extend

Tactic:
simp only [DFunLike.coe, Path.truncate, mem_range_self]

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

Goal state before:
pp: ⊢ sin (-(π / 2)) = -1

Tactic:
rw [sin_neg, sin_pi_div_two]

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

Goal state before:
pp: x : ℝ
⊢ sin (-(π / 2)) < x ↔ -1 < x

Tactic:
rw [sin_neg, sin_pi_div_two]

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

Goal state before:
pp: case neg
x : ℝ
hx₁ : x < -1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
arcsin_of_le_neg_one hx₁.le,

Goal state after:
case neg
x : ℝ
hx₁ : x < -1
⊢ cos (-(π / 2)) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ ‖z‖ = 1 ↔ ∃ θ, cexp (↑θ * I) = z

Tactic:
by
  refine ⟨fun hz => ⟨arg z, ?_⟩, ?_⟩
  · calc
      exp (arg z * I) = ‖z‖ * exp (arg z * I) := by rw [hz, ofReal_one, one_mul]
      _ = z := norm_mul_exp_arg_mul_I z
  · rintro ⟨θ, rfl⟩
    exact Complex.norm_exp_ofReal_mul_I θ

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

Goal state before:
pp: case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
replace hθ := hθ.2
      have hcos : Real.cos θ < 0 := Real.cos_neg_of_pi_div_two_lt_of_lt h₁ (by linarith)
      have hsin : 0 ≤ Real.sin θ := Real.sin_nonneg_of_mem_Icc ⟨by linarith, hθ⟩
      rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith;
        linarith; exact hsin; exact hcos.not_ge]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ log x = expOrderIso.symm ⟨x, hx⟩

Tactic:
rw [log_of_ne_zero hx.ne']

Goal state after:
x : ℝ
hx : 0 < x
⊢ expOrderIso.symm ⟨|x|, ⋯⟩ = expOrderIso.symm ⟨x, hx⟩
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case mp.inr.inr
x : ℝ
h : log x = 0
x_gt_zero : 0 < x
⊢ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
· exact Or.inr (Or.inl (eq_one_of_pos_of_log_eq_zero x_gt_zero h))

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

Goal state before:
pp: x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg

Tactic:
add_im,

Goal state after:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x).im + (log y).im ↔ (x * y).arg = x.arg + y.arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ψ θ : ℝ
⊢ ↑θ = ↑ψ ↔ ∃ k, θ - ψ = 2 * π * ↑k

Tactic:
simp only [eq_comm]
  rw [Angle.coe, Angle.coe, QuotientAddGroup.eq]
  simp only [AddSubgroup.zmultiples_eq_closure,
    AddSubgroup.mem_closure_singleton, zsmul_eq_mul', (sub_eq_neg_add _ _).symm, eq_comm]

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_le_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.Log.Basic

Goal state before:
pp: e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
this : ↑n / ↑d < -1
⊢ 0 < Real.log (↑n / ↑d)

Tactic:
exact Real.log_pos_of_lt_neg_one this

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

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

Tactic:
exact tan_eq_of_two_nsmul_eq h

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

Goal state before:
pp: ⊢ SignType.sign (Real.sin (π / 2)) = 1

Tactic:
sin_pi_div_two,

Goal state after:
⊢ SignType.sign 1 = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ SignType.sign (-Real.sin (π / 2)) = -1

Tactic:
sin_pi_div_two,

Goal state after:
⊢ SignType.sign (-1) = -1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * x + c))) = rexp (log (x ^ (a / (b * x + c))))

Tactic:
log_rpow hx (a / (b * x + c))

Goal state after:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * x + c))) = rexp (a / (b * x + c) * log x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x ↦ |(g x).im|) l, (fun x1 x2 ↦ x1 ≤ x2) x b
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun x ↦ |(f x).arg * (g x).im|) l, (fun x1 x2 ↦ x1 ≤ x2) x (π * b)

Tactic:
eventually_map

Goal state after:
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) |(g a).im| b
⊢ ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) |(f a).arg * (g a).im| (π * b)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ IsBigOWith ((c ^ r⁻¹) ^ r) l (fun x ↦ f x ^ r) fun x ↦ g x ^ r

Tactic:
refine (h.forall_isBigOWith ?_).rpow ?_ ?_ hg

Goal state after:
case refine_1
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ 0 < c ^ r⁻¹

case refine_2
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ 0 ≤ c ^ r⁻¹

case refine_3
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ 0 ≤ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map f l).prod ^ r

Tactic:
← Real.list_prod_map_rpow (l.map f) _ r,

Goal state after:
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map (fun x ↦ x ^ r) (List.map f l)).prod

ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ ∀ x ∈ List.map f l, 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: y : ℝ
hp : 0 < y
A : Tendsto (fun p ↦ rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p ↦ p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ∀ᶠ (x : ℝ × ℝ) in Filter.map (Prod.mk 0) (𝓝 y), x.1 ^ x.2 = 0

Tactic:
eventually_map

Goal state after:
y : ℝ
hp : 0 < y
A : Tendsto (fun p ↦ rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p ↦ p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ∀ᶠ (a : ℝ) in 𝓝 y, (0, a).1 ^ (0, a).2 = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inl
z : ℝ
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ ∞ ^ (0 + z) = ∞ ^ 0 * ∞ ^ z

Tactic:
rw [rpow_zero, one_mul, zero_add]

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

Goal state before:
pp: case neg
y z : ℝ
hyz : 0 < y + z
hx : 0 ≠ ∞
hy' : ¬0 < y
hz' : 0 < z
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

Tactic:
simp [ENNReal.zero_rpow_of_pos hyz, ENNReal.zero_rpow_of_pos hz']

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

Goal state before:
pp: k : Type u_10
V : Type u_11
P : Type u_12
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
⊢ ofLinearEquiv (LinearEquiv.refl k V) p p = refl k P

Tactic:
by
  ext x
  simp [ofLinearEquiv_apply]

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✝ : SMul 𝕜 E
s : Set E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
u : E
hA : StarConvex 𝕜 u s
v : E
hv : v ∈ s
⊢ (fun x1 x2 ↦ x1 + x2) ((fun x ↦ a • x) u) ((fun x ↦ b • x) v) ∈ s

Tactic:
exact hA hv ha hb hab

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:
by
  rw [add_comm] at hs
  simpa only [add_comm] using hs.preimage_add_right

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

Tactic:
exact ⟨p₂, hp₂, v + v₂, (vectorSpan k s).add_mem hv hv₂, rfl⟩

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✝⁷ : 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 • x + b • y ∈ s

Tactic:
suffices (a • (1 : 𝕜)) • x + (b • (1 : 𝕜)) • y ∈ s by simpa using this

Goal state after:
𝕜 : 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
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
hp : p ∈ s₂
⊢ p -ᵥ hn.some ∈ s₁.direction

Tactic:
hd

Goal state after:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
hp : p ∈ s₂
⊢ p -ᵥ hn.some ∈ s₂.direction
Module: Mathlib.Analysis.Convex.Basic

Goal state before:

Tactic:
_ ≤ a • (f x) + b • (f y) := le_trans (hf1 _ _) (add_le_add (hf2 x ha) (hf2 y hb))
    _ ≤ a • B + b • B := by gcongr <;> assumption
    _ ≤ B := by rw [← add_smul, hs, one_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
⊢ 2⁻¹ • s + 2⁻¹ • s = s

Tactic:
rw [← h_conv.add_smul (by norm_num) (by norm_num)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
⊢ (2⁻¹ + 2⁻¹) • s = s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
hs : s.Nonempty
h : vectorSpan k s = ⊤
this : Nonempty ↥(affineSpan k s)
⊢ affineSpan k s = ⊤

Tactic:
obtain ⟨p, hp : p ∈ affineSpan k s⟩ := this
    rw [eq_iff_direction_eq_of_mem hp (mem_top k V p), direction_affineSpan, h, direction_top]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
x : E
⊢ x ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t

Tactic:
by
  simp_rw [balancedCore, mem_sUnion, mem_ofPred_eq, and_assoc]

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
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ↑s₁ ∩ ↑s₂ = ∅
hlt : s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
⊢ False

Tactic:
hd

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
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ↑s₁ ∩ ↑s₂ = ∅
hlt : ⊤ < (s₁ ⊔ s₂).direction
⊢ False
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 : EquicontinuousAt (DFunLike.coe ∘ F) 1
⊢ Equicontinuous (DFunLike.coe ∘ F)

Tactic:
by
  rw [equicontinuous_iff_continuous]
  rw [equicontinuousAt_iff_continuousAt] at hf
  let φ : G →* (ι →ᵤ M) :=
    { toFun := swap ((↑) ∘ F)
      map_one' := by dsimp [UniformFun]; ext; exact map_one _
      map_mul' := fun a b => by dsimp [UniformFun]; ext; exact map_mul _ _ _ }
  exact continuous_of_continuousAt_one φ hf

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 ℝ
r : R
p : Seminorm 𝕜 E
x✝¹ : 𝕜
x✝ : E
⊢ r • p (x✝¹ • x✝) = ‖x✝¹‖ * r • p x✝

Tactic:
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul]
        rw [map_smul_eq_mul, mul_left_comm]

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

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
⊢ map f (affineSpan k s) = affineSpan k (⇑f '' s)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)
  · simp
  apply ext_of_direction_eq
  · simp [direction_affineSpan]
  · exact ⟨f p, mem_image_of_mem f (subset_affineSpan k _ hp),
          subset_affineSpan k _ (mem_image_of_mem f hp)⟩

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₁
V₂ : Type u_8
P₂ : Type u_9
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
s : Set P₁
f g : P₁ →ᵃ[k] P₂
h_agree : EqOn (⇑f) (⇑g) s
⊢ EqOn ⇑f.linear ⇑g.linear ↑(vectorSpan k s)

Tactic:
simp only [vectorSpan_def]

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₁
V₂ : Type u_8
P₂ : Type u_9
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
s : Set P₁
f g : P₁ →ᵃ[k] P₂
h_agree : EqOn (⇑f) (⇑g) s
⊢ EqOn ⇑f.linear ⇑g.linear ↑(Submodule.span k (s -ᵥ s))
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

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

Tactic:
rintro ⟨s, w, hw, rfl⟩

Goal state after:
case mpr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
⊢ (s.weightedVSub p) w ∈ vectorSpan k (Set.range p)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr.refine_1
𝕜 : 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‖⁻¹ * p x < r

Tactic:
←
        mul_lt_mul_iff_right₀ <| norm_pos_iff.mpr hk,

Goal state after:
case inr.refine_1
𝕜 : 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‖⁻¹ * p x) < ‖k‖ * r