mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ¬∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u ≠ ⊤
⊢ IntervalIntegrable (fun x ↦ log ‖f x‖) volume a b

Tactic:
· rw [← hf.exists_meromorphicOrderAt_ne_top_iff_forall (isConnected_Icc inf_le_sup)] at t₀
    push Not at t₀
    have : (log ‖f ·‖) =ᶠ[Filter.codiscreteWithin (Ι a b)] 0 := by
      apply Filter.EventuallyEq.filter_mono _ (Filter.codiscreteWithin_mono Set.uIoc_subset_uIcc)
      filter_upwards [hf.meromorphicNFAt_mem_codiscreteWithin,
        Filter.self_mem_codiscreteWithin [[a, b]]] with x h₁x h₂x
      simp only [Pi.zero_apply, log_eq_zero, norm_eq_zero]
      left
      by_contra hCon
      simp_all [← h₁x.meromorphicOrderAt_eq_zero_iff, t₀ ⟨x, h₂x⟩]
    rw [intervalIntegrable_congr_codiscreteWithin this]
    apply Iff.mpr _root_.intervalIntegrable_const_iff
    tauto

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inr.inl
b : ℝ
h : b = 0
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

pp: case inr.inr
b : ℝ
h : 0 < b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
· simp [h]

Goal state after:
case inr.inr
b : ℝ
h : 0 < b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x = cos a - cos b

Tactic:
rw [integral_deriv_eq_sub' fun x => -cos x]
  · ring
  · simp
  · simp
  · exact continuousOn_sin

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
⊢ (fun x ↦ log ‖circleMap 0 1 x - 1‖) (x + 2 * π) = (fun x ↦ log ‖circleMap 0 1 x - 1‖) x

Tactic:
by simp [periodic_circleMap 0 1 x]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, 1 / (1 + x ^ 2) = arctan b - arctan a

Tactic:
refine integral_deriv_eq_sub' _ Real.deriv_arctan (fun _ _ => differentiableAt_arctan _)
    (continuous_const.div ?_ fun x => ?_).continuousOn

Goal state after:
case refine_1
a b : ℝ
⊢ Continuous fun x ↦ 1 + x ^ 2

case refine_2
a b x : ℝ
⊢ 1 + x ^ 2 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : 1 < ‖a‖
⊢ log ‖-a‖ = log ‖a‖

pp: a : ℂ
h : 1 < ‖a‖
⊢ InnerProductSpace.HarmonicOnNhd (fun x ↦ log ‖x - a‖) (closedBall 0 |1|)

Tactic:
norm_neg

Goal state after:
a : ℂ
h : 1 < ‖a‖
⊢ log ‖a‖ = log ‖a‖

a : ℂ
h : 1 < ‖a‖
⊢ InnerProductSpace.HarmonicOnNhd (fun x ↦ log ‖x - a‖) (closedBall 0 |1|)
Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SeminormedRing β
l : Filter α
f g : α → β
hf : f =o[l] fun _x ↦ 1
hg : l.BoundedAtFilter g
⊢ (f * g) =o[l] fun _x ↦ 1

Tactic:
simpa using! hf.mul_isBigO hg

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

Goal state before:
pp: case refine_1
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
⊢ ¬Dense (f '' U)

pp: case refine_2
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
z : ℂ
hz : z ∈ U
⊢ deriv f z ≠ 0

Tactic:
· -- Take a point `x ∈ U`.
    simp only [Dense, not_forall, mem_closure_iff_frequently, not_frequently]
    rcases hUc.nonempty with ⟨x, hx⟩
    -- Show that `-f x` has a neighborhood disjoint with `f '' U`.
    use -f x
    -- Since `f` is strictly differentiable at `x` with nonzero derivative,
    -- `f '' U` is a neighborhood of `f x`.
    have : f '' U ∈ 𝓝 (f x) := by
      rw [← (hdf x hx).map_nhds_eq (by simpa using hf₀ x hx)]
      exact Filter.image_mem_map <| hUo.mem_nhds hx
    -- Then `-f '' U` is a neighborhood of `-f x`.
    rw [nhds_neg, eventually_neg]
    -- This neighborhood has to be disjoint with `f '' U`,
    -- because `f a = - f b` implies `a = (f a) ^ 2 = (- f b) ^ 2 = b`, hence `f a = f b = 0`,
    -- which is impossible.
    filter_upwards [this]
    rintro _ ⟨a, ha, rfl⟩ ⟨b, hb, hab⟩
    obtain rfl : a = b := by
      rw [← hf_inv b, hab]
      simp [hf_inv a]
    refine hf₀ a ha ?_
    linear_combination hab / 2

Goal state after:
case refine_2
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
z : ℂ
hz : z ∈ U
⊢ deriv f z ≠ 0
Module: Mathlib.Analysis.Complex.JensenFormula

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

Tactic:
have t₀ : c ∈ CB := by simp [CB]

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

Goal state before:
pp: case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this : divisor f CB = 0
⊢ circleAverage (fun x ↦ log ‖f x‖) c R = log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top (by aesop),

Goal state after:
case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this : divisor f CB = 0
⊢ circleAverage (fun x ↦ log ‖f x‖) c R = log ‖0‖
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) a).sqrt = ↑√(re a)

Tactic:
RingEquiv.symm_apply_eq,

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ ((complexRingEquiv h) a).sqrt = (complexRingEquiv h) ↑√(re a)
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) (-a)).sqrt = I * sqrt a

Tactic:
RingEquiv.symm_apply_eq,

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ ((complexRingEquiv h) (-a)).sqrt = (complexRingEquiv h) (I * sqrt a)
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

Tactic:
RingEquiv.symm_apply_eq,

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ ((complexRingEquiv h) I).sqrt = (complexRingEquiv h) (↑√2⁻¹ * (1 - I) * I)
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

Tactic:
RingEquiv.symm_apply_eq,

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ ((complexRingEquiv h) (-I)).sqrt = (complexRingEquiv h) (↑√2⁻¹ * (1 + I) * -I)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp

Goal state before:
pp: ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)

Tactic:
rwa [Periodic.qParam, ofReal_one, div_one, Complex.norm_exp, Real.exp_le_exp,
    mul_right_comm, mul_I_re, neg_le_neg_iff, ← ofReal_ofNat, ← ofReal_mul, im_ofReal_mul,
    mul_comm _ π, mul_assoc, le_mul_iff_one_le_right Real.pi_pos, ← div_le_iff₀' two_pos]

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

Goal state before:
pp: case neg
X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f

Tactic:
have hf' x : f x ∈ Metric.closedBall 0 ‖f‖ := by simpa using! f.norm_coe_le_norm x

Goal state after:
case neg
X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)
hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

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

Tactic:
constructor
  · rintro ⟨z, hz⟩
    linear_combination
      (norm := { simp [σ, h.not_gt, num, denom, z.im_ne_zero, Matrix.trace_fin_two, field] })
      congr($(gl_smul_eq_iff_num_eq.mp hz).im / z.im)
  · intro hadd
    by_cases hc : g 1 0 = 0
    · use ⟨⟨g 0 1 / (2 * g 1 1), 1⟩, one_pos⟩
      simp [gl_smul_eq_self_iff_re_eq, *]
    · use ⟨⟨-g 1 1 / g 1 0, √(-g.val.det) / |g 1 0|⟩, by simp [*]⟩
      simp [gl_smul_eq_self_iff_dist_sq_eq, *, dist_eq_norm, ← Complex.normSq_eq_norm_sq,
        Complex.normSq_apply, ← pow_two, div_pow, h.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 : 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)‖

Tactic:
dist_eq_norm',

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 : ℕ
⊢ ‖g n + F (f - (g n).compContinuous e) - g n‖ = ‖F (f - (g n).compContinuous e)‖
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 : ℕ
⊢ ‖f - (g n).compContinuous e‖ / 3 = 1 / 3 * dist ((g n).compContinuous e) f

Tactic:
dist_eq_norm',

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 : ℕ
⊢ ‖f - (g n).compContinuous e‖ / 3 = 1 / 3 * ‖f - (g n).compContinuous e‖
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

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

Tactic:
aesop (add simp GeneralLinearGroup.center_eq_range_scalar)

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

Goal state before:
pp: z : ℂ
hz : 0 < z.im
⊢ UpperHalfPlane.coe ∘ ↑ofComplex =ᶠ[𝓝 z] id

Tactic:
by
  filter_upwards [isOpen_upperHalfPlaneSet.mem_nhds hz] with x hx
  simp only [Function.comp_apply, ofComplex_apply_of_im_pos hx, id_eq]

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

Goal state before:
pp: τ : ℍ
⊢ J • τ = ↑ofComplex (-(starRingEnd ℂ) ↑τ)

Tactic:
ext
  rw [coe_J_smul, ofComplex_apply_of_im_pos (by simpa using τ.im_pos)]

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

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

Tactic:
refine fun ha ↦ (g ^ 2).det_ne_zero ?_

Goal state after:
case refine_2
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
ha : a = 0
⊢ (↑(g ^ 2)).det = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

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

Tactic:
intro hg11

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

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

Tactic:
intro hg11

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

Goal state before:
pp: z : ℍ
this✝ : ↑√z.im ≠ 0
this : ↑z.re / ↑√z.im + ↑√z.im * Complex.I = ↑z * (↑√z.im)⁻¹
⊢ ↑((algebraMap ℝ ℝ) (↑z.toSL2R 0 0)) * ↑I + ↑((algebraMap ℝ ℝ) (↑z.toSL2R 0 1)) =
    ↑z * (↑((algebraMap ℝ ℝ) (↑z.toSL2R 1 0)) * ↑I + ↑((algebraMap ℝ ℝ) (↑z.toSL2R 1 1)))

Tactic:
simpa [add_comm]

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

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
⊢ -toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (-g)) • z = g • z

Tactic:
congr 1 with i j

Goal state after:
case e_a
g : SL(2, ℤ)
z : ℍ
i j : Fin 2
⊢ ↑(-toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (-g))) i j = ↑((mapGL ℝ) g) i j
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:
not_not

Goal state after:
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
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 : m
hi✝ : (i ≠ k) = False
hi : ¬i ≠ k
j : m
hj✝ : (j ≠ k) = False
hj : ¬j ≠ k
⊢ (auxMat M k).toSquareBlock (fun x ↦ x ≠ k) False ⟨i, hi✝⟩ ⟨j, hj✝⟩ = 1 ⟨i, hi✝⟩ ⟨j, hj✝⟩

Tactic:
not_not

Goal state after:
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i : m
hi✝ : (i ≠ k) = False
hi : i = k
j : m
hj✝ : (j ≠ k) = False
hj : j = k
⊢ (auxMat M k).toSquareBlock (fun x ↦ x ≠ k) False ⟨i, hi✝⟩ ⟨j, hj✝⟩ = 1 ⟨i, hi✝⟩ ⟨j, hj✝⟩
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝ : Infinite ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
rw [Algebra.norm_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bS),
      det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis (bS.smulTower bA))]

Goal state after:
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
⊢ inversion c (dist x c) x = x

Tactic:
inversion_dist_center

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
⊢ x = 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
⊢ Tendsto (f ∘ some) (coclosedCompact X) (𝓝 (f ∞)) ↔
    ∀ s ∈ 𝓝 (f ∞), ∃ t, IsClosed[inst✝¹] t ∧ IsCompact t ∧ MapsTo (f ∘ some) tᶜ s

Tactic:
simp only [hasBasis_coclosedCompact.tendsto_left_iff, and_assoc]

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

Goal state before:
pp: Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint ℕ → Y
⊢ Continuous[_, inst✝] f ↔ Tendsto (fun x ↦ f ↑x) atTop (𝓝 (f ∞))

Tactic:
rw [continuous_iff_from_discrete, Nat.cofinite_eq_atTop]

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

Goal state before:
pp: ⊢ Continuous ↿denom

Tactic:
unfold denom

Goal state after:
⊢ Continuous ↿fun g z ↦ ↑(↑g 1 0) * z + ↑(↑g 1 1)
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤)

Tactic:
logCounting_inv

Goal state after:
f : ℂ → ℂ
h : Meromorphic f
⊢ circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤) =
    circleAverage (fun x ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤)
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:
rw [← sum_apply_smul_single_eq_self_on_univ h, map_sum]
  exact Asymptotics.IsBigO.sum fun _ _ ↦ logCounting_single_isBigO_log

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a : WithTop E
h : a = ⊤
⊢ logCounting f a 0 = 0

Tactic:
simp [logCounting, h]

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

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

Tactic:
simp [logCounting, h]

Goal state after:
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:
rw [← card_image_of_injective s' Subtype.coe_injective]

Goal state after:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
⊢ #(image (fun a ↦ ↑a) s') ≤ #(s'.biUnion fun a' ↦ t ↑a')
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
⊢ Nonempty ↑(limitCone F).pt

Tactic:
use u

Goal state after:
case property
J : Type u
inst✝⁴ : SmallCategory J
F : J ⥤ TopCat
inst✝³ : IsCofilteredOrEmpty J
inst✝² : ∀ (j : J), Nonempty ↑(F.obj j)
inst✝¹ : ∀ (j : J), CompactSpace ↑(F.obj j)
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
u : (j : J) → ↑(F.obj j)
hu : u ∈ ⋂ i, partialSections F i.snd
⊢ u ∈ {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j}
Module: Mathlib.CategoryTheory.CofilteredSystem

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

Tactic:
obtain ⟨k, g, g', he⟩ := cospan f f'

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : i ⟶ j
h : ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))
j' : J
f' : j' ⟶ j
k : J
g : k ⟶ i
g' : k ⟶ j'
he : g ≫ f = g' ≫ f'
⊢ range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map f'))
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
hinj : Injective ↑f
hc : ∀ (x : ↥ι''), ↑f x ∈ t ↑x
i : ι
hi : i ∈ ι'
j : ι
hj : j ∈ ι'
hh : (fun i ↦ ↑f ⟨↑i, ⋯⟩) ⟨i, hi⟩ = (fun i ↦ ↑f ⟨↑i, ⋯⟩) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
simpa only [Subtype.mk_eq_mk] using hinj hh

Goal state after: