mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:

Tactic:
circleAverage (log ‖· - a‖) c R
  _ = circleAverage (fun z ↦ log ‖R * (z + R⁻¹ * (c - a))‖) 0 1 := by
    rw [circleAverage_eq_circleAverage_zero_one]
    congr
    ext z
    congr
    rw [Complex.ofReal_inv R]
    field [Complex.ofReal_ne_zero.mpr hR]
  _ = circleAverage (fun z ↦ log ‖R‖ + log ‖z + R⁻¹ * (c - a)‖) 0 1 := by
    apply circleAverage_congr_codiscreteWithin _ (zero_ne_one' ℝ).symm
    have : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (Metric.sphere (0 : ℂ) |1|) := by
      apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
      intro z hz
      use Set.univ
      simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter,
        true_and]
      apply Set.Subsingleton.finite
      intro z₁ hz₁ z₂ hz₂
      simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_sdiff,
        Set.mem_ofPred_eq, Decidable.not_not]
      rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]
    filter_upwards [this] with z hz
    rw [norm_mul, log_mul (norm_ne_zero_iff.2 (Complex.ofReal_ne_zero.mpr hR)) hz]
    simp
  _ = log R + log⁺ (|R|⁻¹ * ‖c - a‖) := by
    rw [← Pi.add_def, circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1)
      (MeromorphicOn.circleIntegrable_log_norm (fun _ _ ↦ by fun_prop)), circleAverage_const]
    simp
  _ = log R + log⁺ (R⁻¹ * ‖c - a‖) := by
    congr 1
    rcases hR.lt_or_gt with h | h
    · simp [abs_of_neg h]
    · rw [abs_of_pos h]

Goal state after:
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case h_bound
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x

Tactic:
filter_upwards [hr_tendsto.eventually (le_mem_nhds (by linarith : (R + ‖w‖) / 2 < R))] with n hn

Goal state after:
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ :=
  fun θ ↦ (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
n : ℕ
hn : (R + ‖w‖) / 2 ≤ r n
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < ↑n + 2
⊢ R * 1 < R * (↑n + 2)

Tactic:
gcongr; grind

Goal state after:
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: case h
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : ℂ) in 𝓝 (-f x), x ∉ f '' U

Tactic:
rw [nhds_neg, eventually_neg]

Goal state after:
case h
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : ℂ) in 𝓝 (f x), -x ∉ f '' U
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case neg
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∉ Function.support D
⊢ ∑ᶠ (u : ℂ), ↑(D u) * (log R - log ‖c - u‖) = ∑ᶠ (u : ℂ), ↑(D u) * log (R * ‖c - u‖⁻¹) + ↑(D c) * log R

Tactic:
· simp_all only [Function.mem_support, Decidable.not_not, Int.cast_zero, zero_mul, add_zero]
    refine finsum_congr fun x ↦ ?_
    by_cases h₁ : c = x
    · simp_all
    · rw [log_mul hR (inv_ne_zero (norm_ne_zero_iff.mpr (sub_eq_zero.not.2 h₁))), log_inv]
      ring

Goal state after:
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
xs : x ∈ s
hcy : c ≤ y
⊢ f x ≤ f y

Tactic:
· exact (h₁ xs hs.1 hxc.le).trans (h₂ ht.1 (B _ hy hcy) hcy)

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: a : ℝ
⊢ (↑a).sqrt.re = √a

Tactic:
simp only [cpow_inv_two_re, norm_real, Real.norm_eq_abs, ofReal_re, Complex.sqrt]
  grind

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
⊢ ∃ g, g.comp { toFun := e, continuous_toFun := ⋯ } = f

