mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ ⨅ s, ⨅ (_ : s ∈ image2 (fun K U ↦ {f | MapsTo (⇑f) K U}) {K | IsCompact K} {t | IsOpen[inst✝] t} ∧ f ∈ s), 𝓟 s =
    ⨅ K, ⨅ (_ : IsCompact K), ⨅ U, ⨅ (_ : IsOpen[inst✝] U), ⨅ (_ : MapsTo (⇑f) K U), 𝓟 {g | MapsTo (⇑g) K U}

Tactic:
iInf_and,

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ ⨅ s ∈ image2 (fun K U ↦ {f | MapsTo (⇑f) K U}) {K | IsCompact K} {t | IsOpen[inst✝] t}, ⨅ (_ : f ∈ s), 𝓟 s =
    ⨅ K, ⨅ (_ : IsCompact K), ⨅ U, ⨅ (_ : IsOpen[inst✝] U), ⨅ (_ : MapsTo (⇑f) K U), 𝓟 {g | MapsTo (⇑g) K U}
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
| r ^ n * ‖f N‖

Tactic:
← zero_add N

Goal state after:
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
| r ^ n * ‖f (0 + N)‖
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
⊢ ∃ f, Tendsto F l (𝓝 f)

Tactic:
have h :
      ∀ (s₁) (hs₁ : IsCompact s₁) (s₂) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
        f s₁ hs₁ ⟨x, hxs₁⟩ = f s₂ hs₂ ⟨x, hxs₂⟩ := by
      rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
      have := isCompact_iff_compactSpace.mp hs₁
      have := isCompact_iff_compactSpace.mp hs₂
      have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
      have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
      exact tendsto_nhds_unique h₁ h₂

Goal state after:
case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
⊢ ∃ f, Tendsto F l (𝓝 f)
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace (X × Y)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹]
    ((Function.uncurry fun x y ↦ (Function.uncurry (fun x y ↦ x.curry y) x) y) ∘
      ⇑(Homeomorph.prodAssoc C(X × Y, Z) X Y).symm)

Tactic:
exact continuous_eval

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i • z i

Tactic:
have hfa' : Monotone fun n ↦ -f n := fun _ _ hab ↦ neg_le_neg <| hfa hab
  have hf0' : Tendsto (fun n ↦ -f n) atTop (𝓝 0) := by
    convert! hf0.neg
    simp
  convert! (hfa'.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0' hzb).neg
  simp

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ ((Path.pi γ₀).trans (Path.pi γ₁)) t i = (Path.pi fun i ↦ (γ₀ i).trans (γ₁ i)) t i

Tactic:
unfold Path.trans

