mathlib-initiative/mathlib-tactics huggingface dataset:
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

pp: case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

Tactic:
rw [finsum_eq_sum_of_support_subset (s := h₁s.toFinset)]
        try simp_rw [← Finset.sum_add_distrib, ← add_mul]

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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ i ∈ h₁s.toFinset, ↑(((toClosedBall r) D₁) i) * log (r * ‖i‖⁻¹) +
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ i ∈ h₁s.toFinset, ↑(((toClosedBall r) D₁) i) * log (r * ‖i‖⁻¹) +
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

pp: case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

pp: case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

Tactic:
rw [finsum_eq_sum_of_support_subset (s := h₁s.toFinset)]
        try simp_rw [← Finset.sum_add_distrib, ← add_mul]

Goal state after:
case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

pp: case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

pp: case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

Tactic:
rw [finsum_eq_sum_of_support_subset (s := h₁s.toFinset)]
        try simp_rw [← Finset.sum_add_distrib, ← add_mul]

Goal state after:
case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

case e_a.h
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)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset
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₁ f₂ : 𝕜 → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ logCounting (f₁ + f₂) ⊤ ≤ᶠ[atTop] logCounting f₁ ⊤ + logCounting f₂ ⊤

Tactic:
filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ logCounting_add_top_le h₁f₁ h₁f₂ hr

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
p : α → α → α → Prop
f : α → β
p' : β → β → β → Prop
h : ∀ {a b c : α}, p' (f a) (f b) (f c) → p a b c
hl : Triplewise (fun a b c ↦ p' (f a) (f b) (f c)) l
⊢ Triplewise p l

Tactic:
exact hl.imp h

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

Goal state before:
pp: case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 ↦ t ↑x_1)
hb : a ∈ s'.biUnion fun x_1 ↦ t ↑x_1
⊢ #s' ≤ #((s'.biUnion fun x' ↦ t ↑x').erase a)

Tactic:
card_erase_of_mem hb

Goal state after:
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 ↦ t ↑x_1)
hb : a ∈ s'.biUnion fun x_1 ↦ t ↑x_1
⊢ #s' ≤ #(s'.biUnion fun x_1 ↦ t ↑x_1) - 1
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
h : Wbtw R x y z
f : P →ᵃ[R] P'
⊢ Wbtw R (f x) (f y) (f z)

Tactic:
by
  rw [Wbtw, ← affineSegment_image]
  exact Set.mem_image_of_mem _ h

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

Goal state before:
pp: case refine_1
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
x✝ : ∃ p₁ p₂ l', l'.SortedLE ∧ map (⇑(lineMap p₁ p₂)) l' = l
p₁ p₂ : P
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap p₁ p₂)) l' = l
⊢ List.Wbtw R l

Tactic:
subst hl'l
    exact Wbtw.map hl's.wbtw _

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

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
card_ι''_le : Fintype.card ↑ι'' ≤ n
f'' : ↑ι'' → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x
⊢ ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' ⟨x'', hx''⟩ ∉ s.biUnion t

Tactic:
intro x''

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
card_ι''_le : Fintype.card ↑ι'' ≤ n
f'' : ↑ι'' → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x
x'' : ι
⊢ ∀ (hx'' : x'' ∉ s), f'' ⟨x'', hx''⟩ ∉ s.biUnion t
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
⊢ Directed GE.ge fun G ↦ partialSections F G.snd

Tactic:
intro A

Goal state after:
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A : FiniteDiagram J
⊢ ∀ (y : FiniteDiagram J),
    ∃ z,
      (fun G ↦ partialSections F G.snd) A ⊇ (fun G ↦ partialSections F G.snd) z ∧
        (fun G ↦ partialSections F G.snd) y ⊇ (fun G ↦ partialSections F G.snd) z
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case pos
α : 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
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
h : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

pp: case neg
α : 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
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
h : ∃ s, s.Nonempty ∧ s ≠ univ ∧ #(s.biUnion t) ≤ #s
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
· refine hall_hard_inductive_step_A hn ht (@fun ι' => ih' ι') h

Goal state after:
case neg
α : 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
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
h : ∃ s, s.Nonempty ∧ s ≠ univ ∧ #(s.biUnion t) ≤ #s
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x y z : P
h : Wbtw R x y z
⊢ Wbtw R z x y ↔ x = y

Tactic:
by
  rw [← wbtw_rotate_iff R x, and_iff_right h]

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w)
    ((Finset.affineCombination R s p) w₂)

Tactic:
s.affineCombination_congr hr fun _ _ => rfl

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) (r • (w₂ - w₁) + w₁))
    ((Finset.affineCombination R s p) w₂)
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq β
R : SetRel α β
inst✝ : (a : α) → Fintype ↑(R.image {a})
r' : α → Finset β := fun a ↦ (R.image {a}).toFinset
⊢ ∀ (A : Finset α), card ↑(R.image ↑A) = #(A.biUnion r')

Tactic:
intro A

Goal state after:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
R : SetRel α β
inst✝ : (a : α) → Fintype ↑(R.image {a})
r' : α → Finset β := fun a ↦ (R.image {a}).toFinset
A : Finset α
⊢ card ↑(R.image ↑A) = #(A.biUnion r')
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : DecidableRel r
this : DecidableEq β
r' : α → Finset β := fun a ↦ {b | r a b}
⊢ ∀ (A : Finset α), {b | ∃ a ∈ A, r a b} = A.biUnion r'

Tactic:
intro A

Goal state after:
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : DecidableRel r
this : DecidableEq β
r' : α → Finset β := fun a ↦ {b | r a b}
A : Finset α
⊢ {b | ∃ a ∈ A, r a b} = A.biUnion r'
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: case smul
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : x ∈ dual p s
y✝ : M
t : R≥0
y : M
_hy : y ∈ Submodule.span R≥0 s
hy : 0 ≤ (p y) x
⊢ 0 ≤ (p (t • y)) x

Tactic:
| smul t y _hy hy =>

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E},
    s ∈ 𝓝 x → x = 0 → ∃ b, x ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s
hx : ¬x = 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb : 0 ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ -x +ᵥ s
⊢ x ∈ interior ((convexHull ℝ) (range ⇑(x +ᵥ b))) ∧ (convexHull ℝ) (range ⇑(x +ᵥ b)) ⊆ s

Tactic:
simpa [subset_vadd_set_iff, mem_vadd_set_iff_neg_vadd_mem, convexHull_vadd, interior_vadd,
      Pi.vadd_def, -vadd_eq_add, vadd_eq_add (a := -x), ← Set.vadd_set_range] using hb

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case refine_2
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
hcnorm : range ⇑c ⊆ closedBall 0 (cnorm + 1)
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
hdnorm : range ⇑d ⊆ closedBall 0 (ε / 2)
⊢ (convexHull ℝ) (range ⇑d) ⊆ s

Tactic:
calc
      convexHull ℝ (range d) ⊆ closedBall 0 (ε / 2) := convexHull_min hdnorm (convex_closedBall ..)
      _ ⊆ ball 0 ε := closedBall_subset_ball (by linarith)
      _ ⊆ s := hεs

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 B C : Set E
hC : IsExposed 𝕜 B C
hCA : C ⊆ A
⊢ IsExposed 𝕜 (A ∩ B) C

Tactic:
by
  rw [inter_comm]
  exact hC.inter_left hCA

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
g : E → ℝ
inst✝ : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : μ t ≠ 0
h₀' : μ tᶜ ≠ 0
hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  a • ⨍ (x : α) in t, (f x, (g ∘ f) x) ∂μ + b • ⨍ (x : α) in tᶜ, (f x, (g ∘ f) x) ∂μ =
    (⨍ (x : α), f x ∂μ, ⨍ (x : α), (g ∘ f) x ∂μ)
⊢ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ

Tactic:
average_pair hfi.integrableOn hgi.integrableOn,

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
g : E → ℝ
inst✝ : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : μ t ≠ 0
h₀' : μ tᶜ ≠ 0
hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  a • (⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, (g ∘ f) x ∂μ) + b • ⨍ (x : α) in tᶜ, (f x, (g ∘ f) x) ∂μ =
    (⨍ (x : α), f x ∂μ, ⨍ (x : α), (g ∘ f) x ∂μ)
⊢ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
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
g : E → ℝ
inst✝ : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : μ t ≠ 0
h₀' : μ tᶜ ≠ 0
hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  a • (⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, (g ∘ f) x ∂μ) + b • ⨍ (x : α) in tᶜ, (f x, (g ∘ f) x) ∂μ =
    (⨍ (x : α), f x ∂μ, ⨍ (x : α), (g ∘ f) x ∂μ)
⊢ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ

Tactic:
average_pair hfi.integrableOn hgi.integrableOn,

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
g : E → ℝ
inst✝ : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : μ t ≠ 0
h₀' : μ tᶜ ≠ 0
hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  a • (⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, (g ∘ f) x ∂μ) +
      b • (⨍ (x : α) in tᶜ, f x ∂μ, ⨍ (x : α) in tᶜ, (g ∘ f) x ∂μ) =
    (⨍ (x : α), f x ∂μ, ⨍ (x : α), (g ∘ f) x ∂μ)
⊢ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