Tactic:
by
  let e' : X₁ ≃ₜ Set.range e := he.isEmbedding.toHomeomorph
  obtain ⟨g, hg⟩ := (f.comp e'.symm).exists_restrict_eq he.isClosed_range
  exact ⟨g, by ext x; simpa using! congr($(hg) ⟨e' x, x, rfl⟩)⟩

Goal state after:
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case neg
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u ≠ c
⊢ ↑(ENat.map Nat.cast (analyticOrderAt f u)).untop₀ * Real.log (R / r) ≤
    ↑(ENat.map Nat.cast (analyticOrderAt f u)).untop₀ * Real.log (R * ‖c - u‖⁻¹)

Tactic:
simp +singlePass only [← log_abs]

Goal state after:
case neg
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u ≠ c
⊢ ↑(ENat.map Nat.cast (analyticOrderAt f u)).untop₀ * Real.log |R / r| ≤
    ↑(ENat.map Nat.cast (analyticOrderAt f u)).untop₀ * Real.log |R * ‖c - u‖⁻¹|
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f

Tactic:
have g_succ : ∀ n, g (n + 1) = g n + F (f - (g n).compContinuous e) := fun n =>
    Function.iterate_succ_apply' _ _ _

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mp
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
⊢ g ∈ Subgroup.center (GL (Fin 2) ℝ)

Tactic:
by_contra! hgc

Goal state after:
case mp
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
⊢ False
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: h : IsCompact univ
⊢ False

Tactic:
have : IsCompact (Complex.im ⁻¹' Ioi 0) := by
      simpa [isEmbedding_coe.isCompact_iff] using! h
    simpa [closure_preimage_im] using! congr(0 ∈ $this.isClosed.closure_eq)

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z✝ z w : ℍ
m : Matrix (Fin 2) (Fin 2) ℝ := !![w.im, z.im * w.re - w.im * z.re; 0, z.im]
⊢ m.det ≠ 0

Tactic:
simp [m, im_ne_zero]

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

Goal state before:
pp: ⊢ σ J = Complex.conjCAE

Tactic:
by simp [σ, J]

Goal state after:
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 i j : m
lt : i ≠ k ∧ j = k
⊢ auxMat M k i j = 0

Tactic:
rw [auxMat, of_apply, if_pos lt.2, if_neg lt.1]

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

Goal state before:
pp: a b c : ℍ
⊢ dist a c ≤ dist a b + dist b c

Tactic:
rw [dist_le_iff_le_sinh, sinh_half_dist_add_dist, div_mul_eq_div_div _ _ (dist _ _), le_div_iff₀,
    div_mul_eq_mul_div]

Goal state after:
a b c : ℍ
⊢ dist ↑a ↑c * dist (↑b) ((starRingEnd ℂ) ↑b) / (2 * √(a.im * c.im)) ≤
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * √(a.im * c.im))

a b c : ℍ
⊢ 0 < dist (↑b) ((starRingEnd ℂ) ↑b)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case refine_2
x : ℝ
hx : 0 < x
⊢ 0 < cosh x - deriv (fun x ↦ x) x

pp: case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

pp: case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x ↦ x) x

Tactic:
deriv_id'',

Goal state after:
case refine_2
x : ℝ
hx : 0 < x
⊢ 0 < cosh x - (fun x ↦ 1) x

case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x ↦ x) x
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : HasProp P X
A B : CompHausLike P
f : A ⟶ B
hf : IsIso ((forget (CompHausLike P)).map f)
⊢ IsIso f

Tactic:
isIso_iff_bijective

Goal state after:
P : TopCat → Prop
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : HasProp P X
A B : CompHausLike P
f : A ⟶ B
hf : Function.Bijective ⇑(ConcreteCategory.hom ((forget (CompHausLike P)).map f))
⊢ IsIso f
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case hf
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 ↦ (ConcreteCategory.hom (F.map f)) (y i)

Tactic:
exact ((F.map f).hom.hom.continuous).comp (continuous_apply i)

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)
⊢ IsCompact univ

Tactic:
have : Tendsto ((↑) : X → OnePoint X) (cocompact X) (𝓝 ∞) := by
      rw [nhds_infty_eq]
      exact (tendsto_map.mono_left cocompact_le_coclosedCompact).mono_right le_sup_left

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
this : Tendsto some (cocompact X) (𝓝 ∞)
⊢ IsCompact univ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: 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) ⟨0, ⋯⟩) j| ^ 2 ≤ ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2

Tactic:
fin_cases j <;> simp [sq_nonneg]

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

Goal state before:
pp: 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| ^ 2 ≤ ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2

Tactic:
fin_cases j <;> simp [sq_nonneg]

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 : (support D).Finite
⊢ logCounting D =O[atTop] log

Tactic:
← sum_apply_smul_single_eq_self_on_univ h,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : (support D).Finite
⊢ logCounting (∑ z ∈ h.toFinset, single z (D z)) =O[atTop] log
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case refine_1
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
z₁ z₂ : ι
key : ∀ {x : ↑ι'}, y ≠ f' x
⊢ (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) z₁ = (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) z₂ → z₁ = z₂

Tactic:
by_cases h₁ : z₁ = x

Goal state after:
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
z₁ z₂ : ι
key : ∀ {x : ↑ι'}, y ≠ f' x
h₁ : z₁ = x
⊢ (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) z₁ = (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) z₂ → z₁ = z₂

case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
z₁ z₂ : ι
key : ∀ {x : ↑ι'}, y ≠ f' x
h₁ : ¬z₁ = x
⊢ (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) z₁ = (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) z₂ → z₁ = z₂
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case neg
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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : Pairwise (Wbtw R head) (head2 :: tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
hl'' : map (⇑(lineMap ((head2 :: tail).head ht) ((head2 :: tail).getLast ht))) l'' = head2 :: tail
ht2 : ¬tail = []
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head ((head2 :: tail).getLast ht))) l' = head :: head2 :: tail

Tactic:
simp only [head_cons, getLast_cons ht2] at hl'' ⊢

Goal state after:
case neg
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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : Pairwise (Wbtw R head) (head2 :: tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
ht2 : ¬tail = []
hl'' : map (⇑(lineMap head2 (tail.getLast ht2))) l'' = head2 :: tail
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht2))) l' = head :: head2 :: tail
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
x : ↑s
⊢ sSup {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c} x = s.domRestrict φ x

Tactic:
sSup_apply

Goal state after:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
x : ↑s
⊢ ⨆ f, ↑f x = s.domRestrict φ x
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : FiniteDiagramArrow A.fst
hf : f ∈ A.snd
⊢ ∃ a ∈ A.snd, ιA a = ιA f

Tactic:
exact ⟨f, hf, rfl⟩

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : FiniteDiagramArrow B.fst
hf : f ∈ B.snd
⊢ ∃ a ∈ B.snd, ιB a = ιB f

Tactic:
exact ⟨f, hf, rfl⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ univ.domRestrict φ ∧ ∃ l c, f = univ.domRestrict (⇑re ∘ ⇑l) + const (↑univ) c} = univ.domRestrict φ
⊢ sSup {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c} = φ

Tactic:
simp only [domRestrict_eq] at this

Goal state after:
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
⊢ sSup {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c} = φ
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: case e'_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset ↥ι'
⊢ #s' = #(image Subtype.val s')

pp: case e'_4
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset ↥ι'
⊢ #(s'.biUnion fun i ↦ t ↑i) = #((image Subtype.val s').biUnion t)

Tactic:
· simp only [card_image_of_injective s' Subtype.coe_injective]

Goal state after:
case e'_4
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset ↥ι'
⊢ #(s'.biUnion fun i ↦ t ↑i) = #((image Subtype.val s').biUnion t)
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
hz : (s.weightedVSub p) (w₁ - w₂) = 0
hw₁w₂ : ∑ i ∈ s, (w₁ - w₂) i = 0
ha' : (w₁ - w₂) i = 0
⊢ w₁ i = w₂ i

Tactic:
rwa [Pi.sub_apply, sub_eq_zero] at ha'

Goal state after: