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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
z : ℂ
hz : z ∈ sphere 0 |R|
hzR : ‖z‖ = R
⊢ ↑R * cexp (↑z.arg * I) / (↑R * cexp (↑z.arg * I) - w) -
      ↑‖w‖ * cexp (↑z.arg * I) / (↑‖w‖ * cexp (↑z.arg * I) - ↑R * cexp (↑w.arg * I)) =
    ↑R * cexp (↑z.arg * I) / (↑R * cexp (↑z.arg * I) - w) -
      ↑‖w‖ / ↑R * (↑R * cexp (↑z.arg * I)) / (↑‖w‖ / ↑R * (↑R * cexp (↑z.arg * I)) - ↑R * cexp (↑w.arg * I))

Tactic:
field [hR.ne.symm]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : z.re ≤ 0
⊢ |x₀ - z.re| = |(z - ↑x₀).re|

Tactic:
sub_re,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : z.re ≤ 0
⊢ |x₀ - z.re| = |z.re - (↑x₀).re|
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case neg
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)

Tactic:
replace h : -1 < r.re := by tauto

Goal state after:
case neg
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z✝ : ℂ
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z✝.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
z : ℂ
⊢ expR (↑ε * z).re * ‖f z‖ = expR (ε * z.re) * ‖f z‖

Tactic:
re_ofReal_mul

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z✝ : ℂ
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z✝.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
z : ℂ
⊢ expR (ε * z.re) * ‖f z‖ = expR (ε * z.re) * ‖f z‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
c : ℂ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, Complex.exp (c * ↑x) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c

Tactic:
have D : ∀ x : ℝ, HasDerivAt (fun y : ℝ => Complex.exp (c * y) / c) (Complex.exp (c * x)) x := by
    intro x
    conv => congr
    rw [← mul_div_cancel_right₀ (Complex.exp (c * x)) hc]
    apply ((Complex.hasDerivAt_exp _).comp x _).div_const c
    simpa only [mul_one] using! ((hasDerivAt_id (x : ℂ)).const_mul _).comp_ofReal
  rw [integral_deriv_eq_sub' _ (funext fun x => (D x).deriv) fun x _ => (D x).differentiableAt]
  · ring
  · fun_prop

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

Goal state before:
pp: a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
⊢ circleAverage (fun x ↦ log ‖x - a‖) c R = log R

Tactic:
by
  by_cases hR : R = 0
  · simp_all
  rw [circleAverage_log_norm_sub_const_eq_log_radius_add_posLog hR, add_eq_left,
    posLog_eq_zero_iff, abs_mul, abs_inv, abs_of_nonneg (norm_nonneg (c - a))]
  rw [mem_closedBall, dist_eq_norm'] at hu
  apply inv_mul_le_one_of_le₀ hu (abs_nonneg R)

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

Goal state before:
pp: a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, sin x ^ n

Tactic:
field_simp
  convert! eq_sub_iff_add_eq.mp (integral_sin_pow_aux n) using 1
  ring

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
⊢ (fun z ↦ f z - cuspFunction h f 0) =O[I∞] fun z ↦ rexp (-2 * π * z.im / h)

Tactic:
by
  simpa [comp_def, eq_cuspFunction hh.ne' hf, norm_qParam] using
    differentiableAt_cuspFunction_zero hh hf h_hol h_bd |>.isBigO_sub.mono
      nhdsWithin_le_nhds |>.comp_tendsto (qParam_tendsto hh) |>.norm_right

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ s
⊢ x ∈ s

Tactic:
assumption

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ t

Tactic:
assumption

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

Goal state before:
pp: case inl
α : 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
x : α
hxc : x ≤ c
h✝ : x ∈ s
⊢ x ∈ s

Tactic:
assumption

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

Goal state before:
pp: α : 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
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ t

Tactic:
assumption

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

Goal state before:
pp: case refine_3
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 : ℂ
⊢ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
by_cases h1 : u ∈ closedBall c |R|

Goal state after:
case pos
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|
⊢ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)

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|
⊢ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)
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‖)
hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖
g : C(X, E)
hg : ContinuousMap.restrict s g = ↑f
hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f

Tactic:
let g' : X →ᵇ E := .ofNormedAddCommGroup g (map_continuous g) ‖f‖ hg_mem

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 : C(X, E)
hg : ContinuousMap.restrict s g = ↑f
hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case «0»
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
this : cd 0 = 0
h : cd 1 = 0
⊢ cd ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
assumption

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

Goal state before:
pp: case «1»
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
this : cd 0 = 0
h : cd 1 = 0
⊢ cd ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
assumption

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

Goal state before:
pp: g✝ : GL (Fin 2) ℝ
z w : ℍ
g : GL (Fin 2) ℝ
hell : g.IsElliptic
⊢ 0 < ((↑(↑g 0 0) - ↑(↑g 1 1)) / (2 * ↑(↑g 1 0)) + Complex.I * (↑√(-(↑g).discr) / (2 * ↑|↑g 1 0|))).im

Tactic:
by
    simpa [div_pos, Complex.div_re, Complex.div_im, hell.c_ne_zero]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
⊢ g • I = I ↔ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 = -↑g 1 0

Tactic:
rw [gl_smul_eq_iff_num_eq, σ, if_pos hg]
  simp [Complex.ext_iff, num, denom, and_comm]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : m.IsElliptic
⊢ m 0 1 * m 1 0 ≠ 0

Tactic:
intro hc
  rw [IsElliptic, discr_fin_two, trace_fin_two, det_fin_two, hc] at hm
  refine hm.not_ge ?_
  linear_combination sq_nonneg (m 0 0 - m 1 1)

Goal state after:
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 _)
      rw [eq_neg_iff_add_eq_zero, ← Matrix.trace_fin_two] at ha
      rcases eq_or_ne (g 1 0) 0 with hc | hc
      · specialize hg ⟨1 + .I, by simp⟩
        rw [gl_smul_eq_self_iff_re_eq ha hc] at hg
        simp_all
      · have : 0 < 1 + √(-g.val.det) / |g 1 0| := by simp [add_pos, *]
        specialize hg ⟨⟨-g 1 1 / g 1 0, 1 + √(-g.val.det) / |g 1 0|⟩, this⟩
        simp [gl_smul_eq_self_iff_dist_eq hlt ha hc, Complex.dist_eq_re_im, Real.sqrt_sq this.le]
          at hg

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0 → ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))

pp: case mpr
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2)) → C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0

Tactic:
· refine fun hP ↦ ⟨g 0 0, ?_⟩
    have hb : g 0 1 = 0 := by simpa using congr_arg (coeff · 0) hP
    have hc : g 1 0 = 0 := by simpa using congr_arg (coeff · 2) hP
    have hd : g 1 1 = g 0 0 := by simpa [sub_eq_zero] using congr_arg (coeff · 1) hP
    ext i j
    fin_cases i <;>
    fin_cases j <;>
    simp [hb, hc, hd]

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2)) → C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
this : (↑g).trace ^ 2 = 4 * (↑g).det
⊢ (↑g).trace / 2 ≠ 0

Tactic:
div_ne_zero_iff,

Goal state after:
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
this : (↑g).trace ^ 2 = 4 * (↑g).det
⊢ (↑g).trace ≠ 0 ∧ 2 ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : SL(2, ℝ)
hc : ↑g 1 0 ≠ 0
h_denom : ∀ (z : ℍ), denom (toGL g) ↑z ≠ 0
⊢ ∃ u v w, (fun x ↦ g • x) = (fun x ↦ w +ᵥ x) ∘ (fun x ↦ ModularGroup.S • x) ∘ (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x

Tactic:
induction g using Matrix.SpecialLinearGroup.fin_two_induction with | _ a b c d h => ?_

Goal state after:
case h
a b c d : ℝ
h : a * d - b * c = 1
hc : ↑⟨!![a, b; c, d], ⋯⟩ 1 0 ≠ 0
h_denom : ∀ (z : ℍ), denom (toGL ⟨!![a, b; c, d], ⋯⟩) ↑z ≠ 0
⊢ ∃ u v w,
    (fun x ↦ ⟨!![a, b; c, d], ⋯⟩ • x) =
      (fun x ↦ w +ᵥ x) ∘ (fun x ↦ ModularGroup.S • x) ∘ (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x
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:
simp [auxMat, toSquareBlock_def, if_pos hi, if_pos hj, Matrix.one_apply, if_pos (hj ▸ hi)]

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

Goal state before:
pp: case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
let M' := cornerAddX M k

Goal state after:
case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ 0 < sinh x ↔ 0 < x

Tactic:
simpa only [sinh_zero] using @sinh_lt_sinh 0 x

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ ↑(Ultrafilter.map pure g) ≤ 𝓝 g

Tactic:
rw [ultrafilter_converges_iff, ← bind_pure g]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ g >>= pure = joinM (Ultrafilter.map pure (g >>= pure))
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⇑(continuousMapMkNat u p hup) ∘ ULift.down
⊢ Tendsto OnePoint.some cofinite (𝓝 ∞)

Tactic:
← cocompact_eq_cofinite,

Goal state after:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⇑(continuousMapMkNat u p hup) ∘ ULift.down
⊢ Tendsto OnePoint.some (cocompact ℕ) (𝓝 ∞)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe.infty
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
⊢ ↑x✝ ⤳ ∞ ∨ Disjoint (𝓝 ↑x✝) (𝓝 ∞)

Tactic:
exact .inr (key _)

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst✝¹] (s ∩ K)) → IsClosed[inst✝¹] s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst✝¹] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed[inst✝¹] (s ∩ K)

Tactic:
rw [Set.inter_comm, ← Subtype.image_preimage_coe]

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst✝¹] (s ∩ K)) → IsClosed[inst✝¹] s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst✝¹] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed[inst✝¹] (Subtype.val '' Subtype.val ⁻¹' s)
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
⊢ CircleIntegrable (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

Tactic:
by_cases h: ¬MeromorphicAt f 0

Goal state after:
case pos
f : ℂ → ℂ
h : ¬MeromorphicAt f 0
⊢ CircleIntegrable (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

case neg
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
⊢ CircleIntegrable (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1
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
r : ℝ
f : 𝕜 → E
e : WithTop E
hr : 1 ≤ r
h : ¬e = ⊤
⊢ 0 ≤ logCounting f e r

Tactic:
simp [logCounting, h, locallyFinsuppWithin.logCounting_nonneg
      (posPart_nonneg (divisor (f · - e.untop₀) univ)) hr]

Goal state after:
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
inst✝ : Nontrivial P
l : List P
hl✝ : ¬l = []
hlen : ¬l.length = 1
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap (l.head hl✝) (l.getLast hl✝))) l' = l
hl : l.head hl✝ ≠ l.getLast hl✝
⊢ l.head hl✝ ≠ l.getLast hl✝ ∧ ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl✝) (l.getLast hl✝))) l' = l

Tactic:
exact ⟨hl, l', hl's, hl'l⟩

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

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
X Y : J
hX : X ∈ G
hY : Y ∈ G
f : X ⟶ Y
hf : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ (ConcreteCategory.hom (F.map f))
      (if hj : X ∈ G then (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hj))) ⋯.some else ⋯.some) =
    if hj : Y ∈ G then (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hj))) ⋯.some else ⋯.some

Tactic:
rwa [dif_pos hX, dif_pos hY, ← comp_app, ← F.map_comp, @IsCofiltered.infTo_commutes _ _ _ G H]

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

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑(hallMatchingsOn t ι')

Tactic:
rw [hallMatchingsOn]

Goal state after:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑{f | Injective f ∧ ∀ (x : ↥ι'), f x ∈ t ↑x}
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
right✝ : t ≤ 1
⊢ SameRay R ((lineMap x z) t -ᵥ x) (z -ᵥ x)

Tactic:
simp [SameRay.sameRay_nonneg_smul_left (z -ᵥ x) ht0]

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
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
⊢ ((reindex e₂ e₁) Mᵀ)ᵀ ∈ colStochastic R m ↔ M ∈ colStochastic R n

Tactic:
transpose_mem_colStochastic_iff_mem_rowStochastic,

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
⊢ (reindex e₂ e₁) Mᵀ ∈ rowStochastic R m ↔ M ∈ colStochastic R n
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
⊢ M ∈ rowStochastic R n ⊓ colStochastic R n ↔ M ∈ rowStochastic R n ∧ M ∈ colStochastic R n

Tactic:
Submonoid.mem_inf

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
⊢ M ∈ rowStochastic R n ∧ M ∈ colStochastic R n ↔ M ∈ rowStochastic R n ∧ M ∈ colStochastic R n
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: 𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ AffineIndependent 𝕜 Subtype.val

Tactic:
let k := #(minCardFinsetOfMemConvexHull hx) - 1

Goal state after:
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
k : ℕ := #(minCardFinsetOfMemConvexHull hx) - 1
⊢ AffineIndependent 𝕜 Subtype.val