harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/WithDensity.lean
theorem withDensity_tsum [Countable ι] (κ : Kernel α β) [IsSFiniteKernel κ] {f : ι → α → β → ℝ≥0∞}
    (hf : ∀ i, Measurable (Function.uncurry (f i))) :
    withDensity κ (∑' n, f n) = Kernel.sum fun n => withDensity κ (f n)

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
⊢ Function.uncurry (∑' (n : ι), f n) p = (∑' (n : ι), Function.uncurry (f n)) p

Tactic:
simp only [Function.uncurry_def]

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
⊢ (∑' (n : ι), f n) p.1 p.2 = (∑' (n : ι), fun p => f n p.1 p.2) p

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable (Function.uncurry (∑' (n : ι), f n))

Tactic:
have : Function.uncurry (∑' n, f n) = ∑' n, Function.uncurry (f n) := by
  ext1 p
  simp only [Function.uncurry_def]
  rw [tsum_apply h_sum, tsum_apply (h_sum_a _), tsum_apply]
  exact Pi.summable.mpr fun p => ENNReal.summable

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
this : Function.uncurry (∑' (n : ι), f n) = ∑' (n : ι), Function.uncurry (f n)
⊢ Measurable (Function.uncurry (∑' (n : ι), f n))

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n => f n a
h_sum : Summable fun n => f n
a : α
s : Set β
hs : MeasurableSet s
b : β
⊢ (∑' (n : ι), f n) a b = ∑' (n : ι), (fun b => f n a b) b

Tactic:
rw [tsum_apply h_sum, tsum_apply (h_sum_a a)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem drop_eq_nil_of_le {as : List α} {i : Nat} (h : as.length ≤ i) : as.drop i = []

Proof state:
α : Type u
as : List α
i✝ i : Nat
h : nil.length ≤ i
⊢ drop i nil = nil

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
as : List α
i : Nat
h : as.length ≤ i
⊢ drop i as = nil

Tactic:
match as, i with
| [],    i   => simp
| _::_,  0   => simp at h
| _::as, i+1 => simp only [length_cons] at h; exact @drop_eq_nil_of_le as i (Nat.le_of_succ_le_succ h)

Result:
no goals

Proof state:
α : Type u
as✝ : List α
i✝ : Nat
head✝ : α
as : List α
i : Nat
h : as.length + 1 ≤ i + 1
⊢ drop (i + 1) (head✝ :: as) = nil

Tactic:
exact @drop_eq_nil_of_le as i (Nat.le_of_succ_le_succ h)

Result:
no goals

Proof state:
α : Type u
as : List α
i : Nat
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length ≤ 0
⊢ drop 0 (head✝ :: tail✝) = nil

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u
as✝ : List α
i✝ : Nat
head✝ : α
as : List α
i : Nat
h : (head✝ :: as).length ≤ i + 1
⊢ drop (i + 1) (head✝ :: as) = nil

Tactic:
simp only [length_cons] at h

Result:
α : Type u
as✝ : List α
i✝ : Nat
head✝ : α
as : List α
i : Nat
h : as.length + 1 ≤ i + 1
⊢ drop (i + 1) (head✝ :: as) = nil
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem findIdx_take {xs : List α} {n : Nat} {p : α → Bool} :
    (xs.take n).findIdx p = min n (xs.findIdx p)

Proof state:
case nil
α : Type u_1
p : α → Bool
n : Nat
⊢ findIdx p (take n []) = min n (findIdx p [])

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx p (take n xs) = min n (findIdx p xs)
n✝ : Nat
h✝ : ¬p x = true
⊢ min n✝ (findIdx p xs) + 1 = min (n✝ + 1) (findIdx p xs + 1)

Tactic:
rw [Nat.add_min_add_right]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx p (take n xs) = min n (findIdx p xs)
n : Nat
⊢ findIdx p (take n (x :: xs)) = min n (findIdx p (x :: xs))

Tactic:
cases n

Result:
case cons.zero
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx p (take n xs) = min n (findIdx p xs)
⊢ findIdx p (take 0 (x :: xs)) = min 0 (findIdx p (x :: xs))

case cons.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx p (take n xs) = min n (findIdx p xs)
n✝ : Nat
⊢ findIdx p (take (n✝ + 1) (x :: xs)) = min (n✝ + 1) (findIdx p (x :: xs))

Proof state:
case cons.succ.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx p (take n xs) = min n (findIdx p xs)
n✝ : Nat
h✝ : p x = true
⊢ 0 = min (n✝ + 1) 0

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx p (take n xs) = min n (findIdx p xs)
n✝ : Nat
⊢ findIdx p (take (n✝ + 1) (x :: xs)) = min (n✝ + 1) (findIdx p (x :: xs))

Tactic:
simp only [take_succ_cons, findIdx_cons, ih, cond_eq_if]

Result:
case cons.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx p (take n xs) = min n (findIdx p xs)
n✝ : Nat
⊢ (if p x = true then 0 else min n✝ (findIdx p xs) + 1) = min (n✝ + 1) (if p x = true then 0 else findIdx p xs + 1)

Proof state:
case cons.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx p (take n xs) = min n (findIdx p xs)
n✝ : Nat
⊢ (if p x = true then 0 else min n✝ (findIdx p xs) + 1) = min (n✝ + 1) (if p x = true then 0 else findIdx p xs + 1)

Tactic:
split

Result:
case cons.succ.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx p (take n xs) = min n (findIdx p xs)
n✝ : Nat
h✝ : p x = true
⊢ 0 = min (n✝ + 1) 0

case cons.succ.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx p (take n xs) = min n (findIdx p xs)
n✝ : Nat
h✝ : ¬p x = true
⊢ min n✝ (findIdx p xs) + 1 = min (n✝ + 1) (findIdx p xs + 1)

Proof state:
case cons.zero
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx p (take n xs) = min n (findIdx p xs)
⊢ findIdx p (take 0 (x :: xs)) = min 0 (findIdx p (x :: xs))

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/RightDerived.lean
theorem NatTrans.rightDerived_comp {F G H : C ⥤ D} [F.Additive] [G.Additive] [H.Additive]
    (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) :
    NatTrans.rightDerived (α ≫ β) n = NatTrans.rightDerived α n ≫ NatTrans.rightDerived β n

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_1
inst✝⁶ : Category.{u_2, u_1} D
inst✝⁵ : Abelian C
inst✝⁴ : HasInjectiveResolutions C
inst✝³ : Abelian D
F G H : C ⥤ D
inst✝² : F.Additive
inst✝¹ : G.Additive
inst✝ : H.Additive
α : F ⟶ G
β : G ⟶ H
n : ℕ
⊢ rightDerived (α ≫ β) n = rightDerived α n ≫ rightDerived β n

Tactic:
simp [NatTrans.rightDerived]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
    (h : m.WF) {l : List ((a : α) × β a)} {k : α}
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (m.insertMany l).getKey! k = m.getKey! k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List ((a : α) × β a)
k : α
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (m.insertMany l).getKey! k = m.getKey! k

Tactic:
simp_to_raw using Raw₀.getKey!_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem _root_.Real.list_prod_map_rpow' {ι} (l : List ι) (f : ι → ℝ)
    (hl : ∀ i ∈ l, (0 : ℝ) ≤ f i) (r : ℝ) :
    (l.map (f · ^ r)).prod = (l.map f).prod ^ r

Proof state:
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ (List.map (fun x => f x ^ r) l).prod = (List.map ((fun x => x ^ r) ∘ f) l).prod

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ (List.map (fun x => f x ^ r) l).prod = (List.map f l).prod ^ r

Tactic:
rw [← Real.list_prod_map_rpow (l.map f) _ r, List.map_map]

Result:
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ (List.map (fun x => f x ^ r) l).prod = (List.map ((fun x => x ^ r) ∘ f) l).prod

ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ ∀ x ∈ List.map f l, 0 ≤ x

Proof state:
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ ∀ x ∈ List.map f l, 0 ≤ x

Tactic:
simpa using hl

Result:
no goals
-- Mathlib/RingTheory/SurjectiveOnStalks.lean
lemma surjectiveOnStalks_of_isLocalization
    [Algebra R S] [IsLocalization M S] :
    SurjectiveOnStalks (algebraMap R S)

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ (algebraMap R S).SurjectiveOnStalks

Tactic:
refine surjectiveOnStalks_of_exists_div fun s ↦ ?_

Result:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
s : S
⊢ ∃ r s_1, IsUnit ((algebraMap R S) s_1) ∧ (algebraMap R S) s_1 * s = (algebraMap R S) r

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
⊢ ∃ r s_1, IsUnit ((algebraMap R S) s_1) ∧ (algebraMap R S) s_1 * IsLocalization.mk' S x s = (algebraMap R S) r

Tactic:
exact ⟨x, s, IsLocalization.map_units S s, IsLocalization.mk'_spec' S x s⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
s : S
⊢ ∃ r s_1, IsUnit ((algebraMap R S) s_1) ∧ (algebraMap R S) s_1 * s = (algebraMap R S) r

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective M s

Result:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
⊢ ∃ r s_1, IsUnit ((algebraMap R S) s_1) ∧ (algebraMap R S) s_1 * IsLocalization.mk' S x s = (algebraMap R S) r
-- Mathlib/Algebra/Order/Field/Basic.lean
private lemma exists_mul_left_lt₀ {a b c : α} (hc : a * b < c) : ∃ a' > a, a' * b < c

Proof state:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : a * b < c
hb : b ≤ 0
⊢ ∃ a' > a, a' * b < c

Tactic:
obtain ⟨a', ha'⟩ := exists_gt a

Result:
case inl.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : a * b < c
hb : b ≤ 0
a' : α
ha' : a < a'
⊢ ∃ a' > a, a' * b < c

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : a * b < c
⊢ ∃ a' > a, a' * b < c

Tactic:
rcases le_or_lt b 0 with hb | hb

Result:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : a * b < c
hb : b ≤ 0
⊢ ∃ a' > a, a' * b < c

case inr
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : a * b < c
hb : 0 < b
⊢ ∃ a' > a, a' * b < c

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : a * b < c
hb : 0 < b
⊢ ∃ a' > a, a' * b < c

Tactic:
obtain ⟨a', ha', hc'⟩ := exists_between ((lt_div_iff₀ hb).2 hc)

Result:
case inr.intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : a * b < c
hb : 0 < b
a' : α
ha' : a < a'
hc' : a' < c / b
⊢ ∃ a' > a, a' * b < c

Proof state:
case inl.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : a * b < c
hb : b ≤ 0
a' : α
ha' : a < a'
⊢ ∃ a' > a, a' * b < c

Tactic:
exact ⟨a', ha', hc.trans_le' (antitone_mul_right hb ha'.le)⟩

Result:
no goals

Proof state:
case inr.intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : a * b < c
hb : 0 < b
a' : α
ha' : a < a'
hc' : a' < c / b
⊢ ∃ a' > a, a' * b < c

Tactic:
exact ⟨a', ha', (lt_div_iff₀ hb).1 hc'⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem scaleRoots_aeval_eq_zero [Algebra R A] {p : R[X]} {a : A} {r : R} (ha : aeval a p = 0) :
    aeval (algebraMap R A r * a) (scaleRoots p r) = 0

Proof state:
case hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ ∀ (s₁ s₂ : R), Commute ((algebraMap R A) s₁) ((algebraMap R A) s₂)

Tactic:
intros

Result:
case hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
s₁✝ s₂✝ : R
⊢ Commute ((algebraMap R A) s₁✝) ((algebraMap R A) s₂✝)

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ (aeval ((algebraMap R A) r * a)) (p.scaleRoots r) = 0

Tactic:
rw [aeval_def, scaleRoots_eval₂_mul_of_commute, ← aeval_def, ha, mul_zero]

Result:
case hsa
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ Commute ((algebraMap R A) r) a

case hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ ∀ (s₁ s₂ : R), Commute ((algebraMap R A) s₁) ((algebraMap R A) s₂)

Proof state:
case hsa
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ Commute ((algebraMap R A) r) a

Tactic:
apply Algebra.commutes

Result:
no goals

Proof state:
case hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
s₁✝ s₂✝ : R
⊢ Commute ((algebraMap R A) s₁✝) ((algebraMap R A) s₂✝)

Tactic:
rw [Commute, SemiconjBy, ← map_mul, ← map_mul, mul_comm]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem le_boundedBy' {μ : OuterMeasure α} :
    μ ≤ boundedBy m ↔ ∀ s : Set α, s.Nonempty → μ s ≤ m s

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ μ ≤ boundedBy m ↔ ∀ (s : Set α), s.Nonempty → μ s ≤ m s

Tactic:
rw [le_boundedBy, forall_congr']

Result:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ ∀ (a : Set α), μ a ≤ m a ↔ a.Nonempty → μ a ≤ m a

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ ∀ (a : Set α), μ a ≤ m a ↔ a.Nonempty → μ a ≤ m a

Tactic:
intro s

Result:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
⊢ μ s ≤ m s ↔ s.Nonempty → μ s ≤ m s

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
⊢ μ s ≤ m s ↔ s.Nonempty → μ s ≤ m s

Tactic:
rcases s.eq_empty_or_nonempty with h | h <;> simp [h]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem pbind_eq_some {f : ∀ a : α, a ∈ x → Option β} {y : β} :
    x.pbind f = some y ↔ ∃ (z : α) (H : z ∈ x), f z H = some y

Proof state:
case some
α : Type u_1
β : Type u_2
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ (∃ z H, f z H = some y) → f x ⋯ = some y

Tactic:
rintro ⟨z, H, hz⟩

Result:
case some.intro.intro
α : Type u_1
β : Type u_2
y : β
x : α
f : (a : α) → a ∈ some x → Option β
z : α
H : z ∈ some x
hz : f z H = some y
⊢ f x ⋯ = some y

Proof state:
case some.intro.intro
α : Type u_1
β : Type u_2
y : β
x : α
f : (a : α) → a ∈ some x → Option β
z : α
H✝ : z ∈ some x
hz : f z H✝ = some y
H : x = z
⊢ f x ⋯ = some y

Tactic:
simpa [H] using hz

Result:
no goals

Proof state:
case some.intro.intro
α : Type u_1
β : Type u_2
y : β
x : α
f : (a : α) → a ∈ some x → Option β
z : α
H : z ∈ some x
hz : f z H = some y
⊢ f x ⋯ = some y

Tactic:
simp only [mem_def, Option.some_inj] at H

Result:
case some.intro.intro
α : Type u_1
β : Type u_2
y : β
x : α
f : (a : α) → a ∈ some x → Option β
z : α
H✝ : z ∈ some x
hz : f z H✝ = some y
H : x = z
⊢ f x ⋯ = some y

Proof state:
case some
α : Type u_1
β : Type u_2
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ (some x).pbind f = some y ↔ ∃ z H, f z H = some y

Tactic:
simp only [pbind]

Result:
case some
α : Type u_1
β : Type u_2
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ f x ⋯ = some y ↔ ∃ z H, f z H = some y

Proof state:
α : Type u_1
β : Type u_2
x : Option α
f : (a : α) → a ∈ x → Option β
y : β
⊢ x.pbind f = some y ↔ ∃ z H, f z H = some y

Tactic:
rcases x with (_|x)

Result:
case none
α : Type u_1
β : Type u_2
y : β
f : (a : α) → a ∈ none → Option β
⊢ none.pbind f = some y ↔ ∃ z H, f z H = some y

case some
α : Type u_1
β : Type u_2
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ (some x).pbind f = some y ↔ ∃ z H, f z H = some y

Proof state:
case none
α : Type u_1
β : Type u_2
y : β
f : (a : α) → a ∈ none → Option β
⊢ none.pbind f = some y ↔ ∃ z H, f z H = some y

Tactic:
simp

Result:
no goals

Proof state:
case some
α : Type u_1
β : Type u_2
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ f x ⋯ = some y ↔ ∃ z H, f z H = some y

Tactic:
refine ⟨fun h ↦ ⟨x, rfl, h⟩, ?_⟩

Result:
case some
α : Type u_1
β : Type u_2
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ (∃ z H, f z H = some y) → f x ⋯ = some y
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem factorial_mul_factorial_dvd_factorial_add (i j : ℕ) : i ! * j ! ∣ (i + j)!

Proof state:
i j : ℕ
this : i ! * (i + j - i)! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!

Tactic:
rwa [Nat.add_sub_cancel_left i j] at this

Result:
no goals

Proof state:
i j : ℕ
⊢ i ! * j ! ∣ (i + j)!

Tactic:
suffices i ! * (i + j - i) ! ∣ (i + j)! by
  rwa [Nat.add_sub_cancel_left i j] at this

Result:
i j : ℕ
⊢ i ! * (i + j - i)! ∣ (i + j)!

Proof state:
i j : ℕ
⊢ i ! * (i + j - i)! ∣ (i + j)!

Tactic:
exact factorial_mul_factorial_dvd_factorial (Nat.le_add_right _ _)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem circleIntegral_def_Icc (f : ℂ → E) (c : ℂ) (R : ℝ) :
    (∮ z in C(c, R), f z) = ∫ θ in Icc 0 (2 * π),
    deriv (circleMap c R) θ • f (circleMap c R θ)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ (∮ (z : ℂ) in C(c, R), f z) = ∫ (θ : ℝ) in Icc 0 (2 * π), deriv (circleMap c R) θ • f (circleMap c R θ)

Tactic:
rw [circleIntegral, intervalIntegral.integral_of_le Real.two_pi_pos.le,
  Measure.restrict_congr_set Ioc_ae_eq_Icc]

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Operations.lean
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : M →ₙ* N) (hf : Function.Injective f)
    (s : ι → Subsemigroup M) : (iInf s).map f = ⨅ i, (s i).map f

Proof state:
M : Type u_1
N : Type u_2
inst✝² : Mul M
inst✝¹ : Mul N
ι : Sort u_5
inst✝ : Nonempty ι
f : M →ₙ* N
hf : Function.Injective ⇑f
s : ι → Subsemigroup 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✝² : Mul M
inst✝¹ : Mul N
ι : Sort u_5
inst✝ : Nonempty ι
f : M →ₙ* N
hf : Function.Injective ⇑f
s : ι → Subsemigroup M
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Proof state:
case a
M : Type u_1
N : Type u_2
inst✝² : Mul M
inst✝¹ : Mul N
ι : Sort u_5
inst✝ : Nonempty ι
f : M →ₙ* N
hf : Function.Injective ⇑f
s : ι → Subsemigroup 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/Algebra/Group/Semiconj/Defs.lean
theorem pow_right {a x y : M} (h : SemiconjBy a x y) (n : ℕ) : SemiconjBy a (x ^ n) (y ^ n)

Proof state:
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ n) (y ^ n)

Tactic:
induction n with
| zero =>
  rw [pow_zero, pow_zero]
  exact SemiconjBy.one_right _
| succ n ih =>
  rw [pow_succ, pow_succ]
  exact ih.mul_right h

Result:
no goals

Proof state:
case succ
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ]

Result:
case succ
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ n * x) (y ^ n * y)

Proof state:
case zero
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 1

Tactic:
exact SemiconjBy.one_right _

Result:
no goals

Proof state:
case zero
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a (x ^ 0) (y ^ 0)

Tactic:
rw [pow_zero, pow_zero]

Result:
case zero
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a 1 1

Proof state:
case succ
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
ih : SemiconjBy a (x ^ n) (y ^ n)
⊢ SemiconjBy a (x ^ n * x) (y ^ n * y)

Tactic:
exact ih.mul_right h

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
/-- If `prodComparison F A B` is an isomorphism for all `A B` then `F` preserves limits of shape
`Discrete (WalkingPair)`. -/
lemma preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison
    [∀ A B, IsIso (prodComparison F A B)] : PreservesLimitsOfShape (Discrete WalkingPair) F

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F

Tactic:
constructor

Result:
case preservesLimit
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
⊢ autoParam (∀ {K : Discrete WalkingPair ⥤ C}, PreservesLimit K F) _auto✝

Proof state:
case preservesLimit
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
⊢ autoParam (∀ {K : Discrete WalkingPair ⥤ C}, PreservesLimit K F) _auto✝

Tactic:
intro K

Result:
case preservesLimit
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
K : Discrete WalkingPair ⥤ C
⊢ PreservesLimit K F

Proof state:
case preservesLimit
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
K : Discrete WalkingPair ⥤ C
⊢ PreservesLimit (pair (K.obj { as := WalkingPair.left }) (K.obj { as := WalkingPair.right })) F

Tactic:
apply preservesLimit_pair_of_isIso_prodComparison

Result:
no goals

Proof state:
case preservesLimit
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
K : Discrete WalkingPair ⥤ C
⊢ PreservesLimit K F

Tactic:
refine @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoPair K).symm ?_

Result:
case preservesLimit
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
K : Discrete WalkingPair ⥤ C
⊢ PreservesLimit (pair (K.obj { as := WalkingPair.left }) (K.obj { as := WalkingPair.right })) F
-- Mathlib/Computability/TMConfig.lean
theorem zero_eval (v) : zero.eval v = pure [0]

Proof state:
v : List ℕ
⊢ zero.eval v = pure [0]

Tactic:
simp [zero]

Result:
no goals