harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
@[reassoc (attr := simp)]
lemma colimit_ι_zero_cokernel_desc {C : Type*} [Category C]
    [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : f ≫ g = 0) [HasCokernel f] :
    colimit.ι (parallelPair f 0) WalkingParallelPair.zero ≫ cokernel.desc f g h = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0
inst✝ : HasCokernel f
⊢ ((parallelPair f 0).map WalkingParallelPairHom.left ≫ colimit.ι (parallelPair f 0) one) ≫ cokernel.desc f g h = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0
inst✝ : HasCokernel f
⊢ colimit.ι (parallelPair f 0) zero ≫ cokernel.desc f g h = 0

Tactic:
rw [(colimit.w (parallelPair f 0) WalkingParallelPairHom.left).symm]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0
inst✝ : HasCokernel f
⊢ ((parallelPair f 0).map WalkingParallelPairHom.left ≫ colimit.ι (parallelPair f 0) one) ≫ cokernel.desc f g h = 0
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem blsub_type {α : Type u} (r : α → α → Prop) [IsWellOrder α r]
    (f : ∀ a < type r, Ordinal.{max u v}) :
    blsub.{_, v} (type r) f = lsub.{_, v} fun a => f (typein r a) (typein_lt_type _ _) :=
  eq_of_forall_ge_iff fun o => by
    rw [blsub_le_iff, lsub_le_iff]
    exact ⟨fun H b => H _ _, fun H i h => by simpa only [typein_enum] using H (enum r ⟨i, h⟩)⟩

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ (type r).blsub f ≤ o ↔ (lsub fun a => f ((typein r).toRelEmbedding a) ⋯) ≤ o

Tactic:
rw [blsub_le_iff, lsub_le_iff]

Result:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (h : i < type r), f i h < o) ↔ ∀ (i : α), f ((typein r).toRelEmbedding i) ⋯ < o

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (h : i < type r), f i h < o) ↔ ∀ (i : α), f ((typein r).toRelEmbedding i) ⋯ < o

Tactic:
exact ⟨fun H b => H _ _, fun H i h => by simpa only [typein_enum] using H (enum r ⟨i, h⟩)⟩

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
H : ∀ (i : α), f ((typein r).toRelEmbedding i) ⋯ < o
i : Ordinal.{u}
h : i < type r
⊢ f i h < o

Tactic:
simpa only [typein_enum] using H (enum r ⟨i, h⟩)

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean
/-- If a space of multilinear maps from `Π i, E i` to `F` is complete, and each `E i` has a nonzero
element, then `F` is complete. -/
lemma completeSpace_of_completeSpace_continuousMultilinearMap
    [CompleteSpace (ContinuousMultilinearMap 𝕜 M F)]
    {m : ∀ i, M i} (hm : ∀ i, m i ≠ 0) : CompleteSpace F

Proof state:
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
ι : Type u_6
inst✝⁴ : Finite ι
M : ι → Type u_7
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)
inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
⊢ CompleteSpace F

Tactic:
refine Metric.complete_of_cauchySeq_tendsto fun f hf => ?_

Result:
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
ι : Type u_6
inst✝⁴ : Finite ι
M : ι → Type u_7
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)
inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
f : ℕ → F
hf : CauchySeq f
⊢ ∃ a, Tendsto f atTop (𝓝 a)
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem numDenom_div (p : K[X]) {q : K[X]} (hq : q ≠ 0) :
    numDenom (algebraMap _ _ p / algebraMap _ _ q) =
      (Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q),
        Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))

Proof state:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).numDenom =
    (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q), C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))

Tactic:
rw [numDenom, liftOn'_div, if_neg hq]

Result:
case f0
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ∀ (p : K[X]),
    (if 0 = 0 then (0, 1)
      else
        let r := gcd p 0;
        (C (0 / r).leadingCoeff⁻¹ * (p / r), C (0 / r).leadingCoeff⁻¹ * (0 / r))) =
      if 1 = 0 then (0, 1)
      else
        let r := gcd 0 1;
        (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))

Proof state:
case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (if 0 = 0 then (0, 1)
    else
      let r := gcd p 0;
      (C (0 / r).leadingCoeff⁻¹ * (p / r), C (0 / r).leadingCoeff⁻¹ * (0 / r))) =
    if 1 = 0 then (0, 1)
    else
      let r := gcd 0 1;
      (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))

Tactic:
rw [if_pos rfl, if_neg (one_ne_zero' K[X])]

Result:
case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (0, 1) =
    let r := gcd 0 1;
    (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))

Proof state:
case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (0, 1) =
    let r := gcd 0 1;
    (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))

Tactic:
simp

Result:
no goals

Proof state:
case f0
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ∀ (p : K[X]),
    (if 0 = 0 then (0, 1)
      else
        let r := gcd p 0;
        (C (0 / r).leadingCoeff⁻¹ * (p / r), C (0 / r).leadingCoeff⁻¹ * (0 / r))) =
      if 1 = 0 then (0, 1)
      else
        let r := gcd 0 1;
        (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))

Tactic:
intro p

Result:
case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (if 0 = 0 then (0, 1)
    else
      let r := gcd p 0;
      (C (0 / r).leadingCoeff⁻¹ * (p / r), C (0 / r).leadingCoeff⁻¹ * (0 / r))) =
    if 1 = 0 then (0, 1)
    else
      let r := gcd 0 1;
      (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))
-- Mathlib/Order/KrullDimension.lean
lemma krullDim_le_one_iff_forall_isMax {α : Type*} [PartialOrder α] [OrderBot α] :
    krullDim α ≤ 1 ↔ ∀ x : α, x ≠ ⊥ → IsMax x

Proof state:
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ krullDim α ≤ 1 ↔ ∀ (x : α), x ≠ ⊥ → IsMax x

Tactic:
simp [krullDim_le_one_iff, ← or_iff_not_imp_left]

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem injective_toLp (p : ℝ≥0∞) (μ : Measure E

Proof state:
E : Type u_4
F : Type u_5
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : MeasurableSpace E
inst✝² : OpensMeasurableSpace E
inst✝¹ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
inst✝ : Measure.IsOpenPosMeasure μ
f g : 𝓢(E, F)
⊢ (fun f => f.toLp p μ) f = (fun f => f.toLp p μ) g → f = g

Tactic:
simpa [toLp] using (Continuous.ae_eq_iff_eq μ f.continuous g.continuous).mp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_or : eval .or = ((· ||| ·) : BitVec w → BitVec w → BitVec w)

Proof state:
w : Nat
⊢ or.eval = fun x1 x2 => x1 ||| x2

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma rightHomologyMap'_sub :
    rightHomologyMap' (φ - φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ -
      rightHomologyMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' (φ - φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ - rightHomologyMap' φ' h₁ h₂

Tactic:
simp only [sub_eq_add_neg, rightHomologyMap'_add, rightHomologyMap'_neg]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem lt_omega0_opow_succ {a b : Ordinal} : a < ω ^ succ b ↔ ∃ n : ℕ, a < ω ^ b * n

Proof state:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
⊢ ∃ n, a < ω ^ b * ↑n

Tactic:
obtain ⟨c, hc, n, hn⟩ := (lt_omega0_opow (succ_ne_zero b)).1 ha

Result:
case intro.intro.intro
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < succ b
n : ℕ
hn : a < ω ^ c * ↑n
⊢ ∃ n, a < ω ^ b * ↑n

Proof state:
a b : Ordinal.{u_1}
⊢ a < ω ^ succ b ↔ ∃ n, a < ω ^ b * ↑n

Tactic:
refine ⟨fun ha ↦ ?_, fun ⟨n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt (lt_succ b) n)⟩

Result:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
⊢ ∃ n, a < ω ^ b * ↑n

Proof state:
case intro.intro.intro
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < succ b
n : ℕ
hn : a < ω ^ c * ↑n
⊢ ∃ n, a < ω ^ b * ↑n

Tactic:
refine ⟨n, hn.trans_le (mul_le_mul_right' ?_ _)⟩

Result:
case intro.intro.intro
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < succ b
n : ℕ
hn : a < ω ^ c * ↑n
⊢ ω ^ c ≤ ω ^ b

Proof state:
case intro.intro.intro
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < succ b
n : ℕ
hn : a < ω ^ c * ↑n
⊢ ω ^ c ≤ ω ^ b

Tactic:
rwa [opow_le_opow_iff_right one_lt_omega0, ← lt_succ_iff]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem isCycle_finRotate {n : ℕ} : IsCycle (finRotate (n + 2))

Proof state:
n : ℕ
x : Fin (n + 2)
⊢ (finRotate (n + 2) ^ ↑↑x) 0 = x

Tactic:
obtain ⟨x, hx⟩ := x

Result:
case mk
n x : ℕ
hx : x < n + 2
⊢ (finRotate (n + 2) ^ ↑↑⟨x, hx⟩) 0 = ⟨x, hx⟩

Proof state:
case mk.zero
n : ℕ
hx : 0 < n + 2
⊢ ↑((finRotate (n + 2) ^ ↑⟨0, hx⟩) 0) = ↑⟨0, hx⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mk
n x : ℕ
hx : x < n + 2
⊢ (finRotate (n + 2) ^ ↑↑⟨x, hx⟩) 0 = ⟨x, hx⟩

Tactic:
rw [zpow_natCast, Fin.ext_iff, Fin.val_mk]

Result:
case mk
n x : ℕ
hx : x < n + 2
⊢ ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩

Proof state:
case mk.succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ (finRotate (n + 2) ^ x) 0 ≠ Fin.last (n + 1)

Tactic:
rw [Ne, Fin.ext_iff, ih (lt_trans x.lt_succ_self hx), Fin.val_last]

Result:
case mk.succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ ¬↑⟨x, ⋯⟩ = n + 1

Proof state:
case mk.succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ ¬↑⟨x, ⋯⟩ = n + 1

Tactic:
exact ne_of_lt (Nat.lt_of_succ_lt_succ hx)

Result:
no goals

Proof state:
n : ℕ
x : Fin (n + 2)
hx' : (finRotate (n + 2)) x ≠ x
⊢ (finRotate (n + 2) ^ ↑↑x) 0 = x

Tactic:
clear hx'

Result:
n : ℕ
x : Fin (n + 2)
⊢ (finRotate (n + 2) ^ ↑↑x) 0 = x

Proof state:
n : ℕ
⊢ (finRotate (n + 2)) 0 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case mk.succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ ↑((finRotate (n + 2) ^ ↑⟨x + 1, hx⟩) 0) = ↑⟨x + 1, hx⟩

Tactic:
rw [pow_succ', Perm.mul_apply, coe_finRotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)]

Result:
case mk.succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ (finRotate (n + 2) ^ x) 0 ≠ Fin.last (n + 1)

Proof state:
case mk
n x : ℕ
hx : x < n + 2
⊢ ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩

Tactic:
induction' x with x ih

Result:
case mk.zero
n : ℕ
hx : 0 < n + 2
⊢ ↑((finRotate (n + 2) ^ ↑⟨0, hx⟩) 0) = ↑⟨0, hx⟩

case mk.succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ ↑((finRotate (n + 2) ^ ↑⟨x + 1, hx⟩) 0) = ↑⟨x + 1, hx⟩

Proof state:
n : ℕ
⊢ (finRotate (n + 2)).IsCycle

Tactic:
refine ⟨0, by simp, fun x hx' => ⟨x, ?_⟩⟩

Result:
n : ℕ
x : Fin (n + 2)
hx' : (finRotate (n + 2)) x ≠ x
⊢ (finRotate (n + 2) ^ ↑↑x) 0 = x
-- Mathlib/Analysis/RCLike/Basic.lean
theorem abs_im_div_norm_le_one (z : K) : |im z / ‖z‖| ≤ 1

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z| / ‖z‖ ≤ 1

Tactic:
exact div_le_one_of_le₀ (abs_im_le_norm _) (norm_nonneg _)

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z / ‖z‖| ≤ 1

Tactic:
rw [abs_div, abs_norm]

Result:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z| / ‖z‖ ≤ 1
-- Mathlib/Topology/DerivedSet.lean
theorem AccPt.map {β : Type*} [TopologicalSpace β] {F : Filter X} {x : X}
    (h : AccPt x F) {f : X → β} (hf1 : ContinuousAt f x) (hf2 : Function.Injective f) :
    AccPt (f x) (map f F)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ AccPt (f x) (Filter.map f F)

Tactic:
apply map_neBot (m := f) (hf := h) |>.mono

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ Filter.map f (𝓝[≠] x ⊓ F) ≤ 𝓝[≠] f x ⊓ Filter.map f F

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ Filter.map f (𝓝[≠] x ⊓ F) ≤ 𝓝[≠] f x ⊓ Filter.map f F

Tactic:
rw [Filter.map_inf hf2]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ Filter.map f (𝓝[≠] x) ⊓ Filter.map f F ≤ 𝓝[≠] f x ⊓ Filter.map f F

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ Filter.map f (𝓝[≠] x) ⊓ Filter.map f F ≤ 𝓝[≠] f x ⊓ Filter.map f F

Tactic:
gcongr

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ Filter.map f (𝓝[≠] x) ≤ 𝓝[≠] f x

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ ∀ᶠ (x_1 : X) in 𝓝[≠] x, f x_1 ∈ {f x}ᶜ

Tactic:
simpa [hf2.eq_iff] using eventually_mem_nhdsWithin

Result:
no goals

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ Filter.map f (𝓝[≠] x) ≤ 𝓝[≠] f x

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hf1.continuousWithinAt

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ ∀ᶠ (x_1 : X) in 𝓝[≠] x, f x_1 ∈ {f x}ᶜ
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem isRegular_succ {c : Cardinal.{u}} (h : ℵ₀ ≤ c) : IsRegular (succ c) :=
  ⟨h.trans (le_succ c),
    succ_le_of_lt
      (by
        have αe := Cardinal.mk_out (succ c)
        set α := (succ c).out
        rcases ord_eq α with ⟨r, wo, re⟩
        have := isLimit_ord (h.trans (le_succ _))
        rw [← αe, re] at this ⊢
        rcases cof_eq' r this with ⟨S, H, Se⟩
        rw [← Se]
        apply lt_imp_lt_of_le_imp_le fun h => mul_le_mul_right' h c
        rw [mul_eq_self h, ← succ_le_iff, ← αe, ← sum_const']
        refine le_trans ?_ (sum_le_sum (fun (x : S) => card (typein r (x : α))) _ fun i => ?_)
        · simp only [← card_typein, ← mk_sigma]
          exact
            ⟨Embedding.ofSurjective (fun x => x.2.1) fun a =>
                let ⟨b, h, ab⟩ := H a
                ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩⟩
        · rw [← lt_succ_iff, ← lt_ord, ← αe, re]
          apply typein_lt_type)⟩

Proof state:
case intro.intro.intro.intro.refine_1
c : Cardinal.{u}
h : ℵ₀ ≤ c
α : Type u := Quotient.out (succ c)
αe : #α = succ c
r : α → α → Prop
wo : IsWellOrder α r
re : (#α).ord = type r
this : (type r).IsLimit
S : Set α
H : ∀ (a : α), ∃ b ∈ S, r a b
Se : #↑S = (type r).cof
⊢ #α ≤ #((i : ↑S) × { y // r y ↑i })

Tactic:
exact
  ⟨Embedding.ofSurjective (fun x => x.2.1) fun a =>
      let ⟨b, h, ab⟩ := H a
      ⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Pi.lean
theorem Integrable.fintype_prod_dep {ι : Type*} [Fintype ι] {E : ι → Type*}
    {f : (i : ι) → E i → 𝕜} [∀ i, MeasureSpace (E i)] [∀ i, SigmaFinite (volume : Measure (E i))]
    (hf : ∀ i, Integrable (f i)) :
    Integrable (fun (x : (i : ι) → E i) ↦ ∏ i, f i (x i))

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
ι : Type u_2
inst✝² : Fintype ι
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
inst✝¹ : (i : ι) → MeasureSpace (E i)
inst✝ : ∀ (i : ι), SigmaFinite volume
hf : ∀ (i : ι), Integrable (f i) volume
⊢ Integrable (fun x => ∏ i : ι, f i (x i)) volume

Tactic:
let e := (equivFin ι).symm

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
ι : Type u_2
inst✝² : Fintype ι
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
inst✝¹ : (i : ι) → MeasureSpace (E i)
inst✝ : ∀ (i : ι), SigmaFinite volume
hf : ∀ (i : ι), Integrable (f i) volume
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ Integrable (fun x => ∏ i : ι, f i (x i)) volume

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
ι : Type u_2
inst✝² : Fintype ι
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
inst✝¹ : (i : ι) → MeasureSpace (E i)
inst✝ : ∀ (i : ι), SigmaFinite volume
hf : ∀ (i : ι), Integrable (f i) volume
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ Integrable (fun x => ∏ x_1 : Fin (card ι), f (e x_1) (x x_1)) volume

Tactic:
exact .fin_nat_prod (fun i ↦ hf _)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
ι : Type u_2
inst✝² : Fintype ι
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
inst✝¹ : (i : ι) → MeasureSpace (E i)
inst✝ : ∀ (i : ι), SigmaFinite volume
hf : ∀ (i : ι), Integrable (f i) volume
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ Integrable (fun x => ∏ i : ι, f i (x i)) volume

Tactic:
simp_rw [← (volume_measurePreserving_piCongrLeft _ e).integrable_comp_emb
  (MeasurableEquiv.measurableEmbedding _),
  ← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Function.comp_def,
  Equiv.piCongrLeft_apply_apply]

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
ι : Type u_2
inst✝² : Fintype ι
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
inst✝¹ : (i : ι) → MeasureSpace (E i)
inst✝ : ∀ (i : ι), SigmaFinite volume
hf : ∀ (i : ι), Integrable (f i) volume
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ Integrable (fun x => ∏ x_1 : Fin (card ι), f (e x_1) (x x_1)) volume
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem tan_eq_zero_iff {θ : ℂ} : tan θ = 0 ↔ ∃ k : ℤ, k * π / 2 = θ

Proof state:
θ : ℂ
⊢ (∃ k, 2 * θ = ↑k * ↑π) ↔ ∃ k, ↑k * ↑π / 2 = θ

Tactic:
field_simp [mul_comm, eq_comm]

Result:
no goals

Proof state:
θ : ℂ
⊢ tan θ = 0 ↔ ∃ k, ↑k * ↑π / 2 = θ

Tactic:
rw [tan, div_eq_zero_iff, ← mul_eq_zero, ← mul_right_inj' two_ne_zero, mul_zero,
  ← mul_assoc, ← sin_two_mul, sin_eq_zero_iff]

Result:
θ : ℂ
⊢ (∃ k, 2 * θ = ↑k * ↑π) ↔ ∃ k, ↑k * ↑π / 2 = θ
-- Mathlib/CategoryTheory/Limits/Preserves/Presheaf.lean
theorem isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits
    [PreservesFiniteLimits A] : IsFiltered (CostructuredArrow yoneda A)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type v
inst✝ : PreservesFiniteLimits A
⊢ IsFiltered (CostructuredArrow yoneda A)

Tactic:
suffices IsCofiltered A.Elements from
  IsFiltered.of_equivalence (CategoryOfElements.costructuredArrowYonedaEquivalence _)

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type v
inst✝ : PreservesFiniteLimits A
⊢ IsCofiltered A.Elements

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type v
inst✝ : PreservesFiniteLimits A
⊢ HasFiniteLimits A.Elements

Tactic:
exact ⟨fun J _ _ => inferInstance⟩

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type v
inst✝ : PreservesFiniteLimits A
⊢ IsCofiltered A.Elements

Tactic:
suffices HasFiniteLimits A.Elements from IsCofiltered.of_hasFiniteLimits A.Elements

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type v
inst✝ : PreservesFiniteLimits A
⊢ HasFiniteLimits A.Elements
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma comap_id (κ : Kernel α β) : comap κ id measurable_id = κ

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ (κ (id a)) s✝ = (κ a) s✝

Tactic:
simp

Result:
no goals

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.comap id ⋯) a) s✝ = (κ a) s✝

Tactic:
rw [comap_apply]

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ (κ (id a)) s✝ = (κ a) s✝

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ κ.comap id ⋯ = κ

Tactic:
ext a

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.comap id ⋯) a) s✝ = (κ a) s✝
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma comp_neg (α : Ext X Y n) {m : ℕ} (β : Ext Y Z m) {p : ℕ} (h : n + m = p) :
    α.comp (-β) h = -α.comp β h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
⊢ α.comp (-β) h = -α.comp β h

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp (-β) h = -α.comp β h

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (α.comp (-β) h).hom = (-α.comp β h).hom

Tactic:
simp [this, neg_hom']

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp (-β) h = -α.comp β h

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (α.comp (-β) h).hom = (-α.comp β h).hom