Goal state after:
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ { toFun := (fun t ↦ if t ≤ 1 / 2 then (Path.pi γ₀).extend (2 * t) else (Path.pi γ₁).extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      t i =
    (Path.pi fun i ↦
        { toFun := (fun t ↦ if t ≤ 1 / 2 then (γ₀ i).extend (2 * t) else (γ₁ i).extend (2 * t - 1)) ∘ Subtype.val,
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ })
      t i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : √(cos (arcsin x) ^ 2) = √(1 - sin (arcsin x) ^ 2)
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
sq,

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : √(cos (arcsin x) * cos (arcsin x)) = √(1 - sin (arcsin x) ^ 2)
⊢ cos (arcsin x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

pp: case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
· rw [not_le] at hx₁
    rw [arccos_of_le_neg_one hx₁.le, sin_pi, sqrt_eq_zero_of_nonpos]
    nlinarith

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case pos
x y : ℂ
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 1⁻¹

Tactic:
simp [exp_neg]

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

Goal state before:
pp: case neg
x y : ℂ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0⁻¹

Tactic:
simp [exp_neg]

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

Goal state before:
pp: case neg
x y : ℂ
h✝ : ¬x = 0
⊢ cexp (-(log x * y)) = (cexp (log x * y))⁻¹

Tactic:
simp [exp_neg]

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

Goal state before:
pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im

Tactic:
· simp only [him.not_ge]
    rw [iff_false, not_le, arg_of_re_neg_of_im_neg hre him, sub_lt_iff_lt_add', ←
      sub_eq_add_neg, sub_half, Real.arcsin_lt_pi_div_two, div_lt_one, neg_im, ← abs_of_neg him,
      abs_im_lt_norm]
    exacts [hre.ne, norm_pos_iff.mpr <| ne_of_apply_ne re hre.ne]

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

Goal state before:
pp: x n : ℂ
⊢ (x ^ n)⁻¹ = if x.arg = π then (starRingEnd ℂ) (x⁻¹ ^ (starRingEnd ℂ) n) else x⁻¹ ^ n

Tactic:
by
  rw [inv_cpow_eq_ite, apply_ite conj, conj_conj, conj_conj]
  split_ifs with h
  · rfl
  · rw [inv_cpow _ _ h]

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

Goal state before:
pp: θ : Angle
⊢ θ.toReal = π ↔ θ.toReal = (↑π).toReal

Tactic:
toReal_pi

Goal state after:
θ : Angle
⊢ θ.toReal = π ↔ θ.toReal = π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
⊢ ContinuousAt (fun z ↦ ↑z.arg + ↑π) (-x)

Tactic:
replace hs := mem_slitPlane_iff.mpr.mt hs

Goal state after:
case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt (fun z ↦ ↑z.arg + ↑π) (-x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
⊢ x ^ y = rexp (log x * y) * cos (y * π)

Tactic:
rw [rpow_def, Complex.cpow_def, if_neg]

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y) * cos (y * π)

case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬↑x = 0
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 ^ w‖ = 0

Tactic:
zero_cpow,

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.Real

Goal state before:
pp: x : ℝ
⊢ x ^ (-1) = x⁻¹

Tactic:
rpow_neg_eq_inv_rpow,

Goal state after:
x : ℝ
⊢ x⁻¹ ^ 1 = x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
n : ℤ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul, rpow_intCast]

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

Goal state before:
pp: x : ℝ≥0
y : ℝ
n : ℤ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
rw [rpow_mul, rpow_intCast]

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

Goal state before:
pp: x y z : ℝ
hx : 1 < x
⊢ x ^ y < x ^ z ↔ y < z

Tactic:
lt_iff_not_ge,

Goal state after:
x y z : ℝ
hx : 1 < x
⊢ ¬x ^ z ≤ x ^ y ↔ y < z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ x ^ y < x ^ z ↔ z < y

Tactic:
lt_iff_not_ge,

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ ¬x ^ z ≤ x ^ y ↔ z < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ∞
⊢ x ^ (y + -z) = x ^ y / x ^ z

Tactic:
rpow_add _ _ hx h'x,

Goal state after:
x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ∞
⊢ x ^ y * x ^ (-z) = x ^ y / x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
⊢ (x / y) ^ z = x ^ z / y ^ z

Tactic:
rw [div_eq_mul_inv, mul_rpow_of_nonneg _ _ hz, inv_rpow, div_eq_mul_inv]

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

Goal state before:
pp: case inr
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ log x ≤ x ^ ε / ε

Tactic:
rw [le_div_iff₀' hε]

Goal state after:
case inr
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ ε * log x ≤ x ^ ε
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ (-s).re ≠ 0

Tactic:
rw [neg_re]

Goal state after:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ (-s).re ≤ 0

Tactic:
rw [neg_re]

Goal state after:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
rw [coe_le_one_iff] at hx1

Goal state after:
case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos
z : ℝ
H : z < 0
x : ℝ≥0
hx : x = 0
⊢ (↑x ^ z).toNNReal = (↑x).toNNReal ^ z

Tactic:
simp [hx, H, ne_of_lt]

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

Goal state before:
pp: x : ℝ≥0∞
n : ℤ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul, rpow_intCast]

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

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
n : ℤ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
rw [rpow_mul, rpow_intCast]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case hu
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
hu : ↑u < 0
v : Ray R M
⊢ 0 < -↑u

Tactic:
Right.neg_pos_iff

Goal state after:
case hu
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
hu : ↑u < 0
v : Ray R M
⊢ ↑u < 0
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.inl.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
exfalso
      simp [hm0, hy, hm1.ne] at hm

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ insert x (insert y (openSegment 𝕜 x y))

Tactic:
refine hb.eq_or_lt.imp ?_ fun hb' => ha.eq_or_lt.imp ?_ fun ha' => ?_

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 = b → a • x + b • y = x

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
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
⊢ 0 = a → a • x + b • y = y

case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
ha' : 0 < a
⊢ a • x + b • y ∈ openSegment 𝕜 x y
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : AffineSpace V2 P2
inst✝⁷ : AddCommGroup V3
inst✝⁶ : AffineSpace V3 P3
inst✝⁵ : Module k V1
inst✝⁴ : Module k V2
inst✝³ : Module k V3
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
f : V1 →ᵃ[k] V2
p✝ : V1
⊢ ((fun p ↦ p.2.toAffineMap + const k V1 p.1) ((fun f ↦ (f 0, f.linear)) f)) p✝ = f p✝

Tactic:
f.decomp

Goal state after:
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : AffineSpace V2 P2
inst✝⁷ : AddCommGroup V3
inst✝⁶ : AffineSpace V3 P3
inst✝⁵ : Module k V1
inst✝⁴ : Module k V2
inst✝³ : Module k V3
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
f : V1 →ᵃ[k] V2
p✝ : V1
⊢ ((fun p ↦ p.2.toAffineMap + const k V1 p.1) ((fun f ↦ (f 0, f.linear)) f)) p✝ = (⇑f.linear + fun x ↦ f 0) 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 : Set P
h : vectorSpan k s = ⊥
hns : ¬s.Subsingleton
⊢ False

Tactic:
Set.not_subsingleton_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
s : Set P
h : vectorSpan k s = ⊥
hns : s.Nontrivial
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case refine_1
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
⊢ ↑s -ᵥ ↑s ⊆ (fun x ↦ x -ᵥ p) '' ↑s

pp: case refine_2
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
⊢ (fun x ↦ x -ᵥ p) '' ↑s ⊆ ↑s -ᵥ ↑s

Tactic:
· rintro v ⟨p₁, hp₁, p₂, hp₂, rfl⟩
    exact ⟨(p₁ -ᵥ p₂) +ᵥ p,
      vadd_mem_of_mem_direction (vsub_mem_direction hp₁ hp₂) hp, vadd_vsub _ _⟩

Goal state after:
case refine_2
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
⊢ (fun x ↦ x -ᵥ p) '' ↑s ⊆ ↑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
ι : Sort u_4
s : Set (AffineSubspace k P)
c : k
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ ⋂ s' ∈ s, ↑s'
hp₂ : p₂ ∈ ⋂ s' ∈ s, ↑s'
hp₃ : p₃ ∈ ⋂ s' ∈ s, ↑s'
s₂ : AffineSubspace k P
hs₂ : s₂ ∈ s
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ ↑s₂

Tactic:
rw [Set.mem_iInter₂] at *
        exact s₂.smul_vsub_vadd_mem c (hp₁ s₂ hs₂) (hp₂ s₂ hs₂) (hp₃ s₂ 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
S : AffineSpace V P
s : Set P
hs : s.Nonempty
⊢ affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤

Tactic:
refine ⟨vectorSpan_eq_top_of_affineSpan_eq_top k V P, ?_⟩
  intro h
  suffices Nonempty (affineSpan k s) by
    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]
  obtain ⟨x, hx⟩ := hs
  exact ⟨⟨x, mem_affineSpan k hx⟩⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
x✝¹ : 𝕜
x✝ : ‖x✝¹‖ ≤ 1
⊢ x✝¹ • ∅ ⊆ ∅

Tactic:
by rw [smul_set_empty]

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
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
⊢ Balanced 𝕜 (balancedCoreAux 𝕜 s)

Tactic:
rintro a ha x ⟨y, hy, rfl⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCoreAux 𝕜 s
⊢ (fun x ↦ a • x) y ∈ balancedCoreAux 𝕜 s
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 ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ (s.weightedVSubOfPoint p (p j)) w₁ = (s.weightedVSubOfPoint p (p j)) w₂

Tactic:
simp only [Finset.weightedVSubOfPoint_apply]

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
s : Finset ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ ∑ i ∈ s, w₁ i • (p i -ᵥ p j) = ∑ i ∈ s, w₂ i • (p i -ᵥ p j)
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
x : P
hx : x ∈ affineSpan k A
⊢ ⟨x, hx⟩ ∈ affineSpan k (Subtype.val ⁻¹' A)

Tactic:
refine affineSpan_induction' (fun y hy ↦ ?_) (fun c u hu v hv w hw ↦ ?_) hx

Goal state after:
case refine_1
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
x : P
hx : x ∈ affineSpan k A
y : P
hy : y ∈ A
⊢ ⟨y, ⋯⟩ ∈ affineSpan k (Subtype.val ⁻¹' A)

case refine_2
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
x : P
hx : x ∈ affineSpan k A
c : k
u : P
hu : u ∈ affineSpan k A
v : P
hv : v ∈ affineSpan k A
w : P
hw : w ∈ affineSpan k A
⊢ ⟨u, hu⟩ ∈ affineSpan k (Subtype.val ⁻¹' A) →
    ⟨v, hv⟩ ∈ affineSpan k (Subtype.val ⁻¹' A) →
      ⟨w, hw⟩ ∈ affineSpan k (Subtype.val ⁻¹' A) → ⟨c • (u -ᵥ v) +ᵥ w, ⋯⟩ ∈ affineSpan k (Subtype.val ⁻¹' A)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ (((Finset.subtype pred s).weightedVSubOfPoint (fun i ↦ p ↑i) (Classical.choice ⋯)) fun i ↦ w ↑i) +ᵥ
      Classical.choice ⋯ =
    ({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice ⋯)) w +ᵥ Classical.choice ⋯

Tactic:
weightedVSubOfPoint_subtype_eq_filter

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
s : Finset ι
w : ι → k
p : ι → P
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ ({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice ⋯)) w +ᵥ Classical.choice ⋯ =
    ({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice ⋯)) w +ᵥ Classical.choice ⋯
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i j t : ι
hi : t ≠ i
hj : t ≠ j
⊢ weightedVSubVSubWeights k i j t = 0

Tactic:
by simp [weightedVSubVSubWeights, hi, hj]

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

Goal state before:
pp: case neg
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
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
hc : ↑(#{i₁, i₂}) ≠ 0
⊢ ({i₁, i₂}.weightedVSubOfPoint p (p i₁)) (centroidWeights k {i₁, i₂}) +ᵥ p i₁ = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁

Tactic:
simp [h, one_add_one_eq_two]

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
p1 : P
p : ι → P
⊢ p1 ∈ affineSpan k (Set.range p) ↔ ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w

Tactic:
by
  constructor
  · exact eq_affineCombination_of_mem_affineSpan
  · rintro ⟨s, w, hw, rfl⟩
    exact affineCombination_mem_affineSpan hw p

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

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 : Set P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
⊢ LinearIndependent k fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩

Tactic:
let f : { x : s // x ≠ ⟨p₁, hp₁⟩ } → (fun p : P => (p -ᵥ p₁ : V)) '' (s \ {p₁}) := fun x =>
      ⟨((x : s) : P) -ᵥ p₁, ⟨x, ⟨⟨(x : s).property, fun hx => x.property (Subtype.ext hx)⟩, rfl⟩⟩⟩

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 : Set P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
f : { x // x ≠ ⟨p₁, hp₁⟩ } → ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁})) := fun x ↦ ⟨↑↑x -ᵥ p₁, ⋯⟩
⊢ LinearIndependent k fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
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✝ : DecidableEq ι
i j : ι
⊢ (b.coord i) (b j) = if i = j then 1 else 0

Tactic:
rcases eq_or_ne i j with h | h <;> simp [h]

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

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Subsingleton ι
i : ι
q : P
hp : (range ⇑b).Subsingleton
this : Subsingleton P
s : Finset ι := {i}
⊢ i ∈ s

Tactic:
simp [s]

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

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Subsingleton ι
i : ι
q : P
hp : (range ⇑b).Subsingleton
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
⊢ s.sum (Function.const ι 1) = 1

Tactic:
simp [s]

Goal state after: