harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Condexp.lean
theorem _root_.MeasureTheory.Integrable.integral_condExpKernel [NormedSpace ℝ F]
    (hf_int : Integrable f μ) :
    Integrable (fun ω => ∫ y, f y ∂condExpKernel μ m ω) μ

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ

Tactic:
convert Integrable.integral_condDistrib
  (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
  (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ)) using 1

Result:
no goals

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Tactic:
rw [condExpKernel_eq]

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
⊢ Integrable (fun ω => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Tactic:
nontriviality Ω

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma integrable_densityProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (n : ℕ)
    (a : α) {s : Set β} (hs : MeasurableSet s) :
    Integrable (fun x ↦ densityProcess κ ν n a x s) (ν a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ MemLp (fun x => κ.densityProcess ν n a x s) 1 (ν a)

Tactic:
refine ⟨Measurable.aestronglyMeasurable ?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x => κ.densityProcess ν n a x s

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ eLpNorm (fun x => κ.densityProcess ν n a x s) 1 (ν a) < ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun x => κ.densityProcess ν n a x s) (ν a)

Tactic:
rw [← memLp_one_iff_integrable]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ MemLp (fun x => κ.densityProcess ν n a x s) 1 (ν a)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ eLpNorm (fun x => κ.densityProcess ν n a x s) 1 (ν a) < ⊤

Tactic:
exact (eLpNorm_densityProcess_le hκν n a s).trans_lt (measure_lt_top _ _)

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x => κ.densityProcess ν n a x s

Tactic:
exact measurable_densityProcess_right κ ν n a hs

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Icc_subset_Ico_succ_right_of_not_isMax (hb : ¬IsMax b) : Icc a b ⊆ Ico a (succ b)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ici a ∩ Iic b ⊆ Ici a ∩ Iio (succ b)

Tactic:
gcongr

Result:
case H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Iic b ⊆ Iio (succ b)

Proof state:
case H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Iic b ⊆ Iio (succ b)

Tactic:
intro _ h

Result:
case H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
a✝ : α
h : a✝ ∈ Iic b
⊢ a✝ ∈ Iio (succ b)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Icc a b ⊆ Ico a (succ b)

Tactic:
rw [← Ici_inter_Iio, ← Ici_inter_Iic]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ici a ∩ Iic b ⊆ Ici a ∩ Iio (succ b)

Proof state:
case H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
a✝ : α
h : a✝ ∈ Iic b
⊢ a✝ ∈ Iio (succ b)

Tactic:
apply lt_succ_of_le_of_not_isMax h hb

Result:
no goals
-- Mathlib/CategoryTheory/Grothendieck.lean
theorem base_eqToHom {X Y : Grothendieck F} (h : X = Y) :
    (eqToHom h).base = eqToHom (congrArg Grothendieck.base h)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (eqToHom ⋯).base = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
h : X = Y
⊢ (eqToHom h).base = eqToHom ⋯

Tactic:
subst h

Result:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (eqToHom ⋯).base = eqToHom ⋯
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma jacobiTheta₂_conj (z τ : ℂ) :
    conj (jacobiTheta₂ z τ) = jacobiTheta₂ (conj z) (-conj τ)

Proof state:
z τ : ℂ
⊢ ∑' (a : ℤ), (starRingEnd ℂ) (jacobiTheta₂_term a (-z) τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
congr 2 with n

Result:
case e_f.h
z τ : ℂ
n : ℤ
⊢ (starRingEnd ℂ) (jacobiTheta₂_term n (-z) τ) = jacobiTheta₂_term n ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Proof state:
z τ : ℂ
⊢ (starRingEnd ℂ) (jacobiTheta₂ z τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
rw [← jacobiTheta₂_neg_left, jacobiTheta₂, conj_tsum]

Result:
z τ : ℂ
⊢ ∑' (a : ℤ), (starRingEnd ℂ) (jacobiTheta₂_term a (-z) τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Proof state:
case e_f.h
z τ : ℂ
n : ℤ
⊢ (starRingEnd ℂ) (jacobiTheta₂_term n (-z) τ) = jacobiTheta₂_term n ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
simp only [jacobiTheta₂_term, mul_neg, ← exp_conj, map_add, map_neg, map_mul, map_ofNat,
  conj_ofReal, conj_I, map_intCast, neg_mul, neg_neg, map_pow]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pos_of_mem_Ioo {x : ℝ} (hx : x ∈ Ioo (-(π / 2)) (π / 2)) : 0 < cos x :=
  sin_add_pi_div_two x ▸ sin_pos_of_mem_Ioo ⟨by linarith [hx.1], by linarith [hx.2]⟩

Proof state:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ x + π / 2 < π

Tactic:
linarith [hx.2]

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ 0 < x + π / 2

Tactic:
linarith [hx.1]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem compl_iInter₂ (s : ∀ i, κ i → Set α) : (⋂ (i) (j), s i j)ᶜ = ⋃ (i) (j), (s i j)ᶜ

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋂ i, ⋂ j, s i j)ᶜ = ⋃ i, ⋃ j, (s i j)ᶜ

Tactic:
simp_rw [compl_iInter]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem SurjOn.bijOn_subset [Nonempty α] (h : SurjOn f s t) : BijOn f (invFunOn f s '' t) t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ BijOn f (invFunOn f s '' t) t

Tactic:
refine h.invOn_invFunOn.bijOn ?_ (mapsTo_image _ _)

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ MapsTo f (invFunOn f s '' t) t

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ f (invFunOn f s y) ∈ t

Tactic:
rwa [h.rightInvOn_invFunOn hy]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ MapsTo f (invFunOn f s '' t) t

Tactic:
rintro _ ⟨y, hy, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ f (invFunOn f s y) ∈ t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_ofInt {n : Nat} (i : Int) :
  (BitVec.ofInt n i).toNat = (i % (2^n : Nat)).toNat

Proof state:
n : Nat
i : Int
⊢ ((i % Int.ofNat (2 ^ n)).toNat#'⋯).toNat = (i % ↑(2 ^ n)).toNat

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
i : Int
⊢ (BitVec.ofInt n i).toNat = (i % ↑(2 ^ n)).toNat

Tactic:
unfold BitVec.ofInt

Result:
n : Nat
i : Int
⊢ ((i % Int.ofNat (2 ^ n)).toNat#'⋯).toNat = (i % ↑(2 ^ n)).toNat
-- Mathlib/RingTheory/Polynomial/Vieta.lean
theorem prod_X_sub_X_eq_sum_esymm (s : Multiset R) :
    (s.map fun t => X - C t).prod =
      ∑ j ∈ Finset.range (Multiset.card s + 1),
        (-1) ^ j * (C (s.esymm j) * X ^ (Multiset.card s - j))

Proof state:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ (map (fun t => X - C t) s).prod = ∑ j ∈ Finset.range (s.card + 1), (-1) ^ j * (C (s.esymm j) * X ^ (s.card - j))

Tactic:
conv_lhs =>
  congr
  congr
  ext x
  rw [sub_eq_add_neg]
  rw [← map_neg C x]

Result:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ (map (fun x => X + C (-x)) s).prod = ∑ j ∈ Finset.range (s.card + 1), (-1) ^ j * (C (s.esymm j) * X ^ (s.card - j))

Proof state:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ (map (fun x => X + C (-x)) s).prod = (map (fun r => X + C r) (map (fun t => -t) s)).prod

Tactic:
rw [map_map]

Result:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ (map (fun x => X + C (-x)) s).prod = (map ((fun r => X + C r) ∘ fun t => -t) s).prod

Proof state:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ (map (fun x => X + C (-x)) s).prod = ∑ j ∈ Finset.range (s.card + 1), (-1) ^ j * (C (s.esymm j) * X ^ (s.card - j))

Tactic:
convert prod_X_add_C_eq_sum_esymm (map (fun t => -t) s) using 1

Result:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ (map (fun x => X + C (-x)) s).prod = (map (fun r => X + C r) (map (fun t => -t) s)).prod

case h.e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ ∑ j ∈ Finset.range (s.card + 1), (-1) ^ j * (C (s.esymm j) * X ^ (s.card - j)) =
    ∑ j ∈ Finset.range ((map (fun t => -t) s).card + 1),
      C ((map (fun t => -t) s).esymm j) * X ^ ((map (fun t => -t) s).card - j)

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ ∑ j ∈ Finset.range (s.card + 1), (-1) ^ j * (C (s.esymm j) * X ^ (s.card - j)) =
    ∑ j ∈ Finset.range ((map (fun t => -t) s).card + 1),
      C ((map (fun t => -t) s).esymm j) * X ^ ((map (fun t => -t) s).card - j)

Tactic:
simp only [esymm_neg, card_map, mul_assoc, map_mul, map_pow, map_neg, map_one]

Result:
no goals

Proof state:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ (map (fun x => X + C (-x)) s).prod = (map ((fun r => X + C r) ∘ fun t => -t) s).prod

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_mkVector {a b : α} {n} : b ∈ mkVector n a ↔ n ≠ 0 ∧ b = a

Proof state:
α : Type u_1
a b : α
n : Nat
⊢ b ∈ mkVector n a ↔ n ≠ 0 ∧ b = a

Tactic:
unfold mkVector

Result:
α : Type u_1
a b : α
n : Nat
⊢ b ∈ { toArray := mkArray n a, size_toArray := ⋯ } ↔ n ≠ 0 ∧ b = a

Proof state:
α : Type u_1
a b : α
n : Nat
⊢ b ∈ mkArray n a ↔ n ≠ 0 ∧ b = a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a b : α
n : Nat
⊢ b ∈ { toArray := mkArray n a, size_toArray := ⋯ } ↔ n ≠ 0 ∧ b = a

Tactic:
simp only [mem_mk]

Result:
α : Type u_1
a b : α
n : Nat
⊢ b ∈ mkArray n a ↔ n ≠ 0 ∧ b = a
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma pow_right_injective₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Injective (a ^ ·)

Proof state:
case inr
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a : M₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : 1 < a
⊢ Injective fun x => a ^ x

Tactic:
exact (pow_right_strictMono₀ ha₁).injective

Result:
no goals

Proof state:
case inl
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a : M₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : a < 1
⊢ Injective fun x => a ^ x

Tactic:
exact (pow_right_strictAnti₀ ha₀ ha₁).injective

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a : M₀
ha₀ : 0 < a
ha₁ : a ≠ 1
⊢ Injective fun x => a ^ x

Tactic:
obtain ha₁ | ha₁ := ha₁.lt_or_lt

Result:
case inl
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a : M₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : a < 1
⊢ Injective fun x => a ^ x

case inr
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a : M₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : 1 < a
⊢ Injective fun x => a ^ x
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem surjOn_log' : SurjOn log (Iio 0) univ := fun x _ =>
  ⟨-exp x, neg_lt_zero.2 <| exp_pos x, by rw [log_neg_eq_log, log_exp]⟩

Proof state:
x : ℝ
x✝ : x ∈ univ
⊢ log (-rexp x) = x

Tactic:
rw [log_neg_eq_log, log_exp]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_left_inv {x : M} (hxf : x ∈ f.source) : (f.extend I).symm (f.extend I x) = x :=
  (f.extend I).left_inv <| by rwa [f.extend_source]

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hxf : x ∈ f.source
⊢ x ∈ (f.extend I).source

Tactic:
rwa [f.extend_source]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem Coprime.gcd_mul_right_cancel_right (n : Nat)
    (H : Coprime k m) : gcd m (n * k) = gcd m n

Proof state:
k m n : Nat
H : k.Coprime m
⊢ m.gcd (n * k) = m.gcd n

Tactic:
rw [Nat.mul_comm n k, H.gcd_mul_left_cancel_right n]

Result:
no goals
-- Mathlib/MeasureTheory/Covering/Vitali.lean
theorem exists_disjoint_subfamily_covering_enlargement_closedBall
    [PseudoMetricSpace α] (t : Set ι)
    (x : ι → α) (r : ι → ℝ) (R : ℝ) (hr : ∀ a ∈ t, r a ≤ R) (τ : ℝ) (hτ : 3 < τ) :
    ∃ u ⊆ t,
      (u.PairwiseDisjoint fun a => closedBall (x a) (r a)) ∧
        ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Proof state:
case neg.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a => closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ u ⊆ t,
    (u.PairwiseDisjoint fun a => closedBall (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
refine ⟨u, ut'.trans fun a ha => ha.1, u_disj, fun a ha => ?_⟩

Result:
case neg.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a => closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Proof state:
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a => closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
⊢ ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
intro a ha

Result:
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a => closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Proof state:
α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
⊢ 1 < (τ - 1) / 2

Tactic:
linarith

Result:
no goals
-- Mathlib/Control/LawfulFix.lean
theorem ωScottContinuous_uncurry :
    ωScottContinuous (monotoneUncurry α β γ) :=
    .of_map_ωSup_of_orderHom fun c ↦ by
  ext ⟨x, y⟩
  dsimp [uncurry, ωSup]
  rw [map_comp, map_comp]
  rfl

Proof state:
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (c.map ((evalOrderHom y).comp (evalOrderHom x))) =
    ωSup (c.map ((evalOrderHom ⟨x, y⟩).comp (monotoneUncurry α β γ)))

Tactic:
rfl

Result:
no goals

Proof state:
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ (monotoneUncurry α β γ) (ωSup c) ⟨x, y⟩ = ωSup (c.map (monotoneUncurry α β γ)) ⟨x, y⟩

Tactic:
dsimp [uncurry, ωSup]

Result:
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup ((c.map (evalOrderHom x)).map (evalOrderHom y)) =
    ωSup ((c.map (monotoneUncurry α β γ)).map (evalOrderHom ⟨x, y⟩))

Proof state:
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup ((c.map (evalOrderHom x)).map (evalOrderHom y)) =
    ωSup ((c.map (monotoneUncurry α β γ)).map (evalOrderHom ⟨x, y⟩))

Tactic:
rw [map_comp, map_comp]

Result:
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (c.map ((evalOrderHom y).comp (evalOrderHom x))) =
    ωSup (c.map ((evalOrderHom ⟨x, y⟩).comp (monotoneUncurry α β γ)))

Proof state:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
⊢ (monotoneUncurry α β γ) (ωSup c) = ωSup (c.map (monotoneUncurry α β γ))

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ (monotoneUncurry α β γ) (ωSup c) ⟨x, y⟩ = ωSup (c.map (monotoneUncurry α β γ)) ⟨x, y⟩
-- Mathlib/CategoryTheory/Sites/Over.lean
lemma over_map_coverPreserving {X Y : C} (f : X ⟶ Y) :
    CoverPreserving (J.over X) (J.over Y) (Over.map f) where
  cover_preserve {U S} hS

Proof state:
case intro.hS
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ S ∈ J ((Over.map f).obj U).left

Tactic:
simpa [mem_over_iff] using hS

Result:
no goals

Proof state:
case intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ (Sieve.overEquiv ((Over.map f).obj U)).symm S ∈ (J.over Y) ((Over.map f).obj U)

Tactic:
apply overEquiv_symm_mem_over

Result:
case intro.hS
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ S ∈ J ((Over.map f).obj U).left

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U
hS : S ∈ (J.over X) U
⊢ Sieve.functorPushforward (Over.map f) S ∈ (J.over Y) ((Over.map f).obj U)

Tactic:
obtain ⟨S, rfl⟩ := (Sieve.overEquiv U).symm.surjective S

Result:
case intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ Sieve.functorPushforward (Over.map f) ((Sieve.overEquiv U).symm S) ∈ (J.over Y) ((Over.map f).obj U)

Proof state:
case intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ Sieve.functorPushforward (Over.map f) ((Sieve.overEquiv U).symm S) ∈ (J.over Y) ((Over.map f).obj U)

Tactic:
rw [Sieve.functorPushforward_over_map]

Result:
case intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ (Sieve.overEquiv ((Over.map f).obj U)).symm S ∈ (J.over Y) ((Over.map f).obj U)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_flatten (a : α) (l : Vector (Vector α m) n) :
    count a l.flatten = (l.map (count a)).sum

Proof state:
α : Type u_1
inst✝ : BEq α
m n : Nat
a : α
l : Vector (Vector α m) n
⊢ count a l.flatten = (map (count a) l).sum

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
m : Nat
a : α
l : Array (Vector α m)
⊢ count a { toArray := l, size_toArray := ⋯ }.flatten = (map (count a) { toArray := l, size_toArray := ⋯ }).sum

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
m : Nat
a : α
l : Array (Vector α m)
⊢ count a { toArray := l, size_toArray := ⋯ }.flatten = (map (count a) { toArray := l, size_toArray := ⋯ }).sum

Tactic:
simp [Array.count_flatten, Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_singleton (a : α) : head? [a] = some a

Proof state:
α : Type u_1
a : α
⊢ [a].head? = some a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem dvd_prime_pow {p : ℕ} (pp : Prime p) {m i : ℕ} : i ∣ p ^ m ↔ ∃ k ≤ m, i = p ^ k

Proof state:
p : ℕ
pp : Prime p
m i : ℕ
⊢ i ∣ p ^ m ↔ ∃ k, k ≤ m ∧ i = p ^ k

Tactic:
simp_rw [_root_.dvd_prime_pow (prime_iff.mp pp) m, associated_eq_eq]

Result:
no goals