mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (Function.support fun z ↦ ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)) ⊆ ↑hs.toFinset

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
⊢ (Function.support fun z ↦ ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹)) ⊆ ↑hs.toFinset

Tactic:
· intro z
      aesop

Goal state after:
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
⊢ (Function.support fun z ↦ ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹)) ⊆ ↑hs.toFinset
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
α : Type u_3
f : α → 𝕜 → E
r : ℝ
hr : 1 ≤ r
a : α
s : Finset α
ha : a ∉ s
hs : (∀ a ∈ s, Meromorphic (f a)) → logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
h₁f : ∀ a_1 ∈ insert a s, Meromorphic (f a_1)
⊢ logCounting (∑ a ∈ insert a s, f a) ⊤ r ≤ (∑ a ∈ insert a s, logCounting (f a) ⊤) r

Tactic:
Finset.sum_insert ha,

Goal state after:
case insert
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
α : Type u_3
f : α → 𝕜 → E
r : ℝ
hr : 1 ≤ r
a : α
s : Finset α
ha : a ∉ s
hs : (∀ a ∈ s, Meromorphic (f a)) → logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
h₁f : ∀ a_1 ∈ insert a s, Meromorphic (f a_1)
⊢ logCounting (f a + ∑ x ∈ s, f x) ⊤ r ≤ (∑ a ∈ insert a s, logCounting (f a) ⊤) r
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.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✝ : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
h : (Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail) ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
⊢ (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]

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

Tactic:
· rcases h with ⟨⟨hp, ht⟩, hpne⟩
      refine ⟨⟨?_, ?_⟩, ?_⟩
      · clear ih
        induction tail with
        | nil => simp
        | cons head2 tail ih' =>
          rw [pairwise_cons] at hp hpne hpne ⊢
          refine ⟨fun a ha ↦ ⟨hp.1 a ha, ?_⟩, ?_⟩
          · refine ⟨(hpne.1 head2 ?_).symm, hpne.2.1 a ha⟩
            simp
          · rw [wbtw_cons] at ht
            grind [List.pairwise_iff_forall_sublist]
      · rw [pairwise_cons] at hpne
        exact (ih.1 ⟨ht, hpne.2⟩).1
      · grind

Goal state after:
case cons.refine_2
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
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
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
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
⊢ n + 1 - 1 = n

Tactic:
Nat.add_succ_sub_one,

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
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
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
⊢ n + 0 = n
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 : P
⊢ (fun a ↦ Function.const R x a) '' Set.Icc 0 1 = {x}

Tactic:
Function.const,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x : P
⊢ (fun a ↦ x) '' Set.Icc 0 1 = {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
x y z : P
⊢ Wbtw R x y z ↔ Wbtw R z y x

Tactic:
rw [Wbtw, Wbtw, affineSegment_comm]

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

Goal state before:
pp: case neg.cons
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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : Pairwise (Wbtw R head) (head2 :: tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
hl'' : map (⇑(lineMap ((head2 :: tail).head ht) ((head2 :: tail).getLast ht))) l'' = head2 :: tail
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head ((head2 :: tail).getLast ht))) l' = head :: head2 :: tail

Tactic:
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.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
f : P →ᵃ[R] P'
s : AffineSubspace R P
hf : InjOn ⇑f ↑s
hx : x ∈ s
hy : y ∈ s
hz : z ∈ s
⊢ Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z

Tactic:
refine ⟨fun h => ?_, fun h => h.map _⟩
  rwa [Wbtw, ← affineSegment_image, hf.mem_image_iff
    ((affineSegment_subset_affineSpan R x z).trans (affineSpan_le.2 (Set.pair_subset hx hz))) hy]
    at h

Goal state after:
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
f : P ≃ᵃ[R] P'
⊢ Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z

Tactic:
by
  have : Function.Injective f.toAffineMap := f.injective
  -- `refine` or `exact` are very slow, `apply` is fast. Please check before golfing.
  apply this.sbtw_map_iff

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
⊢ ∀ i ∈ ↑H, IsClosed {u | (ConcreteCategory.hom (F.map i.snd.snd.snd.snd)) (u i.fst) = u i.snd.fst}

Tactic:
intro f _

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
f : FiniteDiagramArrow G
a✝ : f ∈ ↑H
⊢ IsClosed {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: case some
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
fj : m
h : f.symm j = some fj
⊢ (∑ j_1, M i j_1 * if j ∈ f j_1 then 1 else 0) = Option.rec 0 (fun val ↦ M i val) (some fj)

Tactic:
· 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: k : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
⊢ (single a b₁).toMatrix * (single b₂ c).toMatrix = 0

Tactic:
rw [← toMatrix_trans, single_trans_single_of_ne hb, toMatrix_bot]

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

Goal state before:
pp: k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁵ : Fintype n
inst✝⁴ : Fintype k
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : Semiring α
a : m
b : n
c : k
M : Matrix k l α
⊢ (single a b).toMatrix * ((single b c).toMatrix * M) = (single a c).toMatrix * M

Tactic:
by
  rw [← Matrix.mul_assoc, single_mul_single]

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✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
ι : Type u_6
i j k : ι
h : Function.Injective ![i, j, k]
T : ι → P
hT : AffineIndependent R T
⊢ ¬Wbtw R (T i) (T j) (T k)

Tactic:
replace hT := hT.comp_embedding ⟨_, h⟩

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
ι : Type u_6
i j k : ι
h : Function.Injective ![i, j, k]
T : ι → P
hT : AffineIndependent R (T ∘ ⇑{ toFun := ![i, j, k], inj' := h })
⊢ ¬Wbtw R (T i) (T j) (T k)
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
z : H ⊗[R] G
⊢ (∃ x,
      (∀ φ ∈ dual (Dual.eval R G) ↑C₁, ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) x) ∧
        ↑(TensorProduct.comm R G H) x = z) →
    ∀ φ ∈ dual (Dual.eval R H) ↑C₂, ∀ ψ ∈ dual (Dual.eval R G) ↑C₁, 0 ≤ ((dualDistrib R H G) (φ ⊗ₜ[R] ψ)) z

Tactic:
rintro ⟨w, hw, rfl⟩ ψ hψ φ hφ

Goal state after:
case refine_1
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw : ∀ φ ∈ dual (Dual.eval R G) ↑C₁, ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) w
ψ : Dual R H
hψ : ψ ∈ dual (Dual.eval R H) ↑C₂
φ : Dual R G
hφ : φ ∈ dual (Dual.eval R G) ↑C₁
⊢ 0 ≤ ((dualDistrib R H G) (ψ ⊗ₜ[R] φ)) (↑(TensorProduct.comm R G H) w)
Module: Mathlib.Analysis.Convex.Cone.TensorProduct

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
⊢ C₁.minTensorProduct ↑C₂ = C₁.maxTensorProduct ↑C₂

Tactic:
apply le_antisymm (minTensorProduct_le_maxTensorProduct C₁ C₂.toPointedCone)

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
⊢ C₁.maxTensorProduct ↑C₂ ≤ C₁.minTensorProduct ↑C₂
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : gauge t x ≠ 0
⊢ gauge t (gaugeRescale s t x) = gauge s x

Tactic:
by
  rw [gaugeRescale, gauge_smul_of_nonneg (div_nonneg (gauge_nonneg _) (gauge_nonneg _)),
    smul_eq_mul, div_mul_cancel₀ _ hx]

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

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

Tactic:
rcases (hf.and hfg).exists with ⟨x₀, h₀⟩

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
s : Set P
t : Set Q
e : ↥(affineSpan 𝕜 (s ×ˢ t)) ≃ₜ ↥(affineSpan 𝕜 s) × ↥(affineSpan 𝕜 t) :=
  (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑(affineSpan 𝕜 s) ↑(affineSpan 𝕜 t))
this : Subtype.val ∘ ⇑e.symm = fun p ↦ (↑p.1, ↑p.2)
h : Subtype.val ⁻¹' s ×ˢ t = ⇑e ⁻¹' (Subtype.val ⁻¹' s) ×ˢ (Subtype.val ⁻¹' t)
⊢ Subtype.val ∘ ⇑e.symm '' interior (Subtype.val ⁻¹' s) ×ˢ interior (Subtype.val ⁻¹' t) =
    (Subtype.val '' interior (Subtype.val ⁻¹' s)) ×ˢ (Subtype.val '' interior (Subtype.val ⁻¹' t))

Tactic:
prod_image_image_eq,

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
s : Set P
t : Set Q
e : ↥(affineSpan 𝕜 (s ×ˢ t)) ≃ₜ ↥(affineSpan 𝕜 s) × ↥(affineSpan 𝕜 t) :=
  (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑(affineSpan 𝕜 s) ↑(affineSpan 𝕜 t))
this : Subtype.val ∘ ⇑e.symm = fun p ↦ (↑p.1, ↑p.2)
h : Subtype.val ⁻¹' s ×ˢ t = ⇑e ⁻¹' (Subtype.val ⁻¹' s) ×ˢ (Subtype.val ⁻¹' t)
⊢ Subtype.val ∘ ⇑e.symm '' interior (Subtype.val ⁻¹' s) ×ˢ interior (Subtype.val ⁻¹' t) =
    (fun p ↦ (↑p.1, ↑p.2)) '' interior (Subtype.val ⁻¹' s) ×ˢ interior (Subtype.val ⁻¹' t)
Module: Mathlib.Analysis.Convex.Measure

Goal state before:
pp: case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s ≠ ⊤
⊢ μ (frontier s) = 0

Tactic:
refine measure_mono_null ?_ (addHaar_affineSubspace _ _ hspan)
    exact frontier_subset_closure.trans
      (closure_minimal (subset_affineSpan _ _) (affineSpan ℝ s).closed_of_finiteDimensional)

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : μ (interior s) ≠ ∞
this : μ (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ μ (interior s)
⊢ μ (frontier s) = 0

Tactic:
rwa [frontier, measure_sdiff interior_subset_closure isOpen_interior.nullMeasurableSet hb,
      tsub_eq_zero_iff_le]

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

Goal state before:
pp: case e_a
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
⊢ ((Finsupp.mapDomain convexCombination f.weights).sum fun x w ↦ w • (x -ᵥ b)) =
    ∑ x ∈ (f.weights.sum fun d r ↦ r • d.weights).support, (f.weights.sum fun d r ↦ r • d.weights) x • (x -ᵥ b)

Tactic:
rw [Finsupp.sum_mapDomain_index (fun _ => by simp) (fun _ _ _ => by simp [add_smul])]

Goal state after:
case e_a
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
⊢ (f.weights.sum fun a m ↦ m • (convexCombination a -ᵥ b)) =
    ∑ x ∈ (f.weights.sum fun d r ↦ r • d.weights).support, (f.weights.sum fun d r ↦ r • d.weights) x • (x -ᵥ b)
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: case e_a
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
⊢ ∑ d ∈ f.weights.support, f.weights d • ∑ x ∈ d.weights.support, d.weights x • (x -ᵥ b) =
    ∑ x ∈ (∑ x ∈ f.weights.support, f.weights x • x.weights).support,
      (∑ x ∈ f.weights.support, f.weights x • x.weights) x • (x -ᵥ b)

Tactic:
Finset.smul_sum,

Goal state after:
case e_a
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
⊢ ∑ x ∈ f.weights.support, ∑ x_1 ∈ x.weights.support, f.weights x • x.weights x_1 • (x_1 -ᵥ b) =
    ∑ x ∈ (∑ x ∈ f.weights.support, f.weights x • x.weights).support,
      (∑ x ∈ f.weights.support, f.weights x • x.weights) x • (x -ᵥ b)
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
ι : Sort u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
s : ι → Set X
hs : ∀ (i : ι), IsStarConvexSet R x (s i)
⊢ IsStarConvexSet R x (⋂ i, s i)

Tactic:
by simp +contextual [IsStarConvexSet, hs _ _]

Goal state after: