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

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ log x ≤ y ↔ x ≤ rexp y

Tactic:
rw [← exp_le_exp, exp_log hx]

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

Goal state before:
pp: z : ℂ
⊢ z.arg < π ↔ 0 ≤ z.re ∨ z.im ≠ 0

Tactic:
by
  rw [(arg_le_pi z).lt_iff_ne, not_iff_comm, not_or, not_le, Classical.not_not, arg_eq_pi_iff]

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

Goal state before:
pp: x : ℝ
hx : x < -1
⊢ 0 < log x

Tactic:
rw [← neg_neg x, log_neg_eq_log]
  have : 1 < -x := by linarith
  exact log_pos this

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

Goal state before:
pp: case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ { re := 0, im := y }.arg = π / 2

Tactic:
rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]

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

Goal state before:
pp: θ : Angle
⊢ 2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
have h : (π : Angle) = ((2 : ℕ) • (π / 2 : ℝ) :) := by rw [two_nsmul, add_halves]
  nth_rw 1 [h]
  rw [coe_nsmul, two_nsmul_eq_iff]
  apply iff_of_eq -- `congr` only works on `Eq`, so rewrite from `Iff` to `Eq`.
  congr
  rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]

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

Goal state before:
pp: x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
by
  rw [sub_eq_add_neg, cpow_add _ _ hx, cpow_neg, div_eq_mul_inv]

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

Goal state before:
pp: ⊢ Real.sin π = 0

Tactic:
Real.sin_pi

Goal state after:
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
ψ : Angle
⊢ |(ψ + ↑π).cos| = |ψ.cos|

Tactic:
rw [cos_add_pi, abs_neg]

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

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ ψ.tan = θ.tan⁻¹

Tactic:
by
  simp_rw [two_zsmul, ← two_nsmul] at h
  exact tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi h

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

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

Tactic:
by
  apply IsBigOWith.of_bound
  filter_upwards [hg, h.bound] with x hgx hx
  calc
    |f x ^ r| ≤ |f x| ^ r := abs_rpow_le_abs_rpow _ _
    _ ≤ (c * |g x|) ^ r := by gcongr; assumption
    _ = c ^ r * |g x ^ r| := by rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]

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

Goal state before:
pp: case inr.inl
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
grind [sign_eq_zero_iff, coe_pi_add_coe_pi]

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

Goal state before:
pp: case inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
⊢ ‖0 ^ w‖ = ‖0‖ ^ w.re / rexp (arg 0 * w.im)

Tactic:
norm_zero

Goal state after:
case inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0‖ = 0

pp: case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ w ≠ 0

Tactic:
norm_zero

Goal state after:
case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ 0 = 0

case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ w ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case pos
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
rw [ha, continuousAt_congr (zero_cpow_eq_nhds h)]

Goal state after:
case pos
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt 0 b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
simp only [rpow_def]
  refine Complex.continuous_re.continuousAt.comp ?_
  refine (continuousAt_const_cpow' ?_).comp Complex.continuous_ofReal.continuousAt
  norm_cast

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

Goal state before:
pp: case inr
p : ℝ × ℝ
hp : 0 < p.1
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) p

Tactic:
continuousAt_congr (rpow_eq_nhds_of_pos hp)

Goal state after:
case inr
p : ℝ × ℝ
hp : 0 < p.1
⊢ ContinuousAt (fun x ↦ rexp (log x.1 * x.2)) p
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]

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

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

Tactic:
rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]

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

Goal state before:
pp: x : ℝ≥0∞
⊢ x ^ 1 = x

Tactic:
cases x
  · exact dif_pos zero_lt_one
  · change ite _ _ _ = _
    simp only [NNReal.rpow_one, ite_eq_right_iff, top_ne_coe, and_imp]
    exact fun _ => zero_le_one.not_gt

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

Goal state before:
pp: x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1

Tactic:
rw [← one_rpow z]
  gcongr

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

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

Tactic:
rw [← one_rpow z]
  gcongr

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

Goal state before:
pp: case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

Tactic:
· simp [← coe_rpow_of_ne_zero h, h]

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

Goal state before:
pp: case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

Tactic:
· simp [← coe_rpow_of_ne_zero h, h]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.inl
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x z : M
hx : x ≠ 0
hz : z ≠ 0
hxy : SameRay R x 0
hyz : SameRay R 0 z
hy : 0 = 0 → x = 0 ∨ z = 0
⊢ SameRay R x z

pp: case inr.inr.inr
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
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
⊢ SameRay R x z

Tactic:
· exact (hy rfl).elim (fun h => (hx h).elim) fun h => (hz h).elim

Goal state after:
case inr.inr.inr
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
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
⊢ SameRay R x z
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: case refine_2
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
q : P2
⊢ (const k P1 q).linear = 0

Tactic:
exact const_linear k P1 q

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V1
inst✝ : Module k V1
p₀ p₁ : V1
c : k
⊢ (lineMap p₀ p₁) c = (1 - c) • p₀ + c • p₁

Tactic:
simp [lineMap_apply_module', smul_sub, sub_smul]

Goal state after:
k : Type u_1
V1 : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V1
inst✝ : Module k V1
p₀ p₁ : V1
c : k
⊢ c • p₁ - c • p₀ + p₀ = p₀ - c • p₀ + c • p₁
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
⊢ ↑{ carrier := ↑s -ᵥ ↑s, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } ⊆ ↑s.direction

Tactic:
direction,

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
⊢ ↑{ carrier := ↑s -ᵥ ↑s, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } ⊆ ↑(vectorSpan k ↑s)
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ x ∈ t • s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']
  exact hs.smul_mem hx (by positivity) (inv_le_one_of_one_le₀ ht)

Goal state after:
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) +ᵥ hn.some ∈ s₁

Tactic:
refine vadd_mem_of_mem_direction ?_ hq1

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:
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'
x : E
hx : x ∈ s
y : E
hy : y ∈ s
b : 𝕜'
hb : 0 ≤ b
r : 𝕜
ha : 0 ≤ σ r
hab : σ r + b = 1
⊢ σ r • f x + b • f y ∈ ⇑f '' s

Tactic:
obtain ⟨t, rfl⟩ : ∃ t : 𝕜, σ t = b := RingHomSurjective.is_surjective ..

