mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ (M * auxMat M k) i j = 0

Tactic:
simp_rw [Matrix.mul_apply, auxMat, of_apply, if_neg lt.2, mul_ite, mul_neg, mul_zero]

Goal state after:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ (∑ x, if x = k then -(M i x * M k j) else if x = j then M i x * M k k else 0) = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case left
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex) z

pp: case right
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContDiffWithinAt ℂ n (↑(extChartAt 𝓘(ℂ, ℂ) (↑ofComplex z)) ∘ ↑ofComplex ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm)
    (Set.range ↑𝓘(ℂ, ℂ)) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)

Tactic:
· -- continuity at z
    rw [ContinuousAt, nhds_induced, tendsto_comap_iff]
    refine Tendsto.congr' (eventuallyEq_coe_comp_ofComplex hz).symm ?_
    simpa [ofComplex_apply_of_im_pos hz] using! tendsto_id

Goal state after:
case right
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContDiffWithinAt ℂ n (↑(extChartAt 𝓘(ℂ, ℂ) (↑ofComplex z)) ∘ ↑ofComplex ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm)
    (Set.range ↑𝓘(ℂ, ℂ)) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: Y : Type u_2
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
s : Set Y
f : ↑s →ᵇ ℝ
hs : IsClosed[inst✝²] s
t : Set ℝ
inst✝ : t.OrdConnected
hf : ∀ (x : ↑s), f x ∈ t
hne : t.Nonempty
g : Y →ᵇ ℝ
hg : ∀ (y : Y), g y ∈ t
hgf : ⇑g ∘ Subtype.val = ⇑f
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.domRestrict s = f

Tactic:
exact ⟨g, hg, DFunLike.coe_injective hgf⟩

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure

Goal state before:
pp: ⊢ SMulInvariantMeasure (GL (Fin 2) ℝ) ℍ volume

Tactic:
refine ((smulInvariantMeasure_tfae _ _).out 2 0).mp fun g s hs ↦ ?_
  rw [volume_eq_lintegral, volume_eq_lintegral, ← Set.image_smul, Set.image_image]
  -- We want to apply the Jacobian change-of-variable formula.
  have hinj : Set.InjOn (fun z ↦ ↑(g • ofComplex z) : ℂ → ℂ) (UpperHalfPlane.coe '' s) :=
    .image_of_comp <| by simp
  have main := MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul
      volume (measurableEmbedding_coe.measurableSet_image.mpr hs)
      (Set.forall_mem_image.mpr fun z hz ↦
        (hasStrictFDerivAt_smul g _).hasFDerivAt.hasFDerivWithinAt)
      hinj
      (fun z ↦ ↑((1 / ‖z.im‖₊) ^ 2 : NNReal))
  convert! main using 1
  · simp [Set.image_image]
  · apply setLIntegral_congr_fun (measurableEmbedding_coe.measurableSet_image.mpr hs)
    rintro _ ⟨τ, -, rfl⟩
    simp only [← Real.enorm_eq_ofReal_abs, enorm_eq_nnnorm]
    have : ‖(SignType.sign g.val.det : ℝ)‖₊ = 1 := by
      rcases g.det_ne_zero.lt_or_gt with h | h <;> simp [h]
    have := g.det_ne_zero
    have := denom_ne_zero g τ
    norm_cast
    ext
    simp [det_smulFDeriv, *, im_smul_eq_div_normSq, Complex.normSq_eq_norm_sq, field]

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
⊢ ∀ t₁ ∈ ultrafilterBasis α, ∀ t₂ ∈ ultrafilterBasis α, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ ultrafilterBasis α, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
by
    rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ u ⟨ua, ub⟩
    refine ⟨_, ⟨a ∩ b, rfl⟩, inter_mem ua ub, fun v hv ↦ ⟨?_, ?_⟩⟩ <;> apply mem_of_superset hv <;>
      simp [inter_subset_right]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a : ℝ
⊢ Isometry fun y ↦ { coe := { re := a, im := rexp y }, coe_im_pos := ⋯ }

Tactic:
refine Isometry.of_dist_eq fun y₁ y₂ => ?_
  rw [dist_of_re_eq]
  exacts [congr_arg₂ _ (log_exp _) (log_exp _), rfl]

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj
              { toTop := (TopCat.limitCone FF).pt, is_compact := ⋯, is_hausdorff := ⋯, prop := trivial }).map
          f ≫
        InducedCategory.homMk ((TopCat.limitCone FF).π.app Y) =
      InducedCategory.homMk ((TopCat.limitCone FF).π.app X) ≫ F.map f

Tactic:
intro _ _ f

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ ((Functor.const J).obj { toTop := (TopCat.limitCone FF).pt, is_compact := ⋯, is_hausdorff := ⋯, prop := trivial }).map
        f ≫
      InducedCategory.homMk ((TopCat.limitCone FF).π.app Y✝) =
    InducedCategory.homMk ((TopCat.limitCone FF).π.app X✝) ≫ F.map f
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ 𝓝[≠] ∞ = map some (coclosedCompact X)

Tactic:
refine (nhdsWithin_basis_open ∞ _).ext (hasBasis_coclosedCompact.map _) ?_ ?_
  · rintro s ⟨hs, hso⟩
    refine ⟨_, (isOpen_iff_of_mem hs).mp hso, ?_⟩
    simp
  · rintro s ⟨h₁, h₂⟩
    refine ⟨_, ⟨mem_compl infty_notMem_image_coe, isOpen_compl_image_coe.2 ⟨h₁, h₂⟩⟩, ?_⟩
    simp [compl_image_coe, ← sdiff_eq]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ Tendsto some (coclosedCompact X) (𝓝 ∞)

Tactic:
nhds_infty_eq

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Tendsto some (coclosedCompact X) (map some (coclosedCompact X) ⊔ pure ∞)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ (𝓝 ∞).HasBasis (fun s ↦ IsClosed[inst✝] s ∧ IsCompact s) fun s ↦ some '' sᶜ ∪ {∞}

Tactic:
nhds_infty_eq

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (map some (coclosedCompact X) ⊔ pure ∞).HasBasis (fun s ↦ IsClosed[inst✝] s ∧ IsCompact s) fun s ↦ some '' sᶜ ∪ {∞}
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
s : Set G
t : Set X
hs : IsClosed[inst✝²] s
ht : IsCompact t
Ψ : G × ↑t → X × ↑t := fun gx ↦ (gx.1 • ↑gx.2, gx.2)
Ψ_proper : IsProperMap Ψ
⊢ IsClosed[inst✝¹] (s • t)

Tactic:
have : s • t = (fst ∘ Ψ) '' fst ⁻¹' s :=
    subset_antisymm
      (smul_subset_iff.mpr fun g hg x hx ↦ mem_image_of_mem (fst ∘ Ψ) (x := ⟨g, ⟨x, hx⟩⟩) hg)
      (image_subset_iff.mpr fun ⟨g, ⟨x, hx⟩⟩ hg ↦ smul_mem_smul hg hx)

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
s : Set G
t : Set X
hs : IsClosed[inst✝²] s
ht : IsCompact t
Ψ : G × ↑t → X × ↑t := fun gx ↦ (gx.1 • ↑gx.2, gx.2)
Ψ_proper : IsProperMap Ψ
this : s • t = fst ∘ Ψ '' fst ⁻¹' s
⊢ IsClosed[inst✝¹] (s • t)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
⊢ Tendsto some (cocompact X) (𝓝 ∞)

Tactic:
nhds_infty_eq

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
⊢ Tendsto some (cocompact X) (map some (coclosedCompact X) ⊔ pure ∞)
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed[inst✝¹] (s ∩ K)
⊢ IsClosed[inst✝¹] s

Tactic:
by
  refine isClosed' fun K _ _ _ f hf ↦ ?_
  rw [← Set.preimage_inter_range]
  exact (hs (isCompact_range hf)).preimage hf

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₁
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r

Tactic:
simp_rw [← norm_mul]
        apply MeromorphicOn.circleIntegrable_posLog_norm
        apply Meromorphic.meromorphicOn
        fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f : ℂ → ℂ
n : ℕ
⊢ proximity (f ^ n) ⊤ = n • proximity f ⊤

Tactic:
by
  ext x
  simp [proximity, ← smul_eq_mul, circleAverage_fun_smul]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt (fun x ↦ -a) 0 < meromorphicOrderAt f 0

Tactic:
rw [meromorphicOrderAt_const]
    aesop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
⊢ e ∈ closedBall 0 |r|

Tactic:
by simpa [abs_of_nonneg ((norm_nonneg e).trans hr)]

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

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
a✝ : x ∈ univ
⊢ (convexHull ℝ) (connectedComponentIn univ x) = univ

Tactic:
rw [connectedComponentIn_univ, PreconnectedSpace.connectedComponent_eq_univ, convexHull_univ]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
e : WithTop E
r : ℝ
⊢ logCounting f e (-r) = logCounting f e r

Tactic:
by_cases h : e = ⊤ <;> simp [logCounting, h, locallyFinsuppWithin.logCounting_even _ r]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inr.inl.refl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zt : z ∈ t
ys : z ∈ s
zy : z ≤ z
⊢ eVariationOn f ((s ∪ t) ∩ {z}) = 0

Tactic:
exact eVariationOn.subsingleton _ fun _ ⟨_, uz⟩ _ ⟨_, vz⟩ => uz.trans vz.symm

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ logCounting (f₁ * f₂) 0 r ≤ (logCounting f₁ 0 + logCounting f₂ 0) r

Tactic:
simp only [logCounting, WithTop.zero_ne_top, reduceDIte, WithTop.untop₀_zero, sub_zero]
  rw [divisor_mul h₁f₁.meromorphicOn h₁f₂.meromorphicOn (fun z _ ↦ h₂f₁ z) (fun z _ ↦ h₂f₂ z),
    ← locallyFinsuppWithin.logCounting.map_add]
  apply locallyFinsuppWithin.logCounting_le _ hr
  apply locallyFinsuppWithin.posPart_add

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
⊢ (support D).Finite

Tactic:
by
  classical
  -- Let (N : ℕ) be a number such that ‖logCounting D x‖ ≤ N * ‖log x‖
  obtain ⟨C, hC⟩ := isBigO_iff.1 hO
  obtain ⟨N, hCN⟩ := exists_nat_gt (max C 0)
  have hCN' : C < N := lt_of_le_of_lt (le_max_left C 0) hCN
  -- Argue by contradiction, let t be a cardinality=N finite subset in the (infinite) support of D
  -- and let D' be the divisor for the indicator function of t
  by_contra! hInf
  obtain ⟨t, htsub, htcard⟩ := hInf.exists_subset_card_eq N
  set D' := ∑ z ∈ t, single z (1 : ℤ) with hD'
  -- The auxiliary divisor `D'` is bounded above by `D`.
  have hle : D' ≤ D := by
    rw [le_def, Pi.le_def]
    intro w
    simp only [hD', coe_sum, Finset.sum_apply, single_apply, Finset.sum_ite_eq]
    by_cases hw : w ∈ t
    · simp only [hw, if_true]
      have h₁ : D w ≠ 0 := mem_support.mp (htsub (Finset.mem_coe.2 hw))
      have h₂ : (0 : ℤ) ≤ D w := by simpa using (le_def.1 h) w
      omega
    · simpa [hw, if_false] using (le_def.1 h) w
  -- A uniform bound on the norms of points in `t`.
  obtain ⟨R₀, hR₀⟩ : ∃ R₀ : ℝ, ∀ z ∈ t, ‖z‖ ≤ R₀ := t.finite_toSet.isBounded.exists_norm_le
  set K := ∑ z ∈ t, log ‖z‖ with hK
  -- Eventually, `logCounting D' = N * log - K`.
  have hEq : ∀ᶠ r in atTop, logCounting D' r = (N : ℝ) * log r - K := by
    filter_upwards [eventually_ge_atTop R₀] with r hr using calc
      logCounting D' r = ∑ c ∈ t, logCounting (single c 1) r := by simp [hD']
       _ = ∑ z ∈ t, (log r - log ‖z‖) := by
        congr! 1 with z hz;
        simpa using logCounting_single_eq_log_sub_const (e := z) (n := 1) ((hR₀ z hz).trans hr)
       _ = (N : ℝ) * log r - K := by simp [Finset.sum_sub_distrib, hK, htcard]
  -- Combine the bounds into a contradiction with `log → ∞`.
  have hFinal : ∀ᶠ r in atTop, ((N : ℝ) - C) * log r ≤ K := by
    filter_upwards [hEq, eventually_ge_atTop (1 : ℝ), hC] with r hr₁ hr₂ hr₃
    grind [logCounting_le hle hr₂, norm_eq_abs, abs_of_nonneg, log_nonneg, logCounting_nonneg]
  have hTendsto : Tendsto (fun r ↦ ((N : ℝ) - C) * log r) atTop atTop :=
    tendsto_log_atTop.const_mul_atTop (sub_pos.mpr hCN')
  obtain ⟨r, hr₁, hr₂⟩ := (hFinal.and (hTendsto.eventually_gt_atTop K)).exists
  linarith

Goal state after:
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑(hallMatchingsOn t ι')

Tactic:
classical
    rw [hallMatchingsOn]
    let g : hallMatchingsOn t ι' → ι' → ι'.biUnion t := by
      rintro f i
      refine ⟨f.val i, ?_⟩
      rw [mem_biUnion]
      exact ⟨i, i.property, f.property.2 i⟩
    apply Finite.of_injective g
    intro f f' h
    ext a
    rw [funext_iff] at h
    simpa [g] using h a

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
x : n → R
hA : M ∈ doublyStochastic R n
⊢ ∑ i, (M *ᵥ x) i = ∑ i, x i

Tactic:
apply sum_mulVec_of_mem_colStochastic

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
x : n → R
hA : M ∈ doublyStochastic R n
⊢ M ∈ colStochastic R n
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: 𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
⊢ ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) = 1

Tactic:
rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]

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

Goal state before:
pp: case refine_1.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
h : Sbtw R x y ((lineMap x y) r)
hrlt : 1 < r
⊢ (lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioi 1

Tactic:
exact Set.mem_image_of_mem _ hrlt

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

Goal state before:
pp: case refine_4
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
⊢ ∑ i ∈ t'.attach, w ↑i = 1

Tactic:
rw [Finset.sum_attach, Finset.sum_filter_ne_zero, hw₂]

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
ι : Sort u_4
f : ι → Set E
⊢ innerDual (⋃ i, f i) = ⨅ i, innerDual (f i)

Tactic:
ext; simp [forall_comm (α := E)]

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
S : Set (Set E)
⊢ innerDual (⋃₀ S) = sInf (innerDual '' S)

Tactic:
ext; simp [forall_comm (α := E)]

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : PartialOrder R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : ClosedIciTopology R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hp : ∀ (x : M), Continuous ⇑(p x)
⊢ IsClosed ↑(dual p s)

Tactic:
← s.biUnion_of_singleton

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : PartialOrder R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : ClosedIciTopology R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hp : ∀ (x : M), Continuous ⇑(p x)
⊢ IsClosed ↑(dual p (⋃ x ∈ s, {x}))
Module: Mathlib.Analysis.Convex.Extrema

Goal state before:
pp: E : Type u_1
β : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
⊢ IsMinOn f s a

Tactic:
intro x x_in_s
  let g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
  have hg0 : g 0 = a := AffineMap.lineMap_apply_zero a x
  have hg1 : g 1 = x := AffineMap.lineMap_apply_one a x
  have hgc : Continuous g := AffineMap.lineMap_continuous
  have h_maps : MapsTo g (Icc 0 1) s := by
    simpa only [g, mapsTo_iff_image_subset, ← segment_eq_image_lineMap]
      using h_conv.1.segment_subset a_in_s x_in_s
  have fg_local_min_on : IsLocalMinOn (f ∘ g) (Icc 0 1) 0 := by
    rw [← hg0] at h_localmin
    exact h_localmin.comp_continuousOn h_maps hgc.continuousOn (left_mem_Icc.2 zero_le_one)
  have fg_min_on : IsMinOn (f ∘ g) (Icc 0 1 : Set ℝ) 0 := by
    refine IsMinOn.of_isLocalMinOn_of_convexOn_Icc one_pos fg_local_min_on ?_
    exact (h_conv.comp_affineMap g).subset h_maps (convex_Icc 0 1)
  simpa only [hg0, hg1, comp_apply, mem_ofPred_eq] using fg_min_on (right_mem_Icc.2 zero_le_one)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : Ring 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
⊢ IsExtreme 𝕜 A B

Tactic:
refine ⟨hAB.subset, fun x₁ hx₁A x₂ hx₂A x hxB hx => ?_⟩
  obtain ⟨l, rfl⟩ := hAB ⟨x, hxB⟩
  have hl : ConvexOn 𝕜 univ l := l.toLinearMap.convexOn convex_univ
  have hlx₁ := hxB.2 x₁ hx₁A
  have hlx₂ := hxB.2 x₂ hx₂A
  refine ⟨hx₁A, fun y hy => ?_⟩
  rw [hlx₁.antisymm (hl.le_left_of_right_le (mem_univ _) (mem_univ _) hx hlx₂)]
  exact hxB.2 y hy

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
inst✝ : IsFiniteMeasure μ
hfi : Integrable f μ
H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬μ t = 0
h₀' : t =ᵐ[μ] univ
⊢ ∫ (x : α) in univ, f x ∂μ = μ.real t • ⨍ (x : α), f x ∂μ

Tactic:
restrict_univ,

Goal state after:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
inst✝ : IsFiniteMeasure μ
hfi : Integrable f μ
H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : ¬μ t = 0
h₀' : t =ᵐ[μ] univ
⊢ ∫ (x : α), f x ∂μ = μ.real t • ⨍ (x : α), f x ∂μ
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: X : Type u_2
K : Type u_8
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : IsDomain K
w : StdSimplex K X
s : Set X
hs : ∃ x ∈ s, w.weights x ≠ 0
inst✝ : DecidablePred fun x ↦ x ∈ s
this : ((filter (fun x ↦ x ∈ s) w.weights).sum fun x k ↦ k) ≠ 0
⊢ ((filter (fun x ↦ x ∈ s) w.weights).sum fun _x k ↦ k)⁻¹ ≠ 0

Tactic:
convert inv_ne_zero this

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
hs : s.Subsingleton
⊢ IsConvexSet R s

Tactic:
obtain rfl | ⟨x, rfl⟩ := hs.eq_empty_or_singleton

Goal state after:
case inl
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
hs : ∅.Subsingleton
⊢ IsConvexSet R ∅

case inr
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
hs : {x}.Subsingleton
⊢ IsConvexSet R {x}
Module: Mathlib.Analysis.Convex.Piecewise

Goal state before:
pp: case inl.inr.inr
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : LinearOrder E
inst✝⁷ : IsOrderedAddMonoid E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : PosSMulMono 𝕜 E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
⊢ (Set.Iic e).piecewise f g (a • x + b • y) ≤ a • f x + b • g y

Tactic:
rw [Set.piecewise_eq_of_notMem (Set.Iic e) f g (Set.notMem_Iic.mpr hc)]

Goal state after:
case inl.inr.inr
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : LinearOrder E
inst✝⁷ : IsOrderedAddMonoid E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : PosSMulMono 𝕜 E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : x ≤ e
hy : e < y
hc : e < a • x + b • y
⊢ g (a • x + b • y) ≤ a • f x + b • g y