mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: z : ℂ
⊢ !![z.re, -z.im; z.im, z.re] 0 0 * !![z.re, -z.im; z.im, z.re] 1 1 -
      !![z.re, -z.im; z.im, z.re] 0 1 * !![z.re, -z.im; z.im, z.re] 1 0 =
    normSq z

Tactic:
normSq_apply

Goal state after:
z : ℂ
⊢ !![z.re, -z.im; z.im, z.re] 0 0 * !![z.re, -z.im; z.im, z.re] 1 1 -
      !![z.re, -z.im; z.im, z.re] 0 1 * !![z.re, -z.im; z.im, z.re] 1 0 =
    z.re * z.re + z.im * z.im
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[Units.instTopologicalSpaceUnits, Units.instTopologicalSpaceUnits] ⇑det

Tactic:
simp_rw [Units.continuous_iff, ← map_inv]
  constructor <;> fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[instTopologicalSpace, Units.instTopologicalSpaceUnits] ⇑toGL

Tactic:
simp_rw [Units.continuous_iff, ← map_inv]
  constructor <;> fun_prop

Goal state after:
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
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst✝²] U
hU₃ : y ∈ U
⊢ ∃ i, IsCompact i ∧ MapsTo f iᶜ N

Tactic:
refine ⟨f⁻¹' Uᶜ, ?_, by simpa using (mapsTo_preimage f U).mono_right hU₁⟩

Goal state after:
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
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst✝²] U
hU₃ : y ∈ U
⊢ IsCompact (f ⁻¹' Uᶜ)
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:

Tactic:
proximity (f₁ * f₂) 0
    _ ≤ (proximity f₁⁻¹ ⊤) + (proximity f₂⁻¹ ⊤) := by
      rw [← proximity_inv, mul_inv]
      apply proximity_mul_top_le h₁f₁.inv h₁f₂.inv
    _ = (proximity f₁ 0) + (proximity f₂ 0) := by
      rw [proximity_inv, proximity_inv]

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

Goal state before:
pp: case neg
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : ¬MeromorphicAt f 0
this : ∀ {a : ℂ}, ¬MeromorphicAt (fun x ↦ f x - a) 0
⊢ circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
simp_all [circleAverage_const]

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

Goal state before:
pp: case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
⊢ ∑ᶠ (z : E), (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹) =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

pp: case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
⊢ (↑(D₁ 0) + ↑(D₂ 0)) * log r = ↑(D₁ 0) * log r + ↑(D₂ 0) * log r

Tactic:
· have h₁s : ((D₁.toClosedBall r).support ∪ (D₂.toClosedBall r).support).Finite := by
        apply Set.finite_union.2
        constructor
        <;> apply finiteSupport _ (isCompact_closedBall 0 |r|)
      repeat
        rw [finsum_eq_sum_of_support_subset (s := h₁s.toFinset)]
        try simp_rw [← Finset.sum_add_distrib, ← add_mul]
      repeat
        intro x hx
        by_contra
        simp_all

Goal state after:
case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
⊢ (↑(D₁ 0) + ↑(D₂ 0)) * log r = ↑(D₁ 0) * log r + ↑(D₂ 0) * log r
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 : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
a✝ : a ≤ b
⊢ logCounting D a ≤ logCounting D b

Tactic:
simp_all only [mem_Ioi, logCounting, AddMonoidHom.coe_mk, ZeroHom.coe_mk]

Goal state after:
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
⊢ ∑ᶠ (z : E), ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹) + ↑(D 0) * log a ≤
    ∑ᶠ (z : E), ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹) + ↑(D 0) * log b
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
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E)ᶜ
y : F
h : y ∈ E
⊢ ∃ z, z ∉ E

Tactic:
rw [← not_forall, ← Submodule.eq_top_iff']
      rintro rfl
      simp at hcodim

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
⊢ ¬∃ c > 0, ∀ᶠ (x : ℝ) in atTop, c * ‖logCounting D x‖ ≤ ‖1 x‖

Tactic:
push Not

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
⊢ ∀ c > 0, ∃ᶠ (x : ℝ) in atTop, ‖1 x‖ < c * ‖logCounting D x‖
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
f : 𝕜 → E
⊢ locallyFinsuppWithin.logCounting ((divisor f univ)⁺ - (divisor f univ)⁻) =
    locallyFinsuppWithin.logCounting (divisor f univ)⁺ - logCounting f ⊤

Tactic:
logCounting_top,

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ locallyFinsuppWithin.logCounting ((divisor f univ)⁺ - (divisor f univ)⁻) =
    locallyFinsuppWithin.logCounting (divisor f univ)⁺ - locallyFinsuppWithin.logCounting (divisor f univ)⁻
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (0 * (y - x))) ↔
    ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

Tactic:
simp only [zero_mul, ENNReal.ofReal_zero, ← eVariationOn.eq_zero_iff]

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) ↔ eVariationOn f s = 0
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: 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 ≠ []
⊢ (∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l) ↔ List.Wbtw R l

Tactic:
by
  refine ⟨fun ⟨l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩
  · rw [← hl'l]
    exact Wbtw.map hl's.wbtw _
  · suffices ∃ l' : List R, (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧
        l'.map (lineMap (l.head hl) (l.getLast hl)) = l by
      rcases this with ⟨l', -, hl'⟩
      exact ⟨l', hl'⟩
    induction l with
    | nil => simp at hl
    | cons head tail ih =>
      by_cases ht : tail = []
      · refine ⟨[0], ?_⟩
        simp [ht, sortedLE_iff_pairwise]
      · rw [wbtw_cons] at h
        replace ih := ih ht h.2
        rcases ih with ⟨l'', hl''0, hl''s, hl''⟩
        simp only [head_cons, getLast_cons ht]
        cases tail with
        | nil => simp at ht
        | cons head2 tail =>
          by_cases ht2 : tail = []
          · exact ⟨[0, 1], by simp [ht2, sortedLE_iff_pairwise]⟩
          · simp only [head_cons, getLast_cons ht2] at hl'' ⊢
            rw [pairwise_cons] at h
            have hw := h.1.1 _ (getLast_mem ht2)
            rcases hw with ⟨r, ⟨hr0, hr1⟩, rfl⟩
            refine ⟨0 :: l''.map fun x ↦ r + (1 - r) * x, ?_, ?_, ?_⟩
            · simp only [mem_cons, mem_map, forall_eq_or_imp, le_refl, forall_exists_index,
                and_imp, forall_apply_eq_imp_iff₂, true_and]
              intro a ha
              have := hl''0 a ha
              nlinarith
            · simp only [sortedLE_iff_pairwise, pairwise_cons, mem_map,
                forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
              refine ⟨?_, ?_⟩
              · intro a ha
                have := hl''0 a ha
                nlinarith
              · refine hl''s.pairwise.map _ fun a b hab ↦ ?_
                gcongr
            · simp only [map_cons, lineMap_apply_zero, map_map, ← hl'', cons.injEq,
                map_inj_left, Function.comp_apply, lineMap_lineMap_left, lineMap_eq_lineMap_iff,
                true_and]
              ring_nf
              simp

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : 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
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s.Nonempty
𝓕 : Set (↑s → ℝ) := {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c}
⊢ BddAbove 𝓕

Tactic:
exact (bddAbove_def.2 ⟨φ ∘ Subtype.val, fun y hy => hy.1⟩)

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
⊢ Wbtw R x y x ↔ y = x

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
  · simpa [Wbtw, affineSegment] using h
  · rw [h]
    exact wbtw_self_left R x x

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

Goal state before:
pp: case refine_1
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✝⁶ : ZeroLEOneClass R
R' : Type u_6
inst✝⁵ : Ring R'
inst✝⁴ : PartialOrder R'
inst✝³ : Module R' V
inst✝² : Module R' R
inst✝¹ : IsScalarTower R' R V
inst✝ : SMulPosMono R' R
x y : P
a : R'
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ 0 ≤ a • 1

Tactic:
← zero_smul R' (1 : R)

Goal state after:
case refine_1
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✝⁶ : ZeroLEOneClass R
R' : Type u_6
inst✝⁵ : Ring R'
inst✝⁴ : PartialOrder R'
inst✝³ : Module R' V
inst✝² : Module R' R
inst✝¹ : IsScalarTower R' R V
inst✝ : SMulPosMono R' R
x y : P
a : R'
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ 0 • 1 ≤ a • 1
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : 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
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕'.Nonempty
f : ℕ → ↑s → ℝ
hf : 𝓕' = range f
l : ℕ → E →L[𝕜] 𝕜
c : ℕ → ℝ
hlc : ∀ (i : ℕ), f i = s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i)
⊢ ∃ l c,
    (∀ (i : ℕ), s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) ≤ s.domRestrict φ) ∧
      ⨆ i, s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) = s.domRestrict φ

Tactic:
refine ⟨l, c, fun i => (hlc i) ▸ (h𝓕'.2.2 (f i) (hf ▸ mem_range_self i)).1, ?_⟩

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : 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
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕'.Nonempty
f : ℕ → ↑s → ℝ
hf : 𝓕' = range f
l : ℕ → E →L[𝕜] 𝕜
c : ℕ → ℝ
hlc : ∀ (i : ℕ), f i = s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i)
⊢ ⨆ i, s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i) = s.domRestrict φ
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ), ¬∃ b, b ∈ f a ∧ a_1 ∈ g b) ↔ ∀ (b : β) (c : γ), b ∈ f a → ¬c ∈ g b

Tactic:
push Not

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ) (b : β), b ∈ f a → ¬a_1 ∈ g b) ↔ ∀ (b : β) (c : γ), b ∈ f a → ¬c ∈ g b
Module: Mathlib.Data.Matrix.PEquiv

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

Tactic:
dsimp [Matrix.mul_apply, toMatrix_apply]
  rcases h : f.symm j with - | fj
  · simp [h, ← f.eq_some_iff]
  · rw [Finset.sum_eq_single fj]
    · simp [h, ← f.eq_some_iff]
    · rintro b - n
      simp [h, ← f.eq_some_iff, n.symm]
    · simp

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

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
⊢ (PEquiv.refl n).toMatrix = 1

Tactic:
ext
  simp [toMatrix_apply, one_apply]

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
M : Matrix n n R
hs : 0 ≤ 0
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = 0) ∧ ∀ (j : n), ∑ i, M i j = 0) →
    ∃ M' ∈ doublyStochastic R n, M = 0 • M'

Tactic:
simp only [zero_smul, exists_and_right, and_imp]

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hs : 0 ≤ 0
⊢ (∀ (i j : n), 0 ≤ M i j) →
    (∀ (i : n), ∑ j, M i j = 0) → (∀ (j : n), ∑ i, M i j = 0) → (∃ x, x ∈ doublyStochastic R n) ∧ M = 0
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: 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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ (((t₁ - t₂ * t₁) * 1 - (t₁ - t₂ * t₁) * (t₂ * t₁)) / (1 - t₂ * t₁) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
rw [← mul_sub, mul_div_assoc]

Goal state after:
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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_2
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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)

Tactic:
← smul_sub,

Goal state after:
case refine_2
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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
⊢ t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w - (x -ᵥ w)) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
x : E
hx : x ∈ s
⊢ x ∈ interior ((convexHull ℝ) (range ⇑b)) + {x}

Tactic:
simpa using hb₁

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
p q : M
⊢ convexCombPair s t hs ht h p q = iConvexComb (duple 0 1 hs ht h) ![p, q]

Tactic:
simp [StdSimplex.iConvexComb, convexCombPair]

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

Goal state before:
pp: case e'_3
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
x : X
hx : x ∈ u
⊢ w.weights (f x) = (onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯) x

Tactic:
exact (if_pos hx).symm

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : LinearOrder E
inst✝⁷ : IsOrderedAddMonoid E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : PosSMulMono 𝕜 E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Iic e) f
hg : ConvexOn 𝕜 (Set.Ici e) g
h_anti : AntitoneOn f (Set.Iic e)
h_mono : MonotoneOn g (Set.Ici e)
h_eq : f e = g e
x : E
x✝¹ : x ∈ Set.univ
y : E
x✝ : y ∈ Set.univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hx : e < x
hy : y ≤ e
hc : e < a • x + b • y
hc' : a • x + b • y ≤ a • x + b • e
⊢ a • g x + b • g e ≤ a • g x + b • f y

Tactic:
rw [← h_eq]
        gcongr
        exact h_anti hy Set.self_mem_Iic hy

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

Goal state before:
pp: V : Type u
⊢ Injective fun x ↦ { Adj := fun v w ↦ ↑x v w = true, symm := ⋯, loopless := ⋯ }

Tactic:
rintro ⟨adj, _⟩ ⟨adj', _⟩
    simp only [mk.injEq, Subtype.mk.injEq]
    intro h
    funext v w
    simpa [Bool.coe_iff_coe] using congr_fun₂ h v w

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

Goal state before:
pp: V : Type u
G₁ G₂ : SimpleGraph V
⊢ (G₁ ⊓ G₂).edgeSet ⊆ ⊥.edgeSet ↔ G₁ ⊓ G₂ ≤ ⊥

Tactic:
OrderEmbedding.le_iff_le

Goal state after:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ G₁ ⊓ G₂ ≤ ⊥ ↔ G₁ ⊓ G₂ ≤ ⊥
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.inr.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
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (y -ᵥ p₂')
⊢ r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ p₁') - r₁ • (p₁ -ᵥ p₁')

Tactic:
← smul_sub,

Goal state after:
case mp.inr.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
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (y -ᵥ p₂')
⊢ r₁ • (x -ᵥ p₁) = r₁ • (x -ᵥ p₁' - (p₁ -ᵥ p₁'))
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: case «0»
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
⊢ 0 ≤ w ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
⊢ 0 ≤ w ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2»
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
⊢ 0 ≤ w ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
· exact mul_nonneg (mul_nonneg haz hav) hbu

Goal state after:
case «1»
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
⊢ 0 ≤ w ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
⊢ 0 ≤ w ((fun i ↦ i) ⟨2, ⋯⟩)