mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: case neg
n : ℕ
x : ℝ
hn : ¬n = 0
⊢ log⁺ (x ^ n) = ↑n * log⁺ x

Tactic:
by_cases hx : |x| ≤ 1

Goal state after:
case pos
n : ℕ
x : ℝ
hn : ¬n = 0
hx : |x| ≤ 1
⊢ log⁺ (x ^ n) = ↑n * log⁺ x

case neg
n : ℕ
x : ℝ
hn : ¬n = 0
hx : ¬|x| ≤ 1
⊢ log⁺ (x ^ n) = ↑n * log⁺ x
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: 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 = ⊤
⊢ (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (Ι a b)] 0

Tactic:
apply Filter.EventuallyEq.filter_mono _ (Filter.codiscreteWithin_mono Set.uIoc_subset_uIcc)

Goal state after:
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 = ⊤
⊢ (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]] 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: r : ℝ
⊢ -((Complex.sin ↑r * Complex.I - -Complex.sin ↑r * Complex.I) * Complex.I) = 2 * Complex.sin ↑r

Tactic:
rw [sub_mul, mul_assoc, mul_assoc, two_mul]

Goal state after:
r : ℝ
⊢ -(Complex.sin ↑r * (Complex.I * Complex.I) - -Complex.sin ↑r * (Complex.I * Complex.I)) =
    Complex.sin ↑r + Complex.sin ↑r
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: b : ℝ
h : b < 0
t : ℝ
| log t

Tactic:
← log_neg_eq_log

Goal state after:
b : ℝ
h : b < 0
t : ℝ
| log (-t)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

Tactic:
simp [mul_sub, circleMap, add_mul, Complex.exp_add]

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

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

Tactic:
circleAverage_log_norm_sub_const₀ h,

Goal state after:
case inr.inr
a : ℂ
h : ‖a‖ < 1
⊢ log⁺ ‖a‖ = 0
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
⊢ Continuous fun θ ↦ herglotzLogIntegrand w ρ (circleMap 0 r θ)

Tactic:
by
  rw [continuous_iff_continuousAt]
  intro θ
  apply ContinuousAt.comp (continuousAt_herglotzLogIntegrand _ _) (by fun_prop)
  all_goals
    by_contra h
    grind [norm_circleMap_zero, lt_of_le_of_lt (Complex.norm_nonneg w) hwr]

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

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ∀ x ∈ U, ¬∀ᶠ (z : E) in 𝓝 x, g z = g x
s : Set E
hs1 : s ⊆ U
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
w : E
hw1 : w ∈ s
⊢ g '' s ∈ 𝓝 (g w)

Tactic:
exact (hg w (hs1 hw1)).eventually_constant_or_nhds_le_map_nhds.resolve_left (h w (hs1 hw1))
        (image_mem_map (hs2.mem_nhds hw1))

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
x : ℂ
hx : x ∈ closure (ball 0 (r n))
this : x ≠ ρ
⊢ ‖x - ρ‖ ≠ 0

Tactic:
by simpa [sub_eq_zero]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : AddCommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
⊢ Monotone f

Tactic:
refine MonotoneOn.Iic_union_Ici (fun x hx y hy hxy => neg_le_neg_iff.1 ?_) h₂
  rw [← h₁, ← h₁]
  exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_le_neg hxy)

Goal state after:
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_sqrt (by simp), cpow_inv_two_re]
  simp [mul_add]

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

Goal state before:
pp: 𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝¹ : NormedSpace ℝ E
this✝ : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
this : Continuous ((Metric.closedBall 0 1).piecewise id g)
⊢ TietzeExtension ↑(Metric.closedBall 0 1)

Tactic:
refine .of_retract ⟨Subtype.val, by fun_prop⟩ ⟨_, this.codRestrict fun x ↦ ?_⟩ ?_

Goal state after:
case refine_1
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝¹ : NormedSpace ℝ E
this✝ : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
this : Continuous ((Metric.closedBall 0 1).piecewise id g)
x : E
⊢ (Metric.closedBall 0 1).piecewise id g x ∈ Metric.closedBall 0 1

case refine_2
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝¹ : NormedSpace ℝ E
this✝ : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
this : Continuous ((Metric.closedBall 0 1).piecewise id g)
⊢ { toFun := codRestrict ((Metric.closedBall 0 1).piecewise id g) (Metric.closedBall 0 1) ⋯,
          continuous_toFun := ⋯ }.comp
      { toFun := Subtype.val, continuous_toFun := ⋯ } =
    ContinuousMap.id ↑(Metric.closedBall 0 1)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝⁸ : TopologicalSpace X₁
X : Type u
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormalSpace X
s✝ : Set X
e : X₁ → X
Y✝ : Type v
inst✝⁵ : TopologicalSpace Y✝
inst✝⁴ : TietzeExtension Y✝
ι : Type u_1
Y : ι → Type v
inst✝³ : (i : ι) → TopologicalSpace (Y i)
inst✝² : ∀ (i : ι), TietzeExtension (Y i)
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, (i : ι) → Y i)
⊢ ∃ g, ContinuousMap.restrict s g = f

Tactic:
obtain ⟨g', hg'⟩ := Classical.skolem.mp <| fun i ↦
      ContinuousMap.exists_restrict_eq hs (ContinuousMap.piEquiv _ _ |>.symm f i)

Goal state after:
X₁ : Type u₁
inst✝⁸ : TopologicalSpace X₁
X : Type u
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormalSpace X
s✝ : Set X
e : X₁ → X
Y✝ : Type v
inst✝⁵ : TopologicalSpace Y✝
inst✝⁴ : TietzeExtension Y✝
ι : Type u_1
Y : ι → Type v
inst✝³ : (i : ι) → TopologicalSpace (Y i)
inst✝² : ∀ (i : ι), TietzeExtension (Y i)
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, (i : ι) → Y i)
g' : (x : ι) → C(X✝, Y x)
hg' : ∀ (x : ι), ContinuousMap.restrict s (g' x) = (ContinuousMap.piEquiv (↑s) Y).symm f x
⊢ ∃ g, ContinuousMap.restrict s g = f
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ (¬∃ y, (diagonal fun x ↦ y) * ↑g = ↑g * m) ∧ m.discr = 0 ↔ (¬∃ y, (diagonal fun x ↦ y) = m) ∧ m.discr = 0

Tactic:
← smul_eq_diagonal_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ (¬∃ y, y • ↑g = ↑g * m) ∧ m.discr = 0 ↔ (¬∃ y, (diagonal fun x ↦ y) = m) ∧ m.discr = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
c : ℝ := ↑g 1 0
⊢ (c * z.im) ^ 2 ≤ Complex.normSq (denom g ↑z)

Tactic:
set d := g 1 1

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
c : ℝ := ↑g 1 0
d : ℝ := ↑g 1 1
⊢ (c * z.im) ^ 2 ≤ Complex.normSq (denom g ↑z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Goal state before:
pp: z : ℂ
hz : z ∈ Complex.im ⁻¹' Set.Ioi 0
⊢ z.im = (↑ofComplex z).im

Tactic:
simp [ofComplex_apply_of_im_pos hz]

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

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

Tactic:
by
  simp [UpperHalfPlane.coe_smul, σ, J, show ¬(1 : ℝ) < 0 by simp, num, denom]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((compRingEquiv m n R) (f.mapMatrix M)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((compRingEquiv m n R) (f.mapMatrix (M * auxMat M k))).det

Tactic:
map_mul,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((compRingEquiv m n R) (f.mapMatrix M)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((compRingEquiv m n R) (f.mapMatrix M) * (compRingEquiv m n R) (f.mapMatrix (auxMat M k))).det
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f (M k k * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det)).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0

Tactic:
map_mul,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f (M k k) * f ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]

Goal state after:
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 α
ha : a ∈ x
⊢ {v | a ∈ v} ∈ u

Tactic:
exact h _ ⟨ha, a, rfl⟩

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

Goal state before:
pp: X Y : CompHaus
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
constructor
  · dsimp [Function.Surjective]
    contrapose!
    rintro ⟨y, hy⟩ hf
    let C := Set.range f
    have hC : IsClosed C := (isCompact_range f.hom.hom.continuous).isClosed
    let D := ({y} : Set Y)
    have hD : IsClosed D := isClosed_singleton
    have hCD : Disjoint C D := by
      rw [Set.disjoint_singleton_right]
      rintro ⟨y', hy'⟩
      exact hy y' hy'
    obtain ⟨φ, hφ0, hφ1, hφ01⟩ := exists_continuous_zero_one_of_isClosed hC hD hCD
    have : CompactSpace (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.compactSpace
    have : T2Space (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.t2Space
    let Z := of (ULift.{u} <| Set.Icc (0 : ℝ) 1)
    let g : Y ⟶ Z := ofHom _
      ⟨fun y' => ⟨⟨φ y', hφ01 y'⟩⟩,
        continuous_uliftUp.comp (φ.continuous.subtype_mk fun y' => hφ01 y')⟩
    let h : Y ⟶ Z := ofHom _
      ⟨fun _ => ⟨⟨0, Set.left_mem_Icc.mpr zero_le_one⟩⟩, continuous_const⟩
    have H : h = g := by
      rw [← cancel_epi f]
      ext x : 4
      simp [g, h, Z, hφ0 (Set.mem_range_self x)]
    apply_fun fun e => (e y).down.1 at H
    dsimp [g, h, Z] at H
    simp only [hφ1 (Set.mem_singleton y), Pi.one_apply] at H
    exact zero_ne_one H
  · rw [← CategoryTheory.ofHom_epi_iff_surjective]
    apply (forget CompHaus).epi_of_epi_map

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed[inst✝¹] (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous[x✝², inst✝¹] f
⊢ IsClosed[x✝²] (f ⁻¹' s)

Tactic:
← Set.preimage_inter_range

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed[inst✝¹] (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous[x✝², inst✝¹] f
⊢ IsClosed[x✝²] (f ⁻¹' (s ∩ range f))
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
p : X
⊢ (fun q ↦ if hq : q = y then ∞ else ↑(Exists.choose ⋯)) ((fun p ↦ p.elim y f) ↑p) = ↑p

Tactic:
have hp : f p ≠ y := by simpa [hy] using mem_range_self (f := f) p
          simpa [hp] using hf.injective (mem_range_self p).choose_spec

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen[inst✝¹] (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous[x✝², inst✝¹] f
⊢ IsOpen[x✝²] (f ⁻¹' s)

Tactic:
← Set.preimage_inter_range

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen[inst✝¹] (s ∩ K)
K : Type u
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X
hf : Continuous[x✝², inst✝¹] f
⊢ IsOpen[x✝²] (f ⁻¹' (s ∩ range f))
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
⊢ CompactlyGeneratedSpace X

Tactic:
by
  refine compactlyGeneratedSpace_of_isClosed fun s hs ↦ h s fun K hK ↦ ?_
  rw [Set.inter_comm, ← Subtype.image_preimage_coe]
  apply hK.isClosed.isClosedMap_subtype_val
  have : CompactSpace ↑K := isCompact_iff_compactSpace.1 hK
  exact hs _ Subtype.val continuous_subtype_val

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : WeaklyLocallyCompactSpace X
⊢ CompactlyGeneratedSpace X

Tactic:
refine compactlyGeneratedSpace_of_isClosed_of_t2 fun s h ↦ ?_
  rw [isClosed_iff_forall_filter]
  intro x ℱ hℱ₁ hℱ₂ hℱ₃
  rcases exists_compact_mem_nhds x with ⟨K, hK, K_mem⟩
  exact Set.mem_of_mem_inter_left <| isClosed_iff_forall_filter.1 (h _ hK) x ℱ hℱ₁
    (Filter.inf_principal ▸ le_inf hℱ₂ (le_trans hℱ₃ <| Filter.le_principal_iff.2 K_mem)) hℱ₃

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
x y : F
hcodim : 1 < Module.rank ℝ (F ⧸ ⊤)
hx : x ∈ (↑⊤)ᶜ
h : y ∈ ⊤
⊢ False

Tactic:
simp at hcodim

Goal state after:
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 b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
s : Set E := ⋯
hs : s.Finite
z : E
hz : z ∈ hs.toFinset
h₂z : ¬z = 0
this : z ∈ closedBall 0 |b|
h₃z : z ∉ closedBall 0 |a|
⊢ 1 * ‖z‖ ≤ b

Tactic:
simp_all [abs_of_pos hb]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : HasConstantSpeedOnWith f s l
hft : HasConstantSpeedOnWith f t l
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
⊢ HasConstantSpeedOnWith f (s ∪ t) l

Tactic:
rw [hasConstantSpeedOnWith_iff_ordered] at hfs hft ⊢
  rintro z (zs | zt) y (ys | yt) zy
  · have : (s ∪ t) ∩ Icc z y = s ∩ Icc z y := by
      ext w; constructor
      · rintro ⟨ws | wt, zw, wy⟩
        · exact ⟨ws, zw, wy⟩
        · exact ⟨(le_antisymm (wy.trans (hs.2 ys)) (ht.2 wt)).symm ▸ hs.1, zw, wy⟩
      · rintro ⟨ws, zwy⟩; exact ⟨Or.inl ws, zwy⟩
    rw [this, hfs zs ys zy]
  · have : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y := by
      ext w; constructor
      · rintro ⟨ws | wt, zw, wy⟩
        exacts [Or.inl ⟨ws, zw, hs.2 ws⟩, Or.inr ⟨wt, ht.2 wt, wy⟩]
      · rintro (⟨ws, zw, wx⟩ | ⟨wt, xw, wy⟩)
        exacts [⟨Or.inl ws, zw, wx.trans (ht.2 yt)⟩, ⟨Or.inr wt, (hs.2 zs).trans xw, wy⟩]
    rw [this, @eVariationOn.union _ _ _ _ f _ _ x, hfs zs hs.1 (hs.2 zs), hft ht.1 yt (ht.2 yt)]
    · have q := ENNReal.ofReal_add (mul_nonneg l.prop (sub_nonneg.mpr (hs.2 zs)))
        (mul_nonneg l.prop (sub_nonneg.mpr (ht.2 yt)))
      simp only [NNReal.val_eq_coe] at q
      rw [← q]
      ring_nf
    exacts [⟨⟨hs.1, hs.2 zs, le_rfl⟩, fun w ⟨_, _, wx⟩ => wx⟩,
      ⟨⟨ht.1, le_rfl, ht.2 yt⟩, fun w ⟨_, xw, _⟩ => xw⟩]
  · cases le_antisymm zy ((hs.2 ys).trans (ht.2 zt))
    simp only [Icc_self, sub_self, mul_zero, ENNReal.ofReal_zero]
    exact eVariationOn.subsingleton _ fun _ ⟨_, uz⟩ _ ⟨_, vz⟩ => uz.trans vz.symm
  · have : (s ∪ t) ∩ Icc z y = t ∩ Icc z y := by
      ext w; constructor
      · rintro ⟨ws | wt, zw, wy⟩
        · exact ⟨le_antisymm ((ht.2 zt).trans zw) (hs.2 ws) ▸ ht.1, zw, wy⟩
        · exact ⟨wt, zw, wy⟩
      · rintro ⟨wt, zwy⟩; exact ⟨Or.inr wt, zwy⟩
    rw [this, hft zt yt zy]

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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ Wbtw R w ((lineMap w ((lineMap w z) t₁)) t₂) z

Tactic:
refine ⟨t₂ * t₁, ⟨mul_nonneg ht₂.1 ht₁.1, mul_le_one₀ ht₂.2 ht₁.1 ht₁.2⟩, ?_⟩

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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ (lineMap w z) (t₂ * t₁) = (lineMap w ((lineMap w z) t₁)) t₂
Module: Mathlib.CategoryTheory.CofilteredSystem

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

Tactic:
(h g).range_eq

Goal state after:
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
h : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
j k : J
g : k ⟶ j
⊢ univ ⊆ univ
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
a b i j : α
⊢ some b = some j ↔ some i = some j

Tactic:
Subsingleton.elim i j,

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
a b i j : α
⊢ some b = some j ↔ some j = some j
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
⊢ (Equiv.toPEquiv (Equiv.swap i j)).toMatrix i✝ j✝ =
    (1 - (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix + (single j i).toMatrix) i✝ j✝

Tactic:
dsimp [toMatrix, single, Equiv.swap_apply_def, Equiv.toPEquiv, Matrix.one_apply]

Goal state after:
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
⊢ (if j✝ ∈ some (if i✝ = i then j else if i✝ = j then i else i✝) then 1 else 0) =
    ((((if i✝ = j✝ then 1 else 0) - if j✝ ∈ if i✝ = i then some i else none then 1 else 0) -
          if j✝ ∈ if i✝ = j then some j else none then 1 else 0) +
        if j✝ ∈ if i✝ = i then some j else none then 1 else 0) +
      if j✝ ∈ if i✝ = j then some i else none then 1 else 0
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
x : n → R
hA : M ∈ colStochastic R n
⊢ ∑ i, (M *ᵥ x) i = ∑ i, x i

Tactic:
by
  simp only [Matrix.mulVec, dotProduct]
  rw [Finset.sum_comm]
  simp [sum_col_of_mem_colStochastic hA, ← Finset.sum_mul]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' : (∀ (i j : n), 0 ≤ M' i j) ∧ (∀ (i : n), ∑ j, M' i j = 1) ∧ ∀ (j : n), ∑ i, M' i j = 1
⊢ (∀ (i j : n), 0 ≤ s * M' i j) ∧ (∀ (i : n), s * ∑ i_1, M' i i_1 = s) ∧ ∀ (j : n), s * ∑ i, M' i j = s

Tactic:
exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩

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
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
hk : k i₀ = 0
⊢ ∑ e ∈ t.erase i₀, k e = ∑ e ∈ t, k e

Tactic:
by
        conv_rhs => rw [← insert_erase hi₀, sum_insert (notMem_erase i₀ t), hk, zero_add]

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.TensorProduct

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
x : E
hx : x ∈ ↑(hull ℝ s)
⊢ x ∈ ↑(Submodule.span ℝ s)

Tactic:
rw [SetLike.mem_coe, PointedCone.mem_hull_set] at hx

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
x : E
hx : ∃ c, ↑c.support ⊆ s ∧ (∀ (y : E), 0 ≤ c y) ∧ (c.sum fun m r ↦ r • m) = x
⊢ x ∈ ↑(Submodule.span ℝ s)