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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
z : ℍ
⊢ (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) (num g ↑z / denom g ↑z) =
    num g ↑z / denom g ↑z

Tactic:
if_pos hg,

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
z : ℍ
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) (num g ↑z / denom g ↑z) = num g ↑z / denom g ↑z
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.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det *
      (((reindex (Equiv.prodComm n { a // (a ≠ k) = True }) (Equiv.prodComm n { a // (a ≠ k) = True }))
            (blockDiagonal fun m ↦ f (M k k))).det *
        ((reindex (Equiv.prodComm n { a // (a ≠ k) = False }) (Equiv.prodComm n { a // (a ≠ k) = False }))
            (blockDiagonal fun m ↦ f 1)).det)

Tactic:
det_reindex_self

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
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det * ((blockDiagonal fun m ↦ f (M k k)).det * (blockDiagonal fun m ↦ f 1).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
⊢ ((reindex (Equiv.prodComm n { a // (a = k) = True }) (Equiv.prodComm n { a // (a = k) = True }))
          (blockDiagonal fun m ↦ 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 =
    (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:
det_reindex_self

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
⊢ (blockDiagonal fun m ↦ 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 =
    (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
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (dist c) (𝓝 c) (𝓝 0)

Tactic:
rw [← dist_self c]

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (dist c) (𝓝 c) (𝓝 (dist c c))
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ ∀ x ∈ {c}ᶜ, dist c x ∈ Ioi 0

Tactic:
aesop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℂ
⊢ HasStrictDerivAt cosh (sinh x) x

Tactic:
by
  simp only [sinh, div_eq_mul_inv]
  convert!
    ((hasStrictDerivAt_exp x).add (hasStrictDerivAt_id x).fun_neg.cexp).mul_const (2 : ℂ)⁻¹ using 1
  rw [id, mul_neg_one, sub_eq_add_neg]

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

Goal state before:
pp: case mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' closedBall z r

Tactic:
· 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.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : DiscreteTopology X
f : OnePoint X → Y
⊢ Continuous[instTopologicalSpace, inst✝¹] f ↔ Tendsto (fun x ↦ f ↑x) cofinite (𝓝 (f ∞))

Tactic:
simp [continuous_iff, cocompact_eq_cofinite, continuous_of_discreteTopology]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
⊢ ∀ (a : ℂ), f a = g a → log⁺ ‖f a‖ = log⁺ ‖g a‖

Tactic:
aesop

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
⊢ ∀ (a_1 : ℂ), f a_1 = g a_1 → log⁺ ‖f a_1 - a.untop₀‖⁻¹ = log⁺ ‖g a_1 - a.untop₀‖⁻¹

Tactic:
aesop

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

Goal state before:
pp: case «0»
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ (fun i ↦ i) ⟨0, ⋯⟩ ∈ Finset.univ → Meromorphic (![f₁, f₂] ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
aesop

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

Goal state before:
pp: case «1»
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ (fun i ↦ i) ⟨1, ⋯⟩ ∈ Finset.univ → Meromorphic (![f₁, f₂] ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
aesop

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

Goal state before:
pp: E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
⊢ (fun r ↦ ∑ᶠ (z : E), ↑(((toClosedBall r) 0) z) * log (r * ‖z‖⁻¹) + ↑(0 0) * log r) = 0

Tactic:
aesop

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

Goal state before:
pp: f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ log ‖meromorphicTrailingCoeffAt (fun x ↦ -a) 0‖ = 0

Tactic:
aesop

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

Goal state before:
pp: f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ (if -a = 0 then ⊤ else 0) < meromorphicOrderAt f 0

Tactic:
aesop

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

Goal state before:
pp: case h₁
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicOrderAt f 0 = if a = 0 then ⊤ else 0

Tactic:
aesop

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

Goal state before:
pp: case neg.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0

Tactic:
aesop

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

Goal state before:
pp: case pos
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ circleAverage (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
simp_rw [norm_sub_rev]

Goal state after:
case pos
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ circleAverage (fun x ↦ log ‖x - meromorphicTrailingCoeffAt f 0‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
⊢ Integrable (fun x ↦ ∫ (α : ℝ) in Ioc 0 (2 * π), ‖cartanKernel f R α x‖) (volume.restrict (Ioc 0 (2 * π)))

Tactic:
have h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ := by
    have : CircleIntegrable (log⁺ ‖f ·‖) 0 R := h.meromorphicOn.circleIntegrable_posLog_norm
    rwa [CircleIntegrable, intervalIntegrable_iff_integrableOn_Ioc_of_le two_pi_pos.le] at this

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
⊢ Integrable (fun x ↦ ∫ (α : ℝ) in Ioc 0 (2 * π), ‖cartanKernel f R α x‖) (volume.restrict (Ioc 0 (2 * π)))
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0

Tactic:
aesop

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

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
hab : a ≤ b
⊢ circleAverage (fun x ↦ logCounting f (↑x) a) 0 1 +
      circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 ≤
    characteristic f ⊤ b

Tactic:
characteristic_top_eq_circleAverage_add_circleAverage h hb.ne'

Goal state after:
f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
hab : a ≤ b
⊢ circleAverage (fun x ↦ logCounting f (↑x) a) 0 1 +
      circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 ≤
    circleAverage (fun x ↦ logCounting f (↑x) b) 0 1 +
      circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ (LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)) →
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))

Tactic:
rintro h x xs y ys xy

Goal state after:
case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case h₁.h
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 := ((toClosedBall b) D).support
hs : s.Finite
z : E
⊢ (z ∈ Function.support fun z ↦ ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)) → z ∈ ↑hs.toFinset

Tactic:
aesop

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
⊢ logCounting D = logCounting (single e 1) + logCounting (D - single e 1)

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Lindelof

Goal state before:
pp: case right
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)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
this : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
A : E → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), {x | s x < d} = ⋃ f ∈ A d, U f d
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval x '' 𝓕')
H : s x < e
⊢ False

Tactic:
rcases D_dense.exists_between H with ⟨d, d_mem, hd⟩

Goal state after:
case right
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)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
this : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
A : E → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), {x | s x < d} = ⋃ f ∈ A d, U f d
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval x '' 𝓕')
H : s x < e
d : E
d_mem : d ∈ D
hd : d ∈ Ioo (s x) e
⊢ False
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a.hf
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ MeromorphicOn f (closedBall 0 |R|)

Tactic:
aesop

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

Goal state before:
pp: case e_a.hz
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ 0 ∈ closedBall 0 |R|

Tactic:
aesop

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

Goal state before:
pp: case e_a.hf
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ MeromorphicOn f univ

Tactic:
aesop

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

Goal state before:
pp: case e_a.hz
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ 0 ∈ univ

Tactic:
aesop

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

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
p₁ p₂ p₃ p₄ : P
⊢ (((Wbtw R p₁ p₂ p₃ ∧ Wbtw R p₁ p₂ p₄) ∧ Wbtw R p₁ p₃ p₄) ∧ Wbtw R p₂ p₃ p₄) ∧
      (¬p₁ = p₂ ∧ ¬p₁ = p₃ ∧ ¬p₁ = p₄) ∧ (¬p₂ = p₃ ∧ ¬p₂ = p₄) ∧ ¬p₃ = p₄ ↔
    (Wbtw R p₁ p₂ p₃ ∧ ¬p₂ = p₁ ∧ ¬p₂ = p₃) ∧
      (Wbtw R p₁ p₂ p₄ ∧ ¬p₂ = p₁ ∧ ¬p₂ = p₄) ∧
        (Wbtw R p₁ p₃ p₄ ∧ ¬p₃ = p₁ ∧ ¬p₃ = p₄) ∧ Wbtw R p₂ p₃ p₄ ∧ ¬p₃ = p₂ ∧ ¬p₃ = p₄

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝³ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
i : J
x : F.obj i
s : Set (F.obj i) := {x}
⊢ ∃ a, (fun s ↦ ↑s i) a = x

Tactic:
have := F.toPreimages_nonempty_of_surjective s Fsur (singleton_nonempty x)

Goal state after:
J : Type u
inst✝³ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
⊢ ∃ a, (fun s ↦ ↑s i) a = x
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
⊢ (of fun i j ↦ star (Perm.permMatrix R σ⁻¹ i j)) = Perm.permMatrix R σ⁻¹

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ ¬f = g → ¬f.toMatrix = g.toMatrix

Tactic:
simp only [Matrix.ext_iff.symm, toMatrix_apply, PEquiv.ext_iff, not_forall, exists_imp]

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ ∀ (x : m), ¬f x = g x → ∃ x x_1, ¬(if x_1 ∈ f x then 1 else 0) = if x_1 ∈ g x 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
hM : M ∈ rowStochastic R n
hx : x ⬝ᵥ 1 = 1
⊢ x ᵥ* M ⬝ᵥ 1 = 1

Tactic:
by
  rw [← dotProduct_mulVec, hM.2, hx]

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
⊢ Convex R ↑(rowStochastic R n)

Tactic:
by
  intro x hx y hy a b ha hb h
  simp only [SetLike.mem_coe, mem_rowStochastic_iff_sum] at hx hy ⊢
  simp [add_nonneg, ha, hb, mul_nonneg, hx, hy, sum_add_distrib, ← mul_sum, h]

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
σ : Equiv.Perm n
i j : n
⊢ 0 ≤ Equiv.Perm.permMatrix R σ i j

Tactic:
aesop

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✝⁷ : Semiring R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : IsOrderedRing R✝
M✝ : Matrix n✝ n✝ R✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
⊢ M * N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}

Tactic:
refine ⟨fun i j => sum_nonneg fun i _ => mul_nonneg (hM.1 _ _) (hN.1 _ _), ?_, ?_⟩

Goal state after:
case refine_1
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✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
⊢ (M * N) *ᵥ 1 = 1

case refine_2
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✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
⊢ 1 ᵥ* (M * N) = 1
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:
by
  simp only [Finset.convexHull_eq, mem_ofPred_eq] at m ⊢
  obtain ⟨f, fpos, fsum, rfl⟩ := m
  obtain ⟨g, gcombo, gsum, gpos⟩ := exists_nontrivial_relation_sum_zero_of_not_affine_ind h
  replace gpos := exists_pos_of_sum_zero_of_exists_nonzero g gsum gpos
  clear h
  let s := {z ∈ t | 0 < g z}
  obtain ⟨i₀, mem, w⟩ : ∃ i₀ ∈ s, ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i := by
    apply s.exists_min_image fun z => f z / g z
    obtain ⟨x, hx, hgx⟩ : ∃ x ∈ t, 0 < g x := gpos
    exact ⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩
  have hg : 0 < g i₀ := by
    rw [mem_filter] at mem
    exact mem.2
  have hi₀ : i₀ ∈ t := filter_subset _ _ mem
  let k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
  have hk : k i₀ = 0 := by simp [k, ne_of_gt hg]
  have ksum : ∑ e ∈ t.erase i₀, k e = 1 := by
    calc
      ∑ e ∈ t.erase i₀, k e = ∑ e ∈ t, k e := by
        conv_rhs => rw [← insert_erase hi₀, sum_insert (notMem_erase i₀ t), hk, zero_add]
      _ = ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) := rfl
      _ = 1 := by rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
  refine ⟨⟨i₀, hi₀⟩, k, ?_, by convert! ksum, ?_⟩
  · simp only [k, and_imp, sub_nonneg, mem_erase, Ne]
    intro e _ het
    by_cases hes : e ∈ s
    · have hge : 0 < g e := by
        rw [mem_filter] at hes
        exact hes.2
      rw [← le_div_iff₀ hge]
      exact w _ hes
    · calc
        _ ≤ 0 := by
          apply mul_nonpos_of_nonneg_of_nonpos
          · apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg)
          · simpa only [s, mem_filter, het, true_and, not_lt] using hes
        _ ≤ f e := fpos e het
  · rw [Subtype.coe_mk, centerMass_eq_of_sum_1 _ id ksum]
    calc
      ∑ e ∈ t.erase i₀, k e • e = ∑ e ∈ t, k e • e := sum_erase _ (by rw [hk, zero_smul])
      _ = ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) • e := rfl
      _ = t.centerMass f id := by
        simp only [sub_smul, mul_smul, sum_sub_distrib, ← smul_sum, gcombo, smul_zero, sub_zero,
          centerMass, fsum, inv_one, one_smul, id]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x y : R
hxz : x ≤ x
⊢ Wbtw R x y x ↔ x ≤ y ∧ y ≤ x

Tactic:
← le_antisymm_iff,

Goal state after:
case inl
R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x y : R
hxz : x ≤ x
⊢ Wbtw R x y x ↔ x = y
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: case h
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
this : ∃ M' ∈ doublyStochastic R n, N = s' • M'
⊢ ∃ x ∈ {i | M i.1 i.2 ≠ 0}, x ∉ {i | N i.1 i.2 ≠ 0}

Tactic:
simp_rw [mem_filter_univ, not_not, Prod.exists]
      exact ⟨i, σ i, hMi'.ne', by simp [N, Equiv.toPEquiv_apply]⟩

Goal state after: