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

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
⊢ circleAverage (fun x ↦ log ‖1 - x⁻¹ * a‖) 0 1 = 0

Tactic:
rw [circleAverage_zero_one_congr_inv (f := fun x ↦ log ‖1 - x * a‖),
      InnerProductSpace.HarmonicOnNhd.circleAverage_eq, zero_mul, sub_zero,
      CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, log_one]

Goal state after:
a : ℂ
h : ‖a‖ < 1
⊢ InnerProductSpace.HarmonicOnNhd (fun x ↦ log ‖1 - x * a‖) (closedBall 0 |1|)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = 0

Tactic:
calc circleAverage (log ‖· - a‖) 0 1
  _ = circleAverage (log ‖1 - ·⁻¹ * a‖) 0 1 := by
    apply circleAverage_congr_sphere
    intro z hz
    simp_all only [abs_one, mem_sphere_iff_norm, sub_zero]
    congr 1
    have : z ≠ 0 := fun h ↦ by simp [h] at hz
    calc ‖z - a‖
    _ = ‖z⁻¹ * (z - a)‖ := by simp [hz]
    _ = ‖1 - z⁻¹ * a‖ := by field_simp
  _ = 0 := by
    rw [circleAverage_zero_one_congr_inv (f := fun x ↦ log ‖1 - x * a‖),
      InnerProductSpace.HarmonicOnNhd.circleAverage_eq, zero_mul, sub_zero,
      CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, log_one]
    intro x hx
    have : ‖x * a‖ < 1 := by
      calc ‖x * a‖
      _ = ‖x‖ * ‖a‖ := by simp
      _ ≤ ‖a‖ := mul_le_of_le_one_left (norm_nonneg _) (by aesop)
      _ < 1 := h
    apply AnalyticAt.harmonicAt_log_norm (by fun_prop)
    rw [sub_ne_zero]
    by_contra! hCon
    rwa [← hCon, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, lt_self_iff_false] at this

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

Goal state before:
pp: r : ℝ
⊢ ∫ (t : ℝ) in -r..r, Complex.exp (Complex.I * ↑t) =
    (Complex.exp (Complex.I * ↑r) - Complex.exp (Complex.I * -↑r)) / Complex.I

Tactic:
integral_exp_mul_complex

Goal state after:
r : ℝ
⊢ (Complex.exp (Complex.I * ↑r) - Complex.exp (Complex.I * ↑(-r))) / Complex.I =
    (Complex.exp (Complex.I * ↑r) - Complex.exp (Complex.I * -↑r)) / Complex.I

r : ℝ
⊢ Complex.I ≠ 0
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
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 : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
H : f z ≠ 0
⊢ ∃ n, C < expR z.re ^ n * ‖f z‖

Tactic:
exact (((tendsto_pow_atTop_atTop_of_one_lt (Real.one_lt_exp_iff.2 hz)).atTop_mul_const
      (norm_pos_iff.2 H)).eventually (eventually_gt_atTop C)).exists

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

Goal state before:
pp: f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
⊢ ∃ c, ∀ x ∈ U, f x = c

Tactic:
by
  obtain ⟨z₀, _⟩ := h₂U.nonempty
  by_contra h₅
  grind [not_isOpen_singleton (c₀ : ℝ), (by aesop : (im '' f '' U) = { c₀ }), isOpenMap_im
    (f '' U) ((h₁f.is_constant_or_isOpen h₂U.isPreconnected).resolve_left h₅ U (by tauto) h₁U)]

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case pos
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
hzP : eval z P = 0
⊢ ∑ x ∈ s, Pi.single z 1 x • (z - x) = 0

Tactic:
rw [Finset.sum_eq_single z] <;> simp_all

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

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ ↑(z - c).re
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * ↑(z - c).re ^ n = f z
hz' : z - c = ↑(z - c).re
n : ℕ
⊢ 0 ≤ ↑(↑n.factorial)⁻¹ * ↑(iteratedDeriv n f c).re * ↑((z - c).re ^ n)

Tactic:
← ofReal_mul,

Goal state after:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ ↑(z - c).re
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * ↑(z - c).re ^ n = f z
hz' : z - c = ↑(z - c).re
n : ℕ
⊢ 0 ≤ ↑((↑n.factorial)⁻¹ * (iteratedDeriv n f c).re) * ↑((z - c).re ^ n)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ :=
  fun θ ↦ (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
⊢ MeromorphicOn (fun z ↦ z - ρ) (sphere 0 |R|)

Tactic:
by intro; fun_prop

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

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

Tactic:
simp [pow_mul, sin_sq, cos_sq, ← sub_sub]

Goal state after:
a b : ℝ
m n : ℕ
⊢ ∫ (x : ℝ) in a..b, (1 - 2⁻¹ - cos (2 * x) / 2) ^ m * (2⁻¹ + cos (2 * x) / 2) ^ n =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: case inr
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : ¬0 ∉ U
a : ℂ
this : ∃ f, Injective f ∧ ¬Dense (f '' (-a +ᵥ U)) ∧ ∀ z ∈ -a +ᵥ U, deriv f z ≠ 0
ha : a ∉ U
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
rcases this with ⟨f, hf_inj, hf_dense, hdf⟩

Goal state after:
case inr
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : ¬0 ∉ U
a : ℂ
ha : a ∉ U
f : ℂ → ℂ
hf_inj : Injective f
hf_dense : ¬Dense (f '' (-a +ᵥ U))
hdf : ∀ z ∈ -a +ᵥ U, deriv f z ≠ 0
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp

Goal state before:
pp: ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ π ≤ (↑2 * ↑π * ξ).im

Tactic:
← ofReal_mul,

Goal state after:
ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ π ≤ (↑(2 * π) * ξ).im
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
a✝ : Nontrivial R
⊢ A.discr = A.trace ^ 2 - 4 * A.det

Tactic:
discr,

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
a✝ : Nontrivial R
⊢ A.charpoly.discr = A.trace ^ 2 - 4 * A.det
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
⊢ denom g z ≠ 0

Tactic:
refine linear_ne_zero_of_im hz fun H ↦ g.det.ne_zero ?_

Goal state after:
g : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
H : ↑g 1 = 0
⊢ ↑(GeneralLinearGroup.det g) = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
⊢ m ∈ Set.range ⇑(scalar (Fin 2)) → m 0 1 = 0

pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
⊢ m 0 1 = 0 → m ∈ Set.range ⇑(scalar (Fin 2))

Tactic:
· rintro ⟨a, rfl⟩
      simp

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
⊢ m 0 1 = 0 → m ∈ Set.range ⇑(scalar (Fin 2))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: case refine_1
g : GL (Fin 2) ℝ
⊢ Continuous ⇑(if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else conjCAE)

pp: case refine_2
g : GL (Fin 2) ℝ
⊢ Continuous fun x ↦ num g ↑x / denom g ↑x

Tactic:
· split_ifs
      exacts [continuous_id, continuous_conj]

Goal state after:
case refine_2
g : GL (Fin 2) ℝ
⊢ Continuous fun x ↦ num g ↑x / denom g ↑x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: ⊢ ContinuousOn (fun t ↦ ↑ofComplex (↑I * ↑t)) (Ioi 0)

Tactic:
simp only [ofComplex_apply_eq_ite, continuousOn_iff_continuous_domRestrict,
    continuous_induced_rng]
  have : Continuous (fun t : ℝ ↦ Complex.I * t) := by fun_prop
  exact (this.comp continuous_subtype_val).congr (by simp +contextual)

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

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i j : m
lt : (fun x ↦ x ≠ k) j < (fun x ↦ x ≠ k) i
⊢ auxMat M k i j = 0

Tactic:
simp_rw [lt_iff_not_ge, le_Prop_eq, Classical.not_imp, not_not] at lt

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: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
⊢ IsIntegral R ((norm K) x)

Tactic:
by_cases h : FiniteDimensional K L

Goal state after:
case pos
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
⊢ IsIntegral R ((norm K) x)

case neg
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : ¬FiniteDimensional K L
⊢ IsIntegral R ((norm K) x)
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
by_cases h : FiniteDimensional K L

Goal state after:
case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
H :
  1 ^ 2 / (dist b a * dist d a) * dist b d ≤
    dist (inversion a 1 b) (inversion a 1 c) + dist (inversion a 1 c) (inversion a 1 d)
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Tactic:
dist_inversion_inversion hb hc,

Goal state after:
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
H :
  1 ^ 2 / (dist b a * dist d a) * dist b d ≤
    1 ^ 2 / (dist b a * dist c a) * dist b c + dist (inversion a 1 c) (inversion a 1 d)
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : StoneCech α → β
h₁ : Continuous[_, inst✝¹] g₁
h₂ : Continuous[_, inst✝¹] g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
x : α
⊢ g₁ (stoneCechUnit x) = g₂ (stoneCechUnit x)

Tactic:
exact congr_fun h x

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

Goal state before:
pp: f : ℂ → ℂ
⊢ proximity f⁻¹ ⊤ = proximity f 0

Tactic:
simp [proximity_zero, proximity_top]

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

Goal state before:
pp: case inr
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
g : SL(2, ℝ)
hg : g • I ∈ K
hδK : δ ≤ 1 / Complex.normSq (denom ((Matrix.SpecialLinearGroup.mapGL ℝ) g) ↑I)
⊢ ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ 1 / δ

Tactic:
rw [le_div_iff₀ (normSq_denom_pos (Matrix.SpecialLinearGroup.mapGL ℝ g) (show I.im ≠ 0 by simp)),
    mul_comm, ← le_div_iff₀ hδ] at hδK

Goal state after:
case inr
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
g : SL(2, ℝ)
hg : g • I ∈ K
hδK : Complex.normSq (denom ((Matrix.SpecialLinearGroup.mapGL ℝ) g) ↑I) ≤ 1 / δ
⊢ ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ 1 / δ
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁⁻¹ * f₂⁻¹) ⊤ ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤

Tactic:
apply proximity_mul_top_le h₁f₁.inv h₁f₂.inv

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

Goal state before:
pp: case neg.inr.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hzero : meromorphicOrderAt f 0 = 0
⊢ CircleIntegrable (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

Tactic:
apply CircleIntegrable.congr_codiscreteWithin
     (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero (not_not.1 h) hzero)

Goal state after:
case neg.inr.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hzero : meromorphicOrderAt f 0 = 0
⊢ CircleIntegrable (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

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

Tactic:
rw [← circleAverage_add (circleIntegrable_logCounting h)
        circleIntegrable_log_meromorphicTrailingCoeffAt, circleAverage_congr_sphere]

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
⊢ EqOn (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R + logCounting f ⊤ R)
    ((fun x ↦ logCounting f (↑x) R) + fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) (sphere 0 |1|)
Module: Mathlib.Topology.Semicontinuity.Lindelof

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : IsGLB 𝓕 s
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ IsGLB 𝓕' s

Tactic:
isGLB_pi

Goal state after:
X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

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

Tactic:
rw [← locallyFinsuppWithin.logCounting_divisor]
  exact locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const h hR

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : IsOrderedRing R
x y z : V
⊢ y ∈ segment R x z ↔ Wbtw R x y z

Tactic:
by
  rw [Wbtw, affineSegment_eq_segment]

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✝⁶ : 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 z : P
⊢ Wbtw R z y x ∧ Wbtw R x z y ↔ y = z

Tactic:
wbtw_comm (z := y),

Goal state after:
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 z : P
⊢ Wbtw R z y x ∧ Wbtw R y z x ↔ y = z
Module: Mathlib.Analysis.Convex.Approximation

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

Tactic:
by ext; simp

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
v : n → R
inst✝ : CommRing R
⊢ Perm.permMatrix R σ *ᵥ v = v ∘ ⇑σ

Tactic:
ext j

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
v : n → R
inst✝ : CommRing R
j : n
⊢ (Perm.permMatrix R σ *ᵥ v) j = (v ∘ ⇑σ) j
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
v : n → R
inst✝ : CommRing R
⊢ v ᵥ* Perm.permMatrix R σ = v ∘ ⇑(Equiv.symm σ)

Tactic:
ext j

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
v : n → R
inst✝ : CommRing R
j : n
⊢ (v ᵥ* Perm.permMatrix R σ) j = (v ∘ ⇑(Equiv.symm σ)) j
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (M * f.toMatrix) i j = Option.casesOn (f.symm j) 0 (M i)

Tactic:
dsimp [Matrix.mul_apply, toMatrix_apply]

Goal state after:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (∑ j_1, M i j_1 * if j ∈ f j_1 then 1 else 0) = Option.rec 0 (fun val ↦ M i val) (f.symm j)
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : n → α
⊢ σ.toPEquiv.toMatrix *ᵥ a = a ∘ ⇑σ

Tactic:
ext j

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : n → α
j : m
⊢ (σ.toPEquiv.toMatrix *ᵥ a) j = (a ∘ ⇑σ) j
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : m → α
⊢ a ᵥ* σ.toPEquiv.toMatrix = a ∘ ⇑σ.symm

Tactic:
ext j

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : m → α
j : n
⊢ (a ᵥ* σ.toPEquiv.toMatrix) j = (a ∘ ⇑σ.symm) j
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₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : p ∈ line[R, t.points i₁, p₁]
h₂' : p ∈ line[R, t.points i₂, p₂]
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ Sbtw R (t.points i₁) p p₁

Tactic:
have hu : (Finset.univ : Finset (Fin 3)) = {i₁, i₂, i₃} := by
    clear h₁ h₂ h₁' h₂'
    decide +revert

Goal state after:
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₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : p ∈ line[R, t.points i₁, p₁]
h₂' : p ∈ line[R, t.points i₂, p₂]
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
⊢ Sbtw R (t.points i₁) p p₁
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 : Matrix n n R
⊢ (∀ (i : n), ∑ j, M j i = 1) → ((∀ (i j : n), 0 ≤ M j i) ↔ ∀ (i j : n), 0 ≤ M i j)

Tactic:
exact fun _ ↦ forall_comm

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 : Matrix n n R
⊢ (∀ (j : n), ∑ i, M j i = 1) → ((∀ (i j : n), 0 ≤ M j i) ↔ ∀ (i j : n), 0 ≤ M i j)

Tactic:
exact fun _ ↦ forall_comm

Goal state after:
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
inst✝ : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 Subtype.val
x : E
m : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ y, x ∈ (convexHull 𝕜) ↑(t.erase ↑y)

Tactic:
simp only [Finset.convexHull_eq, mem_ofPred_eq] at m ⊢

Goal state after:
𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 Subtype.val
x : E
m : ∃ w, (∀ y ∈ t, 0 ≤ w y) ∧ ∑ y ∈ t, w y = 1 ∧ t.centerMass w id = x
⊢ ∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = x
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
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
⊢ ∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id

Tactic:
let k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z

Goal state after:
𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
⊢ ∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id