mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)

Tactic:
by rw [smul_add, smul_add, add_add_add_comm]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)

Tactic:
by rw [smul_add, smul_add, add_add_add_comm]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)

Tactic:
by rw [smul_add, smul_add, add_add_add_comm]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝⁸ : SeminormedRing 𝕜
inst✝⁷ : AddGroup E
inst✝⁶ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x✝ : E
r : ℝ
inst✝⁵ : SMul R ℝ
inst✝⁴ : SMul R ℝ≥0
inst✝³ : IsScalarTower R ℝ≥0 ℝ
inst✝² : Preorder R
inst✝¹ : Zero R
inst✝ : IsOrderedModule R ℝ
a b : R
hab : a ≤ b
p : Seminorm 𝕜 E
x : E
⊢ (a • p) x ≤ (b • p) x

Tactic:
grw [smul_apply, hab, smul_apply]

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

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
hf : Function.Surjective ⇑f
⊢ AffineSubspace.map f ⊤ = ⊤

Tactic:
rw [AffineSubspace.ext_iff]

Goal state after:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
hf : Function.Surjective ⇑f
⊢ ↑(AffineSubspace.map f ⊤) = ↑⊤
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
a : 𝕜
x : E
⊢ ⨆ i, ↑i (a • x) = ‖a‖ * ⨆ i, ↑i x

Tactic:
rw [← smul_eq_mul,
            Real.smul_iSup_of_nonneg (norm_nonneg a) fun i : s => (i : Seminorm 𝕜 E) x]

Goal state after:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
a : 𝕜
x : E
⊢ ⨆ i, ↑i (a • x) = ⨆ i, ‖a‖ • ↑i x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
⊢ comap f ⊤ = ⊤

Tactic:
rw [AffineSubspace.ext_iff]

