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

Goal state before:
pp: case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = (↑x.re).arg - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0

Tactic:
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
      simp [hr.not_gt, ← add_eq_zero_iff_eq_neg, Real.pi_ne_zero]

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

Goal state before:
pp: ⊢ π ≠ 0

Tactic:
exact Real.pi_ne_zero

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

Goal state before:
pp: n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ (↑(n • θ.toReal)).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)

Tactic:
nsmul_eq_mul,

Goal state after:
n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ (↑(↑n * θ.toReal)).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) - π =
    if 0 ≤ a✝.im then Real.arcsin ((-a✝).im / ‖a✝‖) + π else Real.arcsin ((-a✝).im / ‖a✝‖) - π

Tactic:
if_neg him.not_ge

Goal state after:
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) - π = Real.arcsin ((-a✝).im / ‖a✝‖) - π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

Tactic:
rw [zero_rpow h, zero_eq_mul]
    have : y ≠ 0 ∨ z ≠ 0 := not_and_or.1 fun ⟨hy, hz⟩ => h <| hy.symm ▸ hz.symm ▸ zero_add 0
    exact this.imp zero_rpow zero_rpow

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

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

Tactic:
simp [rpow_def, Complex.cpow_neg, Complex.inv_cpow_eq_ite, apply_ite]

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

Goal state before:
pp: case inl.inl
hx : 0 ≤ 0
⊢ ↑0 ^ 0 = (-↑0) ^ 0 * cexp (↑π * I * 0)

Tactic:
simp [*]

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

Goal state before:
pp: case inl.inr
y : ℂ
hx : 0 ≤ 0
hy : y ≠ 0
⊢ ↑0 ^ y = (-↑0) ^ y * cexp (↑π * I * y)

Tactic:
simp [*]

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
w : ℂ
⊢ rexp (Real.log ‖z‖ * w.re) / rexp (z.arg * w.im) = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
Real.rpow_def_of_pos (norm_pos_iff.mpr hz)

Goal state after:
z : ℂ
hz : z ≠ 0
w : ℂ
⊢ rexp (Real.log ‖z‖ * w.re) / rexp (z.arg * w.im) = rexp (Real.log ‖z‖ * w.re) / rexp (z.arg * w.im)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 0 ≤ x
⊢ (fun x ↦ (x ^ (s / r')) ^ r') x = (fun x ↦ x ^ s) x

Tactic:
by simp only [← rpow_mul hx, div_mul_cancel₀ _ hr.ne']

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

Goal state before:
pp: x y z : ℝ
hx : 0 = x ∨ 0 < x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z

Tactic:
rcases hx with hx | hx

Goal state after:
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ x ^ z < y ^ z

case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ x ^ z < y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 < y
⊢ x ^ y < 1 ↔ x < 1

Tactic:
by
  rw [← Real.rpow_lt_rpow_iff hx zero_le_one hy, Real.one_rpow]

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

Goal state before:
pp: case inl
y : ℝ
hx : 0 ≤ 0
⊢ 1 < 0 ^ y ↔ 1 < 0 ∧ 0 < y ∨ 0 < 0 ∧ 0 < 1 ∧ y < 0

pp: case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0

Tactic:
· rcases _root_.em (y = 0) with (rfl | hy) <;> simp [*, (zero_lt_one' ℝ).not_gt]

Goal state after:
case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ 0 < z

Tactic:
simpa [hz] using hy

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

Goal state before:
pp: case inr.inr.coe.top.inl
z : ℝ
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
hz : z < 0
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z

Tactic:
simp [*]

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

Goal state before:
pp: case inr.inr.coe.top.inr
z : ℝ
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
hz : 0 < z
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

Goal state before:
pp: b : ℝ
hb : 1 ≤ b
⊢ Monotone fun x ↦ b ^ x

Tactic:
rcases lt_or_eq_of_le hb with hb | rfl

Goal state after:
case inl
b : ℝ
hb✝ : 1 ≤ b
hb : 1 < b
⊢ Monotone fun x ↦ b ^ x

case inr
hb : 1 ≤ 1
⊢ Monotone fun x ↦ 1 ^ x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ ‖↑↑p ^ (-s)‖ ≤ 1 / 2

Tactic:
rw [norm_natCast_cpow_of_re_ne_zero p <| by rw [neg_re]; linarith only [hs]]

Goal state after:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ ↑↑p ^ (-s).re ≤ 1 / 2
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
rw [one_div, ← Real.rpow_neg_one]

Goal state after:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ 2 ^ (-s).re ≤ 2 ^ (-1)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case hr
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π

Tactic:
· linarith [pi_pos, arg_le_pi x]

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

Goal state before:
pp: case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 < ↑x✝
⊢ ↑x✝ ^ z < 1

Tactic:
simp only [one_lt_coe_iff] at hx

Goal state after:
case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 < x✝
⊢ ↑x✝ ^ z < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 < ↑x✝
⊢ 1 < ↑x✝ ^ z

Tactic:
simp only [one_lt_coe_iff] at hx

Goal state after:
case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 < x✝
⊢ 1 < ↑x✝ ^ z
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_5
inst✝⁵ : CommSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : 0 < (algebraMap S R) a
⊢ 0 < 1

Tactic:
by nontriviality R; exact zero_lt_one

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

Goal state before:
pp: case h
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
f : P1 →ᵃ[k] P2
h : f.linear = 0
p✝ : P1
⊢ f p✝ = Function.const P1 (f (Classical.arbitrary P1)) p✝

Tactic:
Function.const_apply,

Goal state after:
case h
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
f : P1 →ᵃ[k] P2
h : f.linear = 0
p✝ : P1
⊢ f p✝ = f (Classical.arbitrary P1)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
⊢ x ∈ openSegment 𝕜 x y ↔ x = y

Tactic:
by
  constructor
  · rintro ⟨a, b, _, hb, hab, hx⟩
    refine smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 ?_)
    rw [hx, ← add_smul, hab, one_smul]
  · rintro rfl
    rw [openSegment_same]
    exact mem_singleton _

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

Goal state before:
pp: case right
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z

Tactic:
simp [*]

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 : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
⊢ StarConvex 𝕜 (z + x) ((fun x ↦ z + x) '' s)

Tactic:
intro y hy a b ha hb hab
  obtain ⟨y', hy', rfl⟩ := hy
  refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩
  match_scalars <;> simp [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 : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
⊢ StarConvex 𝕜 (x + z) ((fun x ↦ x + z) '' s)

Tactic:
intro y hy a b ha hb hab
  obtain ⟨y', hy', rfl⟩ := hy
  refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩
  match_scalars <;> simp [hab]

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

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

Tactic:
exact convex_convexHull 𝕜 _

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
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
h : p ∈ iInf s
⊢ (sInf (range s)).direction = ⨅ i, (s i).direction

Tactic:
direction_sInf_of_mem_sInf _ p h,

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
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
h : p ∈ iInf s
⊢ ⨅ s_1 ∈ range s, s_1.direction = ⨅ i, (s i).direction
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✝¹ : ContinuousSMul 𝕜 E
inst✝ : IsTopologicalAddGroup E
s t : Set E
⊢ IsVonNBounded 𝕜 (s - t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
by
  simp [sub_eq_add_neg, isVonNBounded_add]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ⇑f
⊢ StrictConvex 𝕜 (⇑f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab
  refine hf.image_interior_subset _ ⟨a • x + b • y, hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, ?_⟩
  rw [map_add, f.map_smul_of_tower a, f.map_smul_of_tower b]

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✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
v : V
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun x ↦ p -ᵥ x) p₂ = v
⊢ v ∈ s -ᵥ s

Tactic:
exact ⟨p, hp, p₂, hp₂, hv⟩

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 : Set P
p : P
hp : p ∈ s
⊢ vectorSpan k s = Submodule.span k ((fun x ↦ p -ᵥ x) '' s)

Tactic:
rw [vectorSpan_def]
  refine le_antisymm ?_ (Submodule.span_mono ?_)
  · rw [Submodule.span_le]
    rintro v ⟨p₁, hp₁, p₂, hp₂, hv⟩
    simp_rw [← vsub_sub_vsub_cancel_left p₁ p₂ p] at hv
    rw [← hv, SetLike.mem_coe, Submodule.mem_span]
    exact fun m hm => Submodule.sub_mem _ (hm ⟨p₂, hp₂, rfl⟩) (hm ⟨p₁, hp₁, rfl⟩)
  · rintro v ⟨p₂, hp₂, hv⟩
    exact ⟨p, hp, p₂, hp₂, hv⟩

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
p₁ p₂ : P
v : V
⊢ v +ᵥ p₂ ∈ line[k, p₁, p₂] ↔ ∃ r, r • (p₁ -ᵥ p₂) = v

Tactic:
vadd_mem_iff_mem_direction _ (right_mem_affineSpan_pair _ _ _),

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
p₁ p₂ : P
v : V
⊢ v ∈ line[k, p₁, p₂].direction ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
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 ι
w : ι → k
p : ι → P
i : ι
⊢ ((s.erase i).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w

Tactic:
rw [weightedVSubOfPoint_apply, 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 ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ∑ i_1 ∈ s.erase i, w i_1 • (p i_1 -ᵥ p i) = ∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)
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 ι
w : ι → k
p : ι → P
i : ι
⊢ ((insert i s).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w

Tactic:
rw [weightedVSubOfPoint_apply, 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 ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ∑ i_1 ∈ insert i s, w i_1 • (p i_1 -ᵥ p i) = ∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)
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:
rw [weightedVSubOfPoint_apply, 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
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ ∑ i ∈ s₁, w i • (p i -ᵥ b) = ∑ i ∈ s₂, (↑s₁).indicator w i • (p i -ᵥ b)
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₁ w₂ : ι → k
p : ι → P
⊢ (s.weightedVSub p) w₁ +ᵥ (affineCombination k s p) w₂ =
    (affineCombination k s p).linear w₁ +ᵥ (affineCombination k s p) w₂

Tactic:
affineCombination_linear

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₁ w₂ : ι → k
p : ι → P
⊢ (s.weightedVSub p) w₁ +ᵥ (affineCombination k s p) w₂ = (s.weightedVSub p) w₁ +ᵥ (affineCombination k s p) w₂
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:
by simp; grind

Goal state after:
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 0)) s₁

Tactic:
constVAdd_zero,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ : AffineSubspace k P
v : V
⊢ s₁ = map (↑(AffineEquiv.refl k P)) s₁
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k univ p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0

Tactic:
rw [univ_fin2]
  convert! centroid_pair k p 0 1

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ (if hx : i1 = i1 then -∑ y ∈ s, g y else g ⟨i1, hx⟩) + ∑ x ∈ s, g x = 0

Tactic:
dif_pos rfl

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
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ -∑ y ∈ s, g y + ∑ x ∈ s, g x = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise

Goal state before:
pp: 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
s : AffineSubspace k P
⊢ (v +ᵥ s).direction = s.direction

Tactic:
rw [pointwise_vadd_eq_map, map_direction]

Goal state after:
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
s : AffineSubspace k P
⊢ Submodule.map (↑(AffineEquiv.constVAdd k P v)).linear s.direction = s.direction
Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise

Goal state before:
pp: k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
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₂
v : V₁
s : AffineSubspace k P₁
⊢ map (f.comp ↑(AffineEquiv.constVAdd k P₁ v)) s = map (↑(AffineEquiv.constVAdd k P₂ (f.linear v))) (map f s)

Tactic:
map_map

Goal state after:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
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₂
v : V₁
s : AffineSubspace k P₁
⊢ map (f.comp ↑(AffineEquiv.constVAdd k P₁ v)) s = map ((↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f) s
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
ι : Type u_4
p : ι → P
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i : ι
hi : i ∈ s
⊢ w i = 0

Tactic:
Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p hw (p i1),

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
ι : Type u_4
p : ι → P
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSubOfPoint p (p i1)) w = 0
i : ι
hi : i ∈ s
⊢ w i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mp
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
⊢ (LinearIndependent k fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) →
    LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v

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

Tactic:
· intro h
    have hv : ∀ v : (fun p => (p -ᵥ p₁ : V)) '' (s \ {p₁}), (v : V) +ᵥ p₁ ∈ s \ {p₁} := fun v =>
      (vsub_left_injective p₁).mem_set_image.1 ((vadd_vsub (v : V) p₁).symm ▸ v.property)
    let f : (fun p : P => (p -ᵥ p₁ : V)) '' (s \ {p₁}) → { x : s // x ≠ ⟨p₁, hp₁⟩ } := fun x =>
      ⟨⟨(x : V) +ᵥ p₁, Set.mem_of_mem_sdiff (hv x)⟩, fun hx =>
        Set.notMem_of_mem_sdiff (hv x) (Subtype.ext_iff.1 hx)⟩
    convert!
      h.comp f fun x1 x2 hx =>
        Subtype.ext (vadd_right_cancel p₁ (Subtype.ext_iff.1 (Subtype.ext_iff.1 hx)))
    ext v
    exact (vadd_vsub (v : V) p₁).symm

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