harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_image_of_injOn {f : α → β} (hf : s.InjOn f) : Nat.card (f '' s) = Nat.card s

Proof state:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
this : Fintype ↑s
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
have := fintypeImage s f

Result:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
this✝ : Fintype ↑s
this : Fintype ↑(f '' s)
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Proof state:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
this✝ : Fintype ↑s
this : Fintype ↑(f '' s)
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
simp_rw [Nat.card_eq_fintype_card, Set.card_image_of_inj_on hf]

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
this✝ : Infinite ↑s
this : Infinite ↑(f '' s)
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
simp [Nat.card_eq_zero_of_infinite]

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
have := hs.fintype

Result:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
this : Fintype ↑s
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Proof state:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
have := hs.to_subtype

Result:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
this : Infinite ↑s
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
obtain hs | hs := s.finite_or_infinite

Result:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Proof state:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
this : Infinite ↑s
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
have := (hs.image hf).to_subtype

Result:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
this✝ : Infinite ↑s
this : Infinite ↑(f '' s)
⊢ Nat.card ↑(f '' s) = Nat.card ↑s
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem mk_leftInverse (hg : g.Monic) : Function.LeftInverse (mk g) (modByMonicHom hg)

Proof state:
R : Type u
inst✝ : CommRing R
g : R[X]
hg : g.Monic
f : AdjoinRoot g
⊢ (mk g) ((modByMonicHom hg) f) = f

Tactic:
induction f using AdjoinRoot.induction_on

Result:
case ih
R : Type u
inst✝ : CommRing R
g : R[X]
hg : g.Monic
p✝ : R[X]
⊢ (mk g) ((modByMonicHom hg) ((mk g) p✝)) = (mk g) p✝

Proof state:
case ih
R : Type u
inst✝ : CommRing R
g : R[X]
hg : g.Monic
p✝ : R[X]
⊢ (mk g) ((modByMonicHom hg) ((mk g) p✝)) = (mk g) p✝

Tactic:
rw [modByMonicHom_mk hg, mk_eq_mk, modByMonic_eq_sub_mul_div _ hg, sub_sub_cancel_left,
  dvd_neg]

Result:
case ih
R : Type u
inst✝ : CommRing R
g : R[X]
hg : g.Monic
p✝ : R[X]
⊢ g ∣ g * (p✝ /ₘ g)

Proof state:
R : Type u
inst✝ : CommRing R
g : R[X]
hg : g.Monic
⊢ Function.LeftInverse ⇑(mk g) ⇑(modByMonicHom hg)

Tactic:
intro f

Result:
R : Type u
inst✝ : CommRing R
g : R[X]
hg : g.Monic
f : AdjoinRoot g
⊢ (mk g) ((modByMonicHom hg) f) = f

Proof state:
case ih
R : Type u
inst✝ : CommRing R
g : R[X]
hg : g.Monic
p✝ : R[X]
⊢ g ∣ g * (p✝ /ₘ g)

Tactic:
apply dvd_mul_right

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem norm_cpow_le (z w : ℂ) : ‖z ^ w‖ ≤ ‖z‖ ^ w.re / Real.exp (arg z * im w)

Proof state:
case pos
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
exact (norm_cpow_of_imp h).le

Result:
no goals

Proof state:
case neg
z w : ℂ
h : z = 0 ∧ w.re = 0 ∧ w ≠ 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
z w : ℂ
h : ¬(z = 0 → w.re = 0 → w = 0)
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
push_neg at h

Result:
case neg
z w : ℂ
h : z = 0 ∧ w.re = 0 ∧ w ≠ 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Proof state:
z w : ℂ
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
by_cases h : z = 0 → w.re = 0 → w = 0

Result:
case pos
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

case neg
z w : ℂ
h : ¬(z = 0 → w.re = 0 → w = 0)
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem mem_twoCocycles_iff (f : G × G → A) :
    f ∈ twoCocycles A ↔ ∀ g h j : G,
      f (g * h, j) + f (g, h) =
        A.ρ g (f (h, j)) + f (g, h * j)

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A.V
⊢ f ∈ twoCocycles A ↔ ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)

Tactic:
simp_rw [mem_twoCocycles_def, sub_eq_zero, sub_add_eq_add_sub, sub_eq_iff_eq_add, eq_comm,
  add_comm (f (_ * _, _))]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem getLast_flatten {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
    (flatten L).getLast (by simpa using h) =
      (L.reverse.findSome? fun l => l.getLast?).get (by simpa using h)

Proof state:
α : Type u_1
L : List (List α)
h : ∃ l, l ∈ L ∧ l ≠ []
⊢ L.flatten.getLast ⋯ = (findSome? (fun l => l.getLast?) L.reverse).get ⋯

Tactic:
simp [getLast_eq_iff_getLast_eq_some, getLast?_flatten]

Result:
no goals

Proof state:
α : Type ?u.28608
L : List (List α)
h : ∃ l, l ∈ L ∧ l ≠ []
⊢ (findSome? (fun l => l.getLast?) L.reverse).isSome = true

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type ?u.28608
L : List (List α)
h : ∃ l, l ∈ L ∧ l ≠ []
⊢ L.flatten ≠ []

Tactic:
simpa using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldlM_start_stop {m} [Monad m] (l : Array α) (f : β → α → m β) (b) (start stop : Nat) :
    l.foldlM f b start stop = (l.extract start stop).foldlM f b

Proof state:
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
start stop : Nat
this :
  foldlM.loop f l (min stop l.size) ⋯ (min stop l.size - start) start b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ (min stop l.size - start) 0 b
⊢ (if h : stop ≤ l.size then foldlM.loop f l stop ⋯ (stop - start) start b
    else foldlM.loop f l l.size ⋯ (l.size - start) start b) =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ (min stop l.size - start) 0 b

Tactic:
split

Result:
case isTrue
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
start stop : Nat
this :
  foldlM.loop f l (min stop l.size) ⋯ (min stop l.size - start) start b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ (min stop l.size - start) 0 b
h✝ : stop ≤ l.size
⊢ foldlM.loop f l stop ⋯ (stop - start) start b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ (min stop l.size - start) 0 b

case isFalse
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
start stop : Nat
this :
  foldlM.loop f l (min stop l.size) ⋯ (min stop l.size - start) start b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ (min stop l.size - start) 0 b
h✝ : ¬stop ≤ l.size
⊢ foldlM.loop f l l.size ⋯ (l.size - start) start b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ (min stop l.size - start) 0 b

Proof state:
case isTrue
α : Type u_1
β : Type u_2
m : Type u_2 → Type u_3
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
start stop : Nat
this✝ :
  foldlM.loop f l (min stop l.size) ⋯ (min stop l.size - start) start b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ (min stop l.size - start) 0 b
h✝ : stop ≤ l.size
this : min stop l.size = stop
⊢ foldlM.loop f l stop ⋯ (stop - start) start b =
    foldlM.loop f (l.extract start stop) (min stop l.size - start) ⋯ (min stop l.size - start) 0 b

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Sigma/Basic.lean
theorem fst_injective [h : ∀ a, Subsingleton (β a)] : Injective (fst : (Σ a, β a) → α)

Proof state:
case mk.mk
α : Type u_1
β : α → Type u_4
h : ∀ (a : α), Subsingleton (β a)
a₁ : α
b₁ b₂ : β a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂⟩

Tactic:
exact congr_arg (mk a₁) <| Subsingleton.elim _ _

Result:
no goals

Proof state:
α : Type u_1
β : α → Type u_4
h : ∀ (a : α), Subsingleton (β a)
⊢ Injective fst

Tactic:
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (rfl : a₁ = a₂)

Result:
case mk.mk
α : Type u_1
β : α → Type u_4
h : ∀ (a : α), Subsingleton (β a)
a₁ : α
b₁ b₂ : β a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂⟩
-- Mathlib/GroupTheory/Nilpotent.lean
theorem normalizerCondition_of_isNilpotent [h : IsNilpotent G] : NormalizerCondition G

Proof state:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
hH' : H'.normalizer = H'
⊢ H = ⊤

Tactic:
apply map_injective_of_ker_le (mk' (center G)) hkh le_top

Result:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), H.normalizer = H → H = ⊤
H : Subgroup G
hH : H.normalizer = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
hH' : H'.normalizer = H'
⊢ Subgroup.map (mk' (center G)) H = Subgroup.map (mk' (center G)) ⊤
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero [HasOrthogonalProjection K]
    {v : E} (hv : v ∈ Kᗮ) : orthogonalProjection K v = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
hv : v ∈ Kᗮ
⊢ (orthogonalProjection K) v = 0

Tactic:
ext

Result:
case a
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
hv : v ∈ Kᗮ
⊢ ↑((orthogonalProjection K) v) = ↑0

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
hv : v ∈ Kᗮ
⊢ ↑((orthogonalProjection K) v) = ↑0

Tactic:
convert eq_orthogonalProjection_of_mem_orthogonal (K := K) _ _ <;> simp [hv]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem add_div_le_sum_sq_div_card (hst : s ⊆ t) (f : ι → 𝕜) (d : 𝕜) (hx : 0 ≤ x)
    (hs : x ≤ |(∑ i ∈ s, f i) / #s - (∑ i ∈ t, f i) / #t|) (ht : d ≤ ((∑ i ∈ t, f i) / #t) ^ 2) :
    d + #s / #t * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / #t

Proof state:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

Tactic:
apply (add_le_add_right ht _).trans

Result:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

Proof state:
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
⊢ |x| ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|

Tactic:
rwa [abs_of_nonneg hx]

Result:
no goals

Proof state:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
h₃ : ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑(#t)) i ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 * ↑(#t) + ∑ x ∈ t, (f x * ↑(#t) - ∑ i ∈ t, f i) ^ 2 / ↑(#t) ^ 2 ≤ ∑ i ∈ t, f i ^ 2

Tactic:
rw [div_pow, ← sum_div, ← mul_div_right_comm _ (#t : 𝕜), ← add_div,
  div_le_iff₀ (sq_pos_of_ne_zero htcard.ne')]

Result:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
h₃ : ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑(#t)) i ^ 2
⊢ (∑ i ∈ t, f i) ^ 2 * ↑(#t) + ∑ i ∈ t, (f i * ↑(#t) - ∑ i ∈ t, f i) ^ 2 ≤ (∑ i ∈ t, f i ^ 2) * ↑(#t) ^ 2
-- Mathlib/Analysis/Convex/Star.lean
theorem starConvex_sUnion {S : Set (Set E)} (hS : ∀ s ∈ S, StarConvex 𝕜 x s) :
    StarConvex 𝕜 x (⋃₀ S)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
S : Set (Set E)
hS : ∀ s ∈ S, StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
S : Set (Set E)
hS : ∀ s ∈ S, StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋃ i, ↑i)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
S : Set (Set E)
hS : ∀ s ∈ S, StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋃ i, ↑i)

Tactic:
exact starConvex_iUnion fun s => hS _ s.2

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem Heap.realSize_deleteMin {s : Heap α} (eq : s.deleteMin le = some (a, s')) :
    s.realSize = s'.realSize + 1

Proof state:
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
m : Nat
ih₁ : ∀ (s : Heap α), (before s).realSize = m + s.realSize
ih₂ : c.realSize + s.realSize + 1 = m + node.realSize + next.realSize + 1
⊢ (cons r a c s).realSize =
    (merge le { before := before, val := val, node := node, next := next }.node.toHeap
          ({ before := before, val := val, node := node, next := next }.before
            { before := before, val := val, node := node, next := next }.next)).realSize +
      1

Tactic:
rw [realSize, Nat.add_right_comm, ih₂]

Result:
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
m : Nat
ih₁ : ∀ (s : Heap α), (before s).realSize = m + s.realSize
ih₂ : c.realSize + s.realSize + 1 = m + node.realSize + next.realSize + 1
⊢ m + node.realSize + next.realSize + 1 =
    (merge le { before := before, val := val, node := node, next := next }.node.toHeap
          ({ before := before, val := val, node := node, next := next }.before
            { before := before, val := val, node := node, next := next }.next)).realSize +
      1

Proof state:
α : Type u_1
le : α → α → Bool
r : Nat
a : α
c : HeapNode α
s : Heap α
⊢ (∀ (s_1 : Heap α), ({ before := id, val := a, node := c, next := s }.before s_1).realSize = 0 + s_1.realSize) ∧
    c.realSize + s.realSize + 1 =
      0 + { before := id, val := a, node := c, next := s }.node.realSize +
          { before := id, val := a, node := c, next := s }.next.realSize +
        1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.sub_eq' [AddCommGroup α] [Neg β] (h : Antiperiodic f c) :
    f (c - x) = -f (-x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddCommGroup α
inst✝ : Neg β
h : Antiperiodic f c
⊢ f (c - x) = -f (-x)

Tactic:
simpa only [sub_eq_neg_add] using h (-x)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_mono_of_nonneg {f g : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hgi : Integrable g μ)
    (h : f ≤ᵐ[μ] g) : ∫ a, f a ∂μ ≤ ∫ a, g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ

Tactic:
by_cases hfm : AEStronglyMeasurable f μ

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfm : AEStronglyMeasurable f μ
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfm : ¬AEStronglyMeasurable f μ
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfm : ¬AEStronglyMeasurable f μ
⊢ 0 ≤ ∫ (a : α), g a ∂μ

Tactic:
exact integral_nonneg_of_ae (hf.trans h)

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfm : AEStronglyMeasurable f μ
⊢ HasFiniteIntegral f μ

Tactic:
refine hgi.hasFiniteIntegral.mono <| h.mp <| hf.mono fun x hf hfg => ?_

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf✝ : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfm : AEStronglyMeasurable f μ
x : α
hf : 0 x ≤ f x
hfg : f x ≤ g x
⊢ ‖f x‖ ≤ ‖g x‖

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf✝ : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfm : AEStronglyMeasurable f μ
x : α
hf : 0 x ≤ f x
hfg : f x ≤ g x
⊢ ‖f x‖ ≤ ‖g x‖

Tactic:
simpa [abs_of_nonneg hf, abs_of_nonneg (le_trans hf hfg)]

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfm : AEStronglyMeasurable f μ
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ

Tactic:
refine integral_mono_ae ⟨hfm, ?_⟩ hgi h

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfm : AEStronglyMeasurable f μ
⊢ HasFiniteIntegral f μ

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfm : ¬AEStronglyMeasurable f μ
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ

Tactic:
rw [integral_non_aestronglyMeasurable hfm]

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
hfm : ¬AEStronglyMeasurable f μ
⊢ 0 ≤ ∫ (a : α), g a ∂μ
-- Mathlib/Probability/Kernel/Composition/ParallelComp.lean
lemma swap_parallelComp {κ : Kernel α β} [IsSFiniteKernel κ]
    {η : Kernel γ δ} [IsSFiniteKernel η] :
    (swap β δ) ∘ₖ (κ ∥ₖ η) = (η ∥ₖ κ) ∘ₖ (swap α γ)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel γ δ
inst✝ : IsSFiniteKernel η
⊢ prodMkLeft α η ×ₖ prodMkRight γ κ = prodMkRight α η ×ₖ prodMkLeft γ κ ∘ₖ swap α γ

Tactic:
ext ac s hs

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel γ δ
inst✝ : IsSFiniteKernel η
ac : α × γ
s : Set (δ × β)
hs : MeasurableSet s
⊢ ((prodMkLeft α η ×ₖ prodMkRight γ κ) ac) s = ((prodMkRight α η ×ₖ prodMkLeft γ κ ∘ₖ swap α γ) ac) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel γ δ
inst✝ : IsSFiniteKernel η
ac : α × γ
s : Set (δ × β)
hs : MeasurableSet s
⊢ ((prodMkLeft α η ×ₖ prodMkRight γ κ) ac) s = ((prodMkRight α η ×ₖ prodMkLeft γ κ ∘ₖ swap α γ) ac) s

Tactic:
rw [comp_apply, swap_apply, Measure.bind_apply hs (Kernel.measurable _),
  lintegral_dirac' _ (Kernel.measurable_coe _ hs), prod_apply, prod_apply, prodMkLeft_apply,
  prodMkLeft_apply, prodMkRight_apply, prodMkRight_apply, Prod.fst_swap, Prod.snd_swap]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel γ δ
inst✝ : IsSFiniteKernel η
⊢ swap β δ ∘ₖ (κ ∥ₖ η) = η ∥ₖ κ ∘ₖ swap α γ

Tactic:
rw [parallelComp, swap_prod, parallelComp]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel γ δ
inst✝ : IsSFiniteKernel η
⊢ prodMkLeft α η ×ₖ prodMkRight γ κ = prodMkRight α η ×ₖ prodMkLeft γ κ ∘ₖ swap α γ
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem measurable_ereal_toENNReal : Measurable EReal.toENNReal :=
  EReal.measurable_of_measurable_real (by simpa using ENNReal.measurable_ofReal)

Proof state:
⊢ Measurable fun p => (↑p).toENNReal

Tactic:
simpa using ENNReal.measurable_ofReal

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addY_neg {P : Fin 3 → R} (hP : W'.Equation P) : W'.addY P (W'.neg P) = -W'.dblZ P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addY P (W'.neg P) = -W'.dblZ P

Tactic:
rw [addY, negY_eq, addX_neg, negAddY_neg hP, addZ_neg, mul_zero, sub_zero, mul_zero, sub_zero]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem Ideal.homogeneous_span (s : Set A) (h : ∀ x ∈ s, SetLike.IsHomogeneousElem 𝒜 x) :
    (Ideal.span s).IsHomogeneous 𝒜

Proof state:
case intro
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
z : { x // x ∈ s✝ }
hz1 : z ∈ s.support
⊢ ↑(((decompose 𝒜) (s z * ↑z)) i) ∈ span s✝

Tactic:
refine Ideal.mul_homogeneous_element_mem_of_mem 𝒜 (s z) z ?_ ?_ i

Result:
case intro.refine_1
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
z : { x // x ∈ s✝ }
hz1 : z ∈ s.support
⊢ IsHomogeneousElem 𝒜 ↑z

case intro.refine_2
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
s✝ : Set A
h : ∀ x ∈ s✝, IsHomogeneousElem 𝒜 x
i : ι
s : { x // x ∈ s✝ } →₀ A
z : { x // x ∈ s✝ }
hz1 : z ∈ s.support
⊢ ↑z ∈ span s✝
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_union_le_aleph0 {α} {P Q : Set α} :
    #(P ∪ Q : Set α) ≤ ℵ₀ ↔ #P ≤ ℵ₀ ∧ #Q ≤ ℵ₀

Proof state:
α : Type u_1
P Q : Set α
⊢ #↑(P ∪ Q) ≤ ℵ₀ ↔ #↑P ≤ ℵ₀ ∧ #↑Q ≤ ℵ₀

Tactic:
simp only [le_aleph0_iff_subtype_countable, mem_union, setOf_mem_eq, Set.union_def,
  ← countable_union]

Result:
no goals