Goal state after:
𝕜 : 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'
x : E
hx : x ∈ s
y : E
hy : y ∈ s
r : 𝕜
ha : 0 ≤ σ r
t : 𝕜
hb : 0 ≤ σ t
hab : σ r + σ t = 1
⊢ σ r • f x + σ t • f y ∈ ⇑f '' s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ Ico x y ↔ ∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
by
  refine ⟨fun hz => ?_, ?_⟩
  · obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ico_subset_Icc_self hz)
    obtain rfl | ha' := ha.eq_or_lt
    · rw [zero_add] at hab
      rw [hab, one_mul, zero_mul, zero_add] at hz
      exact (hz.2.ne rfl).elim
    · exact ⟨a, b, ha', hb, hab, rfl⟩
  · rintro ⟨a, b, ha, hb, hab, rfl⟩
    obtain rfl | hb' := hb.eq_or_lt
    · rw [add_zero] at hab
      rwa [hab, one_mul, zero_mul, add_zero, left_mem_Ico]
    · exact Ioo_subset_Ico_self ((Convex.mem_Ioo h).2 ⟨a, b, ha, hb', hab, rfl⟩)

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: G₀ : Type u_1
inst✝⁴ : GroupWithZero G₀
inst✝³ : Bornology G₀
inst✝² : (cobounded G₀).NeBot
E : Type u_3
inst✝¹ : AddMonoid E
inst✝ : DistribMulAction G₀ E
s : Set E
⊢ Absorbs G₀ s 0 ↔ 0 ∈ s

Tactic:
by
  simp only [absorbs_iff_eventually_cobounded_mapsTo, ← singleton_zero,
    mapsTo_singleton, smul_zero, eventually_const]

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 t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
x : E
hx : x ∈ balancedHull 𝕜 s
⊢ x ∈ t

Tactic:
obtain ⟨r, hr, y, hy, rfl⟩ := mem_balancedHull_iff.1 hx

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
r : 𝕜
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
hx : (fun x ↦ r • x) y ∈ balancedHull 𝕜 s
⊢ (fun x ↦ r • x) y ∈ t
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
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
⊢ (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction

Tactic:
by
  ext v
  rw [Submodule.mem_inf, ← vadd_mem_iff_mem_direction v h₁, ← vadd_mem_iff_mem_direction v h₂, ←
    vadd_mem_iff_mem_direction v ((mem_inf_iff p s₁ s₂).2 ⟨h₁, h₂⟩), mem_inf_iff]

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
t : Set (AffineSubspace k P)
⊢ Submodule.span k (↑(sInf t) -ᵥ ↑(sInf t)) ≤ ⨅ s ∈ t, Submodule.span k (↑s -ᵥ ↑s)

Tactic:
exact le_iInf₂ fun s hs => Submodule.span_mono <| vsub_self_mono <| biInter_subset_of_mem hs

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
inst✝ : Subsingleton P
⊢ affineSpan k s = ⊤ ↔ s.Nonempty

Tactic:
by
  rw [← bot_lt_affineSpan k, IsSimpleOrder.bot_lt_iff_eq_top]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NormedDivisionRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : RegularSpace E
s : Set E
hs : s ∈ 𝓝 0 ∧ IsClosed[inst✝³] s
⊢ IsClosed[inst✝³] (balancedCore 𝕜 s) ∧ Balanced 𝕜 (balancedCore 𝕜 s)

Tactic:
exact ⟨hs.2.balancedCore, balancedCore_balanced s⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : (𝓝 0).HasBasis q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV✝ : V ∈ 𝓝 0
i : ι
hi : q i
hV : s i ⊆ V
⊢ Absorbs 𝕜 V A

Tactic:
exact (hA i hi).mono_left hV

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε

Tactic:
by
  rw [equicontinuousAt_iff_pair]
  constructor <;> intro H
  · intro ε hε
    exact H _ (dist_mem_uniformity hε)
  · intro U hU
    rcases mem_uniformity_dist.mp hU with ⟨ε, hε, hεU⟩
    refine Exists.imp (fun V => And.imp_right fun h => ?_) (H _ hε)
    exact fun x hx x' hx' i => hεU (h _ hx _ hx' i)

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:
by
  rw [eq_top_iff]
  rintro ⟨x, hx⟩ -
  refine affineSpan_induction' (fun y hy ↦ ?_) (fun c u hu v hv w hw ↦ ?_) hx
  · exact subset_affineSpan _ _ hy
  · exact AffineSubspace.smul_vsub_vadd_mem _ _

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 ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ ((s \ s₂).weightedVSubOfPoint p b) w + (s₂.weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w

Tactic:
by
  simp_rw [weightedVSubOfPoint_apply, sum_sdiff h]

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
V₃ : Type u_6
P₃ : Type u_7
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₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
hf : Function.Injective ⇑f
s : AffineSubspace k P₁
p : P₁
⊢ p ∈ comap f (map f s) → p ∈ s

Tactic:
simp; grind

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

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

Tactic:
have hw1 : ∑ i ∈ s, w1 i = 1 := by
      simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
          Finset.sum_const_zero, add_zero]

Goal state after:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
p : ι → P
hnz : ∑ i ∈ s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i ∈ s, w1 i = 1
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

Goal state before:
pp: case right
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
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ p (f' ⟨p x, ⋯⟩) = p x

Tactic:
rw [(hf' _).2]

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

Goal state before:
pp: case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ p₄ ∈ line[k, p₁, p₂]

Tactic:
convert! smul_vsub_vadd_mem_affineSpan_pair ((1 - r₁) * (r₂ - r₁)⁻¹) p₁ p₂

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ p₄ = ((1 - r₁) * (r₂ - r₁)⁻¹) • (p₂ -ᵥ p₁) +ᵥ p₁
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ (⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r

pp: case inr
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ (⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r

Tactic:
· rw [iSup_of_empty', iInter_of_empty, Seminorm.sSup_empty]
    exact closedBall_bot _ hr

Goal state after:
case inr
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ (⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ a • s.centerMass ws zs + b • t.centerMass wt zt =
    (s.disjSum t).centerMass (Sum.elim (fun i ↦ a * ws i) fun j ↦ b * wt j) (Sum.elim zs zt)

Tactic:
s.centerMass_eq_of_sum_1 _ hws,

Goal state after:
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : ∑ i ∈ s, ws i = 1
hwt : ∑ i ∈ t, wt i = 1
a b : R
hab : a + b = 1
⊢ a • ∑ i ∈ s, ws i • zs i + b • t.centerMass wt zt =
    (s.disjSum t).centerMass (Sum.elim (fun i ↦ a * ws i) fun j ↦ b * wt j) (Sum.elim zs zt)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case pos
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 ι
h : (p '' s₂).Subsingleton
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
exact ⟨h₁, Set.subsingleton_of_image ha.injective s₂ h⟩

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
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
t : 𝕜
ht1 : 1 < t
ht : (AffineMap.lineMap x y) t ∈ closure s
⊢ y ∈ openSegment 𝕜 ((AffineMap.lineMap x y) 0) ((AffineMap.lineMap x y) t)

Tactic:
← image_openSegment

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
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
t : 𝕜
ht1 : 1 < t
ht : (AffineMap.lineMap x y) t ∈ closure s
⊢ y ∈ ⇑(AffineMap.lineMap x y) '' openSegment 𝕜 0 t