mathlib-initiative/mathlib-tactics huggingface dataset:
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
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c * ‖1 x‖
⊢ DifferentiableAt ℂ (cuspFunction h f) 0

Tactic:
simp only [norm_one, Pi.one_apply, mul_one] at t

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
⊢ DifferentiableAt ℂ (cuspFunction h f) 0
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: 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
⊢ ↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|)) u) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

Tactic:
trans ∑ᶠ u, (divisor f (closedBall c |r|) u : ℝ)

Goal state after:
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
⊢ ↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|)) u) ≤ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u)

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
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
τ : ℍ
⊢ rexp (-2 * π * (↑τ).im / ↑n) < 1

Tactic:
Real.exp_lt_one_iff,

Goal state after:
n : ℕ
inst✝ : NeZero n
τ : ℍ
⊢ -2 * π * (↑τ).im / ↑n < 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
this : (scalar (Fin 2)) (m.discr / 4) = 0
⊢ m.discr = 0

Tactic:
by
        rw [← map_zero (scalar (Fin 2)), scalar_inj, div_eq_zero_iff] at this
        have : (4 : K) ≠ 0 := by simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _
        tauto

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
⊢ num g ↑I = (ContinuousAlgEquiv.refl ℝ ℂ) ↑I * denom g ↑I ↔ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 = -↑g 1 0

Tactic:
simp [Complex.ext_iff, num, denom, and_comm]

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

Goal state before:
pp: A B A' B' : ℝ
hA : A ≤ A'
hB : B' ≤ B
⊢ verticalStrip A B ⊆ verticalStrip A' B'

Tactic:
by
  rintro z ⟨hzre, hzim⟩
  exact ⟨hzre.trans hA, hB.trans hzim⟩

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

Goal state before:
pp: a : ℍ
hw : ¬0 < (↑a).im
⊢ a.im ≤ 0

Tactic:
by simpa using hw

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
⊢ ((Matrix.comp m m n n R) ((M * auxMat M k).map ⇑f)).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

Tactic:
· simp_rw [((mul_auxMat_blockTriangular M k).map f).comp.det_fintype, Fintype.prod_Prop,
      comp_toSquareBlock (b := (· = k)), det_reindex_self, map_toSquareBlock,
      mul_auxMat_toSquareBlock_eq, smul_one_eq_diagonal,
      diagonal_map (map_zero _), comp_diagonal, det_reindex_self]
    simp

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

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

Tactic:
rw [eventually_nhdsWithin_iff]

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

Goal state before:
pp: x : ℝ
⊢ (-x + √(1 + (-x) ^ 2)) * (x + √(1 + x ^ 2)) = 1

Tactic:
rw [neg_sq, neg_add_eq_sub, add_comm x, mul_comm, ← sq_sub_sq, sq_sqrt, add_sub_cancel_right]

Goal state after:
x : ℝ
⊢ 0 ≤ 1 + x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ (x + √(1 + x ^ 2) - (-x + √(1 + (-x) ^ 2))) / 2 = x

Tactic:
neg_sq

Goal state after:
x : ℝ
⊢ (x + √(1 + x ^ 2) - (-x + √(1 + x ^ 2))) / 2 = x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a b c : ℍ
⊢ (dist ↑a ↑b * dist (↑b) ((starRingEnd ℂ) ↑c) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * (2 * b.im))

Tactic:
mul_comm (dist (b : ℂ) _),

Goal state after:
a b c : ℍ
⊢ (dist ↑a ↑b * dist (↑b) ((starRingEnd ℂ) ↑c) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * √(a.im * c.im) * (2 * b.im))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' closedBall z r = closedBall (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
by
  ext w; constructor
  · rintro ⟨w, hw, rfl⟩
    exact dist_le_iff_dist_coe_center_le.1 hw
  · intro hw
    lift w to ℍ using im_pos_of_dist_center_le hw
    exact mem_image_of_mem _ (dist_le_iff_dist_coe_center_le.2 hw)

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

Goal state before:
pp: α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ x = joinM u

Tactic:
rw [eq_comm, ← Ultrafilter.coe_le_coe]

Goal state after:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ↑(joinM u) ≤ ↑x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' ball z r = ball (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
by
  ext w; constructor
  · rintro ⟨w, hw, rfl⟩
    exact dist_lt_iff_dist_coe_center_lt.1 hw
  · intro hw
    lift w to ℍ using im_pos_of_dist_center_le (ball_subset_closedBall hw)
    exact mem_image_of_mem _ (dist_lt_iff_dist_coe_center_lt.2 hw)

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

Goal state before:
pp: z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ 2 *
      arsinh
        (dist (↑y₁)⁻¹ (↑y₂)⁻¹ /
          (2 * √({ coe := -(↑y₁)⁻¹, coe_im_pos := ⋯ }.im * { coe := -(↑y₂)⁻¹, coe_im_pos := ⋯ }.im))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))

Tactic:
dist_inv_inv₀ y₁.ne_zero y₂.ne_zero,

Goal state after:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ 2 *
      arsinh
        (dist ↑y₁ ↑y₂ / (‖↑y₁‖ * ‖↑y₂‖) /
          (2 * √({ coe := -(↑y₁)⁻¹, coe_im_pos := ⋯ }.im * { coe := -(↑y₂)⁻¹, coe_im_pos := ⋯ }.im))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj
              { toTop := (TopCat.limitCone FF).pt, is_compact := ⋯, is_hausdorff := ⋯, prop := trivial }).map
          f ≫
        InducedCategory.homMk ((TopCat.limitCone FF).π.app Y) =
      InducedCategory.homMk ((TopCat.limitCone FF).π.app X) ≫ F.map f

Tactic:
intro _

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
X✝ : J
⊢ ∀ ⦃Y : J⦄ (f : X✝ ⟶ Y),
    ((Functor.const J).obj
              { toTop := (TopCat.limitCone FF).pt, is_compact := ⋯, is_hausdorff := ⋯, prop := trivial }).map
          f ≫
        InducedCategory.homMk ((TopCat.limitCone FF).π.app Y) =
      InducedCategory.homMk ((TopCat.limitCone FF).π.app X✝) ≫ F.map f
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
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
⊢ f p ≠ y

Tactic:
simpa [hy] using mem_range_self (f := f) p

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

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

Tactic:
by
    rw [MeromorphicOn.circleAverage_log_norm hR hf.meromorphicOn]
    unfold Function.locallyFinsuppWithin.logCounting
    have : (divisor f (closedBall 0 |R|)) = (divisor f Set.univ).toClosedBall R :=
      (divisor_restrict hf.meromorphicOn (by tauto)).symm
    simp [this, toClosedBall, restrictMonoidHom, restrict_apply]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
e : E
hΘ : (fun r ↦ log r - log ‖e‖) =Θ[atTop] log
h₁ : 1 =o[atTop] fun r ↦ log r - log ‖e‖
⊢ 1 =o[atTop] logCounting (single e 1)

Tactic:
refine h₁.congr' EventuallyEq.rfl ?_

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
e : E
hΘ : (fun r ↦ log r - log ‖e‖) =Θ[atTop] log
h₁ : 1 =o[atTop] fun r ↦ log r - log ‖e‖
⊢ (fun r ↦ log r - log ‖e‖) =ᶠ[atTop] logCounting (single e 1)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : 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
⊢ 0 ≤ logCounting f e r

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

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
x y : P
hne : y ≠ x
h : Wbtw R x y x
⊢ False

Tactic:
wbtw_self_iff

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
x y : P
hne : y ≠ x
h : y = x
⊢ False
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
x y : P
h : Wbtw R x y x
hne : y ≠ x
⊢ False

Tactic:
wbtw_self_iff

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
x y : P
h : y = x
hne : y ≠ x
⊢ False
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → ↥ι' → ↥(ι'.biUnion t) := fun f i ↦ ⟨↑f i, ⋯⟩
f f' : ↑(hallMatchingsOn t ι')
h : g f = g f'
a : ↥ι'
⊢ ↑f a = ↑f' a

Tactic:
rw [funext_iff] at h

Goal state after:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → ↥ι' → ↥(ι'.biUnion t) := fun f i ↦ ⟨↑f i, ⋯⟩
f f' : ↑(hallMatchingsOn t ι')
h : ∀ (x : ↥ι'), g f x = g f' x
a : ↥ι'
⊢ ↑f a = ↑f' a
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_4
𝕜 : 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
f : E → ℝ
x✝ : ∃ a ∈ 𝓕, (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) a = f
a : ↑univ → ℝ
h : a ≤ φ ∘ Subtype.val
l : E →L[𝕜] 𝕜
c : ℝ
hlc : a = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c
hb : (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) a = f
⊢ f = ⇑re ∘ ⇑l + const E c

Tactic:
subst hlc

Goal state after:
case refine_4
𝕜 : 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
f : E → ℝ
x✝ : ∃ a ∈ 𝓕, (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) a = f
l : E →L[𝕜] 𝕜
c : ℝ
h : (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c ≤ φ ∘ Subtype.val
hb : (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) ((⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c) = f
⊢ f = ⇑re ∘ ⇑l + const E c
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(ConcreteCategory.hom (F.map f))
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
k m : J
mi : m ⟶ i
h : (ConcreteCategory.hom (F.map (mi ≫ f))) (↑s₀ m) = ↑s₁ j
mk : m ⟶ k
h✝ : True
⊢ ↑s₀ k = ↑s₁ k

Tactic:
← s₁.prop (mi ≫ f)

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(ConcreteCategory.hom (F.map f))
i : J
f : i ⟶ j
s₀ s₁ : ↑F.sections
k m : J
mi : m ⟶ i
h : (ConcreteCategory.hom (F.map (mi ≫ f))) (↑s₀ m) = (ConcreteCategory.hom (F.map (mi ≫ f))) (↑s₁ m)
mk : m ⟶ k
h✝ : True
⊢ ↑s₀ k = ↑s₁ k
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈
      { toFun := fun a ↦ if x✝³ a = x✝² a then x✝³ a else none,
          invFun := fun b ↦ if x✝³.symm b = x✝².symm b then x✝³.symm b else none, inv := ⋯ }
        x✝¹ →
    x✝ ∈ x✝³ x✝¹

Tactic:
simp only [coe_mk, mem_def]

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ (if x✝³ x✝¹ = x✝² x✝¹ then x✝³ x✝¹ else none) = some x✝ → x✝³ x✝¹ = some x✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈
      { toFun := fun a ↦ if x✝³ a = x✝² a then x✝³ a else none,
          invFun := fun b ↦ if x✝³.symm b = x✝².symm b then x✝³.symm b else none, inv := ⋯ }
        x✝¹ →
    x✝ ∈ x✝² x✝¹

Tactic:
simp only [coe_mk, mem_def]

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ (if x✝³ x✝¹ = x✝² x✝¹ then x✝³ x✝¹ else none) = some x✝ → x✝² x✝¹ = some x✝
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
inst✝ : NonAssocSemiring R
σ τ : Perm n
⊢ Perm.permMatrix R (σ * τ)⁻¹ = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹

Tactic:
_root_.mul_inv_rev,

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ✝ τ✝ : Perm n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring R
σ τ : Perm n
⊢ Perm.permMatrix R (τ⁻¹ * σ⁻¹) = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹
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
hM : M ∈ colStochastic R n
hx : ∀ (i : n), 0 ≤ x i
j k : n
a✝ : k ∈ univ
⊢ 0 ≤ x k * M k j

Tactic:
refine Left.mul_nonneg (hx k) ?_

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
x : n → R
hM : M ∈ colStochastic R n
hx : ∀ (i : n), 0 ≤ x i
j k : n
a✝ : k ∈ univ
⊢ 0 ≤ M k j
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
⊢ (convexHull 𝕜) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t

Tactic:
by
  apply Set.Subset.antisymm
  · intro x hx
    simp only [exists_prop, Set.mem_iUnion]
    exact ⟨Caratheodory.minCardFinsetOfMemConvexHull hx,
      Caratheodory.minCardFinsetOfMemConvexHull_subseteq hx,
      Caratheodory.affineIndependent_minCardFinsetOfMemConvexHull hx,
      Caratheodory.mem_minCardFinsetOfMemConvexHull hx⟩
  · iterate 3 convert! Set.iUnion_subset _; intro
    exact convexHull_mono ‹_›

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
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
ht₃ : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i, w i = 1 ∧ ∑ i, w i • z i = x

Tactic:
simp only [t.convexHull_eq, Set.mem_ofPred_eq] at ht₃

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
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
ht₃ : ∃ w, (∀ y ∈ t, 0 ≤ w y) ∧ ∑ y ∈ t, w y = 1 ∧ t.centerMass w id = x
⊢ ∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i, w i = 1 ∧ ∑ i, w i • z i = x
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
⊢ ∑ j, ∑ σ, w σ • Equiv.Perm.permMatrix R σ default j = 1

Tactic:
simp only [← smul_apply (m := n), ← Finset.sum_apply, hw3]

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
⊢ ∑ x, M default x = 1
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
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
⊢ s ⊆ Set.range ⇑b

Tactic:
simp [b]

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

Goal state before:
pp: β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[Icc a b] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
⊢ f a ≤ f c

Tactic:
nhdsWithin_Icc_eq_nhdsGE a_lt_b

Goal state after:
β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
⊢ f a ≤ f c
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ⇑f) x ∈ (convexHull 𝕜) (p ∘ ⇑f '' s)
⊢ f x ∈ ⇑f '' s

Tactic:
exact hc _ _ (by rwa [Set.image_image])

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᵐ[μ] g
this : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
⊢ ∫ (a : α), g a ∂μ ∈ s

Tactic:
have hg : ∀ᵐ x ∂μ, g x ∈ closure (range g ∩ s) := by
    filter_upwards [hfg.rw (fun _ y => y ∈ s) hf] with x hx
    apply subset_closure
    exact ⟨mem_range_self _, hx⟩

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᵐ[μ] g
this : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
⊢ ∫ (a : α), g a ∂μ ∈ s