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

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
        ↑(ENat.map Nat.cast 0).untop₀ * Real.log R +
      Real.log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖

Tactic:
(h₁f c (by simp)).meromorphicTrailingCoeffAt_of_ne_zero h₂f

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
        ↑(ENat.map Nat.cast 0).untop₀ * Real.log R +
      Real.log ‖f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ num g ↑z =
      (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ↑z * denom g ↑z ↔
    ((↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re +
          (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im) *
        ↑g 1 0 ^ 2 =
      -(↑g).det

Tactic:
g.val_det_apply,

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ num g ↑z = (if 0 < (↑g).det then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ↑z * denom g ↑z ↔
    ((↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re +
          (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im) *
        ↑g 1 0 ^ 2 =
      -(↑g).det
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mp
g : GL (Fin 2) ℝ
h : (↑g).det < 0
⊢ (∃ z, g • z = z) → (↑g).trace = 0

Tactic:
rintro ⟨z, hz⟩

Goal state after:
case mp
g : GL (Fin 2) ℝ
h : (↑g).det < 0
z : ℍ
hz : g • z = z
⊢ (↑g).trace = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case left
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ -m ∉ Set.range ⇑(scalar (Fin 2))

Tactic:
rw [← RingHom.coe_range, SetLike.mem_coe, neg_mem_iff]

Goal state after:
case left
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ m ∉ (scalar (Fin 2)).range
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: ⊢ ∀ (g : PGL(2, ℝ)), (∀ (a : ℍ), g • a = a) → g = 1

Tactic:
intro g

Goal state after:
g : PGL(2, ℝ)
⊢ (∀ (a : ℍ), g • a = a) → g = 1
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case refine_1.succ
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n✝ : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
n : ℕ
hn : 1 ≤ n
IH : ((Matrix.scalar (Fin 2)) a + m) ^ n = (Matrix.scalar (Fin 2)) (a ^ n) + (↑n * a ^ (n - 1)) • m
⊢ ((Matrix.scalar (Fin 2)) a + m) ^ (n + 1) = (Matrix.scalar (Fin 2)) (a ^ (n + 1)) + (↑(n + 1) * a ^ (n + 1 - 1)) • m

Tactic:
| succ n hn IH =>

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

Goal state before:
pp: ⊢ J ^ 2 = 1

Tactic:
ext; simp [J, sq, Matrix.one_fin_two]

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case zero
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : IsEmpty m
⊢ det 1 = 1

Tactic:
det_one

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

Goal state before:
pp: case e'_3
g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
hinj : Set.InjOn (fun z ↦ ↑(g • ↑ofComplex z)) (UpperHalfPlane.coe '' s)
main :
  ∫⁻ (x : ℂ) in (fun z ↦ ↑(g • ↑ofComplex z)) '' UpperHalfPlane.coe '' s, ↑((1 / ‖x.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)
⊢ ∫⁻ (z : ℂ) in UpperHalfPlane.coe '' s, ↑((1 / ‖z.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)

Tactic:
apply setLIntegral_congr_fun (measurableEmbedding_coe.measurableSet_image.mpr hs)

Goal state after:
case e'_3
g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
hinj : Set.InjOn (fun z ↦ ↑(g • ↑ofComplex z)) (UpperHalfPlane.coe '' s)
main :
  ∫⁻ (x : ℂ) in (fun z ↦ ↑(g • ↑ofComplex z)) '' UpperHalfPlane.coe '' s, ↑((1 / ‖x.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)
⊢ Set.EqOn (fun x ↦ ↑((1 / ‖x.im‖₊) ^ 2))
    (fun x ↦ ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)) (UpperHalfPlane.coe '' s)
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 x : P
R : ℝ
⊢ inversion c R x = c ↔ x = c ∨ R = 0

Tactic:
by_cases hR : R = 0

Goal state after:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
hR : R = 0
⊢ inversion c R x = c ↔ x = c ∨ R = 0

case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
hR : ¬R = 0
⊢ inversion c R x = c ↔ x = c ∨ R = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
h : z.re = w.re
⊢ dist z w = dist (log z.im) (log w.im)

Tactic:
have h₀ : 0 < z.im / w.im := by positivity
  rw [dist_eq_iff_dist_coe_center_eq, Real.dist_eq, ← abs_sinh, ← log_div z.im_ne_zero w.im_ne_zero,
    sinh_log h₀, dist_of_re_eq, coe_im, coe_im, center_im, cosh_abs, cosh_log h₀, inv_div] <;>
  [skip; exact h]
  nth_rw 4 [← abs_of_pos w.im_pos]
  simp only [← _root_.abs_mul, Real.dist_eq]
  congr 1
  field

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

Goal state before:
pp: α : Type u
b : Ultrafilter α
⊢ b = joinM (map pure b)

Tactic:
ext s

Goal state after:
α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ s ∈ joinM (map pure b)
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
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ g a = g b

Tactic:
← congrFun e a,

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ (Ultrafilter.extend g ∘ pure) a = g b
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case mp
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X ↦ ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X ↦ ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
g : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun y' ↦ { down := ⟨φ y', ⋯⟩ }, continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun x ↦ { down := ⟨0, ⋯⟩ }, continuous_toFun := ⋯ }
H : 0 = φ y
⊢ False

Tactic:
simp only [hφ1 (Set.mem_singleton y), Pi.one_apply] at H

Goal state after:
case mp
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X ↦ ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X ↦ ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
g : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun y' ↦ { down := ⟨φ y', ⋯⟩ }, continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun x ↦ { down := ⟨0, ⋯⟩ }, continuous_toFun := ⋯ }
H : 0 = 1
⊢ False
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)
Y : Type u_3
inst✝ : TopologicalSpace Y
f : ℕ → Y
y : Y
h : Tendsto f atTop (𝓝 y)
⊢ Tendsto f cofinite (𝓝 y)

Tactic:
by rwa [Nat.cofinite_eq_atTop]

Goal state after:
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)
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : { f // ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L) }
f : ℕ → Y
hf : ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L)
⊢ ∃ L, Tendsto (fun x ↦ f x) cofinite (𝓝 L)

Tactic:
by rwa [Nat.cofinite_eq_atTop]

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

Goal state before:
pp: ⊢ ∀ (g : SL(2, ℝ)) (τ : ℍ),
    ContinuousAt
      (fun x ↦
        match x with
        | (h, z) => (↑(↑h 0 0) * ↑z + ↑(↑h 0 1)) / (↑(↑h 1 0) * ↑z + ↑(↑h 1 1)))
      (g, τ)

Tactic:
intro g

Goal state after:
g : SL(2, ℝ)
⊢ ∀ (τ : ℍ),
    ContinuousAt
      (fun x ↦
        match x with
        | (h, z) => (↑(↑h 0 0) * ↑z + ↑(↑h 0 1)) / (↑(↑h 1 0) * ↑z + ↑(↑h 1 1)))
      (g, τ)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case «1»
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
j : Fin 2
⊢ |↑g ((fun i ↦ i) ⟨1, ⋯⟩) j| ≤ max √A √A'

Tactic:
refine le_trans ?_ <| le_max_right √A √A'
    exact Real.le_sqrt_of_sq_le <| le_trans (by fin_cases j <;> simp [sq_nonneg]) (hA' g hg)

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

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ CircleIntegrable (fun x ↦ logCounting f (↑x) R) 0 1

Tactic:
by_cases hR : R = 0

Goal state after:
case pos
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R = 0
⊢ CircleIntegrable (fun x ↦ logCounting f (↑x) R) 0 1

case neg
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : ¬R = 0
⊢ CircleIntegrable (fun x ↦ logCounting f (↑x) R) 0 1
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))

Tactic:
cases hs hx hy

Goal state after:
case refl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx hy : x ∈ s
⊢ eVariationOn f (s ∩ Icc x x) = ENNReal.ofReal (↑l * (x - x))
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ CircleIntegrable (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1

Tactic:
by_cases hR : R = 0

Goal state after:
case pos
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R = 0
⊢ CircleIntegrable (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1

case neg
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : ¬R = 0
⊢ CircleIntegrable (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1
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
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
⊢ ∀ (i : E), D' i ≤ D i

Tactic:
intro w

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
w : E
⊢ D' w ≤ D w
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
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
⊢ False

Tactic:
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

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
⊢ False
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
he : s'.Nonempty
h : image (fun z ↦ ↑z) s' = univ
⊢ False

Tactic:
simpa [← h] using mem_univ x

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✝⁷ : 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
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
⊢ (s.weightedVSub p) (w₁ - w₂) ≠ 0

Tactic:
intro hz

Goal state after:
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
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : (s.weightedVSub p) (w₁ - w₂) = 0
⊢ False
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝⁵ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
this✝ : (j : J) → Fintype (F.obj j)
this : Fintype ↑F.sections
card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections
fn : J → ℕ := fun j ↦ Fintype.card ↑F.sections - Fintype.card (F.obj j)
i : J
f : i ⟶ Function.argmin fn
⊢ Fintype.card ↑F.sections - Fintype.card ((fun X ↦ X) (F.obj (Function.argmin fn))) ≤
    Fintype.card ↑F.sections - Fintype.card (F.obj i)

Tactic:
apply fn.argmin_le

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: case some.h₀
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ ∀ b ∈ Finset.univ, b ≠ fj → (M i b * if j ∈ f b then 1 else 0) = 0

Tactic:
rintro b - n
      simp [h, ← f.eq_some_iff, n.symm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: case g2
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
σ : Equiv.Perm n
⊢ ∀ (i : n), ∑ j, Equiv.Perm.permMatrix R σ i j = 1

Tactic:
case g2 => simp [Equiv.toPEquiv_apply]

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✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
⊢ M *ᵥ N *ᵥ 1 = 1

Tactic:
hN.2.1,

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✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
⊢ M *ᵥ 1 = 1
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x y z : R
hxz : x ≤ z
x✝ : x = z ∨ x < z
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
cases hxz.eq_or_lt with

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

Goal state before:
pp: E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
c : ℝ
hc : 0 ≤ c
x : E
⊢ (c * gauge s x / (c * gauge t x) * c) • x = (c * (gauge s x / gauge t x)) • x

Tactic:
mul_div_mul_comm,

Goal state after:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
c : ℝ
hc : 0 ≤ c
x : E
⊢ (c / c * (gauge s x / gauge t x) * c) • x = (c * (gauge s x / gauge t x)) • x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
⊢ ‖z - x₀‖ < r

Tactic:
by
      calc
        _ = ‖(x - x₀) + (ε / ‖x - y‖) • (x - y)‖ := by simp only [z, add_sub_right_comm]
        _ ≤ ‖x - x₀‖ + ‖(ε / ‖x - y‖) • (x - y)‖ := norm_add_le ..
        _ < r - ε + ε :=
          add_lt_add_of_lt_of_le (mem_ball_iff_norm.1 hx) <| by
            simp [norm_smul, abs_of_nonneg, hε.le, hxy.ne']
        _ = r := by simp

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b c : E
⊢ convexJoin 𝕜 (segment 𝕜 a b) {c, c} = (convexHull 𝕜) {a, b, c, c}

Tactic:
← convexJoin_segments,

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b c : E
⊢ convexJoin 𝕜 (segment 𝕜 a b) {c, c} = convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c c)
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: α : 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, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ)

Tactic:
push Not at H

Goal state after:
α : 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 ∂μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ)
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
⊢ 0 = ENNReal.toReal 0 • ⨍ (x : α), f x ∂μ

Tactic:
ENNReal.toReal_zero,

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
⊢ 0 = 0 • ⨍ (x : α), f x ∂μ
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: K : Type u_4
X : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t✝ : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄, ↑t ⊆ s → t = w.weights.support → sConvexComb w ∈ s
w : StdSimplex K X
hw : ↑(Finset.cons x t hx) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : w.weights x ≠ 0
hwx' : ∃ y, y ≠ x ∧ w.weights y ≠ 0
⊢ ↑t ⊆ s

Tactic:
by grw [← hw, ← Finset.subset_cons]

Goal state after: