harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Combination.lean
theorem convexHull_basis_eq_stdSimplex :
    convexHull R (range fun i j : ι => if i = j then (1 : R) else 0) = stdSimplex R ι

Proof state:
case refine_1.intro
R : Type u_1
ι : Type u_5
inst✝¹ : LinearOrderedField R
inst✝ : Fintype ι
i : ι
⊢ (fun i j => if i = j then 1 else 0) i ∈ stdSimplex R ι

Tactic:
exact ite_eq_mem_stdSimplex R i

Result:
no goals

Proof state:
R : Type u_1
ι : Type u_5
inst✝¹ : LinearOrderedField R
inst✝ : Fintype ι
⊢ (convexHull R) (Set.range fun i j => if i = j then 1 else 0) = stdSimplex R ι

Tactic:
refine Subset.antisymm (convexHull_min ?_ (convex_stdSimplex R ι)) ?_

Result:
case refine_1
R : Type u_1
ι : Type u_5
inst✝¹ : LinearOrderedField R
inst✝ : Fintype ι
⊢ (Set.range fun i j => if i = j then 1 else 0) ⊆ stdSimplex R ι

case refine_2
R : Type u_1
ι : Type u_5
inst✝¹ : LinearOrderedField R
inst✝ : Fintype ι
⊢ stdSimplex R ι ⊆ (convexHull R) (Set.range fun i j => if i = j then 1 else 0)

Proof state:
case refine_1
R : Type u_1
ι : Type u_5
inst✝¹ : LinearOrderedField R
inst✝ : Fintype ι
⊢ (Set.range fun i j => if i = j then 1 else 0) ⊆ stdSimplex R ι

Tactic:
rintro _ ⟨i, rfl⟩

Result:
case refine_1.intro
R : Type u_1
ι : Type u_5
inst✝¹ : LinearOrderedField R
inst✝ : Fintype ι
i : ι
⊢ (fun i j => if i = j then 1 else 0) i ∈ stdSimplex R ι

Proof state:
case refine_2.intro
R : Type u_1
ι : Type u_5
inst✝¹ : LinearOrderedField R
inst✝ : Fintype ι
w : ι → R
hw₀ : ∀ (x : ι), 0 ≤ w x
hw₁ : ∑ x : ι, w x = 1
⊢ w ∈ (convexHull R) (Set.range fun i j => if i = j then 1 else 0)

Tactic:
rw [pi_eq_sum_univ w, ← Finset.univ.centerMass_eq_of_sum_1 _ hw₁]

Result:
case refine_2.intro
R : Type u_1
ι : Type u_5
inst✝¹ : LinearOrderedField R
inst✝ : Fintype ι
w : ι → R
hw₀ : ∀ (x : ι), 0 ≤ w x
hw₁ : ∑ x : ι, w x = 1
⊢ (Finset.univ.centerMass w fun i j => if i = j then 1 else 0) ∈
    (convexHull R) (Set.range fun i j => if i = j then 1 else 0)

Proof state:
case refine_2.intro
R : Type u_1
ι : Type u_5
inst✝¹ : LinearOrderedField R
inst✝ : Fintype ι
w : ι → R
hw₀ : ∀ (x : ι), 0 ≤ w x
hw₁ : ∑ x : ι, w x = 1
⊢ (Finset.univ.centerMass w fun i j => if i = j then 1 else 0) ∈
    (convexHull R) (Set.range fun i j => if i = j then 1 else 0)

Tactic:
exact Finset.univ.centerMass_mem_convexHull (fun i _ => hw₀ i) (hw₁.symm ▸ zero_lt_one)
  fun i _ => mem_range_self i

Result:
no goals

Proof state:
case refine_2
R : Type u_1
ι : Type u_5
inst✝¹ : LinearOrderedField R
inst✝ : Fintype ι
⊢ stdSimplex R ι ⊆ (convexHull R) (Set.range fun i j => if i = j then 1 else 0)

Tactic:
rintro w ⟨hw₀, hw₁⟩

Result:
case refine_2.intro
R : Type u_1
ι : Type u_5
inst✝¹ : LinearOrderedField R
inst✝ : Fintype ι
w : ι → R
hw₀ : ∀ (x : ι), 0 ≤ w x
hw₁ : ∑ x : ι, w x = 1
⊢ w ∈ (convexHull R) (Set.range fun i j => if i = j then 1 else 0)
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem takeDTR_go_eq : ∀ n l, takeDTR.go dflt n l acc = acc.toList ++ takeD n l dflt
  | 0, _ => by simp [takeDTR.go]
  | _+1, [] => by simp [takeDTR.go, replicate_succ]
  | _+1, _::l => by simp [takeDTR.go, takeDTR_go_eq _ l]

Proof state:
α✝ : Type u_1
dflt : α✝
acc : Array α✝
n✝ : Nat
⊢ takeDTR.go dflt (n✝ + 1) [] acc = acc.toList ++ takeD (n✝ + 1) [] dflt

Tactic:
simp [takeDTR.go, replicate_succ]

Result:
no goals

Proof state:
α✝ : Type u_1
dflt : α✝
acc : Array α✝
x✝ : List α✝
⊢ takeDTR.go dflt 0 x✝ acc = acc.toList ++ takeD 0 x✝ dflt

Tactic:
simp [takeDTR.go]

Result:
no goals

Proof state:
α✝ : Type u_1
dflt : α✝
acc : Array α✝
n✝ : Nat
head✝ : α✝
l : List α✝
⊢ takeDTR.go dflt (n✝ + 1) (head✝ :: l) acc = acc.toList ++ takeD (n✝ + 1) (head✝ :: l) dflt

Tactic:
simp [takeDTR.go, takeDTR_go_eq _ l]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem drop_sub_one {l : List α} {n : Nat} (h : 0 < n) :
    l.drop (n - 1) = l[n - 1]?.toList ++ l.drop n

Proof state:
α : Type u_1
l : List α
n : Nat
h : 0 < n
⊢ l[n - 1]?.toList ++ drop (n - 1 + 1) l = l[n - 1]?.toList ++ drop n l

Tactic:
congr

Result:
case e_a.e_a
α : Type u_1
l : List α
n : Nat
h : 0 < n
⊢ n - 1 + 1 = n

Proof state:
case e_a.e_a
α : Type u_1
l : List α
n : Nat
h : 0 < n
⊢ n - 1 + 1 = n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
h : 0 < n
⊢ drop (n - 1) l = l[n - 1]?.toList ++ drop n l

Tactic:
rw [drop_eq_getElem?_toList_append]

Result:
α : Type u_1
l : List α
n : Nat
h : 0 < n
⊢ l[n - 1]?.toList ++ drop (n - 1 + 1) l = l[n - 1]?.toList ++ drop n l
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_pow_sub_sub (x₀ : E') {m : ℕ} (h : 1 < m) :
    (fun x => ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x => x - x₀

Proof state:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
x₀ : E'
m : ℕ
h : 1 < m
⊢ (fun x => ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x => x - x₀

Tactic:
simpa only [isLittleO_norm_right, pow_one] using isLittleO_pow_sub_pow_sub x₀ h

Result:
no goals
-- Mathlib/RingTheory/Support.lean
lemma Module.support_subset_of_injective (hf : Function.Injective f) :
    Module.support R M ⊆ Module.support R N

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
x : PrimeSpectrum R
m : M
hm : ∀ r ∉ x.asIdeal, r • m ≠ 0
r : R
hr : r ∉ x.asIdeal
⊢ r • f m ≠ 0

Tactic:
simpa using hf.ne (hm r hr)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
⊢ ∀ (x : PrimeSpectrum R), (∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0) → ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0

Tactic:
rintro x ⟨m, hm⟩

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
x : PrimeSpectrum R
m : M
hm : ∀ r ∉ x.asIdeal, r • m ≠ 0
⊢ ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
⊢ support R M ⊆ support R N

Tactic:
simp_rw [Set.subset_def, mem_support_iff']

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
⊢ ∀ (x : PrimeSpectrum R), (∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0) → ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
x : PrimeSpectrum R
m : M
hm : ∀ r ∉ x.asIdeal, r • m ≠ 0
⊢ ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0

Tactic:
exact ⟨f m, fun r hr ↦ by simpa using hf.ne (hm r hr)⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_erase' (f : (∀ i, π i) → ℝ≥0∞) (hf : Measurable f) {i : δ}
    (hi : i ∈ s) :
    ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_(erase s i), (fun x ↦ ∫⁻ xᵢ, f (Function.update x i xᵢ) ∂μ i) ∂μ

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∈ s
⊢ ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s.erase i, fun x => ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i ∂μ

Tactic:
simpa [insert_erase hi] using lmarginal_insert' _ hf (not_mem_erase i s)

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
lemma sum_Icc_mu_right (a b : α) : ∑ x ∈ Icc a b, mu 𝕜 a x = if a = b then 1 else 0

Proof state:
case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0

Tactic:
by_cases hab : a ≤ b

Result:
case pos
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0

case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0

Proof state:
case pos
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0

Tactic:
simp [Icc_eq_cons_Ico hab, mu_eq_neg_sum_Ico_of_ne ‹_›]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0

Tactic:
exact sum_eq_zero fun x hx ↦ apply_eq_zero_of_not_le
  (fun hax ↦ hab <| hax.trans (mem_Icc.1 hx).2) _

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = if a = b then 1 else 0

Tactic:
split_ifs with hab

Result:
case pos
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a = b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 1

case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : ¬a = b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0

Proof state:
case pos
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a = b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 1

Tactic:
simp [hab]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem hasMFDerivAt_unique (h₀ : HasMFDerivAt I I' f x f₀') (h₁ : HasMFDerivAt I I' f x f₁') :
    f₀' = f₁'

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h₀ : HasMFDerivAt I I' f x f₀'
h₁ : HasMFDerivAt I I' f x f₁'
⊢ f₀' = f₁'

Tactic:
rw [← hasMFDerivWithinAt_univ] at h₀ h₁

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h₀ : HasMFDerivWithinAt I I' f univ x f₀'
h₁ : HasMFDerivWithinAt I I' f univ x f₁'
⊢ f₀' = f₁'

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h₀ : HasMFDerivWithinAt I I' f univ x f₀'
h₁ : HasMFDerivWithinAt I I' f univ x f₁'
⊢ f₀' = f₁'

Tactic:
exact (uniqueMDiffWithinAt_univ I).eq h₀ h₁

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem unit_leftAdjointUniq_hom_app
    {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :
    adj1.unit.app x ≫ G.map ((leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x

Tactic:
rw [← unit_leftAdjointUniq_hom adj1 adj2]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) =
    (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) =
    (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem denote_monomialToExpr (ctx : Context) (k : Nat) (v : Var) : (monomialToExpr k v).denote ctx = k * v.denote ctx

Proof state:
case pos
ctx : Context
k : Nat
v : Var
h✝ : ¬(v == fixedVar) = true
h : (k == 1) = true
⊢ Var.denote ctx v = k * Var.denote ctx v

Tactic:
simp [eq_of_beq h]

Result:
no goals

Proof state:
case pos
ctx : Context
k : Nat
v : Var
h : (v == fixedVar) = true
⊢ k = k * Var.denote ctx v

Tactic:
simp [eq_of_beq h, Var.denote]

Result:
no goals

Proof state:
case neg
ctx : Context
k : Nat
v : Var
h : ¬(v == fixedVar) = true
⊢ Expr.denote ctx (bif k == 1 then Expr.var v else Expr.mulL k (Expr.var v)) = k * Var.denote ctx v

Tactic:
by_cases h : k == 1 <;> simp [h, Expr.denote]

Result:
case pos
ctx : Context
k : Nat
v : Var
h✝ : ¬(v == fixedVar) = true
h : (k == 1) = true
⊢ Var.denote ctx v = k * Var.denote ctx v

Proof state:
ctx : Context
k : Nat
v : Var
⊢ Expr.denote ctx (bif v == fixedVar then Expr.num k else bif k == 1 then Expr.var v else Expr.mulL k (Expr.var v)) =
    k * Var.denote ctx v

Tactic:
by_cases h : v == fixedVar <;> simp [h, Expr.denote]

Result:
case pos
ctx : Context
k : Nat
v : Var
h : (v == fixedVar) = true
⊢ k = k * Var.denote ctx v

case neg
ctx : Context
k : Nat
v : Var
h : ¬(v == fixedVar) = true
⊢ Expr.denote ctx (bif k == 1 then Expr.var v else Expr.mulL k (Expr.var v)) = k * Var.denote ctx v

Proof state:
ctx : Context
k : Nat
v : Var
⊢ Expr.denote ctx (monomialToExpr k v) = k * Var.denote ctx v

Tactic:
simp [monomialToExpr]

Result:
ctx : Context
k : Nat
v : Var
⊢ Expr.denote ctx (bif v == fixedVar then Expr.num k else bif k == 1 then Expr.var v else Expr.mulL k (Expr.var v)) =
    k * Var.denote ctx v
-- Mathlib/Data/Set/Insert.lean
theorem diff_insert_of_not_mem {x : α} (h : x ∉ s) : s \ insert x t = s \ t

Proof state:
α : Type u
s t : Set α
x : α
h : x ∉ s
y : α
hy : y ∈ s \ t
⊢ y ∈ s \ insert x t

Tactic:
simp only [mem_diff, mem_insert_iff, not_or] at hy ⊢

Result:
α : Type u
s t : Set α
x : α
h : x ∉ s
y : α
hy : y ∈ s ∧ y ∉ t
⊢ y ∈ s ∧ ¬y = x ∧ y ∉ t

Proof state:
α : Type u
s t : Set α
x : α
h : x ∉ s
⊢ s \ insert x t = s \ t

Tactic:
refine Subset.antisymm (diff_subset_diff (refl _) (subset_insert ..)) fun y hy ↦ ?_

Result:
α : Type u
s t : Set α
x : α
h : x ∉ s
y : α
hy : y ∈ s \ t
⊢ y ∈ s \ insert x t

Proof state:
α : Type u
s t : Set α
x : α
h : x ∉ s
y : α
hy : y ∈ s ∧ y ∉ t
⊢ y ∈ s ∧ ¬y = x ∧ y ∉ t

Tactic:
exact ⟨hy.1, fun hxy ↦ h <| hxy ▸ hy.1, hy.2⟩

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
lemma mono_of_mono_f {K L : HomologicalComplex V c} (φ : K ⟶ L)
    (hφ : ∀ i, Mono (φ.f i)) : Mono φ where
  right_cancellation g h eq

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z✝ : HomologicalComplex V c
g h : Z✝ ⟶ K
eq : g ≫ φ = h ≫ φ
⊢ g = h

Tactic:
ext i

Result:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z✝ : HomologicalComplex V c
g h : Z✝ ⟶ K
eq : g ≫ φ = h ≫ φ
i : ι
⊢ g.f i = h.f i

Proof state:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z✝ : HomologicalComplex V c
g h : Z✝ ⟶ K
eq : g ≫ φ = h ≫ φ
i : ι
⊢ g.f i = h.f i

Tactic:
rw [← cancel_mono (φ.f i)]

Result:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z✝ : HomologicalComplex V c
g h : Z✝ ⟶ K
eq : g ≫ φ = h ≫ φ
i : ι
⊢ g.f i ≫ φ.f i = h.f i ≫ φ.f i

Proof state:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z✝ : HomologicalComplex V c
g h : Z✝ ⟶ K
eq : g ≫ φ = h ≫ φ
i : ι
⊢ g.f i ≫ φ.f i = h.f i ≫ φ.f i

Tactic:
exact congr_hom eq i

Result:
no goals
-- Mathlib/Analysis/Convex/Jensen.lean
theorem ConvexOn.le_sup_of_mem_convexHull {t : Finset E} (hf : ConvexOn 𝕜 s f) (hts : ↑t ⊆ s)
    (hx : x ∈ convexHull 𝕜 (t : Set E)) :
    f x ≤ t.sup' (coe_nonempty.1 <| convexHull_nonempty_iff.1 ⟨x, hx⟩) f

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset E
hf : ConvexOn 𝕜 s f
hts : ↑t ⊆ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w _root_.id ∈ (convexHull 𝕜) ↑t
⊢ f (t.centerMass w _root_.id) ≤ t.sup' ⋯ f

Tactic:
exact (hf.map_centerMass_le hw₀ (by positivity) hts).trans
  (centerMass_le_sup hw₀ <| by positivity)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset E
hf : ConvexOn 𝕜 s f
hts : ↑t ⊆ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w _root_.id ∈ (convexHull 𝕜) ↑t
⊢ 0 < ∑ i ∈ t, w i

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
x : E
t : Finset E
hf : ConvexOn 𝕜 s f
hts : ↑t ⊆ s
hx : x ∈ (convexHull 𝕜) ↑t
⊢ f x ≤ t.sup' ⋯ f

Tactic:
obtain ⟨w, hw₀, hw₁, rfl⟩ := mem_convexHull.1 hx

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset E
hf : ConvexOn 𝕜 s f
hts : ↑t ⊆ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w _root_.id ∈ (convexHull 𝕜) ↑t
⊢ f (t.centerMass w _root_.id) ≤ t.sup' ⋯ f
-- Mathlib/Data/ENNReal/Inv.lean
@[simp] lemma inv_mul_ne_top (a : ℝ≥0∞) : a⁻¹ * a ≠ ⊤

Proof state:
a : ℝ≥0∞
⊢ a⁻¹ * a ≠ ⊤

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/Probability/ConditionalProbability.lean
theorem cond_toMeasurable_eq :
    μ[|(toMeasurable μ s)] = μ[|s]

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
⊢ μ[|toMeasurable μ s] = μ[|s]

Tactic:
unfold cond

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
⊢ (μ (toMeasurable μ s))⁻¹ • μ.restrict (toMeasurable μ s) = (μ s)⁻¹ • μ.restrict s

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hnt : ¬μ s = ⊤
⊢ (μ (toMeasurable μ s))⁻¹ • μ.restrict (toMeasurable μ s) = (μ s)⁻¹ • μ.restrict s

Tactic:
simp [Measure.restrict_toMeasurable hnt]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
⊢ (μ (toMeasurable μ s))⁻¹ • μ.restrict (toMeasurable μ s) = (μ s)⁻¹ • μ.restrict s

Tactic:
by_cases hnt : μ s = ∞

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hnt : μ s = ⊤
⊢ (μ (toMeasurable μ s))⁻¹ • μ.restrict (toMeasurable μ s) = (μ s)⁻¹ • μ.restrict s

case neg
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hnt : ¬μ s = ⊤
⊢ (μ (toMeasurable μ s))⁻¹ • μ.restrict (toMeasurable μ s) = (μ s)⁻¹ • μ.restrict s

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hnt : μ s = ⊤
⊢ (μ (toMeasurable μ s))⁻¹ • μ.restrict (toMeasurable μ s) = (μ s)⁻¹ • μ.restrict s

Tactic:
simp [hnt]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem smul_ball {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) : c • ball x r = ball (c • x) (‖c‖ * r)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ y ∈ c • ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ hc]

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ ball (c⁻¹ • c • x) r ↔ y ∈ ball (c • x) (‖c‖ * r)

Tactic:
simp [← div_eq_inv_mul, div_lt_iff₀ (norm_pos_iff.2 hc), mul_comm _ r, dist_smul₀]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • ball x r = ball (c • x) (‖c‖ * r)

Tactic:
ext y

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ y ∈ c • ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)

Tactic:
conv_lhs => rw [← inv_smul_smul₀ hc x]

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ ball (c⁻¹ • c • x) r ↔ y ∈ ball (c • x) (‖c‖ * r)