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

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * (log R - log ‖c - u‖) + log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log (R * ‖c - u‖⁻¹) + ↑((divisor f CB) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
rw [countingFunction_finsum_eq_finsum_add hR h₃f]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
⊢ num g ↑I =
      (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ↑I * denom g ↑I ↔
    ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 = -↑g 1 0

Tactic:
if_pos hg

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
⊢ num g ↑I = (ContinuousAlgEquiv.refl ℝ ℂ) ↑I * denom g ↑I ↔ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 = -↑g 1 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
hb : ↑g 0 1 = 0
⊢ ↑g 1 0 = 0

Tactic:
simpa using congr_arg (coeff · 2) hP

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:

Tactic:
dist (g n) (g (n + 1)) = ‖F (f - (g n).compContinuous e)‖ := by
        rw [g_succ, dist_eq_norm', add_sub_cancel_left]
      _ ≤ ‖f - (g n).compContinuous e‖ / 3 := hF_norm _
      _ = 1 / 3 * dist ((g n).compContinuous e) f := by rw [dist_eq_norm', one_div, div_eq_inv_mul]
      _ ≤ 1 / 3 * ((2 / 3) ^ n * ‖f‖) := mul_le_mul_of_nonneg_left (hgf n) (by norm_num1)
      _ = 1 / 3 * ‖f‖ * (2 / 3) ^ n := by ac_rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp.g
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
hg11 : ↑g 1 1 = -1
⊢ ∃ x, x ≠ 0 ∧ ↑g = ↑(-upperRightHom x)

Tactic:
refine ⟨-g 0 1, neg_eq_zero.not.mpr hg01, ?_⟩
      rw [g.val.eta_fin_two]
      simp_all

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

Goal state before:
pp: ⊢ coe 1 = 1

Tactic:
simp only [coe, map_one]

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

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (fun τ ↦ g • τ) τ

Tactic:
refine contMDiffAt_iff_target.mpr ⟨(continuous_const_smul g).continuousAt, ?_⟩

Goal state after:
n : ℕ∞ω
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (↑(extChartAt 𝓘(ℂ, ℂ) (g • τ)) ∘ fun τ ↦ g • τ) τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure

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

Tactic:
by
  -- It suffices to show `volume (g • s) = volume s` for measurable sets `s`. First
  -- we write this as a lintegral over subsets of `ℂ`.
  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.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ smulFDeriv (J * g) z = -↑Complex.conjCLE ∘SL smulFDeriv g z

Tactic:
ext
  by_cases hg : 0 < g.val.det
  · simp [smulFDeriv, σ, hg, hg.not_gt, neg_div]
  · simp [smulFDeriv, σ, hg, g.det_ne_zero.lt_or_gt.resolve_right hg, neg_div]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ (smulFDeriv g z).det =
    ↑(SignType.sign ↑(Matrix.GeneralLinearGroup.det g)) * ↑(Matrix.GeneralLinearGroup.det g) ^ 2 / ‖denom g z‖ ^ 4

Tactic:
simp only [smulFDeriv, σ]

Goal state after:
g : GL (Fin 2) ℝ
z : ℂ
⊢ (↑↑(if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ∘SL
        ContinuousLinearMap.restrictScalars ℝ
          (ContinuousLinearMap.toSpanSingleton ℂ (↑↑(Matrix.GeneralLinearGroup.det g) / denom g z ^ 2))).det =
    ↑(SignType.sign ↑(Matrix.GeneralLinearGroup.det g)) * ↑(Matrix.GeneralLinearGroup.det g) ^ 2 / ‖denom g z‖ ^ 4
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
H :
  1 ^ 2 / (dist b a * dist d a) * dist b d ≤
    1 ^ 2 / (dist b a * dist c a) * dist b c + dist (inversion a 1 c) (inversion a 1 d)
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Tactic:
dist_inversion_inversion hc hd,

Goal state after:
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
H :
  1 ^ 2 / (dist b a * dist d a) * dist b d ≤
    1 ^ 2 / (dist b a * dist c a) * dist b c + 1 ^ 2 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case refine_2
z w : ℍ
r : ℝ
⊢ PseudoMetricSpace.toUniformSpace.toTopologicalSpace ≤ instTopologicalSpace

Tactic:
let : MetricSpace ℍ := metricSpaceAux
      refine le_of_nhds_le_nhds fun z => ?_
      rw [nhds_induced]
      refine (nhds_basis_ball.le_basis_iff (nhds_basis_ball.comap _)).2 fun R hR => ?_
      have h₁ : 1 < R / im z + 1 := lt_add_of_pos_left _ (div_pos hR z.im_pos)
      have h₀ : 0 < R / im z + 1 := one_pos.trans h₁
      refine ⟨log (R / im z + 1), Real.log_pos h₁, ?_⟩
      refine fun w hw => (dist_coe_le w z).trans_lt ?_
      rwa [← lt_div_iff₀' z.im_pos, sub_lt_iff_lt_add, ← Real.lt_log_iff_exp_lt h₀]

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

Goal state before:
pp: α : Type u
⊢ induced pure Ultrafilter.topologicalSpace = ⊥

Tactic:
apply eq_bot_of_singletons_open
  intro x
  use { u : Ultrafilter α | {x} ∈ u }, ultrafilter_isOpen_basic _
  simp

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

Goal state before:
pp: case hg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := ⋯
this :
  {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j} =
    ⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}
i j : J
f : i ⟶ j
⊢ Continuous fun y ↦ y j

Tactic:
· exact continuous_apply j

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

Goal state before:
pp: case infty
X : Type u_1
inst✝ : TopologicalSpace X
y : OnePoint X
⊢ Inseparable ∞ y ↔ ∞ = ∞ ∧ y = ∞ ∨ ∃ x', ∞ = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'

Tactic:
induction y using OnePoint.rec

Goal state after:
case infty.infty
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Inseparable ∞ ∞ ↔ ∞ = ∞ ∧ ∞ = ∞ ∨ ∃ x', ∞ = ↑x' ∧ ∃ y', ∞ = ↑y' ∧ Inseparable x' y'

case infty.coe
X : Type u_1
inst✝ : TopologicalSpace X
x✝ : X
⊢ Inseparable ∞ ↑x✝ ↔ ∞ = ∞ ∧ ↑x✝ = ∞ ∨ ∃ x', ∞ = ↑x' ∧ ∃ y', ↑x✝ = ↑y' ∧ Inseparable x' y'
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe
X : Type u_1
inst✝ : TopologicalSpace X
y : OnePoint X
x✝ : X
⊢ Inseparable (↑x✝) y ↔ ↑x✝ = ∞ ∧ y = ∞ ∨ ∃ x', ↑x✝ = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'

Tactic:
induction y using OnePoint.rec

Goal state after:
case coe.infty
X : Type u_1
inst✝ : TopologicalSpace X
x✝ : X
⊢ Inseparable ↑x✝ ∞ ↔ ↑x✝ = ∞ ∧ ∞ = ∞ ∨ ∃ x', ↑x✝ = ↑x' ∧ ∃ y', ∞ = ↑y' ∧ Inseparable x' y'

case coe.coe
X : Type u_1
inst✝ : TopologicalSpace X
x✝¹ x✝ : X
⊢ Inseparable ↑x✝¹ ↑x✝ ↔ ↑x✝¹ = ∞ ∧ ↑x✝ = ∞ ∨ ∃ x', ↑x✝¹ = ↑x' ∧ ∃ y', ↑x✝ = ↑y' ∧ Inseparable x' y'
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case infty
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
y : OnePoint X
⊢ ∞ ⤳ y ∨ Disjoint (𝓝 ∞) (𝓝 y)

Tactic:
induction y using OnePoint.rec

Goal state after:
case infty.infty
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
⊢ ∞ ⤳ ∞ ∨ Disjoint (𝓝 ∞) (𝓝 ∞)

case infty.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
⊢ ∞ ⤳ ↑x✝ ∨ Disjoint (𝓝 ∞) (𝓝 ↑x✝)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
y : OnePoint X
x✝ : X
⊢ ↑x✝ ⤳ y ∨ Disjoint (𝓝 ↑x✝) (𝓝 y)

Tactic:
induction y using OnePoint.rec

Goal state after:
case coe.infty
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
⊢ ↑x✝ ⤳ ∞ ∨ Disjoint (𝓝 ↑x✝) (𝓝 ∞)

case coe.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (𝓝 ↑x✝¹) (𝓝 ↑x✝)
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
this : (ENNReal.ofReal (↑l * (x - y))).toReal = ↑l * (x - y)
⊢ -(ENNReal.ofReal (↑l * (x - y))).toReal = ↑l * (y - x)

Tactic:
simp_all only [NNReal.val_eq_coe]

Goal state after:
case mp.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
this : (ENNReal.ofReal (↑l * (x - y))).toReal = ↑l * (x - y)
⊢ -(↑l * (x - y)) = ↑l * (y - x)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := ⋯
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ 0 ≤ logCounting (single e 1) ℓ

Tactic:
apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ

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

Goal state before:
pp: case hbc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := ⋯
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ |logCounting D ℓ| < |logCounting D (1 + ℓ)|

Tactic:
abs_of_nonneg (logCounting_nonneg h h₂ℓ),

Goal state after:
case hbc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ logCounting D ℓ < |logCounting D (1 + ℓ)|
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
a : WithTop E
a₀ : E
h : ¬a = ⊤
⊢ ℝ → ℝ

Tactic:
exact (divisor (f · - a.untop₀) univ)⁺.logCounting

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

Goal state before:
pp: 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
p₁ p₂ p₃ p₄ : P
⊢ List.Sbtw R [p₁, p₂, p₃, p₄] ↔ Sbtw R p₁ p₂ p₃ ∧ Sbtw R p₁ p₂ p₄ ∧ Sbtw R p₁ p₃ p₄ ∧ Sbtw R p₂ p₃ p₄

Tactic:
simp [List.Sbtw, List.Wbtw, triplewise_cons, Sbtw]
  aesop

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) - (tx * ty) • (z -ᵥ x) + ty • (z -ᵥ x) = 0
⊢ x = (lineMap x z) ty

Tactic:
← sub_smul,

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 - tx * ty) • (z -ᵥ x) + ty • (z -ᵥ x) = 0
⊢ x = (lineMap x z) ty
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : i ⟶ j
⊢ F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map f)) ↔
    ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))

Tactic:
by
  rw [subset_antisymm_iff, eventualRange, and_iff_right (iInter₂_subset _ _), subset_iInter₂_iff]
  refine ⟨fun h k g => h _ _, fun h j' f' => ?_⟩
  obtain ⟨k, g, g', he⟩ := cospan f f'
  refine (h g).trans ?_
  rw [he, F.map_comp, types_comp]
  apply range_comp_subset_range

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq β
R : SetRel α β
inst✝ : (a : α) → Fintype ↑(R.image {a})
A : Finset α
⊢ Fintype ↑(R.image ↑A)

Tactic:
have h : R.image A = (A.biUnion fun a => (R.image {a}).toFinset : Set β) := by
    ext
    simp [SetRel.image]

Goal state after:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
R : SetRel α β
inst✝ : (a : α) → Fintype ↑(R.image {a})
A : Finset α
h : R.image ↑A = ↑(A.biUnion fun a ↦ (R.image {a}).toFinset)
⊢ Fintype ↑(R.image ↑A)
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f g : α ≃. β
a : α
b : β
⊢ (if f.symm b = g.symm b then f.symm b else none) = some a ↔ (if f a = g a then f a else none) = some b

Tactic:
have hf := @mem_iff_mem _ _ f a b
          have hg := @mem_iff_mem _ _ g a b
          simp only [Option.mem_def] at *
          grind

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
left✝ : 0 ≤ t
ht1 : t ≤ 1
⊢ SameRay R (z -ᵥ x) (z -ᵥ (lineMap x z) t)

Tactic:
simp [SameRay.sameRay_nonneg_smul_right (z -ᵥ x) (sub_nonneg.2 ht1)]

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✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0

Tactic:
let f (i : n) : Finset n := {j | M i j ≠ 0}

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := fun i ↦ {j | M i j ≠ 0}
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
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
s : Finset E := {z ∈ t | 0 < g z}
x : E
hx : x ∈ t
hgx : 0 < g x
⊢ s.Nonempty

Tactic:
exact ⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩

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 ∈ t.erase i₀, k e = ∑ e ∈ t, k e

Tactic:
conv_rhs => rw [← insert_erase hi₀, sum_insert (notMem_erase i₀ t), hk, zero_add]

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

Goal state before:
pp: 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 z : P
h : Wbtw R x y z
hne : x ≠ y
⊢ z ∈ line[R, x, y]

Tactic:
rcases h.right_mem_image_Ici_of_left_ne hne with ⟨r, ⟨-, rfl⟩⟩

Goal state after:
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
hne : x ≠ y
r : R
h : Wbtw R x y ((lineMap x y) r)
⊢ (lineMap x y) r ∈ line[R, x, y]
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_2
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
hne : x ≠ y
r : R
hr : 1 < r
⊢ 1 • (y -ᵥ x) - r • (y -ᵥ x) ≠ 0

Tactic:
← sub_smul,

Goal state after:
case refine_2
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
hne : x ≠ y
r : R
hr : 1 < r
⊢ (1 - r) • (y -ᵥ x) ≠ 0
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: case refine_5
𝕜 : 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₃ : ∑ i ∈ t, w i • id i = x
t' : Finset E := {i ∈ t | w i ≠ 0}
⊢ ∑ x ∈ t, w x • x = x

Tactic:
exact hw₃

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

Goal state before:
pp: case refine_5
𝕜 : 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}
⊢ ∀ x ∈ t, w x • x ≠ 0 → w x ≠ 0

Tactic:
· intro e _ hwe contra
      apply hwe
      rw [contra, zero_smul]

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

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K ↑C
x₀ : E
hx₀ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, f a < u
huv : u < v
hv : ∀ b ∈ ↑C, v < f b
hv₀ : v < 0
⊢ ∃ f, (∀ x ∈ C, 0 ≤ f x) ∧ ∀ x ∈ K, f x < 0

Tactic:
refine ⟨f, fun x hx ↦ ?_, fun x hx ↦ (hu x hx).trans_le <| huv.le.trans hv₀.le⟩

Goal state after:
case inr
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K ↑C
x₀ : E
hx₀ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, f a < u
huv : u < v
hv : ∀ b ∈ ↑C, v < f b
hv₀ : v < 0
x : E
hx : x ∈ C
⊢ 0 ≤ f x
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'
hψ : ψ ∈ dual (Dual.eval R H') ↑(map g C₂)
h_eq : (dualDistrib R G' H') (φ ⊗ₜ[R] ψ) ∘ₗ TensorProduct.map f g = (dualDistrib R G H) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g))
⊢ 0 ≤ ((dualDistrib R G' H') (φ ⊗ₜ[R] ψ)) ((↑{ c // 0 ≤ c } (TensorProduct.map f g)) w)

Tactic:
convert! hw (φ.comp f) (fun x hx ↦ hφ ⟨x, hx, rfl⟩) (ψ.comp g) (fun y hy ↦ hψ ⟨y, hy, rfl⟩)

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₂)
h_eq : (dualDistrib R G' H') (φ ⊗ₜ[R] ψ) ∘ₗ TensorProduct.map f g = (dualDistrib R G H) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g))
⊢ ((dualDistrib R G' H') (φ ⊗ₜ[R] ψ)) ((↑{ c // 0 ≤ c } (TensorProduct.map f g)) w) =
    ((dualDistrib R G H) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g))) w