harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem existsUnique_add_zpow_mem_Ioc {a : α} (ha : 1 < a) (b c : α) :
    ∃! m : ℤ, b * a ^ m ∈ Set.Ioc c (c * a) :=
  (Equiv.addRight (1 : ℤ)).bijective.existsUnique_iff.2 <| by
    simpa only [zpow_add_one, div_lt_iff_lt_mul', le_div_iff_mul_le', ← mul_assoc, and_comm,
      mem_Ioc, Equiv.coe_addRight, mul_le_mul_iff_right] using
      existsUnique_zpow_near_of_one_lt ha (c / b)

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedCommGroup α
inst✝ : MulArchimedean α
a : α
ha : 1 < a
b c : α
⊢ ∃! x, b * a ^ (Equiv.addRight 1) x ∈ Ioc c (c * a)

Tactic:
simpa only [zpow_add_one, div_lt_iff_lt_mul', le_div_iff_mul_le', ← mul_assoc, and_comm,
  mem_Ioc, Equiv.coe_addRight, mul_le_mul_iff_right] using
  existsUnique_zpow_near_of_one_lt ha (c / b)

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem get_set_of_ne {v : Vector α n} {i j : Fin n} (h : i ≠ j) (a : α) :
    (v.set i a).get j = v.get j

Proof state:
case mk.mk.mk
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ (set ⟨val✝², property✝⟩ ⟨val✝¹, isLt✝¹⟩ a).get ⟨val✝, isLt✝⟩ = get ⟨val✝², property✝⟩ ⟨val✝, isLt✝⟩

Tactic:
simp only [get_eq_get_toList, toList_set, toList_mk, Fin.cast_mk, List.get_eq_getElem]

Result:
case mk.mk.mk
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ (val✝².set val✝¹ a)[val✝] = val✝²[val✝]

Proof state:
case mk.mk.mk.h
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ val✝¹ ≠ val✝

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
h : i ≠ j
a : α
⊢ (v.set i a).get j = v.get j

Tactic:
cases v

Result:
case mk
α : Type u_1
n : ℕ
i j : Fin n
h : i ≠ j
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ (set ⟨val✝, property✝⟩ i a).get j = get ⟨val✝, property✝⟩ j

Proof state:
case mk.mk.mk
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ (val✝².set val✝¹ a)[val✝] = val✝²[val✝]

Tactic:
rw [List.getElem_set_of_ne]

Result:
case mk.mk.mk.h
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ val✝¹ ≠ val✝

Proof state:
case mk
α : Type u_1
n : ℕ
i j : Fin n
h : i ≠ j
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ (set ⟨val✝, property✝⟩ i a).get j = get ⟨val✝, property✝⟩ j

Tactic:
cases i

Result:
case mk.mk
α : Type u_1
n : ℕ
j : Fin n
a : α
val✝¹ : List α
property✝ : val✝¹.length = n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝, isLt✝⟩ ≠ j
⊢ (set ⟨val✝¹, property✝⟩ ⟨val✝, isLt✝⟩ a).get j = get ⟨val✝¹, property✝⟩ j

Proof state:
case mk.mk
α : Type u_1
n : ℕ
j : Fin n
a : α
val✝¹ : List α
property✝ : val✝¹.length = n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝, isLt✝⟩ ≠ j
⊢ (set ⟨val✝¹, property✝⟩ ⟨val✝, isLt✝⟩ a).get j = get ⟨val✝¹, property✝⟩ j

Tactic:
cases j

Result:
case mk.mk.mk
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ (set ⟨val✝², property✝⟩ ⟨val✝¹, isLt✝¹⟩ a).get ⟨val✝, isLt✝⟩ = get ⟨val✝², property✝⟩ ⟨val✝, isLt✝⟩
-- Mathlib/Data/Finset/Grade.lean
@[simp] lemma covBy_cons (ha : a ∉ s) : s ⋖ s.cons a ha

Proof state:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
⊢ s ⋖ cons a s ha

Tactic:
simp [← val_covBy_val]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem image_mem_functorPushforward (R : Presieve X) {f : Y ⟶ X} (h : R f) :
    R.functorPushforward F (F.map f) :=
  ⟨Y, f, 𝟙 _, h, by simp⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
R : Presieve X
f : Y ⟶ X
h : R f
⊢ F.map f = 𝟙 (F.obj Y) ≫ F.map f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
    (hl : DistinctKeys l) :
    getEntry? a (eraseKey k l) = if k == a then none else getEntry? a l

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : (k == a) = false
⊢ getEntry? a (eraseKey k l) = if false = true then none else getEntry? a l

Tactic:
simp [getEntry?_eraseKey_of_false h, h]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
⊢ getEntry? a (eraseKey k l) = if (k == a) = true then none else getEntry? a l

Tactic:
cases h : k == a

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : (k == a) = false
⊢ getEntry? a (eraseKey k l) = if false = true then none else getEntry? a l

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : (k == a) = true
⊢ getEntry? a (eraseKey k l) = if true = true then none else getEntry? a l

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : (k == a) = true
⊢ getEntry? a (eraseKey k l) = if true = true then none else getEntry? a l

Tactic:
simp [getEntry?_eraseKey_of_beq hl h, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_toVector (l : Array α) (f : (i : Nat) → α → (h : i < l.size) → β) :
    l.toVector.mapFinIdx f = (l.mapFinIdx f).toVector.cast (by simp)

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ l.toVector.mapFinIdx f = Vector.cast ⋯ (l.mapFinIdx f).toVector

Tactic:
ext <;> simp

Result:
no goals

Proof state:
α : Type ?u.6195
β : Type ?u.6219
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ (l.mapFinIdx f).size = l.size

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem unattach_attachWith {p : α → Prop} {l : Vector α n}
    {H : ∀ a ∈ l, p a} :
    (l.attachWith p H).unattach = l

Proof state:
α : Type u_1
n : Nat
p : α → Prop
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
⊢ (l.attachWith p H).unattach = l

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
p : α → Prop
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith p H).unattach =
    { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Prop
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith p H).unattach =
    { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma comp_hom {a b : ℕ} (α : Ext X Y a) (β : Ext Y Z b) {c : ℕ} (h : a + b = c) :
    (α.comp β h).hom = α.hom.comp β.hom (by omega)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y Z T : C
inst✝ : HasDerivedCategory C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
⊢ ↑b + ↑a = ↑c

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y Z : C
inst✝ : HasDerivedCategory C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
⊢ (α.comp β h).hom = α.hom.comp β.hom ⋯

Tactic:
apply SmallShiftedHom.equiv_comp

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Set.Finite.ciInf_mem_image {s : Set ι} (hs : s.Finite) (h : ∃ x ∈ s, f x ≤ sInf ∅) :
    ⨅ i ∈ s, f i ∈ f '' s

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ i ∈ s, f i ∈ f '' s

Tactic:
lift s to Finset ι using hs

Result:
case intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ ↑s, f x ≤ sInf ∅
⊢ ⨅ i ∈ ↑s, f i ∈ f '' ↑s

Proof state:
case intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ ↑s, f x ≤ sInf ∅
⊢ ⨅ i ∈ ↑s, f i ∈ f '' ↑s

Tactic:
simp only [Finset.mem_coe] at h

Result:
case intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ i ∈ ↑s, f i ∈ f '' ↑s

Proof state:
case intro
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ i ∈ ↑s, f i ∈ f '' ↑s

Tactic:
simpa using Finset.ciInf_mem_image f h

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.zsmul_sub_eq [AddCommGroup α] [AddGroup β] (h : Antiperiodic f c) (n : ℤ) :
    f (n • c - x) = (n.negOnePow : ℤ) • f (-x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddCommGroup α
inst✝ : AddGroup β
h : Antiperiodic f c
n : ℤ
⊢ f (n • c - x) = ↑n.negOnePow • f (-x)

Tactic:
rw [sub_eq_add_neg, add_comm]

Result:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddCommGroup α
inst✝ : AddGroup β
h : Antiperiodic f c
n : ℤ
⊢ f (-x + n • c) = ↑n.negOnePow • f (-x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddCommGroup α
inst✝ : AddGroup β
h : Antiperiodic f c
n : ℤ
⊢ f (-x + n • c) = ↑n.negOnePow • f (-x)

Tactic:
exact h.add_zsmul_eq n

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_mul_right_Ioo (a b : α) {c : α} (h : 0 < c) :
    (fun x => x * c) '' Ioo a b = Ioo (a * c) (b * c) :=
  ((Units.mk0 c h.ne').mulRight.image_eq_preimage _).trans (by simp [h, division_def])

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : 0 < c
⊢ ⇑(Equiv.symm (Units.mk0 c ⋯).mulRight) ⁻¹' Ioo a b = Ioo (a * c) (b * c)

Tactic:
simp [h, division_def]

Result:
no goals
-- Mathlib/Data/List/Lattice.lean
theorem cons_bagInter_of_neg (l₁ : List α) (h : a ∉ l₂) :
    (a :: l₁).bagInter l₂ = l₁.bagInter l₂

Proof state:
α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = l₁.bagInter l₂

Tactic:
cases l₂

Result:
case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ []
⊢ (a :: l₁).bagInter [] = l₁.bagInter []

case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
l₁ : List α
head✝ : α
tail✝ : List α
h : ¬a ∈ head✝ :: tail✝
⊢ (a :: l₁).bagInter (head✝ :: tail✝) = l₁.bagInter (head✝ :: tail✝)

Proof state:
case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ []
⊢ (a :: l₁).bagInter [] = l₁.bagInter []

Tactic:
simp only [bagInter_nil]

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
l₁ : List α
head✝ : α
tail✝ : List α
h : ¬a ∈ head✝ :: tail✝
⊢ (a :: l₁).bagInter (head✝ :: tail✝) = l₁.bagInter (head✝ :: tail✝)

Tactic:
simp only [erase_of_not_mem h, List.bagInter, if_neg (mt mem_of_elem_eq_true h)]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem singularPart_le (μ ν : Measure α) : μ.singularPart ν ≤ μ

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 ≤ μ

Tactic:
exact Measure.zero_le μ

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ≤ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
exact Measure.le_add_right le_rfl

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ≤ μ

Tactic:
rw [singularPart, dif_neg hl]

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 ≤ μ

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ≤ μ

Tactic:
conv_rhs => rw [haveLebesgueDecomposition_add μ ν]

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ≤ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ≤ μ

Tactic:
by_cases hl : HaveLebesgueDecomposition μ ν

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ≤ μ

case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ≤ μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.true_or (b : Bool) : (true || b) = true

Proof state:
b : Bool
⊢ (true || b) = true

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma absolutelyContinuous_compProd_of_compProd [SigmaFinite μ] [SigmaFinite ν]
    (hκη : μ ⊗ₘ κ ≪ ν ⊗ₘ η) :
    μ ⊗ₘ κ ≪ μ ⊗ₘ η

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
h : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
refine h.trans (AbsolutelyContinuous.compProd_left ?_ _)

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
h : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
⊢ μ.withDensity (ν.rnDeriv μ) ≪ μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
have h := absolutelyContinuous_of_add_of_mutuallySingular hκη
  ((mutuallySingular_singularPart _ _).symm.compProd_of_left _ _)

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
h : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
h : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
⊢ μ.withDensity (ν.rnDeriv μ) ≪ μ

Tactic:
exact withDensity_absolutelyContinuous _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
rw [ν.haveLebesgueDecomposition_add μ, compProd_add_left, add_comm] at hκη

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η
-- Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
@[reassoc (attr := simp)]
lemma map_reflexion_comp_map_right (F : WalkingReflexivePair ⥤ C) :
    F.map reflexion ≫ F.map right = 𝟙 (F.obj zero)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ F.map reflexion ≫ F.map right = 𝟙 (F.obj zero)

Tactic:
rw [← F.map_comp, reflexion_comp_right, F.map_id]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem splitMax_eq :
    ∀ (s l) (x : α) (r), splitMax' l x r = (eraseMax (node s l x r), findMax' x r)
  | _, _, _, nil => rfl
  | _, l, x, node ls ll lx lr => by rw [splitMax', splitMax_eq ls ll lx lr, findMax', eraseMax]

Proof state:
α : Type u_1
x✝ : ℕ
l : Ordnode α
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ l.splitMax' x (node ls ll lx lr) = ((node x✝ l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))

Tactic:
rw [splitMax', splitMax_eq ls ll lx lr, findMax', eraseMax]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_prod {ι : Type u} (c : ι → Cardinal.{v}) :
    lift.{w} (prod c) = prod fun i => lift.{w} (c i)

Proof state:
ι : Type u
c : ι → Cardinal.{v}
⊢ lift.{w, max v u} (prod c) = prod fun i => lift.{w, v} (c i)

Tactic:
lift c to ι → Type v using fun _ => trivial

Result:
case intro
ι : Type u
c : ι → Type v
⊢ lift.{w, max v u} (prod fun i => #(c i)) = prod fun i => lift.{w, v} ((fun i => #(c i)) i)

Proof state:
case intro
ι : Type u
c : ι → Type v
⊢ lift.{w, max v u} (prod fun i => #(c i)) = prod fun i => lift.{w, v} ((fun i => #(c i)) i)

Tactic:
simp only [← mk_pi, ← mk_uLift]

Result:
case intro
ι : Type u
c : ι → Type v
⊢ #(ULift.{w, max u v} ((i : ι) → c i)) = #((i : ι) → ULift.{w, v} (c i))

Proof state:
case intro
ι : Type u
c : ι → Type v
⊢ #(ULift.{w, max u v} ((i : ι) → c i)) = #((i : ι) → ULift.{w, v} (c i))

Tactic:
exact mk_congr (Equiv.ulift.trans <| Equiv.piCongrRight fun i => Equiv.ulift.symm)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
    get? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some v else get? m a

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β
⊢ get? (m.insertIfNew k v) a = if (k == a) = true ∧ m.contains k = false then some v else get? m a

Tactic:
simp_to_raw using Raw₀.Const.get?_insertIfNew

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β
⊢ get? (m.insertIfNew k v) a = if (k == a) = true ∧ ¬k ∈ m then some v else get? m a

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β
⊢ get? (m.insertIfNew k v) a = if (k == a) = true ∧ m.contains k = false then some v else get? m a
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem mem_toCone : x ∈ hs.toCone s ↔ ∃ c : 𝕜, 0 < c ∧ ∃ y ∈ s, c • y = x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ x ∈ toCone s hs ↔ ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x

Tactic:
simp only [toCone, ConvexCone.mem_mk, mem_iUnion, mem_smul_set, eq_comm, exists_prop]

Result:
no goals
-- Mathlib/Combinatorics/Derangements/Finite.lean
theorem numDerangements_succ (n : ℕ) :
    (numDerangements (n + 1) : ℤ) = (n + 1) * (numDerangements n : ℤ) - (-1) ^ n

Proof state:
case succ
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ (↑n + ↑1) * (↑(numDerangements n) + ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n)) =
    (↑n + ↑1 + 1) * ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n) - (-1) ^ n * -1

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
⊢ ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n

Tactic:
induction n with
| zero => rfl
| succ n hn =>
  simp only [numDerangements_add_two, hn, pow_succ, Int.ofNat_mul, Int.ofNat_add]
  ring

Result:
no goals

Proof state:
case succ
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ ↑(numDerangements (n + 1 + 1)) = (↑(n + 1) + 1) * ↑(numDerangements (n + 1)) - (-1) ^ (n + 1)

Tactic:
simp only [numDerangements_add_two, hn, pow_succ, Int.ofNat_mul, Int.ofNat_add]

Result:
case succ
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ (↑n + ↑1) * (↑(numDerangements n) + ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n)) =
    (↑n + ↑1 + 1) * ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n) - (-1) ^ n * -1

Proof state:
case zero

⊢ ↑(numDerangements (0 + 1)) = (↑0 + 1) * ↑(numDerangements 0) - (-1) ^ 0

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem hom_eq_iff {X Y : CostructuredArrow S T} (f g : X ⟶ Y) : f = g ↔ f.left = g.left :=
  ⟨fun h ↦ by rw [h], hom_ext _ _⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
X Y : CostructuredArrow S T
f g : X ⟶ Y
h : f = g
⊢ f.left = g.left

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tendsto_tan_pi_div_two : Tendsto tan (𝓝[<] (π / 2)) atTop

Proof state:
case h.e'_3

⊢ tan = fun x => cos⁻¹ x * sin x

Tactic:
simp only [Pi.inv_apply, ← div_eq_inv_mul, ← tan_eq_sin_div_cos]

Result:
no goals

Proof state:
⊢ Tendsto tan (𝓝[<] (π / 2)) atTop

Tactic:
convert tendsto_cos_pi_div_two.inv_tendsto_nhdsGT_zero.atTop_mul zero_lt_one
  tendsto_sin_pi_div_two using 1

Result:
case h.e'_3

⊢ tan = fun x => cos⁻¹ x * sin x
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_left_surjective {x : ℝ} (hx : x ≠ 0) : Function.Surjective fun y : ℝ≥0 => y ^ x :=
  fun y => ⟨y ^ x⁻¹, by simp_rw [← rpow_mul, inv_mul_cancel₀ hx, rpow_one]⟩

Proof state:
x : ℝ
hx : x ≠ 0
y : ℝ≥0
⊢ (fun y => y ^ x) (y ^ x⁻¹) = y

Tactic:
simp_rw [← rpow_mul, inv_mul_cancel₀ hx, rpow_one]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem isPath_reverse_iff {u v : V} (p : G.Walk u v) : p.reverse.IsPath ↔ p.IsPath

Proof state:
case h.e'_5
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
⊢ p = p.reverse.reverse

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsPath ↔ p.IsPath

Tactic:
constructor <;> intro h <;> convert h.reverse

Result:
case h.e'_5
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
⊢ p = p.reverse.reverse
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_fromBlocks_zero₁₂ (A : Matrix m m R) (C : Matrix n m R) (D : Matrix n n R) :
    (Matrix.fromBlocks A 0 C D).det = A.det * D.det

Proof state:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
C : Matrix n m R
D : Matrix n n R
⊢ (fromBlocks A 0 C D).det = A.det * D.det

Tactic:
rw [← det_transpose, fromBlocks_transpose, transpose_zero, det_fromBlocks_zero₂₁, det_transpose,
  det_transpose]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.kerTotal_mkQ_single_algebraMap (x y) : (y𝖣algebraMap R S x) = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
y : S
⊢ (y𝖣(algebraMap R S) x) = 0

Tactic:
rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, ← Finsupp.smul_single_one _ y]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
y : S
⊢ y • single ((algebraMap R S) x) 1 ∈ kerTotal R S

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
y : S
⊢ y • single ((algebraMap R S) x) 1 ∈ kerTotal R S

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span (Or.inr <| ⟨_, rfl⟩))

Result:
no goals