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✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : IsOrderedAddMonoid β
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := 2⁻¹ • x + 2⁻¹ • y
hz : z ∈ s
⊢ 2⁻¹ • f x + 2⁻¹ • f y ≤ 2⁻¹ • f z + 2⁻¹ • f z

Tactic:
gcongr; exacts [hfx hz, hfy hz]

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

Goal state before:
pp: case inr.inr.hn
k : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : AffineSpace W Q
s : Set P
t : Set Q
hs : s.Nonempty
ht : t.Nonempty
⊢ (↑(affineSpan k (s ×ˢ t)) ∩ ↑((affineSpan k s).prod (affineSpan k t))).Nonempty

Tactic:
obtain ⟨x, hx⟩ := hs
    obtain ⟨y, hy⟩ := ht
    use ⟨x, y⟩
    simp [mem_affineSpan, hx, hy]

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

Goal state before:
pp: case refine_3
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₁ s₂ : AffineSubspace k P
h : s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
⊢ s₁ ∥ s₂

Tactic:
rcases h with ⟨hd, hb⟩
    by_cases hs₁ : s₁ = ⊥
    · rw [hs₁, bot_parallel_iff_eq_bot]
      exact hb.1 hs₁
    · have hs₂ : s₂ ≠ ⊥ := hb.not.1 hs₁
      rcases (nonempty_iff_ne_bot s₁).2 hs₁ with ⟨p₁, hp₁⟩
      rcases (nonempty_iff_ne_bot s₂).2 hs₂ with ⟨p₂, hp₂⟩
      refine ⟨p₂ -ᵥ p₁, (eq_iff_direction_eq_of_mem hp₂ ?_).2 ?_⟩
      · rw [mem_map]
        refine ⟨p₁, hp₁, ?_⟩
        simp
      · simpa using hd.symm

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

Goal state before:
pp: ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (p '' s')

Tactic:
rw [Set.image_eq_range]

Goal state after:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range fun x ↦ p ↑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 ∪ s2, (↑s1).indicator w1 i = 1
hw2 : ∑ i ∈ s1 ∪ s2, (↑s2).indicator w2 i = 1
heq : (affineCombination k (s1 ∪ s2) p) ((↑s1).indicator w1) = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
hws : ∑ i ∈ s1 ∪ s2, ((↑s1).indicator w1 - (↑s2).indicator w2) i = 0
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0

Tactic:
Finset.affineCombination_indicator_subset w2 p s1.subset_union_right,

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 ∈ s1 ∪ s2, (↑s2).indicator w2 i = 1
heq : (affineCombination k (s1 ∪ s2) p) ((↑s1).indicator w1) = (affineCombination k (s1 ∪ s2) p) ((↑s2).indicator w2)
i : ι
hi : i ∈ s1 ∪ s2
hws : ∑ i ∈ s1 ∪ s2, ((↑s1).indicator w1 - (↑s2).indicator w2) i = 0
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0
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 :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
⊢ ∑ i ∈ s, w1 i = 1

Tactic:
Finset.sum_update_of_mem hi0

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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
⊢ 1 + ∑ x ∈ s \ {i0}, const ι 0 x = 1
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
j : ι
hj : j ∈ s
hjx : (p j) x ≠ 0
this : (s.sup p) x ≠ 0
y : E
hle : ε / ‖c‖ ≤ (s.sup p) y
hlt : (s.sup p) y < ε
i : ι
hi : i ∈ s
hiy : (s.sup p) y = (p i) y
⊢ q y ≤ C • (p i) y

Tactic:
exact hf y (fun k hk ↦ (le_finset_sup_apply hk).trans_lt hlt) i hi (hiy ▸ hle)

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := hs.fintype
⊢ (convexHull R) s = (convexHull R) (range (⇑(∑ x, (LinearMap.proj x).smulRight ↑x) ∘ fun i j ↦ if i = j then 1 else 0))

Tactic:
apply congr_arg

Goal state after:
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := ⋯
⊢ s = range (⇑(∑ x, (LinearMap.proj x).smulRight ↑x) ∘ fun i j ↦ if i = j then 1 else 0)
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: case h₁
𝕜 : Type u_1
ι : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : OrderClosedTopology 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ IsClosed (⋂ x, {f | 0 ≤ f x})

Tactic:
apply isClosed_iInter

Goal state after:
case h₁
𝕜 : Type u_1
ι : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : OrderClosedTopology 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ ∀ (i : ι), IsClosed {f | 0 ≤ f i}
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₂)
hs : ∃ s w, ∑ i ∈ s, w i = 0 ∧ p i -ᵥ p j = (s.weightedVSub fun x ↦ p ↑x) w
⊢ False

Tactic:
obtain ⟨fs, w, hw, hs⟩ := hs

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
⊢ 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
x : V × V
⊢ x.1 * x.2 = (x.1 * x.2) • p /ₛ p

Tactic:
smul_sdiv

Goal state after:
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
x : V × V
⊢ x.1 * x.2 = x.1 * x.2
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: 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⟩
⊢ ∃ x ∈ t, (fun x ↦ if hx : x ∈ t then f x hx else 0) x ≠ 0

Tactic:
use i; simp [f, hi]

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
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ (s.weightedVSub p) w ∈ vectorSpan k {(affineCombination k s p) w₁, (affineCombination k s p) w₂} ↔
    ∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ i)

Tactic:
mem_vectorSpan_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
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ (∃ r, r • ((affineCombination k s p) w₁ -ᵥ (affineCombination k s p) w₂) = (s.weightedVSub p) w) ↔
    ∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
t✝ : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
i✝ : ι
t : Finset ι
hi✝ : i✝ ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i ∈ insert i✝ t, 0 ≤ w i
hpos : 0 < w i✝ + ∑ x ∈ t, w x
hmem : ∀ i ∈ insert i✝ t, z i ∈ s
zi : z i✝ ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ∑ j ∈ t, w j = 0
ws : ∀ j ∈ t, w j = 0
i : ι
hi : i ∈ t
⊢ w i • z i = 0

Tactic:
by simp [ws i hi]

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

Goal state before:
pp: case inl
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
h : AffineIndependent k fun p ↦ ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent (ι := ↑(Basis.ofVectorSpaceIndex k V)) k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
have h0 : ∀ v : V, v ∈ Basis.ofVectorSpaceIndex k V → v ≠ 0 := by
      intro v hv
      simpa [hsv] using hsv.ne_zero ⟨v, hv⟩

Goal state after:
case inl
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
h : AffineIndependent k fun p ↦ ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent (ι := ↑(Basis.ofVectorSpaceIndex k V)) k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
h0 : ∀ v ∈ Basis.ofVectorSpaceIndex k V, v ≠ 0
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case neg
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
i : ι
hi : i ∉ K
⊢ IsPathConnected (K.piecewise (fun i ↦ pathComponentIn (t i) (x i)) (fun x ↦ univ) i)

Tactic:
rw [piecewise_eq_of_notMem _ _ _ hi]

Goal state after:
case neg
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
i : ι
hi : i ∉ K
⊢ IsPathConnected univ
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i ∈ s, w i = 1
hx : (affineCombination R s ⇑b) w ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
hx' : (affineCombination R s ⇑b) w ∈ affineSpan R (Set.range ⇑b)
⊢ (affineCombination R s ⇑b) w ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s ⇑b) w = x}

Tactic:
refine ⟨s, w, ?_, hw₁, rfl⟩

Goal state after:
case refine_2
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i ∈ s, w i = 1
hx : (affineCombination R s ⇑b) w ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
hx' : (affineCombination R s ⇑b) w ∈ affineSpan R (Set.range ⇑b)
⊢ ∀ i ∈ s, 0 ≤ w i
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_11
E : Type u_12
ι : Type u_13
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous[inst✝, _] ⇑(p i)
U : Set E
hU : U ∈ p.basisSets
⊢ U ∈ 𝓝 0

Tactic:
by
  obtain ⟨s, r, hr, rfl⟩ := p.basisSets_iff.mp hU
  clear hU
  refine Seminorm.ball_mem_nhds ?_ hr
  classical
  induction s using Finset.induction_on with
  | empty => simpa using continuous_zero
  | insert a s _ hs =>
    simp only [Finset.sup_insert, coe_sup]
    exact Continuous.max (hp a) hs

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

Goal state before:
pp: case inl
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
⊢ ∃ C s, (∅.sup q).comp f ≤ C • s.sup p

pp: case inr
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
s' : Finset ι'
h✝ : s'.Nonempty
⊢ ∃ C s, (s'.sup q).comp f ≤ C • s.sup p

Tactic:
· exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩

Goal state after:
case inr
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
s' : Finset ι'
h✝ : s'.Nonempty
⊢ ∃ C s, (s'.sup q).comp f ≤ C • s.sup p
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : FunLike 𝓕 E F
inst✝¹ : SemilinearMapClass 𝓕 σ₁₂ E F
inst✝ : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ∀ x_1 ∈ ball x r, x_1 ∈ Set.range ⇑f
⊢ ∀ x ∈ ball 0 r, x ∈ ↑(↑f).range

Tactic:
SetLike.mem_coe

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : FunLike 𝓕 E F
inst✝¹ : SemilinearMapClass 𝓕 σ₁₂ E F
inst✝ : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ∀ x_1 ∈ ball x r, x_1 ∈ Set.range ⇑f
⊢ ∀ x ∈ ball 0 r, x ∈ (↑f).range
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ IsClosed {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}

Tactic:
simp only [ofPred_and, ofPred_forall]

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ IsClosed ({a | 0 ≤ a} ∩ ⋂ i, {x | ‖f i‖ ≤ x * ‖i‖})
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = (w.sup fun x ↦ p).ball 0 r
w_ne : w ≠ ∅
⊢ t = p.ball 0 r

Tactic:
have : w = Finset.univ := by
        rcases Finset.nonempty_of_ne_empty w_ne with ⟨i, hi⟩
        ext j
        simp only [Subsingleton.elim j i, hi, Finset.mem_univ]

Goal state after:
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = (w.sup fun x ↦ p).ball 0 r
w_ne : w ≠ ∅
this : w = Finset.univ
⊢ t = p.ball 0 r
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝³ : SeminormedAddCommGroup E
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NontrivialTopology E
⊢ 1 ≤ ‖ContinuousLinearMap.id 𝕜 E‖

Tactic:
by
    let ⟨x, hx⟩ := exists_norm_ne_zero E
    have := (ContinuousLinearMap.id 𝕜 E).ratio_le_opNorm x
    rwa [id_apply, div_self hx] at this

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✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ WithSeminorms fun i ↦ (Finset.Iic i).sup p

Tactic:
by
  refine hp.congr ?_ ?_
  · intro i
    refine ⟨Finset.Iic i, 1, ?_⟩
    rw [one_smul]
    rfl
  · intro i
    refine ⟨{i}, 1, ?_⟩
    rw [Finset.sup_singleton, one_smul]
    exact (Finset.le_sup (Finset.mem_Iic.mpr le_rfl) : p i ≤ (Finset.Iic i).sup p)

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

Goal state before:
pp: case hconvex
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedSpace ℝ 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
s : Set E
hs : ∃ i i_1, ∃ (_ : 0 < i_1), s ∈ {(i.sup p).ball 0 i_1}
⊢ Convex ℝ (id s)

Tactic:
Set.mem_singleton_iff

Goal state after:
case hconvex
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedSpace ℝ 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
s : Set E
hs : ∃ i i_1, ∃ (_ : 0 < i_1), s = (i.sup p).ball 0 i_1
⊢ Convex ℝ (id s)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕜₂
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
𝕜 : Type u_11
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
hp : Continuous[inst✝², _] ⇑p
inst✝ : PolynormableSpace 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsInducing ⇑f
⊢ ∃ p₂, Continuous[inst✝⁵, _] ⇑p₂ ∧ p ≤ p₂.comp f

Tactic:
obtain ⟨s, C, -, hqC⟩ := Seminorm.bound_comp_of_isInducing hp
    (PolynormableSpace.withSeminorms 𝕜₂ F) hf

Goal state after:
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕜₂
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
𝕜 : Type u_11
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
hp : Continuous[inst✝², _] ⇑p
inst✝ : PolynormableSpace 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsInducing ⇑f
s : Finset { p // Continuous[inst✝⁵, _] ⇑p }
C : ℝ≥0
hqC : p ≤ (C • s.sup fun p ↦ ↑p).comp f
⊢ ∃ p₂, Continuous[inst✝⁵, _] ⇑p₂ ∧ p ≤ p₂.comp f
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
⊢ map id = id

Tactic:
ext ⟨f⟩

Goal state after:
case mk
α : Type u_1
β : Type u_2
l : Filter α
x✝ : l.Germ β
f : α → β
⊢ map id (Quot.mk (⇑(l.germSetoid β)) f) = id (Quot.mk (⇑(l.germSetoid β)) f)
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 σ₁₃
f : E →SL[σ₁₂] F
g : E →SL[σ₁₃] G
h : ∀ (x : E), ‖f x‖ = ‖g x‖
c : ℝ
hc : c ≥ 0
h₂ : ∀ (x : E), ‖f x‖ ≤ c * ‖x‖
z : E
⊢ ‖g z‖ ≤ c * ‖z‖

Tactic:
rw [← h z]
      exact h₂ z

Goal state after: