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

Goal state before:
pp: s : Set ℍ
this :
  MeasurePreserving UpperHalfPlane.coe (Measure.comap UpperHalfPlane.coe volume)
    (volume.restrict (Set.range UpperHalfPlane.coe))
⊢ volume s = ∫⁻ (z : ℂ) in UpperHalfPlane.coe '' s, ↑((1 / ‖z.im‖₊) ^ 2)

Tactic:
rw [volume_def, withDensity_apply',
    ← Set.inter_eq_self_of_subset_left (Set.image_subset_range _ _),
    ← Measure.restrict_restrict', ← this.setLIntegral_comp_emb measurableEmbedding_coe]

Goal state after:
s : Set ℍ
this :
  MeasurePreserving UpperHalfPlane.coe (Measure.comap UpperHalfPlane.coe volume)
    (volume.restrict (Set.range UpperHalfPlane.coe))
⊢ ∫⁻ (a : ℍ) in s, ↑((1 / NNReal.mk a.im ⋯) ^ 2) ∂Measure.comap UpperHalfPlane.coe volume =
    ∫⁻ (a : ℍ) in s, ↑((1 / ‖(↑a).im‖₊) ^ 2) ∂Measure.comap UpperHalfPlane.coe volume

s : Set ℍ
this :
  MeasurePreserving UpperHalfPlane.coe (Measure.comap UpperHalfPlane.coe volume)
    (volume.restrict (Set.range UpperHalfPlane.coe))
⊢ MeasurableSet (Set.range UpperHalfPlane.coe)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n fun x ↦ denom g ↑x ^ k

Tactic:
intro τ
  have : AnalyticAt ℂ (· ^ k) (denom g τ) := (differentiableOn_zpow k _ (by tauto)).analyticOnNhd
    isOpen_compl_singleton _ (denom_ne_zero g τ)
  exact this.contDiffAt.contMDiffAt.comp τ (contMDiff_denom g τ)

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

Goal state before:
pp: z : ℍ
⊢ z.center 0 = z

Tactic:
apply ext_re_im <;> simp

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

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

Tactic:
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.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ sinh (-x) - -x = -(sinh x - x)

Tactic:
by simp; abel

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

Goal state before:
pp: z : ℍ
r : ℝ
⊢ dist ↑z ↑(z.center r) = z.im * (Real.cosh r - 1)

Tactic:
rw [dist_of_re_eq (z.center_re r).symm, dist_comm, Real.dist_eq, mul_sub, mul_one]
  exact abs_of_nonneg (sub_nonneg.2 <| le_mul_of_one_le_right z.im_pos.le (one_le_cosh _))

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

Goal state before:
pp: case refine_2
z w : ℍ
r : ℝ
⊢ PseudoMetricSpace.toUniformSpace.toTopologicalSpace ≤ instTopologicalSpace

Tactic:
let : MetricSpace ℍ := metricSpaceAux

Goal state after:
case refine_2
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
⊢ PseudoMetricSpace.toUniformSpace.toTopologicalSpace ≤ instTopologicalSpace
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
b : Ultrafilter α
⊢ Tendsto pure (↑b) (𝓝 b)

Tactic:
rw [Tendsto, ← coe_map, ultrafilter_converges_iff]
  ext s
  change s ∈ b ↔ {t | s ∈ t} ∈ map pure b
  simp_rw [mem_map, preimage_ofPred_eq, mem_pure, ofPred_mem_eq]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ 𝓝 ∞ = map some (coclosedCompact X) ⊔ pure ∞

Tactic:
← nhdsNE_infty_eq,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ 𝓝 ∞ = 𝓝[≠] ∞ ⊔ pure ∞
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ CircleIntegrable (fun x ↦ log⁺ ‖∑ c ∈ s, f c x‖) 0 r

Tactic:
apply (Meromorphic.fun_sum hf).meromorphicOn.circleIntegrable_posLog_norm

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

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ S • K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A

Tactic:
convert! hA (S * g) (by rwa [mul_smul, Set.smul_mem_smul_set_iff]) using 1

Goal state after:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ S • K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 = ↑(S * g) 1 0 ^ 2 + ↑(S * g) 1 1 ^ 2
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ characteristic (f₁ * f₂) ⊤ r ≤ (characteristic f₁ ⊤ + characteristic f₂ ⊤) r

Tactic:
simp only [characteristic, Pi.add_apply]
  rw [add_add_add_comm]
  apply add_le_add (proximity_mul_top_le h₁f₁ h₁f₂ r)
    (logCounting_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂)

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 a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
← circleAverage_congr_codiscreteWithin
      (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero hf h) zero_ne_one.symm

Goal state after:
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‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int :
  Integrable (fun p ↦ cartanKernel f R p.1 p.2)
    ((volume.restrict (Ioc 0 (2 * π))).prod (volume.restrict (Ioc 0 (2 * π))))
⊢ IntegrableOn (fun x ↦ ∫ (β : ℝ) in 0..2 * π, cartanKernel f R x β) (Ioc 0 (2 * π)) volume

Tactic:
simpa [IntegrableOn, intervalIntegral.integral_of_le two_pi_pos.le, Cartan.cartanKernel]
    using h_int.integral_prod_left

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
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
inst✝ : TopologicalSpace E
s : Set F
h : AmpleSet s
L : E ≃ᴬ[ℝ] F
⊢ AmpleSet (⇑L ⁻¹' s)

Tactic:
by
  rw [← L.image_symm_eq_preimage]
  exact h.image L.symm

Goal state after:
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
  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.ConstantSpeed

Goal state before:
pp: case inr.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal (↑l * (y - z))

Tactic:
· 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.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
p₁ p₂ p₃ p₄ : P
⊢ List.Wbtw R [p₁, p₂, p₃, p₄] ↔ Wbtw R p₁ p₂ p₃ ∧ Wbtw R p₁ p₂ p₄ ∧ Wbtw R p₁ p₃ p₄ ∧ Wbtw R p₂ p₃ p₄

Tactic:
by
  simp [List.Wbtw, triplewise_cons, and_assoc]

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

Goal state before:
pp: case cons.refine_2.refine_1.cons.inl
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
head : P
tail : List P
x✝ :
  (Pairwise (Sbtw R head) (head :: tail) ∧ Triplewise (Sbtw R) (head :: tail)) ∧
    ∀ (a : P), head :: head :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head :: tail)
ha : ∀ (a : P), head :: head :: tail ≠ [a, a]
ht' : List.Wbtw R (head :: tail)
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail) ↔ ∀ (a : P), head :: tail ≠ [a, a]
ha' : head ∈ head :: tail
⊢ False

pp: case cons.refine_2.refine_1.cons.inr
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
head head2 : P
tail : List P
x✝ :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
hat : head ∈ tail
⊢ False

Tactic:
· cases tail with
            | nil => simp at ha
            | cons head3 tail => simpa using hp.1 head3

Goal state after:
case cons.refine_2.refine_1.cons.inr
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
head head2 : P
tail : List P
x✝ :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
hat : head ∈ tail
⊢ False
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case refine_1.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
l : List P
hl : l ≠ []
x✝ : ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
hla : l.head hl ≠ l.getLast hl
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl))) l')

Tactic:
· exact (hl's.pairwise.imp LT.lt.ne).map _ fun _ _ ↦ (lineMap_injective _ hla).ne

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

Goal state before:
pp: case intro.ind.succ
α : Type v
inst✝¹ : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι],
      (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) →
        ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
· have ih' : ∀ (ι' : Type u) [Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n →
        (∀ s' : Finset ι', #s' ≤ #(s'.biUnion t')) →
        ∃ f : ι' → α, Function.Injective f ∧ ∀ x, f x ∈ t' x := by
      intro ι' _ _ hι' ht'
      exact ih _ (Nat.lt_succ_of_le hι') ht' _ rfl
    by_cases! h : ∀ s : Finset ι, s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
    · refine hall_hard_inductive_step_A hn ht (@fun ι' => ih' ι') h
    · rcases h with ⟨s, sne, snu, sle⟩
      exact hall_hard_inductive_step_B hn ht (@fun ι' => ih' ι')
        s sne snu (Nat.le_antisymm (ht _) sle)

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

Goal state before:
pp: case mp
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
⊢ ∃ f, Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
have : ∀ ι' : (Finset ι)ᵒᵖ, Finite ((hallMatchingsFunctor t).obj ι') := by
        intro ι'
        rw [hallMatchingsFunctor]
        infer_instance
      -- Apply the compactness argument
      obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (hallMatchingsFunctor t)
      -- Interpret the resulting section of the inverse limit
      refine ⟨?_, ?_, ?_⟩
      · -- Build the matching function from the section
        exact fun i =>
          (u (Opposite.op ({i} : Finset ι))).val ⟨i, by simp only [mem_singleton]⟩
      · -- Show that it is injective
        intro i i'
        have subi : ({i} : Finset ι) ⊆ {i, i'} := by simp
        have subi' : ({i'} : Finset ι) ⊆ {i, i'} := by simp
        simp only
        rw [← hu (CategoryTheory.homOfLE subi).op, ← hu (CategoryTheory.homOfLE subi').op]
        let uii' := u (Opposite.op ({i, i'} : Finset ι))
        exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)
      · -- Show that it maps each index to the corresponding finite set
        intro i
        apply (u (Opposite.op ({i} : Finset ι))).property.2

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq β
R : SetRel α β
inst✝ : (a : α) → Fintype ↑(R.image {a})
⊢ (∀ (A : Finset α), #A ≤ card ↑(R.image ↑A)) ↔ ∃ f, Injective f ∧ ∀ (x : α), (x, f x) ∈ R

Tactic:
by
  let r' a := (R.image {a}).toFinset
  have h : ∀ A : Finset α, Fintype.card (R.image A) = #(A.biUnion r') := by
    intro A
    rw [← Set.toFinset_card]
    apply congr_arg
    ext b
    simp [r', SetRel.image]
  have h' : ∀ (f : α → β) (x), x ~[R] f x ↔ f x ∈ r' x := by simp [r', SetRel.image]
  simp only [h, h']
  apply Finset.all_card_le_biUnion_card_iff_exists_injective

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
hM : M ∈ doublyStochastic R n
i j : n
⊢ M i j ≤ 1

Tactic:
rw [← sum_row_of_mem_doublyStochastic hM i]

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
hM : M ∈ doublyStochastic R n
i j : n
⊢ M i j ≤ ∑ j, M i 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₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : w i₁ + (w i₂ + w i₃) = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
hss : SignType.sign (w i₃) = 1
hs' : SignType.sign (∑ i, w i) = SignType.sign (w i₃)
hs : ∀ (i : Fin 3), 0 < w i
⊢ w i₁ < 1

Tactic:
by_contra hle
    rw [not_lt] at hle
    exact (hle.trans_lt (lt_add_of_pos_right _ (Left.add_pos (hs i₂) (hs i₃)))).ne' hw

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x✝ : ∅.Nonempty
w✝ : E
hx : w✝ ∈ ∅
⊢ ∃ l, ∅ = {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}

Tactic:
exfalso
  exact hx

Goal state after:
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)
⊢ p (f x) ∈ (convexHull 𝕜) (p '' ⇑f '' s)

Tactic:
by rwa [Set.image_image]

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hc : ConvexIndependent 𝕜 Subtype.val
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ (convexHull 𝕜) t
⊢ ↑⟨x, hxs⟩ ∈ (convexHull 𝕜) (Subtype.val '' {x | ↑x ∈ t})

Tactic:
rw [Subtype.coe_image_of_subset h]

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hc : ConvexIndependent 𝕜 Subtype.val
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ (convexHull 𝕜) t
⊢ ↑⟨x, hxs⟩ ∈ (convexHull 𝕜) t
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hc : ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t
t : Set { x // x ∈ s }
x : { x // x ∈ s }
h : ↑x ∈ (convexHull 𝕜) (Subtype.val '' t)
⊢ ↑x ∈ (fun a ↦ ↑a) '' t

Tactic:
exact hc (t.image ((↑) : s → E)) (Subtype.coe_image_subset s t) ⟨x.prop, h⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ConvexIndependent 𝕜 Subtype.val ↔ ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t

Tactic:
constructor
  · rintro hc t h x ⟨hxs, hxt⟩
    refine hc { x | ↑x ∈ t } ⟨x, hxs⟩ ?_
    rw [Subtype.coe_image_of_subset h]
    exact hxt
  · intro hc t x h
    rw [← Subtype.coe_injective.mem_set_image]
    exact hc (t.image ((↑) : s → E)) (Subtype.coe_image_subset s t) ⟨x.prop, h⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ a = b

Tactic:
rw [← mem_singleton]

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ a ∈ {b}
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsne : (interior s).Nonempty
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
e : E ≃ₜ E
h₁ : ⇑e '' interior s = interior t
h₂ : ⇑e '' closure[inst✝³] s = closure[inst✝³] t
⊢ ⇑e '' frontier s = frontier t

Tactic:
← closure_sdiff_interior,

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsne : (interior s).Nonempty
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
e : E ≃ₜ E
h₁ : ⇑e '' interior s = interior t
h₂ : ⇑e '' closure[inst✝³] s = closure[inst✝³] t
⊢ ⇑e '' (closure[inst✝³] s \ interior s) = closure[inst✝³] t \ interior t
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: X : Type u_2
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
w : StdSimplex K X
s : Set X
hs : ∃ x ∈ s, w.weights x ≠ 0
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (w.restrict s hs).weights = ((filter (fun x ↦ x ∈ s) w.weights).sum fun _x k ↦ k)⁻¹ • filter (fun x ↦ x ∈ s) w.weights

Tactic:
by
  simp [restrict]; congr

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 α
t : Set α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
ht : μ t ≠ ∞
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
⊢ f =ᵐ[μ.restrict t] const α (⨍ (x : α) in t, f x ∂μ) ∨ ‖∫ (x : α) in t, f x ∂μ‖ < μ.real t * C

Tactic:
by
  have := Fact.mk ht.lt_top
  rw [← measureReal_restrict_apply_univ]
  exact ae_eq_const_or_norm_integral_lt_of_norm_le_const h_le

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
ι : Type u_6
X : ι → Type u_7
inst✝ : (i : ι) → ConvexSpace R (X i)
s : Set ι
x : (i : ι) → X i
t : (i : ι) → Set (X i)
ht : ∀ i ∈ s, IsStarConvexSet R (x i) (t i)
y : (i : ι) → X i
hy : y ∈ s.pi t
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hi : i ∈ s
⊢ convexCombPair a b ha hb hab x y i ∈ t i

Tactic:
by simpa using ht _ hi (hy _ hi) _ ..

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: case refine_1
R : Type u_3
X : Type u_5
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
s : Set X
Y : Type u_7
inst✝ : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : ↑w.weights.support ⊆ s ×ˢ t
⊢ Prod.fst '' s ×ˢ t ⊆ s

Tactic:
fst_image_prod_subset

Goal state after:
case refine_1
R : Type u_3
X : Type u_5
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
s : Set X
Y : Type u_7
inst✝ : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : ↑w.weights.support ⊆ s ×ˢ t
⊢ s ⊆ s