Goal state after:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
⊢ ↑(comap f ⊤) = ↑⊤
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case right
ι : 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
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := (↑s).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ((Finsupp.onFinset s w' hwx).sum fun i a ↦ a • (p i -ᵥ p i0)) = ∑ i ∈ s, w i • (p i -ᵥ p i0)

Tactic:
Finsupp.onFinset_sum hwx

Goal state after:
case right
ι : 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
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := (↑s).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∑ a ∈ s, w' a • (p a -ᵥ p i0) = ∑ i ∈ s, w i • (p i -ᵥ p i0)

case right
ι : 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
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := (↑s).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∀ (a : ι), 0 • (p a -ᵥ p i0) = 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ (k / k) • x = x

Tactic:
div_self (norm_pos_iff.mp hk),

Goal state after:
case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ 1 • x = x
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
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0

Tactic:
← Finset.sum_indicator_subset w1 (s1.subset_union_left (s₂ := s2))

Goal state after:
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
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1 ∪ s2, (↑s1).indicator w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0
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
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ (↑s1).indicator w1 i = (↑s2).indicator w2 i

Tactic:
rw [← sub_eq_zero]
        rw [← Finset.sum_indicator_subset w1 (s1.subset_union_left (s₂ := s2))] at hw1
        rw [← Finset.sum_indicator_subset w2 (s1.subset_union_right)] at hw2
        have hws : (∑ i ∈ s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i) = 0 := by
          simp [hw1, hw2]
        rw [Finset.affineCombination_indicator_subset w1 p (s1.subset_union_left (s₂ := s2)),
          Finset.affineCombination_indicator_subset w2 p s1.subset_union_right,
          ← @vsub_eq_zero_iff_eq V, Finset.affineCombination_vsub] at heq
        exact ha (s1 ∪ s2) (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) hws heq i hi

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

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty ↥E
φ : P₁ →ᵃ[k] P₂
⊢ Nonempty ↥(map φ E)

Tactic:
obtain ⟨x, hx⟩ := id Ene
  exact ⟨⟨φ x, AffineSubspace.mem_map.mpr ⟨x, hx, rfl⟩⟩⟩

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
hw : s.sum (Function.const ι 1) = 1
hq : q = (Finset.affineCombination k s ⇑b) (Function.const ι 1)
⊢ (b.coord i) q = 1 q

Tactic:
rw [Pi.one_apply, hq, b.coord_apply_combination_of_mem hi hw, Function.const_apply]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ (normSeminorm 𝕜 E).ball = Metric.ball

Tactic:
ext x r y
  simp only [Seminorm.mem_ball, Metric.mem_ball, coe_normSeminorm, dist_eq_norm]

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
a b : E
⊢ Continuous fun t ↦ ↑t • (b - a) + a

Tactic:
fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected {0}ᶜ
⊢ ⇑(p.prodEquivOfIsCompl q hpq) '' {0}ᶜ ×ˢ univ = Subtype.val '' {0}ᶜ + ↑q

Tactic:
· ext
    simp [mem_add, and_assoc]

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : OrderClosedTopology 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ Continuous fun f ↦ ∑ x, f x

Tactic:
fun_prop

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

Goal state before:
pp: case inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Subsingleton ι
h : Nonempty ι
⊢ Metric.diam (stdSimplex ℝ ι) = 0

Tactic:
| inr h =>

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
⊢ False

Tactic:
have hw' : ∑ t ∈ fs.map (Embedding.subtype _), w' t = 0 := by
    simp only [sum_map, Embedding.subtype_apply, ← hw]
    exact sum_congr rfl fun t ht ↦ by simp [w']

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
hw' : ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t = 0
⊢ False
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : TopologicalSpace V
inst✝² : Torsor V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
p : P
⊢ Continuous[instTopologicalSpaceProd, inst✝³] fun x ↦ x.1 • x.2 • p /ₛ p

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : TopologicalSpace V
inst✝² : Torsor V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
p : P
⊢ Continuous[inst✝³, inst✝³] fun v ↦ p /ₛ v • p

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
α : Type u_3
inst✝⁵ : Group V
inst✝⁴ : TopologicalSpace V
inst✝³ : Torsor V P
inst✝² : TopologicalSpace P
inst✝¹ : IsTopologicalTorsor P
inst✝ : TopologicalSpace α
p : P
this : IsTopologicalGroup V
⊢ Continuous[inst✝⁴, inst✝²] (Equiv.constSDiv p).invFun

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
α : Type u_3
inst✝⁵ : Group V
inst✝⁴ : TopologicalSpace V
inst✝³ : Torsor V P
inst✝² : TopologicalSpace P
inst✝¹ : IsTopologicalTorsor P
inst✝ : TopologicalSpace α
p : P
⊢ Continuous[inst✝⁴, inst✝²] (Equiv.constSDiv p).invFun

Tactic:
have := IsTopologicalTorsor.to_isTopologicalGroup V P
    fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦ x.1 / x.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
W : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁹ : CommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : Torsor V P
inst✝⁶ : TopologicalSpace P
inst✝⁵ : IsTopologicalTorsor P
inst✝⁴ : CommGroup W
inst✝³ : TopologicalSpace W
inst✝² : Torsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalTorsor Q
⊢ Continuous[instTopologicalSpaceProd, inst✝⁶] fun p ↦ p.1.1 • p.2.1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
W : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁹ : CommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : Torsor V P
inst✝⁶ : TopologicalSpace P
inst✝⁵ : IsTopologicalTorsor P
inst✝⁴ : CommGroup W
inst✝³ : TopologicalSpace W
inst✝² : Torsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalTorsor Q
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ p.1.2 • p.2.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
W : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁹ : CommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : Torsor V P
inst✝⁶ : TopologicalSpace P
inst✝⁵ : IsTopologicalTorsor P
inst✝⁴ : CommGroup W
inst✝³ : TopologicalSpace W
inst✝² : Torsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalTorsor Q
⊢ Continuous[instTopologicalSpaceProd, inst✝⁸] fun x ↦ x.1.1 /ₛ x.2.1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
W : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁹ : CommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : Torsor V P
inst✝⁶ : TopologicalSpace P
inst✝⁵ : IsTopologicalTorsor P
inst✝⁴ : CommGroup W
inst✝³ : TopologicalSpace W
inst✝² : Torsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalTorsor Q
⊢ Continuous[instTopologicalSpaceProd, inst✝³] fun x ↦ x.1.2 /ₛ x.2.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: ι : Type u_1
V : ι → Type u_2
P : ι → Type u_3
inst✝⁴ : (i : ι) → CommGroup (V i)
inst✝³ : (i : ι) → TopologicalSpace (V i)
inst✝² : (i : ι) → Torsor (V i) (P i)
inst✝¹ : (i : ι) → TopologicalSpace (P i)
inst✝ : ∀ (i : ι), IsTopologicalTorsor (P i)
⊢ ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst✝¹ i] fun a ↦ a.1 i • a.2 i

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: ι : Type u_1
V : ι → Type u_2
P : ι → Type u_3
inst✝⁴ : (i : ι) → CommGroup (V i)
inst✝³ : (i : ι) → TopologicalSpace (V i)
inst✝² : (i : ι) → Torsor (V i) (P i)
inst✝¹ : (i : ι) → TopologicalSpace (P i)
inst✝ : ∀ (i : ι), IsTopologicalTorsor (P i)
⊢ ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst✝³ i] fun a ↦ a.1 i /ₛ a.2 i

Tactic:
fun_prop

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

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
hp : p ∈ affineSpan k (Set.range (s.map f hf).points)
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, f x = p

pp: case neg
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, f x = p

Tactic:
· obtain ⟨w, hw1, hw⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp
    rw [hw, Affine.Simplex.affineCombination_mem_setInterior_iff hw1, Simplex.map_points,
      ← Finset.map_affineCombination _ _ _ hw1]
    simp_rw [hf.eq_iff]
    simp [Affine.Simplex.affineCombination_mem_setInterior_iff hw1]

Goal state after:
case neg
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, f x = p
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: 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✝³ : Ring R
inst✝² : Module R V
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousSMul R V
⊢ Continuous fun pqt ↦ pqt.2.2 • (pqt.2.1 -ᵥ pqt.1) +ᵥ pqt.1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: 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✝³ : Ring R
inst✝² : Module R V
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousSMul R V
p q : P
⊢ Continuous ⇑(lineMap p q)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: 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✝⁴ : Ring R
inst✝³ : Module R V
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R V
X : Type u_6
inst✝ : TopologicalSpace X
f₁ f₂ : X → P
g : X → R
x : X
h₁ : ContinuousAt f₁ x
h₂ : ContinuousAt f₂ x
hg : ContinuousAt g x
⊢ ContinuousAt (fun x ↦ (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: 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✝⁴ : Ring R
inst✝³ : Module R V
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R V
X : Type u_6
inst✝ : TopologicalSpace X
f₁ f₂ : X → P
g : X → R
s : Set X
h₁ : ContinuousOn f₁ s
h₂ : ContinuousOn f₂ s
hg : ContinuousOn g s
⊢ ContinuousOn (fun x ↦ (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) s

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: 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✝⁴ : Ring R
inst✝³ : Module R V
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R V
X : Type u_6
inst✝ : TopologicalSpace X
f₁ f₂ : X → P
g : X → R
h₁ : Continuous[inst✝, inst✝⁶] f₁
h₂ : Continuous[inst✝, inst✝⁶] f₂
hg : Continuous[inst✝, inst✝²] g
⊢ Continuous[inst✝, inst✝⁶] fun x ↦ (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: 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✝² : CommRing R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
⊢ Continuous fun p ↦ t • (p -ᵥ x) +ᵥ x

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝¹⁰ : Ring 𝕜
inst✝⁹ : LinearOrder 𝕜
inst✝⁸ : IsStrictOrderedRing 𝕜
inst✝⁷ : DenselyOrdered 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : OrderTopology 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous fun θ ↦ (1 - θ) • x + θ • y

Tactic:
fun_prop

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
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
⊢ ∑ i ∈ s, (AffineMap.lineMap w₁ w₂) c i = 1

Tactic:
· simp [AffineMap.lineMap_apply, sum_add_distrib, ← mul_sum, hw₁, hw₂]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝¹³ : Ring 𝕜
inst✝¹² : LinearOrder 𝕜
inst✝¹¹ : IsStrictOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous fun θ ↦ (1 - θ) • x + θ • y

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • closure s + b • interior s ⊆ interior s

Tactic:
rw [add_comm]
  exact hs.combo_interior_closure_subset_interior hb ha (add_comm a b ▸ hab)

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x : X
⊢ nhdsKer {x} = (𝓝 x).ker

Tactic:
by simp [nhdsKer]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocallyPathConnectedSpace X
hF : IsOpen[inst✝¹] F
x : X
⊢ IsOpen[inst✝¹] (pathComponentIn F x)

Tactic:
rw [isOpen_iff_mem_nhds]
  intro y hy
  let ⟨s, hs⟩ := (path_connected_basis y).mem_iff.mp (hF.mem_nhds (pathComponentIn_subset hy))
  exact mem_of_superset hs.1.1 <| pathComponentIn_congr hy ▸
    hs.1.2.subset_pathComponentIn (mem_of_mem_nhds hs.1.1) hs.2

Goal state after: