harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
lemma rpow_abs_le_mul_max_exp (x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : t ≠ 0) :
    |x| ^ p ≤ (p / |t|) ^ p * max (exp (t * x)) (exp (- t * x))

Proof state:
case inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / -t) ^ p * (rexp (-t * x) ⊔ rexp (t * x))

Tactic:
convert rpow_abs_le_mul_max_exp_of_pos x hp (t := -t) (by simp [ht_neg])

Result:
case h.e'_4.h.e'_6.h.e'_4.h.e'_1.h.e'_5
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ t = - -t

Proof state:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ 0 < -t

Tactic:
simp [ht_neg]

Result:
no goals

Proof state:
case inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_pos : t > 0
⊢ |x| ^ p ≤ (p / t) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

Tactic:
exact rpow_abs_le_mul_max_exp_of_pos x hp ht_pos

Result:
no goals

Proof state:
case inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

Tactic:
rw [abs_of_nonpos ht_neg.le, sup_comm]

Result:
case inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / -t) ^ p * (rexp (-t * x) ⊔ rexp (t * x))

Proof state:
case h.e'_4.h.e'_6.h.e'_4.h.e'_1.h.e'_5
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ t = - -t

Tactic:
simp

Result:
no goals

Proof state:
case inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_pos : t > 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

Tactic:
rw [abs_of_nonneg ht_pos.le]

Result:
case inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_pos : t > 0
⊢ |x| ^ p ≤ (p / t) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

Proof state:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

Tactic:
rcases lt_or_gt_of_ne ht with ht_neg | ht_pos

Result:
case inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

case inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_pos : t > 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * (rexp (t * x) ⊔ rexp (-t * x))
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem fromCoset_ne_of_nin_range {b : B} (hb : b ∉ f.hom.range) :
    fromCoset ⟨b • ↑f.hom.range, b, rfl⟩ ≠ fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩

Proof state:
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b⁻¹ ∈ (Hom.hom f).range
⊢ False

Tactic:
exact hb (inv_inv b ▸ Subgroup.inv_mem _ r)

Result:
no goals

Proof state:
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b • ↑(Hom.hom f).range = 1 • ↑(Hom.hom f).range
⊢ False

Tactic:
rw [leftCoset_eq_iff, mul_one] at r

Result:
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b⁻¹ ∈ (Hom.hom f).range
⊢ False

Proof state:
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b • ↑(Hom.hom f).range = ↑(Hom.hom f).range
⊢ False

Tactic:
nth_rw 2 [show (f.hom.range : Set B) = (1 : B) • f.hom.range from (one_leftCoset _).symm] at r

Result:
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b • ↑(Hom.hom f).range = 1 • ↑(Hom.hom f).range
⊢ False

Proof state:
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
⊢ False

Tactic:
simp only [fromCoset.injEq, Subtype.mk.injEq] at r

Result:
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b • ↑(Hom.hom f).range = ↑(Hom.hom f).range
⊢ False

Proof state:
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
⊢ fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ ≠ fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
intro r

Result:
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
⊢ False
-- Mathlib/Data/Complex/Norm.lean
theorem lim_eq_lim_im_add_lim_re (f : CauSeq ℂ (‖·‖)) :
    lim f = ↑(lim (cauSeqRe f)) + ↑(lim (cauSeqIm f)) * I :=
  lim_eq_of_equiv_const <|
    letI : IsAbsoluteValue (‖·‖ : ℂ → ℝ) := inferInstance
    calc
      f ≈ _ := equiv_limAux f
      _ = CauSeq.const (‖·‖) (↑(lim (cauSeqRe f)) + ↑(lim (cauSeqIm f)) * I) :=
        CauSeq.ext fun _ ↦
          Complex.ext (by simp [limAux, cauSeqRe, ofReal]) (by simp [limAux, cauSeqIm, ofReal])

Proof state:
f : CauSeq ℂ fun x => ‖x‖
this : IsAbsoluteValue fun x => ‖x‖ := inferInstance
x✝ : ℕ
⊢ (↑(const (fun x => ‖x‖) (limAux f)) x✝).re =
    (↑(const (fun x => ‖x‖) (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I)) x✝).re

Tactic:
simp [limAux, cauSeqRe, ofReal]

Result:
no goals

Proof state:
f : CauSeq ℂ fun x => ‖x‖
this : IsAbsoluteValue fun x => ‖x‖ := inferInstance
x✝ : ℕ
⊢ (↑(const (fun x => ‖x‖) (limAux f)) x✝).im =
    (↑(const (fun x => ‖x‖) (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I)) x✝).im

Tactic:
simp [limAux, cauSeqIm, ofReal]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem image_mem_map_iff (hf : Injective m) : m '' s ∈ map m f ↔ s ∈ f :=
  ⟨fun h => by rwa [← preimage_image_eq s hf], image_mem_map⟩

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
s : Set α
hf : Injective m
h : m '' s ∈ map m f
⊢ s ∈ f

Tactic:
rwa [← preimage_image_eq s hf]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Lattice.lean
theorem pullback_eq_inf [SemilatticeInf α] [OrderTop α] {x y z : α} (f : x ⟶ z) (g : y ⟶ z) :
    pullback f g = x ⊓ y :=
  calc
    pullback f g = limit (cospan f g) := rfl
    _ = Finset.univ.inf (cospan f g).obj

Proof state:
α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
⊢ limit (cospan f g) = Finset.univ.inf (cospan f g).obj

Tactic:
rw [finite_limit_eq_finset_univ_inf]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
⊢ z ⊓ (x ⊓ (y ⊓ ⊤)) = z ⊓ (x ⊓ y)

Tactic:
rw [inf_top_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma norm_natCast_cpow_le_norm_natCast_cpow_of_pos {n : ℕ} (hn : 0 < n) {w z : ℂ}
    (h : w.re ≤ z.re) :
    ‖(n : ℂ) ^ w‖ ≤ ‖(n : ℂ) ^ z‖

Proof state:
n : ℕ
hn : 0 < n
w z : ℂ
h : w.re ≤ z.re
⊢ ‖↑n ^ w‖ ≤ ‖↑n ^ z‖

Tactic:
simp_rw [norm_natCast_cpow_of_pos hn]

Result:
n : ℕ
hn : 0 < n
w z : ℂ
h : w.re ≤ z.re
⊢ ↑n ^ w.re ≤ ↑n ^ z.re

Proof state:
n : ℕ
hn : 0 < n
w z : ℂ
h : w.re ≤ z.re
⊢ 1 ≤ ↑n

Tactic:
exact_mod_cast hn

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
w z : ℂ
h : w.re ≤ z.re
⊢ ↑n ^ w.re ≤ ↑n ^ z.re

Tactic:
exact Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast hn) h

Result:
no goals
-- Mathlib/Order/Hom/CompleteLattice.lean
theorem map_iInf [InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : ι → α) :
    f (⨅ i, g i) = ⨅ i, f (g i)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Sort u_6
inst✝³ : FunLike F α β
inst✝² : InfSet α
inst✝¹ : InfSet β
inst✝ : sInfHomClass F α β
f : F
g : ι → α
⊢ f (⨅ i, g i) = ⨅ i, f (g i)

Tactic:
simp [iInf, ← Set.range_comp, Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem add_self : a + a = 0

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ a + a = (a + a) * (a + a)

Tactic:
rw [mul_self]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ (a + a) * (a + a) = a * a + a * a + (a * a + a * a)

Tactic:
rw [add_mul, mul_add]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ a + a = 0

Tactic:
have : a + a = a + a + (a + a) :=
  calc
    a + a = (a + a) * (a + a) := by rw [mul_self]
    _ = a * a + a * a + (a * a + a * a) := by rw [add_mul, mul_add]
    _ = a + a + (a + a) := by rw [mul_self]

Result:
α : Type u_1
inst✝ : BooleanRing α
a : α
this : a + a = a + a + (a + a)
⊢ a + a = 0

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a : α
this : a + a = a + a + (a + a)
⊢ a + a = 0

Tactic:
rwa [self_eq_add_left] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ a * a + a * a + (a * a + a * a) = a + a + (a + a)

Tactic:
rw [mul_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem any_eq {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ i : Nat, ∃ h, p (xs[i]'h))

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ¬xs.any p = true
⊢ xs.any p = decide (∃ i h, p xs[i] = true)

Tactic:
simp_all [any_eq_false]

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ xs.any p = decide (∃ i h, p xs[i] = true)

Tactic:
by_cases h : xs.any p

Result:
case pos
α : Type u_1
xs : Array α
p : α → Bool
h : xs.any p = true
⊢ xs.any p = decide (∃ i h, p xs[i] = true)

case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ¬xs.any p = true
⊢ xs.any p = decide (∃ i h, p xs[i] = true)

Proof state:
case pos
α : Type u_1
xs : Array α
p : α → Bool
h : xs.any p = true
⊢ xs.any p = decide (∃ i h, p xs[i] = true)

Tactic:
simp_all [any_eq_true]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem toSpanSingleton_add [ContinuousAdd M₁] (x y : M₁) :
    toSpanSingleton R₁ (x + y) = toSpanSingleton R₁ x + toSpanSingleton R₁ y

Proof state:
R₁ : Type u_1
inst✝⁶ : Semiring R₁
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : TopologicalSpace R₁
inst✝¹ : ContinuousSMul R₁ M₁
inst✝ : ContinuousAdd M₁
x y : M₁
⊢ toSpanSingleton R₁ (x + y) = toSpanSingleton R₁ x + toSpanSingleton R₁ y

Tactic:
ext1

Result:
case h
R₁ : Type u_1
inst✝⁶ : Semiring R₁
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : TopologicalSpace R₁
inst✝¹ : ContinuousSMul R₁ M₁
inst✝ : ContinuousAdd M₁
x y : M₁
⊢ (toSpanSingleton R₁ (x + y)) 1 = (toSpanSingleton R₁ x + toSpanSingleton R₁ y) 1

Proof state:
case h
R₁ : Type u_1
inst✝⁶ : Semiring R₁
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : TopologicalSpace R₁
inst✝¹ : ContinuousSMul R₁ M₁
inst✝ : ContinuousAdd M₁
x y : M₁
⊢ (toSpanSingleton R₁ (x + y)) 1 = (toSpanSingleton R₁ x + toSpanSingleton R₁ y) 1

Tactic:
simp [toSpanSingleton_apply]

Result:
no goals
-- Mathlib/Topology/Order/NhdsSet.lean
theorem nhdsSet_Ici : 𝓝ˢ (Ici a) = 𝓝 a ⊔ 𝓟 (Ioi a)

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a : α
⊢ 𝓝ˢ (Ici a) = 𝓝 a ⊔ 𝓟 (Ioi a)

Tactic:
rw [← Ioi_insert, nhdsSet_insert, nhdsSet_Ioi]

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
/-- The number of dependent maps `f : Π j, s j` for which the `i` component is `a` is the product
over all `j ≠ i` of `#(s j)`.

Note that this is just a composition of easier lemmas, but there's some glue missing to make that
smooth enough not to need this lemma. -/
lemma card_filter_piFinset_eq_of_mem [∀ i, DecidableEq (α i)]
    (s : ∀ i, Finset (α i)) (i : ι) {a : α i} (ha : a ∈ s i) :
    #{f ∈ piFinset s | f i = a} = ∏ j ∈ univ.erase i, #(s j)

Proof state:
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
j : ι
⊢ #(Function.update s i {a} j) = Function.update (fun j => #(s j)) i 1 j

Tactic:
obtain rfl | hji := eq_or_ne j i <;> simp [*]

Result:
no goals

Proof state:
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ ∏ j : ι, Function.update (fun j => #(s j)) i 1 j = ∏ j ∈ univ.erase i, #(s j)

Tactic:
simp [prod_update_of_mem, erase_eq]

Result:
no goals

Proof state:
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ #(filter (fun f => f i = a) (piFinset s)) = ∏ j : ι, #(Function.update s i {a} j)

Tactic:
rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset]

Result:
no goals

Proof state:
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ #(filter (fun f => f i = a) (piFinset s)) = ∏ j ∈ univ.erase i, #(s j)

Tactic:
calc
  _ = ∏ j, #(Function.update s i {a} j) := by
    rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset]
  _ = ∏ j, Function.update (fun j ↦ #(s j)) i 1 j :=
    Fintype.prod_congr _ _ fun j ↦ by obtain rfl | hji := eq_or_ne j i <;> simp [*]
  _ = _ := by simp [prod_update_of_mem, erase_eq]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_nat_eq_ascFactorial (n : ℕ) :
    ∀ k, (ascPochhammer ℕ k).eval n = n.ascFactorial k
  | 0 => by rw [ascPochhammer_zero, eval_one, Nat.ascFactorial_zero]
  | t + 1 => by
    rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]

Proof state:
n : ℕ
⊢ eval n (ascPochhammer ℕ 0) = n.ascFactorial 0

Tactic:
rw [ascPochhammer_zero, eval_one, Nat.ascFactorial_zero]

Result:
no goals

Proof state:
n t : ℕ
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)

Tactic:
rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
  eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_toMeasurable (h : μ s ≠ ∞) : μ.restrict (toMeasurable μ s) = μ.restrict s :=
  ext fun t ht => by
    rw [restrict_apply ht, restrict_apply ht, inter_comm, measure_toMeasurable_inter ht h,
      inter_comm]

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ⊤
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (toMeasurable μ s)) t = (μ.restrict s) t

Tactic:
rw [restrict_apply ht, restrict_apply ht, inter_comm, measure_toMeasurable_inter ht h,
  inter_comm]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
lemma imp_sup_right (φ ψ : L.BoundedFormula α n) : ψ ⟹[T] φ ⊔ ψ := fun M v xs => by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]
  exact Or.inr

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ ψ.Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs

Tactic:
exact Or.inr

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (ψ ⟹ φ ⊔ ψ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ ψ.Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem condDistrib_ae_eq_of_measure_eq_compProd (hX : Measurable X) (hY : Measurable Y)
    (κ : Kernel β Ω) [IsFiniteKernel κ] (hκ : μ.map (fun x => (X x, Y x)) = μ.map X ⊗ₘ κ) :
    ∀ᵐ x ∂μ.map X, κ x = condDistrib Y X μ x

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x => (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Measure.map X μ = (Measure.map (fun x => (X x, Y x)) μ).fst
⊢ Measure.map (fun a => (X a, Y a)) μ = (Measure.map (fun a => (X a, Y a)) μ).fst ⊗ₘ κ

Tactic:
convert hκ

Result:
case h.e'_3.h.e'_5
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x => (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Measure.map X μ = (Measure.map (fun x => (X x, Y x)) μ).fst
⊢ (Measure.map (fun a => (X a, Y a)) μ).fst = Measure.map X μ

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x => (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Measure.map X μ = (Measure.map (fun x => (X x, Y x)) μ).fst
⊢ ∀ᵐ (x : β) ∂(Measure.map (fun x => (X x, Y x)) μ).fst, κ x = (Measure.map (fun a => (X a, Y a)) μ).condKernel x

Tactic:
refine eq_condKernel_of_measure_eq_compProd _ ?_

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x => (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Measure.map X μ = (Measure.map (fun x => (X x, Y x)) μ).fst
⊢ Measure.map (fun a => (X a, Y a)) μ = (Measure.map (fun a => (X a, Y a)) μ).fst ⊗ₘ κ
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem projRestricts_eq_comp (hJK : ∀ i, J i → K i) (hKL : ∀ i, K i → L i) :
    ProjRestricts C hJK ∘ ProjRestricts C hKL = ProjRestricts C (fun i ↦ hKL i ∘ hJK i)

Proof state:
case h.a.h
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
hJK : ∀ (i : I), J i → K i
hKL : ∀ (i : I), K i → L i
x : ↑(π C L)
i : I
⊢ (if J i then if K i then ↑x i else false else false) = if J i then ↑x i else false

Tactic:
aesop

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
hJK : ∀ (i : I), J i → K i
hKL : ∀ (i : I), K i → L i
⊢ ProjRestricts C hJK ∘ ProjRestricts C hKL = ProjRestricts C ⋯

Tactic:
ext x i

Result:
case h.a.h
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
hJK : ∀ (i : I), J i → K i
hKL : ∀ (i : I), K i → L i
x : ↑(π C L)
i : I
⊢ ↑((ProjRestricts C hJK ∘ ProjRestricts C hKL) x) i = ↑(ProjRestricts C ⋯ x) i

Proof state:
case h.a.h
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
hJK : ∀ (i : I), J i → K i
hKL : ∀ (i : I), K i → L i
x : ↑(π C L)
i : I
⊢ ↑((ProjRestricts C hJK ∘ ProjRestricts C hKL) x) i = ↑(ProjRestricts C ⋯ x) i

Tactic:
simp only [π, Proj, Function.comp_apply, ProjRestricts_coe]

Result:
case h.a.h
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
hJK : ∀ (i : I), J i → K i
hKL : ∀ (i : I), K i → L i
x : ↑(π C L)
i : I
⊢ (if J i then if K i then ↑x i else false else false) = if J i then ↑x i else false
-- Mathlib/Algebra/Order/Floor.lean
theorem le_floor_iff' (hn : n ≠ 0) : n ≤ ⌊a⌋₊ ↔ (n : α) ≤ a

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ 0 ↔ ↑n ≤ a

Tactic:
exact
  iff_of_false (Nat.pos_of_ne_zero hn).not_le
    (not_le_of_lt <| ha.trans_lt <| cast_pos.2 <| Nat.pos_of_ne_zero hn)

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

Tactic:
obtain ha | ha := le_total a 0

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

case inr
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

Tactic:
exact le_floor_iff ha

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

Tactic:
rw [floor_of_nonpos ha]

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ 0 ↔ ↑n ≤ a
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f)
    (s : ι → Submonoid M) : (iInf s).map f = ⨅ i, (s i).map f

Proof state:
M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
mc : MonoidHomClass F M N
ι : Sort u_5
inst✝ : Nonempty ι
f : F
hf : Injective ⇑f
s : ι → Submonoid M
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Result:
case a
M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
mc : MonoidHomClass F M N
ι : Sort u_5
inst✝ : Nonempty ι
f : F
hf : Injective ⇑f
s : ι → Submonoid M
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Proof state:
case a
M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
mc : MonoidHomClass F M N
ι : Sort u_5
inst✝ : Nonempty ι
f : F
hf : Injective ⇑f
s : ι → Submonoid M
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem find?_range_eq_none {n : Nat} {p : Nat → Bool} :
    (range n).find? p = none ↔ ∀ i, i < n → !p i

Proof state:
n : Nat
p : Nat → Bool
⊢ find? p (range n) = none ↔ ∀ (i : Nat), i < n → (!p i) = true

Tactic:
simp only [← List.toArray_range, List.find?_toArray, List.find?_range_eq_none]

Result:
no goals
-- Mathlib/Analysis/Convex/Jensen.lean
theorem ConvexOn.map_sum_le (hf : ConvexOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1)
    (hmem : ∀ i ∈ t, p i ∈ s) : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)

Tactic:
simpa only [centerMass, h₁, inv_one, one_smul] using
  hf.map_centerMass_le h₀ (h₁.symm ▸ zero_lt_one) hmem

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
@[to_additive]
lemma left_mul_prod_Ioc (h : a ≤ b) : f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a b : α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x

Tactic:
rw [Icc_eq_cons_Ioc h, prod_cons]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attachWith_eq_some_iff {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) {x : {x // p x}} :
    o.attachWith p H = some x ↔ o = some x.val

Proof state:
α : Type u_1
p : α → Prop
o : Option α
H : ∀ (a : α), a ∈ o → p a
x : { x // p x }
⊢ o.attachWith p H = some x ↔ o = some x.val

Tactic:
cases o <;> cases x <;> simp

Result:
no goals