harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Presentation.lean
lemma relation_mem_ker (i : P.rels) : P.relation i ∈ P.ker

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S
i : P.rels
⊢ P.relation i ∈ Set.range P.relation

Tactic:
use i

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S
i : P.rels
⊢ P.relation i ∈ Ideal.span (Set.range P.relation)

Tactic:
apply Ideal.subset_span

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S
i : P.rels
⊢ P.relation i ∈ Set.range P.relation

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S
i : P.rels
⊢ P.relation i ∈ P.ker

Tactic:
rw [← P.span_range_relation_eq_ker]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Presentation R S
i : P.rels
⊢ P.relation i ∈ Ideal.span (Set.range P.relation)
-- Mathlib/Order/Minimal.lean
theorem minimal_mem_image_monotone_iff (ha : a ∈ s)
    (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) :
    Minimal (· ∈ f '' s) (f a) ↔ Minimal (· ∈ s) a

Proof state:
α : Type u_1
a : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun x => x ∈ f '' s) (f a)
y : α
hys : (fun x => x ∈ s) y
⊢ y ≤ a → a ≤ y

Tactic:
rw [← hf ha hys, ← hf hys ha]

Result:
α : Type u_1
a : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun x => x ∈ f '' s) (f a)
y : α
hys : (fun x => x ∈ s) y
⊢ f y ≤ f a → f a ≤ f y

Proof state:
α : Type u_1
a : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
⊢ Minimal (fun x => x ∈ f '' s) (f a) ↔ Minimal (fun x => x ∈ s) a

Tactic:
refine ⟨fun h ↦ ⟨ha, fun y hys ↦ ?_⟩, minimal_mem_image_monotone hf⟩

Result:
α : Type u_1
a : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun x => x ∈ f '' s) (f a)
y : α
hys : (fun x => x ∈ s) y
⊢ y ≤ a → a ≤ y

Proof state:
α : Type u_1
a : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun x => x ∈ f '' s) (f a)
y : α
hys : (fun x => x ∈ s) y
⊢ f y ≤ f a → f a ≤ f y

Tactic:
exact h.le_of_le (mem_image_of_mem f hys)

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem Cospherical.subset {ps₁ ps₂ : Set P} (hs : ps₁ ⊆ ps₂) (hc : Cospherical ps₂) :
    Cospherical ps₁

Proof state:
P : Type u_2
inst✝ : MetricSpace P
ps₁ ps₂ : Set P
hs : ps₁ ⊆ ps₂
hc : Cospherical ps₂
⊢ Cospherical ps₁

Tactic:
rcases hc with ⟨c, r, hcr⟩

Result:
case intro.intro
P : Type u_2
inst✝ : MetricSpace P
ps₁ ps₂ : Set P
hs : ps₁ ⊆ ps₂
c : P
r : ℝ
hcr : ∀ p ∈ ps₂, dist p c = r
⊢ Cospherical ps₁

Proof state:
case intro.intro
P : Type u_2
inst✝ : MetricSpace P
ps₁ ps₂ : Set P
hs : ps₁ ⊆ ps₂
c : P
r : ℝ
hcr : ∀ p ∈ ps₂, dist p c = r
⊢ Cospherical ps₁

Tactic:
exact ⟨c, r, fun p hp => hcr p (hs hp)⟩

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
lemma dens_inter_add_dens_union (s t : Finset α) :
    dens (s ∩ t) + dens (s ∪ t) = dens s + dens t

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∩ t).dens + (s ∪ t).dens = s.dens + t.dens

Tactic:
rw [add_comm, dens_union_add_dens_inter]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FinallySmall.lean
theorem finallySmall_iff_exists_small_weakly_terminal_set [IsFilteredOrEmpty J] :
    FinallySmall.{v} J ↔ ∃ (s : Set J) (_ : Small.{v} s), ∀ i, ∃ j ∈ s, Nonempty (i ⟶ j)

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFilteredOrEmpty J
⊢ FinallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)

Tactic:
refine ⟨fun _ => FinallySmall.exists_small_weakly_terminal_set _, fun h => ?_⟩

Result:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFilteredOrEmpty J
h : ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
⊢ FinallySmall J

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFilteredOrEmpty J
h : ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
⊢ FinallySmall J

Tactic:
rcases h with ⟨s, hs, hs'⟩

Result:
case intro.intro
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFilteredOrEmpty J
s : Set J
hs : Small.{v, u} ↑s
hs' : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
⊢ FinallySmall J

Proof state:
case intro.intro
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFilteredOrEmpty J
s : Set J
hs : Small.{v, u} ↑s
hs' : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
⊢ FinallySmall J

Tactic:
exact finallySmall_of_small_weakly_terminal_set s hs'

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean
/-- A zero functor preserves limits. -/
lemma preservesLimitsOfShape_of_isZero : PreservesLimitsOfShape J G where
  preservesLimit {K} := ⟨fun _ => ⟨by
    rw [Functor.isZero_iff] at hG
    exact IsLimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)⟩⟩

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : ∀ (X : C), IsZero (G.obj X)
J : Type u_1
inst✝ : Category.{u_2, u_1} J
K : J ⥤ C
c✝ : Cone K
x✝ : IsLimit c✝
⊢ IsLimit (G.mapCone c✝)

Tactic:
exact IsLimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : IsZero G
J : Type u_1
inst✝ : Category.{u_2, u_1} J
K : J ⥤ C
c✝ : Cone K
x✝ : IsLimit c✝
⊢ IsLimit (G.mapCone c✝)

Tactic:
rw [Functor.isZero_iff] at hG

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : ∀ (X : C), IsZero (G.obj X)
J : Type u_1
inst✝ : Category.{u_2, u_1} J
K : J ⥤ C
c✝ : Cone K
x✝ : IsLimit c✝
⊢ IsLimit (G.mapCone c✝)
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
theorem Sigma.ι_desc {β : Type w} {f : β → C} [HasCoproduct f] {P : C} (p : ∀ b, f b ⟶ P) (b : β) :
    Sigma.ι f b ≫ Sigma.desc p = p b

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
β : Type w
f : β → C
inst✝ : HasCoproduct f
P : C
p : (b : β) → f b ⟶ P
b : β
⊢ ι f b ≫ desc p = p b

Tactic:
simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_assoc (s t u : Set E) :
    convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u)

Tactic:
refine (convexJoin_assoc_aux _ _ _).antisymm ?_

Result:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) ⊆ convexJoin 𝕜 (convexJoin 𝕜 s t) u

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 u t) s ⊆ convexJoin 𝕜 u (convexJoin 𝕜 t s)

Tactic:
exact convexJoin_assoc_aux _ _ _

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) ⊆ convexJoin 𝕜 (convexJoin 𝕜 s t) u

Tactic:
simp_rw [convexJoin_comm s, convexJoin_comm _ u]

Result:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 u t) s ⊆ convexJoin 𝕜 u (convexJoin 𝕜 t s)
-- Mathlib/Analysis/Polynomial/CauchyBound.lean
@[simp]
lemma cauchyBound_smul {x : K} (hx : x ≠ 0) (p : K[X]) : cauchyBound (x • p) = cauchyBound p

Proof state:
K : Type u_1
inst✝ : NormedDivisionRing K
x : K
hx : x ≠ 0
p : K[X]
⊢ (x • p).cauchyBound = p.cauchyBound

Tactic:
simp only [cauchyBound, (isRegular_of_ne_zero hx).left.isSMulRegular,
  natDegree_smul_of_smul_regular, coeff_smul, smul_eq_mul, nnnorm_mul, ← mul_finset_sup,
  leadingCoeff_smul_of_smul_regular, add_left_inj]

Result:
K : Type u_1
inst✝ : NormedDivisionRing K
x : K
hx : x ≠ 0
p : K[X]
⊢ (‖x‖₊ * (range p.natDegree).sup fun a => ‖p.coeff a‖₊) / (‖x‖₊ * ‖p.leadingCoeff‖₊) =
    ((range p.natDegree).sup fun a => ‖p.coeff a‖₊) / ‖p.leadingCoeff‖₊

Proof state:
case hc
K : Type u_1
inst✝ : NormedDivisionRing K
x : K
hx : x ≠ 0
p : K[X]
⊢ ‖x‖₊ ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
K : Type u_1
inst✝ : NormedDivisionRing K
x : K
hx : x ≠ 0
p : K[X]
⊢ (‖x‖₊ * (range p.natDegree).sup fun a => ‖p.coeff a‖₊) / (‖x‖₊ * ‖p.leadingCoeff‖₊) =
    ((range p.natDegree).sup fun a => ‖p.coeff a‖₊) / ‖p.leadingCoeff‖₊

Tactic:
apply mul_div_mul_left

Result:
case hc
K : Type u_1
inst✝ : NormedDivisionRing K
x : K
hx : x ≠ 0
p : K[X]
⊢ ‖x‖₊ ≠ 0
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedSup_union (hs : a ∈ lowerClosure s) (ht : a ∈ lowerClosure t) :
    truncatedSup (s ∪ t) a = truncatedSup s a ⊔ truncatedSup t a

Proof state:
α : Type u_1
inst✝³ : SemilatticeSup α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ (s ∪ t).truncatedSup a = s.truncatedSup a ⊔ t.truncatedSup a

Tactic:
simpa only [truncatedSup_of_mem, hs, ht, lower_aux.2 (Or.inl hs), filter_union] using
  sup'_union _ _ _

Result:
no goals
-- Mathlib/MeasureTheory/Integral/PeakFunction.lean
theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn
    [MetrizableSpace α] [IsLocallyFiniteMeasure μ] [IsOpenPosMeasure μ] (hs : IsCompact s)
    {c : α → ℝ} (hc : ContinuousOn c s) (h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀)
    (hnc : ∀ x ∈ s, 0 ≤ c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ ∈ closure (interior s))
    (hmg : ContinuousOn g s) :
    Tendsto (fun n : ℕ => (∫ x in s, c x ^ n ∂μ)⁻¹ • ∫ x in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀)) :=
  haveI : x₀ ∈ s

Proof state:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝³ : CompleteSpace E
inst✝² : MetrizableSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ closure (interior s)
hmg : ContinuousOn g s
⊢ x₀ ∈ closure s

Tactic:
exact closure_mono interior_subset h₀

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝³ : CompleteSpace E
inst✝² : MetrizableSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ closure (interior s)
hmg : ContinuousOn g s
⊢ x₀ ∈ s

Tactic:
rw [← hs.isClosed.closure_eq]

Result:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝³ : CompleteSpace E
inst✝² : MetrizableSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ closure (interior s)
hmg : ContinuousOn g s
⊢ x₀ ∈ closure s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem lt_add_of_pos_left (h : 0 < k) : n < k + n

Proof state:
k n : Nat
h : 0 < k
⊢ n < k + n

Tactic:
rw [Nat.add_comm]

Result:
k n : Nat
h : 0 < k
⊢ n < n + k

Proof state:
k n : Nat
h : 0 < k
⊢ n < n + k

Tactic:
exact Nat.add_lt_add_left h n

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- The q-ary entropy function is continuous everywhere.
This is due to definition of `Real.log` for negative numbers. -/
@[fun_prop] lemma qaryEntropy_continuous : Continuous (qaryEntropy q)

Proof state:
q : ℕ
⊢ Continuous fun p => p * log ↑(↑q - 1) + binEntropy p

Tactic:
fun_prop

Result:
no goals

Proof state:
q : ℕ
⊢ Continuous (qaryEntropy q)

Tactic:
unfold qaryEntropy

Result:
q : ℕ
⊢ Continuous fun p => p * log ↑(↑q - 1) + binEntropy p
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem singleton_eq_pair_iff {x y z : ZFSet} : ({x} : ZFSet) = {y, z} ↔ x = y ∧ x = z

Proof state:
x y z : ZFSet.{u_1}
⊢ y = x ∧ z = x ↔ x = y ∧ x = z

Tactic:
simp_rw [eq_comm]

Result:
no goals

Proof state:
x y z : ZFSet.{u_1}
⊢ {x} = {y, z} ↔ x = y ∧ x = z

Tactic:
rw [eq_comm, pair_eq_singleton_iff]

Result:
x y z : ZFSet.{u_1}
⊢ y = x ∧ z = x ↔ x = y ∧ x = z
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem ae_measure_lt_top {s : Set (α × β)} (hs : MeasurableSet s) (h2s : (μ.prod ν) s ≠ ∞) :
    ∀ᵐ x ∂μ, ν (Prod.mk x ⁻¹' s) < ∞

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) < ⊤

Tactic:
exact ae_lt_top (measurable_measure_prod_mk_left hs) h2s

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) < ⊤

Tactic:
rw [prod_apply hs] at h2s

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) < ⊤
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem measurable_map (f : α → β) (hf : Measurable f) :
    Measurable fun μ : Measure α => map f μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ Measurable fun μ => map f μ

Tactic:
refine measurable_of_measurable_coe _ fun s hs => ?_

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => (map f b) s

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => b (f ⁻¹' s)

Tactic:
exact measurable_coe (hf hs)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => (map f b) s

Tactic:
simp_rw [map_apply hf hs]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => b (f ⁻¹' s)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem modify_eq_alter [BEq α] [EquivBEq α] {a : α} {f : β → β} {l : AssocList α (fun _ => β)} :
    modify a f l = alter a (·.map f) l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
f : β → β
l : AssocList α fun x => β
⊢ modify a f l = alter a (fun x => Option.map f x) l

Tactic:
induction l

Result:
case nil
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
f : β → β
⊢ modify a f nil = alter a (fun x => Option.map f x) nil

case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
f : β → β
key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
tail_ih✝ : modify a f tail✝ = alter a (fun x => Option.map f x) tail✝
⊢ modify a f (cons key✝ value✝ tail✝) = alter a (fun x => Option.map f x) (cons key✝ value✝ tail✝)

Proof state:
case nil
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
f : β → β
⊢ modify a f nil = alter a (fun x => Option.map f x) nil

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
f : β → β
key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
ih : modify a f tail✝ = alter a (fun x => Option.map f x) tail✝
⊢ modify a f (cons key✝ value✝ tail✝) = alter a (fun x => Option.map f x) (cons key✝ value✝ tail✝)

Tactic:
simp only [modify, beq_iff_eq, alter, Option.map_some', ih]

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
f : β → β
key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
tail_ih✝ : modify a f tail✝ = alter a (fun x => Option.map f x) tail✝
⊢ modify a f (cons key✝ value✝ tail✝) = alter a (fun x => Option.map f x) (cons key✝ value✝ tail✝)

Tactic:
next ih => simp only [modify, beq_iff_eq, alter, Option.map_some', ih]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem List.nnnorm_prod_le [NormOneClass α] (l : List α) : ‖l.prod‖₊ ≤ (l.map nnnorm).prod :=
  l.norm_prod_le.trans_eq <| by simp [NNReal.coe_list_prod, List.map_map]

Proof state:
α : Type u_2
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
l : List α
⊢ (map norm l).prod = (fun a => ↑a) (map nnnorm l).prod

Tactic:
simp [NNReal.coe_list_prod, List.map_map]

Result:
no goals
-- Mathlib/Analysis/Convex/Hull.lean
theorem convexHull_empty_iff : convexHull 𝕜 s = ∅ ↔ s = ∅

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s = ∅ ↔ s = ∅

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s = ∅ → s = ∅

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ s = ∅ → (convexHull 𝕜) s = ∅

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s = ∅ → s = ∅

Tactic:
intro h

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : (convexHull 𝕜) s = ∅
⊢ s = ∅

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
⊢ (convexHull 𝕜) ∅ = ∅

Tactic:
exact convexHull_empty

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : (convexHull 𝕜) s = ∅
⊢ s ⊆ (convexHull 𝕜) s

Tactic:
exact subset_convexHull 𝕜 _

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : (convexHull 𝕜) s = ∅
⊢ s = ∅

Tactic:
rw [← Set.subset_empty_iff, ← h]

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : (convexHull 𝕜) s = ∅
⊢ s ⊆ (convexHull 𝕜) s

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ s = ∅ → (convexHull 𝕜) s = ∅

Tactic:
rintro rfl

Result:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
⊢ (convexHull 𝕜) ∅ = ∅
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} :
    (zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : Nat
l₂ : Vector β n✝
f : α → β → γ
i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n✝
⊢ (zipWith f { toArray := toArray✝, size_toArray := size_toArray✝ } l₂)[i]? =
    (Option.map f { toArray := toArray✝, size_toArray := size_toArray✝ }[i]?).bind fun g => Option.map g l₂[i]?

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : Nat
f : α → β → γ
i : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n✝
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n✝
⊢ (zipWith f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }
        { toArray := toArray✝, size_toArray := size_toArray✝ })[i]? =
    (Option.map f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }[i]?).bind fun g =>
      Option.map g { toArray := toArray✝, size_toArray := size_toArray✝ }[i]?

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : Nat
l₁ : Vector α n✝
l₂ : Vector β n✝
f : α → β → γ
i : Nat
⊢ (zipWith f l₁ l₂)[i]? = (Option.map f l₁[i]?).bind fun g => Option.map g l₂[i]?

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : Nat
l₂ : Vector β n✝
f : α → β → γ
i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n✝
⊢ (zipWith f { toArray := toArray✝, size_toArray := size_toArray✝ } l₂)[i]? =
    (Option.map f { toArray := toArray✝, size_toArray := size_toArray✝ }[i]?).bind fun g => Option.map g l₂[i]?

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : Nat
f : α → β → γ
i : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n✝
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n✝
⊢ (zipWith f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }
        { toArray := toArray✝, size_toArray := size_toArray✝ })[i]? =
    (Option.map f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }[i]?).bind fun g =>
      Option.map g { toArray := toArray✝, size_toArray := size_toArray✝ }[i]?

Tactic:
simp [Array.getElem?_zipWith']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVec.lean
theorem get_in_bound (s : RefVec aig len) (idx : Nat) (alt : Ref aig) (hidx : idx < len) :
    s.getD idx alt = s.get idx hidx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
alt : aig.Ref
hidx : idx < len
⊢ (if hidx : idx < len then s.get idx hidx else alt) = s.get idx hidx

Tactic:
simp [hidx]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
alt : aig.Ref
hidx : idx < len
⊢ s.getD idx alt = s.get idx hidx

Tactic:
unfold getD

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
alt : aig.Ref
hidx : idx < len
⊢ (if hidx : idx < len then s.get idx hidx else alt) = s.get idx hidx