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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬↑r₁ = r₂
⊢ ↑r₁ • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}

Tactic:
hr₁,

Goal state after:
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
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬↑r₁ = r₂
⊢ p₅ -ᵥ p₄ + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ ‖a • 1‖ * p x + ‖b • 1‖ * p y = a * p x + b * p y

Tactic:
rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
        Real.norm_of_nonneg hb]

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✝ : Nontrivial ι
i : ι
⊢ Function.Surjective ⇑(b.coord i)

Tactic:
classical
    intro x
    obtain ⟨j, hij⟩ := exists_ne i
    let s : Finset ι := {i, j}
    have hi : i ∈ s := by simp [s]
    let w : ι → k := fun j' => if j' = i then x else 1 - x
    have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]
    use s.affineCombination k b w
    simp [w, b.coord_apply_combination_of_mem hi hw]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
⊢ f ∈ Metric.closedBall 0 1

Tactic:
by
  rw [Metric.mem_closedBall, dist_pi_le_iff zero_le_one]
  intro x
  rw [Pi.zero_apply, Real.dist_0_eq_abs, abs_of_nonneg <| hf.1 x]
  exact (mem_Icc_of_mem_stdSimplex hf x).2

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
hw' : ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t = 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun x ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun x ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun x ↦ x ∈ s₂) fs)).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p) w''
hw'' : ∑ t ∈ fs', w'' t = 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
hj : j ∈ fs'
hw''' : ∑ t ∈ fs', w''' t = 0
hs''' : (fs'.weightedVSub p) w''' = 0
⊢ False

Tactic:
have h0 := ha fs' w''' hw''' hs''' i hi

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
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun x ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun x ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun x ↦ x ∈ s₂) fs)).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p) w''
hw'' : ∑ t ∈ fs', w'' t = 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
hj : j ∈ fs'
hw''' : ∑ t ∈ fs', w''' t = 0
hs''' : (fs'.weightedVSub p) w''' = 0
h0 : w''' i = 0
⊢ False
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 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
⊢ ∑ x ∈ s.disjSum t, Sum.elim (fun x ↦ a • ws x • zs x) (fun x ↦ b • wt x • zt x) x =
    (s.disjSum t).centerMass (Sum.elim (fun i ↦ a * ws i) fun j ↦ b * wt j) (Sum.elim zs zt)

Tactic:
Finset.centerMass_eq_of_sum_1

Goal state after:
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
⊢ ∑ x ∈ s.disjSum t, Sum.elim (fun x ↦ a • ws x • zs x) (fun x ↦ b • wt x • zt x) x =
    ∑ i ∈ s.disjSum t, Sum.elim (fun i ↦ a * ws i) (fun j ↦ b * wt j) i • Sum.elim zs zt i

case hw
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
⊢ ∑ i ∈ s.disjSum t, Sum.elim (fun i ↦ a * ws i) (fun j ↦ b * wt j) i = 1
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
i : ι
t : Finset ι
z : ι → E
inst✝ : DecidableEq ι
hi : i ∈ t
⊢ t.centerMass (fun j ↦ if i = j then 1 else 0) z = z i

Tactic:
Finset.centerMass_eq_of_sum_1

Goal state after:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i : ι
t : Finset ι
z : ι → E
inst✝ : DecidableEq ι
hi : i ∈ t
⊢ ∑ i_1 ∈ t, (if i = i_1 then 1 else 0) • z i_1 = z i

case hw
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i : ι
t : Finset ι
z : ι → E
inst✝ : DecidableEq ι
hi : i ∈ t
⊢ (∑ i_1 ∈ t, if i = i_1 then 1 else 0) = 1
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ([x -[𝕜] y] \ frontier s).Nonempty
⊢ StrictConvex 𝕜 s

Tactic:
refine hs.strictConvex' <| h.imp_on fun x hx y hy _ => ?_

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ([x -[𝕜] y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
⊢ fun ⦃a b⦄ ↦ ([a -[𝕜] b] \ frontier s).Nonempty → ∃ c, (lineMap a b) c ∈ interior s
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ([x -[𝕜] y] \ frontier s).Nonempty
⊢ StrictConvex 𝕜 s

Tactic:
by
  refine hs.strictConvex' <| h.imp_on fun x hx y hy _ => ?_
  simp only [segment_eq_image_lineMap, ← self_sdiff_frontier]
  rintro ⟨_, ⟨⟨c, hc, rfl⟩, hcs⟩⟩
  refine ⟨c, hs.segment_subset hx.1 hy.1 ?_, hcs⟩
  exact lineMap_mem_segment 𝕜 x y hc

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr✝ : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
rw [Metric.tendsto_nhds] at hy hz

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (y x_1) x < ε
hz : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (z x_1) x < ε
hr✝ : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝[s] x, r p.1 p.2
seg : ∀ᶠ (χ : α) in f, [y χ -[ℝ] z χ] ⊆ s
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
refine seg.mp <| .mono ?_ (fun _ => forall₂_imp)
  apply Eventually.segment_of_prod_nhds hy hz
  simpa [nhdsWithin, prod_eq_inf, ← inf_assoc, eventually_inf_principal] using hr

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
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 → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
i : ι
hi : i ∈ {i ∈ t | w i ≠ 0}
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ ∃ i ∈ t, f y ≤ f (p i)

Tactic:
rw [mem_filter] at hi

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
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 → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
i : ι
hi : i ∈ t ∧ w i ≠ 0
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ ∃ i ∈ t, f y ≤ f (p i)
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 → β
t✝ : Set E
hf : ConvexOn 𝕜 s f
hts : t✝ ⊆ s
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hp : ∀ i ∈ t, p i ∈ t✝
⊢ ∃ y ∈ t✝, f (t.centerMass w p) ≤ f y

Tactic:
obtain ⟨i, hit, Hi⟩ := hf.exists_ge_of_centerMass hw₀ (hw₁.symm ▸ zero_lt_one)
    fun i hi ↦ hts (hp i hi)

Goal state after:
𝕜 : 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 → β
t✝ : Set E
hf : ConvexOn 𝕜 s f
hts : t✝ ⊆ s
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hp : ∀ i ∈ t, p i ∈ t✝
i : α
hit : i ∈ t
Hi : f (t.centerMass w p) ≤ f (p i)
⊢ ∃ y ∈ t✝, f (t.centerMass w p) ≤ f y
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case mp
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
⊢ (Finset.affineCombination 𝕜 u s.points) w ∈ s.closedInterior

Tactic:
have hw' : ∀ i ∈ u, w i ≤ 1 := by
      intro i hi
      rw [← hw1]
      apply Finset.single_le_sum (fun j hj ↦ hw j hj) hi

Goal state after:
case mp
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
⊢ (Finset.affineCombination 𝕜 u s.points) w ∈ s.closedInterior
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_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
u : UniformSpace F
hu : IsUniformAddGroup F
hq : WithSeminorms q
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
⊢ [EquicontinuousAt (DFunLike.coe ∘ f) 0, ∀ (k : ι'), Equicontinuous (DFunLike.coe ∘ f),
      ∀ (k : ι'), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∀ (i : ι'), ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
      ∀ (i : ι'),
        BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧
          Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))].TFAE

Tactic:
equicontinuousAt_iInf_rng

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
u : UniformSpace F
hu : IsUniformAddGroup F
hq : WithSeminorms q
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
⊢ [∀ (k : ι'), EquicontinuousAt (DFunLike.coe ∘ f) 0, ∀ (k : ι'), Equicontinuous (DFunLike.coe ∘ f),
      ∀ (k : ι'), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∀ (i : ι'), ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
      ∀ (i : ι'),
        BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧
          Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))].TFAE
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
t : TopologicalSpace E
hp : WithSeminorms p
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ t = q.moduleFilterBasis.topology

Tactic:
hp.topology_eq_withSeminorms

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
t : TopologicalSpace E
hp : WithSeminorms p
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ p.moduleFilterBasis.topology = q.moduleFilterBasis.topology
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst✝¹⁸ : SeminormedAddCommGroup E
inst✝¹⁷ : SeminormedAddCommGroup Eₗ
inst✝¹⁶ : SeminormedAddCommGroup F
inst✝¹⁵ : SeminormedAddCommGroup Fₗ
inst✝¹⁴ : SeminormedAddCommGroup G
inst✝¹³ : SeminormedAddCommGroup Gₗ
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : NontriviallyNormedField 𝕜₃
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 Eₗ
inst✝⁷ : NormedSpace 𝕜₂ F
inst✝⁶ : NormedSpace 𝕜 Fₗ
inst✝⁵ : NormedSpace 𝕜₃ G
inst✝⁴ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : FunLike 𝓕 E F
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
z : F
x y : E
⊢ (f (x + y)) z = (f x) z + (f y) z

Tactic:
simp only [f.map_add, add_apply]

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

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u_1
pi : ι → Prop
s : ι → Set (β × β)
h : (𝓤 β).HasBasis pi s
⊢ (Filter.comap (fun x ↦ (x.1.toUniformOnFunIsCompact, x.2.toUniformOnFunIsCompact))
        (𝓤 (α →ᵤ[{K | IsCompact K}] β))).HasBasis
    (fun p ↦ IsCompact p.1 ∧ pi p.2) fun p ↦ {fg | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2}

Tactic:
exact .comap _ <| UniformOnFun.hasBasis_uniformity_of_basis _ _ {K | IsCompact K}
    ⟨∅, isCompact_empty⟩ (directedOn_of_sup_mem fun _ _ ↦ IsCompact.union) h

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
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst✝³² : SeminormedAddCommGroup E
inst✝³¹ : SeminormedAddCommGroup Eₗ
inst✝³⁰ : SeminormedAddCommGroup F
inst✝²⁹ : SeminormedAddCommGroup Fₗ
inst✝²⁸ : SeminormedAddCommGroup G
inst✝²⁷ : SeminormedAddCommGroup Gₗ
inst✝²⁶ : NontriviallyNormedField 𝕜
inst✝²⁵ : NontriviallyNormedField 𝕜₂
inst✝²⁴ : NontriviallyNormedField 𝕜₃
inst✝²³ : NormedSpace 𝕜 E
inst✝²² : NormedSpace 𝕜 Eₗ
inst✝²¹ : NormedSpace 𝕜₂ F
inst✝²⁰ : NormedSpace 𝕜 Fₗ
inst✝¹⁹ : NormedSpace 𝕜₃ G
inst✝¹⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : FunLike 𝓕 E F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁴ : RingHomInvPair σ₂₁ σ₁₂
E' : Type u_11
F' : Type u_12
inst✝¹³ : SeminormedAddCommGroup E'
inst✝¹² : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst✝¹¹ : NontriviallyNormedField 𝕜₁'
inst✝¹⁰ : NontriviallyNormedField 𝕜₂'
inst✝⁹ : NormedSpace 𝕜₁' E'
inst✝⁸ : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁷ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst✝⁶ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝⁵ : RingHomIsometric σ₂₃
inst✝⁴ : RingHomIsometric σ₁₃'
inst✝³ : RingHomIsometric σ₂₃'
inst✝² : RingHomIsometric σ₁₃
inst✝¹ : RingHomIsometric σ₁'
inst✝ : RingHomIsometric σ₂'
m : 𝕜
c : StrongDual 𝕜 E
⊢ smulRightₗ (m • c) = (RingHom.id 𝕜) m • smulRightₗ c

Tactic:
by
        ext x
        simp [smul_smul]

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 α
⊢ IsComplete {g | EqOn (⇑g) f s}

Tactic:
intro l

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
⊢ Cauchy l → l ≤ 𝓟 {g | EqOn (⇑g) f s} → ∃ x ∈ {g | EqOn (⇑g) f s}, l ≤ 𝓝 x
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: case inr
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
h : μ s ≠ 0
⊢ μ s / μ s = 0 ∨ μ s / μ s = 1

Tactic:
rcases eq_or_ne (μ s) ∞ with h' | h'

Goal state after:
case inr.inl
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
h : μ s ≠ 0
h' : μ s = ∞
⊢ μ s / μ s = 0 ∨ μ s / μ s = 1

case inr.inr
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
h : μ s ≠ 0
h' : μ s ≠ ∞
⊢ μ s / μ s = 0 ∨ μ s / μ s = 1
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (uniformOn s) u * (uniformOn (s ∪ t)) s + (uniformOn t) u * (uniformOn (s ∪ t)) t = (uniformOn (s ∪ t)) u

Tactic:
rw [uniformOn, uniformOn, uniformOn, cond_apply hs.measurableSet,
    cond_apply ht.measurableSet, cond_apply (hs.union ht).measurableSet,
    cond_apply (hs.union ht).measurableSet, cond_apply (hs.union ht).measurableSet]

Goal state after:
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (Measure.count s)⁻¹ * Measure.count (s ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ s)) +
      (Measure.count t)⁻¹ * Measure.count (t ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ t)) =
    (Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ u)
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
| (uniformOn (s ∩ u ∪ s ∩ uᶜ)) t

Tactic:
← uniformOn_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
      (disjoint_compl_right.mono inf_le_right inf_le_right)

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
| (uniformOn (s ∩ u)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
    (uniformOn (s ∩ uᶜ)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : MeasurableSingletonClass Ω
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : Finite Ω
f : ι → Set Ω
⊢ uniformOn (Set.univ.pi f) = Measure.pi fun i ↦ uniformOn (f i)

Tactic:
refine (MeasureTheory.Measure.pi_eq fun t ht ↦ ?_).symm
  lift f to ι → Finset Ω using by simp [Set.toFinite]
  lift t to ι → Finset Ω using by simp [Set.toFinite]
  classical
  simp [← Fintype.coe_piFinset, uniformOn_apply_finset, ← Fintype.piFinset_inter,
    ENNReal.prod_div_distrib_of_ne_top]

Goal state after:
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := ⋯
A : 0 < (μ.restrict t) t
⊢ t ⊆ s

Tactic:
apply subset_trans _ hsf

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := ⋯
A : 0 < (μ.restrict t) t
⊢ t ⊆ Function.support f