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

Goal state before:
pp: a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x ↦ cos (2 * x) ^ 2
x✝ : ℝ
⊢ cos x✝ * sin x✝ = sin (2 * x✝) / 2

Tactic:
sin_two_mul

Goal state after:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x ↦ cos (2 * x) ^ 2
x✝ : ℝ
⊢ cos x✝ * sin x✝ = 2 * sin x✝ * cos x✝ / 2
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: ⊢ (-I).sqrt = ↑√2⁻¹ * (1 - I)

Tactic:
rw [sqrt, ← re_add_im ((-I) ^ 2⁻¹), cpow_inv_two_im_eq_neg_sqrt (by simp), cpow_inv_two_re]
  simp [mul_sub, ← sub_eq_add_neg]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) I).sqrt = ↑√2⁻¹ * (1 - I) * I

pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : ¬im I = 1
⊢ ↑√(re I) = ↑√2⁻¹ * (1 - I) * I

Tactic:
· simp_rw [RingEquiv.symm_apply_eq, map_mul]
    simp [h, mul_assoc, mul_add, add_comm, Complex.sqrt_I, add_mul]

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : ¬im I = 1
⊢ ↑√(re I) = ↑√2⁻¹ * (1 - I) * I
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_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ dist (g n) (g (n + 1)) = ‖F (f - (g n).compContinuous e)‖

Tactic:
g_succ,

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)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ dist (g n) (g n + F (f - (g n).compContinuous e)) = ‖F (f - (g n).compContinuous e)‖
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mp.inl
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g).det < 0
⊢ False

Tactic:
obtain ⟨ha, hb⟩ := (gl_smul_I_eq_I_iff_of_neg hlt).mp (hg _)

Goal state after:
case mp.inl
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g).det < 0
ha : ↑g 0 0 = -↑g 1 1
hb : ↑g 0 1 = ↑g 1 0
⊢ False
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
⊢ ∃ ε > 0, Metric.ball ‖↑τ‖ ε ⊆ U

Tactic:
refine ⟨ε, hεpos, subset_trans (fun r hr ↦ ?_) hs'⟩

Goal state after:
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
⊢ r ∈ (fun τ ↦ ‖↑τ‖) '' s
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
⊢ (diagonal fun x ↦ a ^ n * a) + (a * (↑n * a ^ (n - 1)) + a ^ n) • m =
    (diagonal fun x ↦ a ^ n * a) + (↑n * a ^ n + a ^ n) • m

Tactic:
(by lia : n = n - 1 + 1),

Goal state after:
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
⊢ (diagonal fun x ↦ a ^ (n - 1 + 1) * a) + (a * (↑(n - 1 + 1) * a ^ (n - 1 + 1 - 1)) + a ^ (n - 1 + 1)) • m =
    (diagonal fun x ↦ a ^ (n - 1 + 1) * a) + (↑(n - 1 + 1) * a ^ (n - 1 + 1) + a ^ (n - 1 + 1)) • m
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case 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
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)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
hge : (atTop.limUnder g).compContinuous e = f
⊢ ‖f‖ ≤ ‖atTop.limUnder g‖

Tactic:
rw [← hge]
    exact norm_compContinuous_le _ _

Goal state after:
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 : X → Y
he : IsClosedEmbedding e
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ ⇑g ∘ e = ⇑f

Tactic:
rcases exists_extension_norm_eq_of_isClosedEmbedding' f ⟨e, he.continuous⟩ he with ⟨g, hg, rfl⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
e : X → Y
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hg : ‖g‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ }‖
⊢ ∃ g_1,
    ‖g_1‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ }‖ ∧
      ⇑g_1 ∘ e = ⇑(g.compContinuous { toFun := e, continuous_toFun := ⋯ })
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ↑g 1 0 = 0
⊢ Tendsto (fun τ ↦ |↑g 0 0 / ↑g 1 1| * τ.im) atImInfty atTop

Tactic:
apply tendsto_comap.const_mul_atTop

Goal state after:
g : GL (Fin 2) ℝ
hg : ↑g 1 0 = 0
⊢ 0 < |↑g 0 0 / ↑g 1 1|
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: z : ℍ
⊢ !![√z.im, z.re / √z.im; 0, 1 / √z.im].det = 1

Tactic:
simp [mul_inv_cancel₀ (Real.sqrt_ne_zero'.mpr z.im_pos)]

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

Goal state before:
pp: f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (a : ℍ) in 𝓝 τ, ↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0
a : ℍ
⊢ (↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0) → a ∈ {τ}ᶜ → f a ≠ 0

Tactic:
ha

Goal state after:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (a : ℍ) in 𝓝 τ, ↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0
a : ℍ
ha : ↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0
⊢ a ∈ {τ}ᶜ → f a ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case convert_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (a : ℍ) in 𝓝 τ, ↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0
⊢ ∀ᶠ (x : ℍ) in 𝓝 τ, x ∈ {τ}ᶜ → f x ≠ 0

Tactic:
filter_upwards [hτ] with a ha

Goal state after:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (a : ℍ) in 𝓝 τ, ↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0
a : ℍ
ha : ↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0
⊢ a ∈ {τ}ᶜ → f a ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
hd : HasDerivAt (fun x ↦ denom g x) ↑(↑g 1 0) ↑τ
this : HasDerivAt ((fun x ↦ x ^ k) ∘ denom g) (↑k * denom g ↑τ ^ (k - 1) * ↑(↑g 1 0)) ↑τ
⊢ HasDerivAt (fun z ↦ denom g z ^ k) (↑k * ↑(↑g 1 0) * denom g ↑τ ^ (k - 1)) ↑τ

Tactic:
simpa only [Function.comp_def, mul_right_comm] using this

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

Goal state before:
pp: case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
x₁

Goal state after:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ : ↑X.toTop
⊢ ∀ ⦃a₂ : (fun X ↦ ↑X.toTop) X⦄, (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) a₂ → x₁ = a₂
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s ↦ {u | s ∈ u}) → i ∈ ↑u
a : Set α
⊢ a ∈ x → {v | a ∈ v} ∈ u

Tactic:
ha

Goal state after:
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s ↦ {u | s ∈ u}) → i ∈ ↑u
a : Set α
ha : a ∈ x
⊢ {v | a ∈ v} ∈ u
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:
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:
rwa [Nat.cofinite_eq_atTop]

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

Goal state before:
pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
⊢ a ∈ sphere 0 |1| →
    (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) a = (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0‖) a

Tactic:
ha

Goal state after:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) a = (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0‖) a
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
a : ℂ
⊢ a ∈ sphere 0 |1| →
    (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R + logCounting f ⊤ R) a =
      ((fun x ↦ logCounting f (↑x) R) + fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) a

Tactic:
ha

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R + logCounting f ⊤ R) a =
    ((fun x ↦ logCounting f (↑x) R) + fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) a
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R + logCounting f ⊤ R) a =
    ((fun x ↦ logCounting f (↑x) R) + fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) a

Tactic:
simp [logCounting_add_log_trailingCoeff_eq_circleAverage_add_logCounting_top h hR a]

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

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
a : ℝ
⊢ a ∈ Ioi 0 → ∀ ⦃b : ℝ⦄, b ∈ Ioi 0 → a ≤ b → characteristic f ⊤ a ≤ characteristic f ⊤ b

Tactic:
ha

Goal state after:
f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
⊢ ∀ ⦃b : ℝ⦄, b ∈ Ioi 0 → a ≤ b → characteristic f ⊤ a ≤ characteristic f ⊤ b
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a : ℝ
⊢ a ∈ Ioi 0 → ∀ ⦃b : ℝ⦄, b ∈ Ioi 0 → a ≤ b → logCounting D a ≤ logCounting D b

Tactic:
ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a : ℝ
ha : a ∈ Ioi 0
⊢ ∀ ⦃b : ℝ⦄, b ∈ Ioi 0 → a ≤ b → logCounting D a ≤ logCounting D b
Module: Mathlib.Analysis.ConstantSpeed

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

Tactic:
ENNReal.ofReal_toReal (h.1 x y xs ys)

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

Goal state before:
pp: 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 : ℝ
⊢ a > 0 → ∃ᶠ (x : ℝ) in atTop, ‖1 x‖ < a * ‖logCounting D x‖

Tactic:
ha

Goal state after:
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
⊢ ∃ᶠ (x : ℝ) in atTop, ‖1 x‖ < a * ‖logCounting D x‖
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 : ℝ
⊢ a ∈ Ioi ‖e‖ → ∀ ⦃b : ℝ⦄, b ∈ Ioi ‖e‖ → a < b → logCounting (single e 1) a < logCounting (single e 1) b

Tactic:
ha

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 : a ∈ Ioi ‖e‖
⊢ ∀ ⦃b : ℝ⦄, b ∈ Ioi ‖e‖ → a < b → logCounting (single e 1) a < logCounting (single e 1) b
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
⊢ a ∈ Ioi ‖e‖ → ∀ ⦃b : ℝ⦄, b ∈ Ioi ‖e‖ → a ≤ b → logCounting (D - single e 1) a ≤ logCounting (D - single e 1) b

Tactic:
ha

Goal state after:
case hg
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 : a ∈ Ioi ‖e‖
⊢ ∀ ⦃b : ℝ⦄, b ∈ Ioi ‖e‖ → a ≤ b → logCounting (D - single e 1) a ≤ logCounting (D - single e 1) b
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case neg.e_6
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
⊢ divisor (fun x ↦ f x - a.untop₀) univ = divisor (fun x ↦ g x - a.untop₀) univ

Tactic:
apply divisor_congr_codiscreteWithin _ isOpen_univ

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
⊢ (fun x ↦ f x - a.untop₀) =ᶠ[codiscreteWithin univ] fun x ↦ g x - a.untop₀
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
⊢ logCounting (divisor f univ) R = circleAverage (fun x ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
have h₁f : MeromorphicOn f (closedBall 0 |R|) := by tauto
  simp only [MeromorphicOn.circleAverage_log_norm hR h₁f, logCounting, AddMonoidHom.coe_mk,
    ZeroHom.coe_mk, zero_sub, norm_neg, add_sub_cancel_right]
  congr 1
  · simp_all
  · rw [divisor_apply, divisor_apply]
    all_goals aesop

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: case nil
α : Type u_1
l₁ l₂ : List α
p : α → α → α → Prop
⊢ Triplewise p ([] ++ l₂) ↔
    Triplewise p [] ∧
      Triplewise p l₂ ∧ (∀ (a : α), a ∈ [] → Pairwise (p a) l₂) ∧ ∀ (a : α), a ∈ l₂ → Pairwise (fun x y ↦ p x y a) []

Tactic:
grind [pairwise_cons]

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: case cons
α : Type u_1
l₁ l₂ : List α
p : α → α → α → Prop
head✝ : α
tail✝ : List α
tail_ih✝ :
  Triplewise p (tail✝ ++ l₂) ↔
    Triplewise p tail✝ ∧
      Triplewise p l₂ ∧
        (∀ (a : α), a ∈ tail✝ → Pairwise (p a) l₂) ∧ ∀ (a : α), a ∈ l₂ → Pairwise (fun x y ↦ p x y a) tail✝
⊢ Triplewise p (head✝ :: tail✝ ++ l₂) ↔
    Triplewise p (head✝ :: tail✝) ∧
      Triplewise p l₂ ∧
        (∀ (a : α), a ∈ head✝ :: tail✝ → Pairwise (p a) l₂) ∧
          ∀ (a : α), a ∈ l₂ → Pairwise (fun x y ↦ p x y a) (head✝ :: tail✝)

Tactic:
grind [pairwise_cons]

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

Goal state before:
pp: case cons.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]
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)

Tactic:
have ht' : tail.Wbtw R := ht.imp _root_.Sbtw.wbtw

Goal state after:
case cons.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]
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
⊢ #s' ≤ #(s'.biUnion fun a' ↦ t ↑a')

Tactic:
classical
    rw [← card_image_of_injective s' Subtype.coe_injective]
    convert! ht (s'.image fun z => z.1) using 1
    apply congr_arg
    ext y
    simp

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

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

Tactic:
ha

Goal state after:
case neg.refine_1
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
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2)) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2)) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw R ((lineMap head (tail.getLast ht2)) r :: tail)
ht : ¬(lineMap head (tail.getLast ht2)) r :: tail = []
hl'' :
  map (⇑(lineMap ((lineMap head (tail.getLast ht2)) r) (tail.getLast ht2))) l'' =
    (lineMap head (tail.getLast ht2)) r :: tail
a : R
ha : a ∈ l''
⊢ 0 ≤ r + (1 - r) * a
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case neg.refine_2.refine_1
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
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2)) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2)) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw R ((lineMap head (tail.getLast ht2)) r :: tail)
ht : ¬(lineMap head (tail.getLast ht2)) r :: tail = []
hl'' :
  map (⇑(lineMap ((lineMap head (tail.getLast ht2)) r) (tail.getLast ht2))) l'' =
    (lineMap head (tail.getLast ht2)) r :: tail
a : R
⊢ a ∈ l'' → 0 ≤ r + (1 - r) * a

Tactic:
ha

Goal state after:
case neg.refine_2.refine_1
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
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2)) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2)) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw R ((lineMap head (tail.getLast ht2)) r :: tail)
ht : ¬(lineMap head (tail.getLast ht2)) r :: tail = []
hl'' :
  map (⇑(lineMap ((lineMap head (tail.getLast ht2)) r) (tail.getLast ht2))) l'' =
    (lineMap head (tail.getLast ht2)) r :: tail
a : R
ha : a ∈ l''
⊢ 0 ≤ r + (1 - r) * a
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
x✝ : α
⊢ x✝ ∈ image f s → x✝ ∈ s.biUnion t

Tactic:
mem_image,

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
x✝ : α
⊢ (∃ a ∈ s, f a = x✝) → x✝ ∈ s.biUnion t
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg : ∀ (a : α) (b : β), b ∈ f a → b ∈ g a
gf : ∀ (a : α) (b : β), b ∈ g a → b ∈ f a
a : α
b : β
h : g a = some b
⊢ f a = some b

Tactic:
exact gf _ _ h

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : Matrix n n R
hx : x ∈ ↑(rowStochastic R n)
y : Matrix n n R
hy : y ∈ ↑(rowStochastic R n)
a b : R
⊢ 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ ↑(rowStochastic R n)

Tactic:
ha

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
x : Matrix n n R
hx : x ∈ ↑(rowStochastic R n)
y : Matrix n n R
hy : y ∈ ↑(rowStochastic R n)
a b : R
ha : 0 ≤ a
⊢ 0 ≤ b → a + b = 1 → a • x + b • y ∈ ↑(rowStochastic R n)