mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
this : HasStrictDerivAt (num g / denom g) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ
⊢ num g / denom g =ᶠ[𝓝 ↑τ] fun z ↦ ↑(g • ↑ofComplex z)

Tactic:
← isOpenEmbedding_coe.map_nhds_eq,

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
this : HasStrictDerivAt (num g / denom g) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ
⊢ num g / denom g =ᶠ[map UpperHalfPlane.coe (𝓝 τ)] fun z ↦ ↑(g • ↑ofComplex z)
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
a R : ℝ
x : P
⊢ inversion c (a * R) x = (homothety c (a ^ 2)) (inversion c R x)

Tactic:
by
  simp only [inversion_eq_lineMap, ← homothety_eq_lineMap, ← homothety_mul_apply, mul_div_assoc,
    mul_pow]

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

Goal state before:
pp: n : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : CommRing S
inst✝ : TopologicalSpace S
f : R →+* S
hf : Continuous[inst✝², inst✝] ⇑f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] ⇑(map f)

Tactic:
refine IsInducing.subtypeVal.continuous_iff.mpr ?_
  exact (continuous_id.matrix_map hf).comp continuous_subtype_val

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ ↑(Ultrafilter.map g G) ≤ 𝓝 (g x)

Tactic:
G.coe_map

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ map g ↑G ≤ 𝓝 (g x)
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
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
this : range f = {1} ×ˢ univ
⊢ IsClosed[instTopologicalSpaceProd] ({1} ×ˢ univ)

Tactic:
exact isClosed_singleton.prod isClosed_univ

Goal state after:
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
h_proper : ProperSMul G X
inst✝ : T1Space G
⊢ T2Space X

Tactic:
by
  let f := fun x : X ↦ ((1 : G), x)
  have proper_f : IsProperMap f := by
    refine IsClosedEmbedding.isProperMap ⟨isEmbedding_prodMkRight 1, ?_⟩
    have : range f = ({1} ×ˢ univ) := by simp [f, Set.singleton_prod]
    rw [this]
    exact isClosed_singleton.prod isClosed_univ
  rw [t2_iff_isClosed_diagonal]
  let g := fun gx : G × X ↦ (gx.1 • gx.2, gx.2)
  have proper_g : IsProperMap g := (properSMul_iff G X).1 h_proper
  have : g ∘ f = Function.diag := by ext x <;> simp [f, g]
  have range_gf : range (g ∘ f) = diagonal X := by simp [this]
  rw [← range_gf]
  exact (proper_g.comp proper_f).isClosed_range

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f : Ultrafilter (OnePoint X)
⊢ ↑f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed[inst✝] s → IsCompact s → some '' s ∉ f

Tactic:
simp only [le_nhds_infty, ← compl_image_coe, Ultrafilter.mem_coe,
    Ultrafilter.compl_mem_iff_notMem]

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: X : Type u_2
inst✝⁴ : TopologicalSpace X
G : Type u_3
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
⊢ IsCompact {g | (g • U ∩ V).Nonempty}

Tactic:
by
  convert!
    ((ProperSMul.isProperMap_smul_pair (G := G)).isCompact_preimage (hV.prod hU)).image
      continuous_fst
  ext g
  suffices (∃ v, v ∈ g • U ∧ v ∈ V) ↔ ∃ u, g • u ∈ V ∧ u ∈ U by simpa
  rw [← (MulAction.toPerm g).exists_congr_right]
  simp [and_comm]

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

Goal state before:
pp: ⊢ Continuous ↿num

Tactic:
unfold num; fun_prop

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

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 =
    circleAverage (fun x ↦ log⁺ ‖f₁ x‖) 0 + circleAverage (fun x ↦ log⁺ ‖f₂ x‖) 0

Tactic:
by
      ext r
      apply circleAverage_add
      · exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₁ x)
      · exact MeromorphicOn.circleIntegrable_posLog_norm (fun x a ↦ h₁f₂ x)

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

Goal state before:
pp: case neg
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
a : E
h₁a : ¬a = 0
h₂a : a ∉ closedBall 0 |r|
⊢ 0 ≤ ↑(((toClosedBall r) f) a) * log (r * ‖a‖⁻¹)

Tactic:
· simp [apply_eq_zero_of_notMem ((toClosedBall r) _) h₂a]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inr.inl
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
y : ℝ
ys : y ∈ s
zy : z ≤ y
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal (↑l * (y - z))

Tactic:
cases le_antisymm zy ((hs.2 ys).trans (ht.2 zt))
    simp only [Icc_self, sub_self, mul_zero, ENNReal.ofReal_zero]
    exact eVariationOn.subsingleton _ fun _ ⟨_, uz⟩ _ ⟨_, vz⟩ => uz.trans vz.symm

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

Goal state before:
pp: case inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
ht : 1 ∈ Set.Icc 0 1
hyx : (lineMap x z) 1 ≠ x
hyz : (lineMap x z) 1 ≠ z
⊢ (lineMap x z) 1 ∈ ⇑(lineMap x z) '' Set.Ioo 0 1

Tactic:
exfalso
    exact hyz (lineMap_apply_one _ _)

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
⊢ Sbtw R 1 x 0 ↔ x ∈ Set.Ioo 0 1

Tactic:
rw [sbtw_comm, sbtw_zero_one_iff]

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

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : tx • (z -ᵥ x - ty • (z -ᵥ x)) + ty • (z -ᵥ x) = 0
⊢ x = (lineMap x z) ty

Tactic:
smul_sub,

Goal state after:
case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : tx • (z -ᵥ x) - tx • ty • (z -ᵥ x) + ty • (z -ᵥ x) = 0
⊢ x = (lineMap x z) ty
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mp.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : z -ᵥ x = 0
⊢ x = (lineMap x z) ty

Tactic:
· rw [vsub_eq_zero_iff_eq] at h
      rw [h, lineMap_same_apply]

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

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
p : P
⊢ p ∈ affineSegment R (s.points 0) (s.points 1) → p ∈ s.closedInterior

Tactic:
· rintro ⟨r, ⟨h0, h1⟩, rfl⟩
    rw [← Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _), affineCombination_mem_closedInterior_iff
        (Finset.sum_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _) _)]
    intro i
    fin_cases i <;> simp [h0, h1]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : b ∈ f a₁
h₂ : b ∈ f a₂
⊢ a₁ = a₂

Tactic:
rw [← mem_iff_mem] at *

Goal state after:
α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : a₁ ∈ f.symm b
h₂ : a₂ ∈ f.symm b
⊢ a₁ = a₂
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ f.trans f.symm = PEquiv.refl α ↔ ∀ (a : α), (f a).isSome = true

Tactic:
rw [self_trans_symm, ofSet_eq_refl, Set.eq_univ_iff_forall]

Goal state after:
α : Type u
β : Type v
f : α ≃. β
⊢ (∀ (x : α), x ∈ {a | (f a).isSome = true}) ↔ ∀ (a : α), (f a).isSome = true
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

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 : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
⊢ (reindex e₁ e₂) M ∈ colStochastic R m ↔ M ∈ colStochastic R n

Tactic:
by
  rw [← transpose_transpose (reindex e₁ e₂ M), transpose_reindex,
    transpose_mem_colStochastic_iff_mem_rowStochastic, reindex_mem_rowStochastic_iff,
    ← transpose_mem_colStochastic_iff_mem_rowStochastic, transpose_transpose]

Goal state after:
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 ∈ insert i₀ (t.erase i₀), k e

Tactic:
sum_insert (notMem_erase i₀ t),

Goal state after:
𝕜 : 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
| k i₀ + ∑ x ∈ t.erase i₀, k x
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: case refine_2
𝕜 : 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
ksum : ∑ e ∈ t.erase i₀, k e = 1
⊢ (t.erase ↑⟨i₀, hi₀⟩).centerMass k id = t.centerMass f id

Tactic:
· rw [Subtype.coe_mk, centerMass_eq_of_sum_1 _ id ksum]
    calc
      ∑ e ∈ t.erase i₀, k e • e = ∑ e ∈ t, k e • e := sum_erase _ (by rw [hk, zero_smul])
      _ = ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) • e := rfl
      _ = t.centerMass f id := by
        simp only [sub_smul, mul_smul, sum_sub_distrib, ← smul_sum, gcombo, smul_zero, sub_zero,
          centerMass, fsum, inv_one, one_smul, id]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ Set.extremePoints R ↑(doublyStochastic R n) = {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
refine subset_antisymm ?_ ?_

Goal state after:
case refine_1
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ Set.extremePoints R ↑(doublyStochastic R n) ⊆ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

case refine_2
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x} ⊆ Set.extremePoints R ↑(doublyStochastic R n)
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
z : H ⊗[R] G
hz : ∀ φ ∈ dual (Dual.eval R H) ↑C₂, ∀ ψ ∈ dual (Dual.eval R G) ↑C₁, 0 ≤ ((dualDistrib R H G) (φ ⊗ₜ[R] ψ)) z
φ : Dual R G
hφ : φ ∈ dual (Dual.eval R G) ↑C₁
ψ : Dual R H
⊢ ψ ∈ dual (Dual.eval R H) ↑C₂ → 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) ((TensorProduct.comm R H G) z)

Tactic:
hψ

Goal state after:
case refine_2
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
z : H ⊗[R] G
hz : ∀ φ ∈ dual (Dual.eval R H) ↑C₂, ∀ ψ ∈ dual (Dual.eval R G) ↑C₁, 0 ≤ ((dualDistrib R H G) (φ ⊗ₜ[R] ψ)) z
φ : Dual R G
hφ : φ ∈ dual (Dual.eval R G) ↑C₁
ψ : Dual R H
hψ : ψ ∈ dual (Dual.eval R H) ↑C₂
⊢ 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) ((TensorProduct.comm R H G) z)
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : LinearOrder R
inst✝⁸ : IsStrictOrderedRing R
G : Type u_2
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
H : Type u_3
inst✝⁵ : AddCommGroup H
inst✝⁴ : Module R H
G' : Type u_4
H' : Type u_5
inst✝³ : AddCommGroup G'
inst✝² : Module R G'
inst✝¹ : AddCommGroup H'
inst✝ : Module R H'
f : G →ₗ[R] G'
g : H →ₗ[R] H'
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw : ∀ φ ∈ dual (Dual.eval R G) ↑C₁, ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) w
φ : Dual R G'
hφ : φ ∈ dual (Dual.eval R G') ↑(map f C₁)
ψ : Dual R H'
⊢ ψ ∈ dual (Dual.eval R H') ↑(map g C₂) →
    0 ≤ ((dualDistrib R G' H') (φ ⊗ₜ[R] ψ)) ((↑{ c // 0 ≤ c } (TensorProduct.map f g)) w)

Tactic:
hψ

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : LinearOrder R
inst✝⁸ : IsStrictOrderedRing R
G : Type u_2
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
H : Type u_3
inst✝⁵ : AddCommGroup H
inst✝⁴ : Module R H
G' : Type u_4
H' : Type u_5
inst✝³ : AddCommGroup G'
inst✝² : Module R G'
inst✝¹ : AddCommGroup H'
inst✝ : Module R H'
f : G →ₗ[R] G'
g : H →ₗ[R] H'
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw : ∀ φ ∈ dual (Dual.eval R G) ↑C₁, ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) w
φ : Dual R G'
hφ : φ ∈ dual (Dual.eval R G') ↑(map f C₁)
ψ : Dual R H'
hψ : ψ ∈ dual (Dual.eval R H') ↑(map g C₂)
⊢ 0 ≤ ((dualDistrib R G' H') (φ ⊗ₜ[R] ψ)) ((↑{ c // 0 ≤ c } (TensorProduct.map f g)) w)
Module: Mathlib.Analysis.Convex.Cone.TensorProduct

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_3
b : Basis ι R M
C : PointedCone R M
hC : ↑C ⊆ ↑(hull R (Set.range ⇑b))
i : ι
⊢ b.coord i ∈ dual (Dual.eval R M) ↑C

Tactic:
refine dual_le_dual hC ?_

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_3
b : Basis ι R M
C : PointedCone R M
hC : ↑C ⊆ ↑(hull R (Set.range ⇑b))
i : ι
⊢ b.coord i ∈ dual (Dual.eval R M) ↑(hull R (Set.range ⇑b))
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Tactic:
replace hf' : IsBounded ((-f) '' ball x₀ r) := by convert! hf'.neg; ext; simp [neg_eq_iff_eq_neg]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded ((-f) '' ball x₀ r)
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s

Tactic:
intrinsicInterior_union_intrinsicFrontier

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ intrinsicClosure 𝕜 s = intrinsicClosure 𝕜 s
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
h : P → R → V := fun x w ↦ w • (x -ᵥ b)
h_rhs :
  ∑ a ∈ (∑ d ∈ f.weights.support, f.weights d • d.weights).support,
      h a ((∑ d ∈ f.weights.support, f.weights d • d.weights) a) =
    ∑ d ∈ f.weights.support, ∑ a ∈ (f.weights d • d.weights).support, h a ((f.weights d • d.weights) a)
d : StdSimplex R P
hd : ¬f.weights d = 0
p : P
⊢ p ∈ d.weights.support ↔ p ∈ (f.weights d • d.weights).support

Tactic:
simp only [Finsupp.mem_support_iff, ne_eq]

Goal state after:
case neg
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
h : P → R → V := fun x w ↦ w • (x -ᵥ b)
h_rhs :
  ∑ a ∈ (∑ d ∈ f.weights.support, f.weights d • d.weights).support,
      h a ((∑ d ∈ f.weights.support, f.weights d • d.weights) a) =
    ∑ d ∈ f.weights.support, ∑ a ∈ (f.weights d • d.weights).support, h a ((f.weights d • d.weights) a)
d : StdSimplex R P
hd : ¬f.weights d = 0
p : P
⊢ ¬d.weights p = 0 ↔ ¬(f.weights d • d.weights) p = 0
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: ι : Type u_1
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 : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), w.weights i ≠ 0 → f i ∈ s
⊢ ↑(StdSimplex.map f w).weights.support ⊆ s

Tactic:
grw [StdSimplex.weights_map, mapDomain_support]

Goal state after:
ι : Type u_1
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 : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), w.weights i ≠ 0 → f i ∈ s
⊢ ↑(Finset.image f w.weights.support) ⊆ s
Module: Mathlib.Analysis.Convex.Quasiconvex

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_6
γ : Type u_7
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
⊢ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}

Tactic:
intro a b ha hb hab

Goal state after:
𝕜 : Type u_4
E : Type u_5
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_6
γ : Type u_7
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
| 1 * dist x y - s * dist x y

Tactic:
one_mul

Goal state after:
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
| dist x y - s * dist x y
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y x' y' : X
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s t hs ht h x' y') ≤ s * dist x x' + t * dist y y'

Tactic:
convert dist_iConvexComb_le (.duple (M := Fin 2) 0 1 hs ht h) ![x, y] ![x', y']
  · simp [convexCombPair_def]
  · simp [convexCombPair_def]
  · simp [Finsupp.sum_fintype, Fin.sum_univ_succ, StdSimplex.duple, iConvexComb_eq_sum]

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

Goal state before:
pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ 1 * max (dist x.1 y.1) (dist x.2 y.2) ≤ max (dist x.1 y.1) (dist x.2 y.2)

Tactic:
one_mul

Goal state after:
case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ max (dist x.1 y.1) (dist x.2 y.2) ≤ max (dist x.1 y.1) (dist x.2 y.2)