mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case «0»
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₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₃, p₂, p₁] ∘ ⇑(Equiv.swap 0 2)) ((fun i ↦ i) ⟨0, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₃, p₂, p₁] ∘ ⇑(Equiv.swap 0 2)) ((fun i ↦ i) ⟨1, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₃, p₂, p₁] ∘ ⇑(Equiv.swap 0 2)) ((fun i ↦ i) ⟨2, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
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₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₃, p₂, p₁] ∘ ⇑(Equiv.swap 0 2)) ((fun i ↦ i) ⟨0, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨0, ⋯⟩)

case «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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₃, p₂, p₁] ∘ ⇑(Equiv.swap 0 2)) ((fun i ↦ i) ⟨1, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨1, ⋯⟩)

case «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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ (![p₃, p₂, p₁] ∘ ⇑(Equiv.swap 0 2)) ((fun i ↦ i) ⟨2, ⋯⟩) = ![p₁, p₂, p₃] ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x
x : E
hx : ∃ j ∈ s, (p j) x ≠ 0
⊢ q x ≤ (C • s.sup p) x

Tactic:
rcases hx with ⟨j, hj, hjx⟩

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x
x : E
j : ι
hj : j ∈ s
hjx : (p j) x ≠ 0
⊢ q x ≤ (C • s.sup p) x
Module: Mathlib.Analysis.Convex.PathConnected

Goal state before:
pp: case e'_2
x y : ℝ
h : x < y
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ico 0 1
⊢ a✝¹ * (y - x) + x = (y - x) * a✝¹ + x

pp: case e'_3.e'_3
x y : ℝ
h : x < y
⊢ x = (y - x) * 0 + x

pp: case e'_3.e'_4
x y : ℝ
h : x < y
⊢ y = (y - x) * 1 + x

Tactic:
<;>

Goal state after:
case e'_2
x y : ℝ
h : x < y
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ico 0 1
⊢ a✝¹ * (y - x) + x = (y - x) * a✝¹ + x

case e'_3.e'_3
x y : ℝ
h : x < y
⊢ x = (y - x) * 0 + x

case e'_3.e'_4
x y : ℝ
h : x < y
⊢ y = (y - x) * 1 + x
Module: Mathlib.Analysis.Convex.PathConnected

Goal state before:
pp: case e'_2
x y : ℝ
h : x < y
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioc 0 1
⊢ a✝¹ * (y - x) + x = (y - x) * a✝¹ + x

pp: case e'_3.e'_3
x y : ℝ
h : x < y
⊢ x = (y - x) * 0 + x

pp: case e'_3.e'_4
x y : ℝ
h : x < y
⊢ y = (y - x) * 1 + x

Tactic:
<;>

Goal state after:
case e'_2
x y : ℝ
h : x < y
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioc 0 1
⊢ a✝¹ * (y - x) + x = (y - x) * a✝¹ + x

case e'_3.e'_3
x y : ℝ
h : x < y
⊢ x = (y - x) * 0 + x

case e'_3.e'_4
x y : ℝ
h : x < y
⊢ y = (y - x) * 1 + x
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: case refine_2
R : Type u_1
ι : Type u_2
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ stdSimplex R ι ⊆ (convexHull R) (range fun i j ↦ if i = j then 1 else 0)

Tactic:
rintro w ⟨hw₀, hw₁⟩
    rw [pi_eq_sum_univ w]
    rw [← Finset.univ.centerMass_eq_of_sum_1 _ hw₁]
    exact Finset.univ.centerMass_mem_convexHull (fun i _ => hw₀ i) (hw₁.symm ▸ zero_lt_one)
      fun i _ => mem_range_self i

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

Goal state before:
pp: case refine_2
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
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
x✝ : (affineCombination k univ s.points) w ∈ Simplex.setInterior I s
⊢ (affineCombination k univ ((s.points ∘ ⇑e.symm) ∘ ⇑e.toEmbedding)) ((w ∘ ⇑e.symm) ∘ ⇑e.toEmbedding) ∈
    Simplex.setInterior I (s.reindex e)

Tactic:
← Finset.univ.affineCombination_map e.toEmbedding,

Goal state after:
case refine_2
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
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
x✝ : (affineCombination k univ s.points) w ∈ Simplex.setInterior I s
⊢ (affineCombination k (Finset.map e.toEmbedding univ) (s.points ∘ ⇑e.symm)) (w ∘ ⇑e.symm) ∈
    Simplex.setInterior I (s.reindex e)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case e_f.inl
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
val✝ : ι
⊢ Sum.elim (fun x ↦ a • ws x • zs x) (fun x ↦ b • wt x • zt x) (Sum.inl val✝) =
    Sum.elim (fun i ↦ a * ws i) (fun j ↦ b * wt j) (Sum.inl val✝) • Sum.elim zs zt (Sum.inl val✝)

pp: case e_f.inr
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
val✝ : ι'
⊢ Sum.elim (fun x ↦ a • ws x • zs x) (fun x ↦ b • wt x • zt x) (Sum.inr val✝) =
    Sum.elim (fun i ↦ a * ws i) (fun j ↦ b * wt j) (Sum.inr val✝) • Sum.elim zs zt (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case e_f.inl
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
val✝ : ι
⊢ Sum.elim (fun x ↦ a • ws x • zs x) (fun x ↦ b • wt x • zt x) (Sum.inl val✝) =
    Sum.elim (fun i ↦ a * ws i) (fun j ↦ b * wt j) (Sum.inl val✝) • Sum.elim zs zt (Sum.inl val✝)

case e_f.inr
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
val✝ : ι'
⊢ Sum.elim (fun x ↦ a • ws x • zs x) (fun x ↦ b • wt x • zt x) (Sum.inr val✝) =
    Sum.elim (fun i ↦ a * ws i) (fun j ↦ b * wt j) (Sum.inr val✝) • Sum.elim zs zt (Sum.inr val✝)
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case inl
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
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
j : Fin (n + 1)
⊢ Pi.single j 1 j ∈ Set.Icc 0 1

pp: case inr
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
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
i j : Fin (n + 1)
hj : j ≠ i
⊢ Pi.single i 1 j ∈ Set.Icc 0 1

Tactic:
<;>

Goal state after:
case inl
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
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
j : Fin (n + 1)
⊢ Pi.single j 1 j ∈ Set.Icc 0 1

case inr
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
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
i j : Fin (n + 1)
hj : j ≠ i
⊢ Pi.single i 1 j ∈ Set.Icc 0 1
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : ↥t → k
hw : ∑ i, w i = 0
i : ↥t
hi : ¬w i = 0
hwt : ∑ x, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx ↦ w ⟨x, hx⟩
this : (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) = 0
x : V
a✝ hx : x ∈ t
⊢ (fun x ↦ if hx : x ∈ t then f x hx else 0) x • x = if hx : x ∈ t then f x hx • x else 0

pp: case neg
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : ↥t → k
hw : ∑ i, w i = 0
i : ↥t
hi : ¬w i = 0
hwt : ∑ x, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx ↦ w ⟨x, hx⟩
this : (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) = 0
x : V
a✝ : x ∈ t
hx : x ∉ t
⊢ (fun x ↦ if hx : x ∈ t then f x hx else 0) x • x = if hx : x ∈ t then f x hx • x else 0

Tactic:
<;>

Goal state after:
case pos
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : ↥t → k
hw : ∑ i, w i = 0
i : ↥t
hi : ¬w i = 0
hwt : ∑ x, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx ↦ w ⟨x, hx⟩
this : (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) = 0
x : V
a✝ hx : x ∈ t
⊢ (fun x ↦ if hx : x ∈ t then f x hx else 0) x • x = if hx : x ∈ t then f x hx • x else 0

case neg
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : ↥t → k
hw : ∑ i, w i = 0
i : ↥t
hi : ¬w i = 0
hwt : ∑ x, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx ↦ w ⟨x, hx⟩
this : (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) = 0
x : V
a✝ : x ∈ t
hx : x ∉ t
⊢ (fun x ↦ if hx : x ∈ t then f x hx else 0) x • x = if hx : x ∈ t then f x hx • x else 0
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: case l_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
⊢ Function.LeftInverse ⇑(homothety x t) ⇑(homothety x t⁻¹)

pp: case r_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
⊢ Function.RightInverse ⇑(homothety x t) ⇑(homothety x t⁻¹)

Tactic:
<;>

Goal state after:
case l_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
⊢ Function.LeftInverse ⇑(homothety x t) ⇑(homothety x t⁻¹)

case r_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
⊢ Function.RightInverse ⇑(homothety x t) ⇑(homothety x t⁻¹)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → V
hp : AffineIndependent k p
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (w₁ - w₂) i = 0

pp: case refine_2
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → V
hp : AffineIndependent k p
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (w₁ - w₂) i • p i = 0

Tactic:
<;>

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → V
hp : AffineIndependent k p
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (w₁ - w₂) i = 0

case refine_2
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → V
hp : AffineIndependent k p
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (w₁ - w₂) i • p i = 0
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: case l_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
e : P
⊢ (homothety x t) ((homothety x t⁻¹) e) = e

pp: case r_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
e : P
⊢ (homothety x t⁻¹) ((homothety x t) e) = e

Tactic:
<;>

Goal state after:
case l_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
e : P
⊢ (homothety x t) ((homothety x t⁻¹) e) = e

case r_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
e : P
⊢ (homothety x t⁻¹) ((homothety x t) e) = e
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w₁ w₂ : V → k
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i
i : V
hi : i ∈ s
⊢ ∑ x ∈ s, (w₁ - w₂) x = 0

pp: case refine_2
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w₁ w₂ : V → k
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i
i : V
hi : i ∈ s
⊢ ∑ x ∈ s, (w₁ - w₂) x • x = 0

Tactic:
<;>

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w₁ w₂ : V → k
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i
i : V
hi : i ∈ s
⊢ ∑ x ∈ s, (w₁ - w₂) x = 0

case refine_2
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w₁ w₂ : V → k
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i
i : V
hi : i ∈ s
⊢ ∑ x ∈ s, (w₁ - w₂) x • x = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case pos
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
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0
hp' : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
i : Fin (n + 1)
hi : i ∈ fs
⊢ w i ∈ Set.Icc 0 1

pp: case neg
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
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0
hp' : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
i : Fin (n + 1)
hi : i ∉ fs
⊢ w i ∈ Set.Icc 0 1

Tactic:
<;>

Goal state after:
case pos
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
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0
hp' : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
i : Fin (n + 1)
hi : i ∈ fs
⊢ w i ∈ Set.Icc 0 1

case neg
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
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0
hp' : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
i : Fin (n + 1)
hi : i ∉ fs
⊢ w i ∈ Set.Icc 0 1
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
ha : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
c : k
⊢ (affineCombination k s p) w = (AffineMap.lineMap ((affineCombination k s p) w₁) ((affineCombination k s p) w₂)) c ↔
    ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i)) c

Tactic:
by
  rw [← AffineMap.apply_lineMap, ha.affineCombination_eq_iff_eq hw]
  · simp [AffineMap.lineMap_apply]
  · simp [AffineMap.lineMap_apply, sum_add_distrib, ← mul_sum, hw₁, hw₂]

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
⊢ nhdsKer (s ×ˢ t) = ⋃ p ∈ s ×ˢ t, nhdsKer {p}

Tactic:
by
    conv_lhs => rw [← biUnion_of_singleton (s ×ˢ t), nhdsKer_biUnion]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ IsOpen[inst✝¹] (⋂₀ {t | IsOpen[inst✝¹] t ∧ s ⊆ t})

Tactic:
exact isOpen_sInter fun _ ↦ And.left

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

Goal state before:
pp: case neg.convert_3.inl
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
h✝ : i = x
⊢ i ∈ s

pp: case neg.convert_3.inr
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
h✝ : i = y
⊢ i ∈ s

Tactic:
<;>

Goal state after:
case neg.convert_3.inl
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
h✝ : i = x
⊢ i ∈ s

case neg.convert_3.inr
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
h✝ : i = y
⊢ i ∈ s
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case neg.convert_3.inl
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ x ∈ s

pp: case neg.convert_3.inr
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ y ∈ s

Tactic:
<;>

Goal state after:
case neg.convert_3.inl
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ x ∈ s

case neg.convert_3.inr
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ y ∈ s
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ ¬w i ≠ 0
⊢ ∀ i ∈ s, w i = 0

Tactic:
Classical.not_not

Goal state after:
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
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ w i = 0
⊢ ∀ i ∈ s, w i = 0