mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.refine_2
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
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
⊢ dist ((g.compContinuous e) x) (f x) ≤ 2 / 3 * ‖f‖

Tactic:
rcases le_total (f x) (-‖f‖ / 3) with hle₁ | hle₁

Goal state after:
case inr.refine_2.inl
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
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
hle₁ : f x ≤ -‖f‖ / 3
⊢ dist ((g.compContinuous e) x) (f x) ≤ 2 / 3 * ‖f‖

case inr.refine_2.inr
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
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ f x
⊢ dist ((g.compContinuous e) x) (f x) ≤ 2 / 3 * ‖f‖
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
⊢ g • z = z ↔ ‖↑z - -↑(↑g 1 1) / ↑(↑g 1 0)‖ ^ 2 * ↑g 1 0 ^ 2 = -(↑g).det

Tactic:
← Complex.normSq_eq_norm_sq,

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ g • z = z ↔ Complex.normSq (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)) * ↑g 1 0 ^ 2 = -(↑g).det
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: w w' : ℂ
hw : w.im ≤ 0
hw' : w'.im ≤ 0
⊢ ↑ofComplex w = ↑ofComplex w'

Tactic:
simp [ofComplex_apply_of_im_nonpos, hw, hw']

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
hgf : ⇑g ∘ e = ⇑f
ha' : ¬∃ x, f x = a
⊢ Disjoint (range e) (⇑g ⁻¹' {a})

Tactic:
Set.disjoint_left

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
hgf : ⇑g ∘ e = ⇑f
ha' : ¬∃ x, f x = a
⊢ ∀ ⦃a_1 : Y⦄, a_1 ∈ range e → a_1 ∉ ⇑g ⁻¹' {a}
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((evalRingHom 0).mapMatrix (↑(compRingEquiv m n R[X]) ((cornerAddX M k).map ⇑f.polyToMatrix))).det =
    (↑(compRingEquiv m n R) (M.map ⇑f)).det

Tactic:
← RingHom.mapMatrix_apply,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((evalRingHom 0).mapMatrix (↑(compRingEquiv m n R[X]) (f.polyToMatrix.mapMatrix (cornerAddX M k)))).det =
    (↑(compRingEquiv m n R) (f.mapMatrix M)).det
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
⊢ Disjoint (range e) (⇑g ⁻¹' {b})

Tactic:
Set.disjoint_left

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
⊢ ∀ ⦃a : Y⦄, a ∈ range e → a ∉ ⇑g ⁻¹' {b}
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: f : ℍ → ℂ
τ : ℍ
⊢ MDiffAt f τ ↔ DifferentiableAt ℂ (f ∘ ↑ofComplex) ↑τ

Tactic:
← mdifferentiableAt_iff_differentiableAt

Goal state after:
f : ℍ → ℂ
τ : ℍ
⊢ MDiffAt f τ ↔ MDiffAt (f ∘ ↑ofComplex) ↑τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

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

Tactic:
← add_div,

Goal state after:
a b c : ℍ
⊢ (dist ↑a ↑b * dist (↑b) ((starRingEnd ℂ) ↑c) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
⊢ dist b c * dist b d ≤ dist b b * dist c d + dist b c * dist b d

Tactic:
dist_self,

Goal state after:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
⊢ dist b c * dist b d ≤ 0 * dist c d + dist b c * dist b d
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ c
⊢ dist c c * dist b d ≤ dist c b * dist c d + dist b c * dist c d

Tactic:
dist_self,

Goal state after:
case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ c
⊢ 0 * dist b d ≤ dist c b * dist c d + dist b c * dist c d
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
⊢ dist d c * dist b d ≤ dist d b * dist c d + dist b c * dist d d

Tactic:
dist_self,

Goal state after:
case inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
⊢ dist d c * dist b d ≤ dist d b * dist c d + dist b c * 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z✝ w : ℍ
r : ℝ
z : ℍ
⊢ 2 * arsinh (dist ↑z ↑z / (2 * √(z.im * z.im))) = 0

Tactic:
dist_self,

Goal state after:
z✝ w : ℍ
r : ℝ
z : ℍ
⊢ 2 * arsinh (0 / (2 * √(z.im * z.im))) = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case e_a
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ |↑a| * dist ↑y₁ ↑y₂ / (2 * (|↑a| * √(y₁.im * y₂.im))) = dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))

Tactic:
mul_left_comm

Goal state after:
case e_a
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ |↑a| * dist ↑y₁ ↑y₂ / (|↑a| * (2 * √(y₁.im * y₂.im))) = dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
⊢ T2Space (Quotient (MulAction.orbitRel G X))

Tactic:
t2_iff_isClosed_diagonal

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
⊢ IsClosed[instTopologicalSpaceProd] (diagonal (Quotient (MulAction.orbitRel G X)))
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
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
⊢ IsClosed {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}

Tactic:
apply isClosed_eq

Goal state after:
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)

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
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)
proper_f : IsProperMap f
⊢ T2Space X

Tactic:
t2_iff_isClosed_diagonal

Goal state after:
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)
proper_f : IsProperMap f
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
⊢ Continuous[instTopologicalSpace, inst✝] f ↔
    Tendsto (fun x ↦ f ↑x) (coclosedCompact X) (𝓝 (f ∞)) ∧ Continuous[inst✝¹, inst✝] fun x ↦ f ↑x

Tactic:
by
  simp only [continuous_iff_continuousAt, OnePoint.forall, continuousAt_coe, continuousAt_infty',
    Function.comp_def]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
z : E
f : locallyFinsupp E ℤ
ha : z ∈ closedBall 0 |r|
⊢ ((toClosedBall r) f) z = f z

Tactic:
by
  unfold toClosedBall
  simp_all [restrict_apply]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
⊢ |characteristic f ⊤ r - characteristic (fun x ↦ f x - a₀) ⊤ r| ≤ log⁺ ‖a₀‖ + log 2

Tactic:
have h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r := by
    apply MeromorphicOn.circleIntegrable_posLog_norm
    apply h.meromorphicOn.sub (MeromorphicOn.const a₀)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ |characteristic f ⊤ r - characteristic (fun x ↦ f x - a₀) ⊤ r| ≤ log⁺ ‖a₀‖ + log 2
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
α : ℝ
⊢ (cartanKernel f R α β)⁺ = log⁺ ‖f (circleMap 0 R β) + -circleMap 0 1 α‖

Tactic:
simp [cartanKernel, posLog_def, posPart, max_comm, sub_eq_add_neg]

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

Goal state before:
pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : ‖e‖ < a
b : ℝ
hb : ‖e‖ < b
hab : a < b
⊢ logCounting (single e 1) a < logCounting (single e 1) b

Tactic:
logCounting_single_eq_log_sub_const ha.le,

Goal state after:
case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : ‖e‖ < a
b : ℝ
hb : ‖e‖ < b
hab : a < b
⊢ ↑1 * (log a - log ‖e‖) < logCounting (single e 1) b
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.refine_1.refine_2
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
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : (∀ a' ∈ tail, head ≠ a') ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ Triplewise (Sbtw R) tail

Tactic:
exact (ih.1 ⟨ht, hpne.2⟩).1

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

Goal state before:
pp: case refine_1
𝕜 : 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
l : E →L[𝕜] 𝕜
c : ℝ
hlc : s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c ≤ s.domRestrict φ ∧ re (l ↑x) + c = φ ↑x - 1
⊢ (range fun f ↦ ↑f x).Nonempty

Tactic:
exact ⟨φ x - 1, hlc.2 ▸ ⟨⟨s.domRestrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩, rfl⟩⟩

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

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
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
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
⊢ Fintype.card ↥sᶜ < Fintype.card ι

Tactic:
rwa [Fintype.card_coe, card_compl_lt_iff_nonempty]

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

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
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
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
have card_ι''_le : Fintype.card ι'' ≤ n := by
    simp_rw [ι'', ← Nat.lt_succ_iff, ← hn, ← Finset.coe_compl, coe_sort_coe]
    rwa [Fintype.card_coe, card_compl_lt_iff_nonempty]

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
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
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
card_ι''_le : Fintype.card ↑ι'' ≤ n
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
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
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
card_ι''_le : Fintype.card ↑ι'' ≤ n
f'' : ↑ι'' → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' ⟨x'', hx''⟩ ∉ s.biUnion t
im_disj : ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s), f' ⟨x', hx'⟩ ≠ f'' ⟨x'', hx''⟩
x : ι
h : x ∉ s
⊢ f'' ⟨x, h⟩ ∈ t x

Tactic:
exact sdiff_subset (hsf'' ⟨x, h⟩)

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

Goal state before:
pp: case pos
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 y : P
r : R
hxy : x = y
⊢ Wbtw R x ((lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1

Tactic:
rw [hxy, lineMap_same_apply]

Goal state after:
case pos
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 y : P
r : R
hxy : x = y
⊢ Wbtw R y y y ↔ y = y ∨ r ∈ Set.Icc 0 1
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
f : FiniteDiagramArrow G
a✝ : f ∈ ↑H
⊢ IsClosed {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}

Tactic:
apply isClosed_eq

Goal state after:
case hf
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
f : FiniteDiagramArrow G
a✝ : f ∈ ↑H
⊢ Continuous fun y ↦ (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (y f.fst)

case hg
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
f : FiniteDiagramArrow G
a✝ : f ∈ ↑H
⊢ Continuous fun y ↦ y f.snd.fst
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ f b
x✝ : α
a✝ : γ
⊢ (if x✝ = a then some b else none).bind ⇑f = some a✝ ↔ (if x✝ = a then some c else none) = some a✝

Tactic:
split_ifs <;> simp_all

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝¹ : δ
a✝¹ : γ
h : ∀ (a : δ), ¬f a = some b
x✝ : β
a✝ : f x✝¹ = some x✝
⊢ ¬(if x✝ = b then some c else none) = some a✝¹

Tactic:
split_ifs <;> simp_all

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

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
⊢ (if j✝ ∈ some (if i✝ = i then j else if i✝ = j then i else i✝) then 1 else 0) =
    ((((if i✝ = j✝ then 1 else 0) - if j✝ ∈ if i✝ = i then some i else none then 1 else 0) -
          if j✝ ∈ if i✝ = j then some j else none then 1 else 0) +
        if j✝ ∈ if i✝ = i then some j else none then 1 else 0) +
      if j✝ ∈ if i✝ = j then some i else none then 1 else 0

Tactic:
split_ifs <;> simp_all

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✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁' : p ∈ line[R, t.points i₁, p₁]
h₂' : p ∈ line[R, t.points i₂, p₂]
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₁)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₁)
⊢ False

Tactic:
simp at h₂

Goal state after: