mathlib-initiative/mathlib-tactics huggingface dataset:
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
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
⊢ p i ∈ affineSpan k (p '' s) → i ∈ s

Tactic:
intro hs
    have h :=
      AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan ha hs
        (mem_affineSpan k (Set.mem_image_of_mem _ (Set.mem_singleton _)))
    rwa [← Set.nonempty_def, Set.inter_singleton_nonempty] at h

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.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
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ Simplex.setInterior I (s.reindex e) = Simplex.setInterior I s

Tactic:
by
  ext p
  refine ⟨fun ⟨w, hw, hwI, h⟩ ↦ ?_, fun ⟨w, hw, hwI, h⟩ ↦ ?_⟩
  · subst h
    simp_rw [reindex]
    rw [← Function.comp_id w, ← e.self_comp_symm, ← Function.comp_assoc,
      ← Equiv.coe_toEmbedding, ← Finset.univ.affineCombination_map e.symm.toEmbedding,
      map_univ_equiv]
    have hw' : ∑ i, (w ∘ e) i = 1 := by rwa [sum_comp_equiv, map_univ_equiv]
    rw [affineCombination_mem_setInterior_iff hw']
    exact fun i ↦ hwI (e i)
  · subst h
    rw [← Function.comp_id w, ← Function.comp_id s.points, ← e.symm_comp_self,
      ← Function.comp_assoc, ← Function.comp_assoc, ← e.coe_toEmbedding,
      ← Finset.univ.affineCombination_map e.toEmbedding, map_univ_equiv]
    change Finset.univ.affineCombination k (s.reindex e).points _ ∈ _
    have hw' : ∑ i, (w ∘ e.symm) i = 1 := by rwa [sum_comp_equiv, map_univ_equiv]
    rw [affineCombination_mem_setInterior_iff hw']
    exact fun i ↦ hwI (e.symm i)

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

Goal state before:
pp: case neg.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
⊢ False

pp: case neg.inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
i : ι
his₂ : i ∈ s₂
his₁ : i ∉ s₁
⊢ False

Tactic:
· exact ha.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton his₁ his₂ h₁ h

Goal state after:
case neg.inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
i : ι
his₂ : i ∈ s₂
his₁ : i ∉ s₁
⊢ False
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
ι : Type u_5
ι' : Type u_6
α : Type u_7
inst✝¹¹ : Field R
inst✝¹⁰ : Field R'
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : AddCommGroup α
inst✝⁶ : LinearOrder α
inst✝⁵ : Module R E
inst✝⁴ : Module R F
inst✝³ : Module R α
s : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid α
inst✝ : PosSMulMono R α
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ ∅, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ ∅, w i
⊢ False

Tactic:
simp at hw₁

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.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
inst✝³ : PartialOrder k
inst✝² : Nontrivial k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i j : Fin (n + 1)
⊢ s.points j ∈ (s.faceOpposite i).closedInterior ↔ j ≠ i

Tactic:
by
  simp [faceOpposite]

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

Goal state before:
pp: case hws
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ 0 < ∑ i ∈ s, w i

pp: case hz
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ ∀ i ∈ s, v i ∈ Set.range v

Tactic:
· simp [hw₁]

Goal state after:
case hz
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ ∀ i ∈ s, v i ∈ Set.range v
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ ∃ t ⊆ pathComponentIn u (inl x), IsOpen[instTopologicalSpaceSum] t ∧ inl x ∈ t

Tactic:
refine ⟨Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x, ?_, ?_, ?_⟩
    · apply IsPathConnected.subset_pathComponentIn
      · exact (isPathConnected_pathComponentIn (by exact hxu)).image continuous_inl
      · exact ⟨x, mem_pathComponentIn_self hxu, rfl⟩
      · exact (image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)
    · exact isOpenMap_inl _ <| (hu.preimage continuous_inl).pathComponentIn _
    · exact ⟨x, mem_pathComponentIn_self hxu, rfl⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ IsConnected {y | SameRay ℝ x y}

Tactic:
by_cases hx : x = 0; · simpa [hx] using isConnected_univ (α := E)
  simp_rw [← exists_nonneg_left_iff_sameRay hx]
  exact isConnected_Ici.image _ (by fun_prop)

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

Goal state before:
pp: case neg
R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : (s.sup p) v ≤ 0
⊢ {x | 0 < r} ∈ 𝓝 0

Tactic:
hr

Goal state after:
case neg
R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : (s.sup p) v ≤ 0
⊢ {x | True} ∈ 𝓝 0
Module: Mathlib.Analysis.Convex.Jensen

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
x y z : E
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ [x -[𝕜] y]
⊢ f z ≤ max (f x) (f y)

Tactic:
by
  rw [← convexHull_pair] at hz; simpa using hf.exists_ge_of_mem_convexHull (pair_subset hx hy) hz

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ (𝓝 0).HasBasis (fun sr ↦ 0 < sr.2) fun sr ↦ (sr.1.sup p).ball 0 sr.2

Tactic:
refine ⟨fun V => ?_⟩
  simp only [hp.hasBasis.mem_iff, SeminormFamily.basisSets_iff, Prod.exists, id_eq]
  grind

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

Goal state before:
pp: case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0)
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] ⇑(p i)
⊢ ⨅ i, comap (⇑↑i) (𝓝 0) ≤ 𝓝 0

Tactic:
simp_rw [hp, le_iInf_iff]
      intro i
      exact iInf_le (ι := {p : Seminorm 𝕜 E // Continuous p}) _ ⟨p i, hp' i⟩

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

Goal state before:
pp: case mp
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s) → ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
intro h I
    simp only [id] at h
    specialize h ((I.sup p).ball 0 1) (p.basisSets_mem I zero_lt_one)
    rcases h.exists_pos with ⟨r, hr, h⟩
    obtain ⟨a, ha⟩ := NormedField.exists_lt_norm 𝕜 r
    specialize h a (le_of_lt ha)
    rw [Seminorm.smul_ball_zero (norm_pos_iff.1 <| hr.trans ha), mul_one] at h
    refine ⟨‖a‖, lt_trans hr ha, ?_⟩
    intro x hx
    specialize h hx
    exact (Finset.sup I p).mem_ball_zero.mp h

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
⊢ instUniformSpace σ F 𝔖₁ ≤ instUniformSpace σ F 𝔖₂

Tactic:
simp_rw [uniformSpace_eq]
  exact UniformSpace.comap_mono (UniformOnFun.mono (le_refl _) h)

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₂ F
𝕜₁ : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup G
𝕜₃ : Type u_7
inst✝⁸ : NormedField 𝕜₃
inst✝⁷ : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst✝⁶ : RingHomSurjective τ
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousConstSMul 𝕜₂ F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] E →SLᵤ[σ, 𝔖] F
hB : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (B p.1) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
V : Set G
hV : V ∈ 𝓝 0
W : Set E
hW : W ∈ 𝓝 0
hVW : V ×ˢ W ⊆ (fun p ↦ (B p.1) p.2) ⁻¹' U
c : 𝕜₁
hc : MapsTo (fun x ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : τ d = σ c
⊢ τ d ≠ 0

Tactic:
hd,

Goal state after:
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₂ F
𝕜₁ : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup G
𝕜₃ : Type u_7
inst✝⁸ : NormedField 𝕜₃
inst✝⁷ : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst✝⁶ : RingHomSurjective τ
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousConstSMul 𝕜₂ F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] E →SLᵤ[σ, 𝔖] F
hB : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (B p.1) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
V : Set G
hV : V ∈ 𝓝 0
W : Set E
hW : W ∈ 𝓝 0
hVW : V ×ˢ W ⊆ (fun p ↦ (B p.1) p.2) ⁻¹' U
c : 𝕜₁
hc : MapsTo (fun x ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : τ d = σ c
⊢ σ c ≠ 0
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₂ F
𝕜₁ : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup G
𝕜₃ : Type u_7
inst✝⁸ : NormedField 𝕜₃
inst✝⁷ : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst✝⁶ : RingHomSurjective τ
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousConstSMul 𝕜₂ F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] E →SLᵤ[σ, 𝔖] F
hB : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (B p.1) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
V : Set G
hV : V ∈ 𝓝 0
W : Set E
hW : W ∈ 𝓝 0
hVW : V ×ˢ W ⊆ (fun p ↦ (B p.1) p.2) ⁻¹' U
c : 𝕜₁
hc : MapsTo (fun x ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : τ d = σ c
d_ne : d ≠ 0
a : G
ha : a ∈ V
x : E
hx : x ∈ S
⊢ (τ d • B a) x ∈ U

Tactic:
hd,

Goal state after:
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₂ F
𝕜₁ : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup G
𝕜₃ : Type u_7
inst✝⁸ : NormedField 𝕜₃
inst✝⁷ : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst✝⁶ : RingHomSurjective τ
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousConstSMul 𝕜₂ F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] E →SLᵤ[σ, 𝔖] F
hB : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (B p.1) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
V : Set G
hV : V ∈ 𝓝 0
W : Set E
hW : W ∈ 𝓝 0
hVW : V ×ˢ W ⊆ (fun p ↦ (B p.1) p.2) ⁻¹' U
c : 𝕜₁
hc : MapsTo (fun x ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : τ d = σ c
d_ne : d ≠ 0
a : G
ha : a ∈ V
x : E
hx : x ∈ S
⊢ (σ c • B a) x ∈ U
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁵ : NormedField 𝕜₁
inst✝¹⁴ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E✝ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝¹ x✝ : (i : ι) → E →Lᵤ[𝕜, 𝔖] F i
⊢ ContinuousLinearMap.pi (x✝¹ + x✝) = ContinuousLinearMap.pi x✝¹ + ContinuousLinearMap.pi x✝

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁵ : NormedField 𝕜₁
inst✝¹⁴ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E✝ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝¹ : 𝕜
x✝ : (i : ι) → E →Lᵤ[𝕜, 𝔖] F i
⊢ ContinuousLinearMap.pi (x✝¹ • x✝) = (RingHom.id 𝕜) x✝¹ • ContinuousLinearMap.pi x✝

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁵ : NormedField 𝕜₁
inst✝¹⁴ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E✝ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝ : (i : ι) → E →Lᵤ[𝕜, 𝔖] F i
⊢ (fun f i ↦ ContinuousLinearMap.proj i ∘SL f) ((fun F_1 ↦ ContinuousLinearMap.pi F_1) x✝) = x✝

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁵ : NormedField 𝕜₁
inst✝¹⁴ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E✝ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝ : E →Lᵤ[𝕜, 𝔖] (i : ι) → F i
⊢ (fun F_1 ↦ ContinuousLinearMap.pi F_1) ((fun f i ↦ ContinuousLinearMap.proj i ∘SL f) x✝) = x✝

Tactic:
ext; rfl

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

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
inst✝ : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : IsInducing ⇑f
⊢ WithSeminorms (q.comp f)

Tactic:
rw [hf.eq_induced]
  exact f.withSeminorms_induced hq

Goal state after:
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
b : β
⊢ (↑fun x ↦ b).IsConstant

Tactic:
use b

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
κ : ι → Type u_11
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
⊢ WithSeminorms (SeminormFamily.sigma p)

Tactic:
have : ∀ i, @IsTopologicalAddGroup E (t i) _ :=
    fun i ↦ @WithSeminorms.topologicalAddGroup _ _ _ _ _ _ (t i) _ (hp i)

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
κ : ι → Type u_11
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this : ∀ (i : ι), IsTopologicalAddGroup E
⊢ WithSeminorms (SeminormFamily.sigma p)
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyCoherentSpace X
⊢ Continuous[inst✝¹, instTopologicalSpace] ⇑(CompactCoherentification.mk X)

Tactic:
rw [CompactlyCoherentSpace.isCoherentWith.continuous_iff]
  exact fun K hK ↦ continuousOn_isCompact_mk hK

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
⊢ ‖f.flip‖ₑ = ‖f‖ₑ

Tactic:
by
  simp [enorm_eq_nnnorm]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂✝ : Type u_2
inst✝³⁶ : NormedField 𝕜₁
inst✝³⁵ : NormedField 𝕜₂✝
σ : 𝕜₁ →+* 𝕜₂✝
E✝ : Type u_3
F✝ : Type u_4
G✝ : Type u_5
inst✝³⁴ : AddCommGroup E✝
inst✝³³ : Module 𝕜₁ E✝
inst✝³² : TopologicalSpace E✝
inst✝³¹ : AddCommGroup F✝
inst✝³⁰ : Module 𝕜₂✝ F✝
𝕜 : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
𝕜₄ : Type u_9
E : Type u_10
F : Type u_11
G : Type u_12
H : Type u_13
inst✝²⁹ : AddCommGroup E
inst✝²⁸ : AddCommGroup F
inst✝²⁷ : AddCommGroup G
inst✝²⁶ : AddCommGroup H
inst✝²⁵ : NormedField 𝕜
inst✝²⁴ : NormedField 𝕜₂
inst✝²³ : NormedField 𝕜₃
inst✝²² : NormedField 𝕜₄
inst✝²¹ : Module 𝕜 E
inst✝²⁰ : Module 𝕜₂ F
inst✝¹⁹ : Module 𝕜₃ G
inst✝¹⁸ : Module 𝕜₄ H
inst✝¹⁷ : TopologicalSpace E
inst✝¹⁶ : TopologicalSpace F
inst✝¹⁵ : TopologicalSpace G
inst✝¹⁴ : TopologicalSpace H
inst✝¹³ : IsTopologicalAddGroup G
inst✝¹² : IsTopologicalAddGroup H
inst✝¹¹ : ContinuousConstSMul 𝕜₃ G
inst✝¹⁰ : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst✝⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁷ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁶ : RingHomInvPair σ₄₃ σ₃₄
inst✝⁵ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁴ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
h : ∀ (t : Set F), t ∈ 𝔗 ↔ ⇑e₁₂ ⁻¹' t ∈ 𝔖
s : Set E
⊢ s ∈ 𝔖 → (fun x ↦ ⇑e₁₂ '' x) s ∈ 𝔗

Tactic:
by simp [h, preimage_image_eq _ e₁₂.injective]

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) (f' x)
H₂ : ∀ (x : α), Inseparable (s.piecewise f (⇑f') x) (f' x)
g : C(α, β) := { toFun := s.piecewise f ⇑f', continuous_toFun := ⋯ }
⊢ ∃ x ∈ {g | EqOn (⇑g) f s}, l ≤ 𝓝 x

Tactic:
refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) (f' x)
H₂ : ∀ (x : α), Inseparable (s.piecewise f (⇑f') x) (f' x)
g : C(α, β) := { toFun := s.piecewise f ⇑f', continuous_toFun := ⋯ }
⊢ 𝓝 f' = 𝓝 g
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
hg : Continuous[inst✝¹, inst✝] g
f : α →ₘ[μ] β
⊢ comp g hg f = mk (g ∘ ↑f) ⋯

Tactic:
rw [← comp_mk g hg f f.aestronglyMeasurable, mk_coeFn]

Goal state after: