harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem replaceEntry_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k}
    (h : containsKey k l = false) : replaceEntry k v l = l

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
v : β k
h : containsKey k [] = false
⊢ replaceEntry k v [] = []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
k✝ : BEq α
k : α
v✝ : β k
v : (a : α) × β a
l : List ((a : α) × β a)
ih : containsKey k l = false → replaceEntry k v✝ l = l
h : (v.fst == k) = false ∧ containsKey k l = false
⊢ replaceEntry k v✝ (v :: l) = v :: l

Tactic:
rw [replaceEntry_cons_of_false h.1, ih h.2]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
k✝ : BEq α
k : α
v✝ : β k
v : (a : α) × β a
l : List ((a : α) × β a)
ih : containsKey k l = false → replaceEntry k v✝ l = l
h : containsKey k (v :: l) = false
⊢ replaceEntry k v✝ (v :: l) = v :: l

Tactic:
rw [containsKey_cons_eq_false] at h

Result:
α : Type u
β : α → Type v
k✝ : BEq α
k : α
v✝ : β k
v : (a : α) × β a
l : List ((a : α) × β a)
ih : containsKey k l = false → replaceEntry k v✝ l = l
h : (v.fst == k) = false ∧ containsKey k l = false
⊢ replaceEntry k v✝ (v :: l) = v :: l

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
v : β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : containsKey k tail✝ = false → replaceEntry k v tail✝ = tail✝
h : containsKey k (head✝ :: tail✝) = false
⊢ replaceEntry k v (head✝ :: tail✝) = head✝ :: tail✝

Tactic:
next k v l ih =>
rw [containsKey_cons_eq_false] at h
rw [replaceEntry_cons_of_false h.1, ih h.2]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = false
⊢ replaceEntry k v l = l

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
v : β k
h : containsKey k [] = false
⊢ replaceEntry k v [] = []

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
v : β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : containsKey k tail✝ = false → replaceEntry k v tail✝ = tail✝
h : containsKey k (head✝ :: tail✝) = false
⊢ replaceEntry k v (head✝ :: tail✝) = head✝ :: tail✝
-- Mathlib/Data/Nat/Bitwise.lean
/-- Note that the LHS is the expression used within `Std.BitVec.append`, hence the name. -/
lemma append_lt {x y n m} (hx : x < 2 ^ n) (hy : y < 2 ^ m) : y <<< n ||| x < 2 ^ (n + m)

Proof state:
case right
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ x < 2 ^ (n + m)

Tactic:
apply lt_of_lt_of_le hx <| Nat.pow_le_pow_right (le_succ _) (le_add_right _ _)

Result:
no goals

Proof state:
case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (n + m)

Tactic:
rw [add_comm]

Result:
case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (m + n)

Proof state:
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n ||| x < 2 ^ (n + m)

Tactic:
apply bitwise_lt_two_pow

Result:
case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (n + m)

case right
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ x < 2 ^ (n + m)

Proof state:
case left
x y n m : ℕ
hx : x < 2 ^ n
hy : y < 2 ^ m
⊢ y <<< n < 2 ^ (m + n)

Tactic:
apply shiftLeft_lt hy

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.not_iff_forall : ¬FiniteMultiplicity a b ↔ ∀ n : ℕ, a ^ n ∣ b :=
  ⟨fun h n =>
    Nat.casesOn n
      (by
        rw [_root_.pow_zero]
        exact one_dvd _)
      (by simpa [FiniteMultiplicity] using h),
    by simp [FiniteMultiplicity, multiplicity]; tauto⟩

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ (∀ (n : ℕ), a ^ n ∣ b) → ¬FiniteMultiplicity a b

Tactic:
simp [FiniteMultiplicity, multiplicity]

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ (∀ (n : ℕ), a ^ n ∣ b) → ∀ (x : ℕ), a ^ (x + 1) ∣ b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ ∀ (n : ℕ), a ^ n.succ ∣ b

Tactic:
simpa [FiniteMultiplicity] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ (∀ (n : ℕ), a ^ n ∣ b) → ∀ (x : ℕ), a ^ (x + 1) ∣ b

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ 1 ∣ b

Tactic:
exact one_dvd _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ a ^ zero ∣ b

Tactic:
rw [_root_.pow_zero]

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ 1 ∣ b
-- Mathlib/Algebra/Homology/BifunctorAssociator.lean
@[reassoc (attr := simp)]
lemma ι_D₂ :
    ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' =
      d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²³ : Category.{u_15, u_1} C₁
inst✝²² : Category.{u_17, u_2} C₂
inst✝²¹ : Category.{u_16, u_5} C₃
inst✝²⁰ : Category.{u_13, u_6} C₄
inst✝¹⁹ : Category.{u_14, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
⊢ ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' =
    d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'

Tactic:
simp [D₂]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
/--
If the image of `s` under `f` is finite, and each fiber of `f` has a finite intersection
with `s`, then `s` is itself finite.

It is useful to give `f` explicitly here so this can be used with `apply`.
-/
lemma Finite.of_finite_fibers (f : α → β) {s : Set α} (himage : (f '' s).Finite)
    (hfibers : ∀ x ∈ f '' s, (s ∩ f ⁻¹' {x}).Finite) : s.Finite :=
  (himage.biUnion hfibers).subset fun x ↦ by aesop

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
himage : (f '' s).Finite
hfibers : ∀ x ∈ f '' s, (s ∩ f ⁻¹' {x}).Finite
x : α
⊢ x ∈ s → x ∈ ⋃ i ∈ f '' s, s ∩ f ⁻¹' {i}

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_replicate {f : α → Option β} :
    (replicate n a).filterMap f = match f a with | none => [] | .some b => replicate n b

Proof state:
α : Type u_1
β : Type u_2
n : Nat
a : α
f : α → Option β
⊢ filterMap f (replicate n a) =
    match f a with
    | none => []
    | some b => replicate n b

Tactic:
induction n with
| zero => split <;> simp
| succ n ih =>
  simp only [replicate_succ, filterMap_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case succ
α : Type u_1
β : Type u_2
a : α
f : α → Option β
n : Nat
ih :
  filterMap f (replicate n a) =
    match f a with
    | none => []
    | some b => replicate n b
⊢ (match f a with
    | none => filterMap f (replicate n a)
    | some b => b :: filterMap f (replicate n a)) =
    match f a with
    | none => []
    | some b => b :: replicate n b

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case succ
α : Type u_1
β : Type u_2
a : α
f : α → Option β
n : Nat
ih :
  filterMap f (replicate n a) =
    match f a with
    | none => []
    | some b => replicate n b
⊢ filterMap f (replicate (n + 1) a) =
    match f a with
    | none => []
    | some b => replicate (n + 1) b

Tactic:
simp only [replicate_succ, filterMap_cons]

Result:
case succ
α : Type u_1
β : Type u_2
a : α
f : α → Option β
n : Nat
ih :
  filterMap f (replicate n a) =
    match f a with
    | none => []
    | some b => replicate n b
⊢ (match f a with
    | none => filterMap f (replicate n a)
    | some b => b :: filterMap f (replicate n a)) =
    match f a with
    | none => []
    | some b => b :: replicate n b

Proof state:
case zero
α : Type u_1
β : Type u_2
a : α
f : α → Option β
⊢ filterMap f (replicate 0 a) =
    match f a with
    | none => []
    | some b => replicate 0 b

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearPMap.lean
theorem IsClosable.graph_closure_eq_closure_graph {f : E →ₗ.[R] F} (hf : f.IsClosable) :
    f.graph.topologicalClosure = f.closure.graph

Proof state:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.graph.topologicalClosure = (Exists.choose hf).graph

Tactic:
exact hf.choose_spec

Result:
no goals

Proof state:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.graph.topologicalClosure = f.closure.graph

Tactic:
rw [closure_def hf]

Result:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.graph.topologicalClosure = (Exists.choose hf).graph
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblX_eq {P : Fin 3 → F} (hP : W.Equation P) (hPz : P z ≠ 0) : W.dblX P =
    ((eval P W.polynomialX ^ 2 - W.a₁ * eval P W.polynomialX * P z * (P y - W.negY P)
      - W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 - 2 * P x * P z * (P y - W.negY P) ^ 2)
      * (P y - W.negY P)) / P z

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
⊢ W.dblX P =
    ((eval P) W.polynomialX ^ 2 - W.a₁ * (eval P) W.polynomialX * P z * (P y - W.negY P) -
            W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
          2 * P x * P z * (P y - W.negY P) ^ 2) *
        (P y - W.negY P) /
      P z

Tactic:
rw [← dblX_eq' hP, mul_div_cancel_right₀ _ hPz]

Result:
no goals
-- Mathlib/Data/List/TakeWhile.lean
lemma find?_not_eq_head_dropWhile (h : ∃ x ∈ l, ¬p x) :
    l.find? (fun x ↦ ! (p x)) = some ((l.dropWhile p).head (by simpa using h))

Proof state:
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ find? (fun x => !p x) l = some ((dropWhile p l).head ⋯)

Tactic:
convert l.find?_eq_head_dropWhile_not ?_

Result:
case h.e'_3.h.e'_2.h.e'_2.h.e'_2.h
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
x✝ : α
⊢ p x✝ = !!p x✝

case convert_2
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ ∃ x, x ∈ l ∧ (!p x) = true

Proof state:
case convert_2
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ ∃ x, x ∈ l ∧ (!p x) = true

Tactic:
simpa using h

Result:
no goals

Proof state:
case h.e'_3.h.e'_2.h.e'_2.h.e'_2.h
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
x✝ : α
⊢ p x✝ = !!p x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ ¬p x = true
⊢ dropWhile p l ≠ []

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
/-- If `G ≤ H` then `G.degree v ≤ H.degree v` for any vertex `v`. -/
lemma degree_le_of_le {H : SimpleGraph V} [Fintype (H.neighborSet v)] (hle : G ≤ H) :
    G.degree v ≤ H.degree v

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
H : SimpleGraph V
inst✝ : Fintype ↑(H.neighborSet v)
hle : G ≤ H
⊢ Fintype.card ↑(G.neighborSet v) ≤ Fintype.card ↑(H.neighborSet v)

Tactic:
exact Set.card_le_card fun v hv => hle hv

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
H : SimpleGraph V
inst✝ : Fintype ↑(H.neighborSet v)
hle : G ≤ H
⊢ G.degree v ≤ H.degree v

Tactic:
simp_rw [← card_neighborSet_eq_degree]

Result:
V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
H : SimpleGraph V
inst✝ : Fintype ↑(H.neighborSet v)
hle : G ≤ H
⊢ Fintype.card ↑(G.neighborSet v) ≤ Fintype.card ↑(H.neighborSet v)
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_mul_right_add_right (m n k : ℕ) : Coprime m (k * m + n) ↔ Coprime m n

Proof state:
m n k : ℕ
⊢ m.Coprime (k * m + n) ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_mul_right_add_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList

Proof state:
α : Type u_1
i : Nat
a : Array α
h : i < a.size
⊢ a[i] ∈ a.toList

Tactic:
simp only [← getElem_toList, List.getElem_mem]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem oneCocycles_map_mul_of_isTrivial [A.IsTrivial] (f : oneCocycles A) (g h : G) :
    f (g * h) = f g + f h

Proof state:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : ↥(oneCocycles A)
g h : G
⊢ f (g * h) = f g + f h

Tactic:
rw [(mem_oneCocycles_iff f).1 f.2, isTrivial_apply A.ρ g (f h), add_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_intCast (z : ℤ) : fract (z : α) = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
⊢ fract ↑z = 0

Tactic:
unfold fract

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
⊢ ↑z - ↑⌊↑z⌋ = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
⊢ ↑z - ↑⌊↑z⌋ = 0

Tactic:
rw [floor_intCast]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
⊢ ↑z - ↑z = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
⊢ ↑z - ↑z = 0

Tactic:
exact sub_self _

Result:
no goals
-- Mathlib/MeasureTheory/Group/AEStabilizer.lean
@[to_additive]
lemma stabilizer_le_aestabilizer (s : Set α) : stabilizer G s ≤ aestabilizer G μ s

Proof state:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
⊢ stabilizer G s ≤ aestabilizer G μ s

Tactic:
intro g hg

Result:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
g : G
hg : g ∈ stabilizer G s
⊢ g ∈ aestabilizer G μ s

Proof state:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
g : G
hg : g ∈ stabilizer G s
⊢ g ∈ aestabilizer G μ s

Tactic:
simp_all

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem ext (I J : HasZeroMorphisms C) : I = J

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
⊢ Zero.zero = Zero.zero

Tactic:
have : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (I.zero X Y).zero := by
  apply I.zero_comp X (J.zero Y Y).zero

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero = Zero.zero

Proof state:
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
⊢ I = J

Tactic:
apply ext_aux

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
⊢ ∀ (X Y : C), Zero.zero = Zero.zero

Proof state:
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
⊢ Zero.zero ≫ Zero.zero = Zero.zero

Tactic:
apply I.zero_comp X (J.zero Y Y).zero

Result:
no goals

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
⊢ ∀ (X Y : C), Zero.zero = Zero.zero

Tactic:
intro X Y

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
⊢ Zero.zero = Zero.zero

Proof state:
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero ≫ Zero.zero = Zero.zero

Tactic:
apply J.comp_zero (I.zero X Y).zero Y

Result:
no goals

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero = Zero.zero

Tactic:
have that : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (J.zero X Y).zero := by
  apply J.comp_zero (I.zero X Y).zero Y

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
that : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero = Zero.zero

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
that : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero = Zero.zero

Tactic:
rw [← this, ← that]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forM_map [Monad m] [LawfulMonad m] (l : Array α) (g : α → β) (f : β → m PUnit) :
    forM (l.map g) f = forM l (fun a => f (g a))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
g : α → β
f : β → m PUnit
⊢ forM (map g l) f = forM l fun a => f (g a)

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : α → β
f : β → m PUnit
toList✝ : List α
⊢ forM (map g { toList := toList✝ }) f = forM { toList := toList✝ } fun a => f (g a)

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : α → β
f : β → m PUnit
toList✝ : List α
⊢ forM (map g { toList := toList✝ }) f = forM { toList := toList✝ } fun a => f (g a)

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bddAbove_image {s : Set Ordinal.{u}} (hf : BddAbove s)
    (f : Ordinal.{u} → Ordinal.{max u v}) : BddAbove (f '' s)

Proof state:
s : Set Ordinal.{u}
hf : BddAbove s
f : Ordinal.{u} → Ordinal.{max u v}
⊢ BddAbove (f '' s)

Tactic:
rw [bddAbove_iff_small] at hf ⊢

Result:
s : Set Ordinal.{u}
hf : Small.{u, u + 1} ↑s
f : Ordinal.{u} → Ordinal.{max u v}
⊢ Small.{max u v, (max u v) + 1} ↑(f '' s)

Proof state:
s : Set Ordinal.{u}
hf : Small.{u, u + 1} ↑s
f : Ordinal.{u} → Ordinal.{max u v}
⊢ Small.{max u v, (max u v) + 1} ↑(f '' s)

Tactic:
exact small_lift _

Result:
no goals
-- Mathlib/Probability/Kernel/Integral.lean
theorem integral_deterministic' (hg : Measurable g) (hf : StronglyMeasurable f) :
    ∫ x, f x ∂deterministic g hg a = f (g a)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
a : α
inst✝ : CompleteSpace E
g : α → β
hg : Measurable g
hf : StronglyMeasurable f
⊢ ∫ (x : β), f x ∂(deterministic g hg) a = f (g a)

Tactic:
rw [deterministic_apply, integral_dirac' _ _ hf]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Icc_sub_one_right_eq_Ico (a b : α) : Icc a (b - 1) = Ico a b

Proof state:
α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Icc_pred_right_eq_Ico a b

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Defs.lean
theorem sub_mem_iff_left (hy : y ∈ p) : x - y ∈ p ↔ x ∈ p

Proof state:
R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hy : y ∈ p
⊢ x - y ∈ p ↔ x ∈ p

Tactic:
rw [sub_eq_add_neg, p.add_mem_iff_left (p.neg_mem hy)]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma differentialIdeal_le_iff {I : Ideal B} (hI : I ≠ ⊥) [NoZeroSMulDivisors A B] :
    differentIdeal A B ≤ I ↔ (((I⁻¹ : FractionalIdeal B⁰ L) : Submodule B L).restrictScalars A).map
      ((Algebra.trace K L).restrictScalars A) ≤ 1 :=
  (FractionalIdeal.coeIdeal_le_coeIdeal _).symm.trans
    (differentialIdeal_le_fractionalIdeal_iff (I := (I : FractionalIdeal B⁰ L)) (by simpa))

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsDomain A
inst✝⁷ : IsFractionRing A K
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra.IsSeparable K L
inst✝⁴ : IsIntegralClosure B A L
inst✝³ : IsIntegrallyClosed A
inst✝² : IsDedekindDomain B
inst✝¹ : IsFractionRing B L
I : Ideal B
hI : I ≠ ⊥
inst✝ : NoZeroSMulDivisors A B
⊢ ↑I ≠ 0

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ici_add_one_eq_Ioi (a : α) : Ici (a + 1) = Ioi a

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Ici (a + 1) = Ioi a

Tactic:
simpa [succ_eq_add_one] using Ici_succ_eq_Ioi a

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
@[simp] lemma iSup_zero : ⨆ _ : ι, (0 : ℝ≥0∞) = 0

Proof state:
ι : Sort u_1
⊢ ⨆ x, 0 = 0

Tactic:
simp

Result:
no goals