harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem of_mono_eq_zero {X Y : C} (f : X ⟶ Y) [Mono f] (h : f = 0) : IsZero X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Mono 0
⊢ IsZero X

Tactic:
apply of_mono_zero X Y

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : f = 0
⊢ IsZero X

Tactic:
subst h

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Mono 0
⊢ IsZero X
-- Mathlib/RingTheory/AdicCompletion/Algebra.lean
theorem val_smul_eq_evalₐ_smul (n : ℕ) (r : AdicCompletion I R)
    (x : M ⧸ (I ^ n • ⊤ : Submodule R M)) : r.val n • x = evalₐ I n r • x

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
r : AdicCompletion I R
x : M ⧸ I ^ n • ⊤
⊢ ↑r n • x = (evalₐ I n) r • x

Tactic:
apply induction_on I R r (fun r ↦ ?_)

Result:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
r✝ : AdicCompletion I R
x : M ⧸ I ^ n • ⊤
r : AdicCauchySequence I R
⊢ ↑((mk I R) r) n • x = (evalₐ I n) ((mk I R) r) • x

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
r✝ : AdicCompletion I R
x : M ⧸ I ^ n • ⊤
r : AdicCauchySequence I R
⊢ ↑((mk I R) r) n • x = (evalₐ I n) ((mk I R) r) • x

Tactic:
exact Quotient.inductionOn' x (fun x ↦ rfl)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Gamma.lean
theorem integral_exp_neg_mul_rpow {p b : ℝ} (hp : 0 < p) (hb : 0 < b) :
    ∫ x in Ioi (0 : ℝ), exp (- b * x ^ p) = b ^ (- 1 / p) * Gamma (1 / p + 1)

Proof state:
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ p) = b ^ (-1 / p) * Gamma (1 / p + 1)

Tactic:
convert (integral_rpow_mul_exp_neg_mul_rpow hp neg_one_lt_zero hb) using 1

Result:
case h.e'_2
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ 0 * rexp (-b * x ^ p)

case h.e'_3
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-(0 + 1) / p) * (1 / p) * Gamma ((0 + 1) / p)

Proof state:
case h.e'_3
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-(0 + 1) / p) * (1 / p) * Gamma ((0 + 1) / p)

Tactic:
rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp)), mul_assoc]

Result:
no goals

Proof state:
case h.e'_2
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ 0 * rexp (-b * x ^ p)

Tactic:
simp_rw [rpow_zero, one_mul]

Result:
no goals
-- Mathlib/Order/OrderIsoNat.lean
theorem not_acc_of_decreasing_seq (f : ((· > ·) : ℕ → ℕ → Prop) ↪r r) (k : ℕ) : ¬Acc r (f k)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 => x1 > x2) ↪r r
k : ℕ
⊢ Nonempty { f_1 // f k ∈ Set.range ⇑f_1 }

Tactic:
exact ⟨⟨f, k, rfl⟩⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 => x1 > x2) ↪r r
k : ℕ
⊢ ¬Acc r (f k)

Tactic:
rw [acc_iff_no_decreasing_seq, not_isEmpty_iff]

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 => x1 > x2) ↪r r
k : ℕ
⊢ Nonempty { f_1 // f k ∈ Set.range ⇑f_1 }
-- Mathlib/SetTheory/Game/Nim.lean
theorem toRightMovesNim_one_symm (i) :
    (@toRightMovesNim 1).symm i = ⟨0, Set.mem_Iio.mpr zero_lt_one⟩

Proof state:
i : (nim 1).RightMoves
⊢ toRightMovesNim.symm i = ⟨0, ⋯⟩

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
lemma set_mul_subset {s : Set R} {I : TwoSidedIdeal R} (h : s ⊆ I) (t : Set R):
    t * s ⊆ I

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
⊢ t * s ⊆ ↑I

Tactic:
rintro - ⟨r, -, x, hx, rfl⟩

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
r x : R
hx : x ∈ s
⊢ (fun x1 x2 => x1 * x2) r x ∈ ↑I

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
r x : R
hx : x ∈ s
⊢ (fun x1 x2 => x1 * x2) r x ∈ ↑I

Tactic:
exact mul_mem_left _ _ _ (h hx)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
@[simp]
lemma eval₂_ofNat {S : Type*} [Semiring S] (n : ℕ) [n.AtLeastTwo] (f : R →+* S) (a : S) :
    (ofNat(n) : R[X]).eval₂ f a = ofNat(n)

Proof state:
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Semiring S
n : ℕ
inst✝ : n.AtLeastTwo
f : R →+* S
a : S
⊢ eval₂ f a (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
simp [OfNat.ofNat]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.matrix_components (m : ∀ j k, f j ⟶ g k) (j : J) (k : K) :
    biproduct.components (biproduct.matrix m) j k = m j k

Proof state:
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
j : J
k : K
⊢ components (matrix m) j k = m j k

Tactic:
simp [biproduct.components]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.rotateL_lemma₃ {a b c : ℕ} (H2 : 3 * a ≤ b + c) (h : b < 2 * c) : a + b < 3 * c

Proof state:
a b c : ℕ
H2 : 3 * a ≤ b + c
h : b < 2 * c
⊢ a + b < 3 * c

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem get?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
    get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (mem_of_get? H)

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
h : ∀ (a : α), a ∈ l → p a
n : Nat
⊢ (pmap f l h)[n]? = Option.pmap f l[n]? ⋯

Tactic:
simp [getElem?_pmap, h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
h : ∀ (a : α), a ∈ l → p a
n : Nat
⊢ (pmap f l h).get? n = Option.pmap f (l.get? n) ⋯

Tactic:
simp only [get?_eq_getElem?]

Result:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
h : ∀ (a : α), a ∈ l → p a
n : Nat
⊢ (pmap f l h)[n]? = Option.pmap f l[n]? ⋯
-- Mathlib/Data/List/Flatten.lean
/-- See `List.countP_flatMap` for the corresponding statement using `List.sum`. -/
@[deprecated "Use `List.countP_flatMap`." (since := "2024-10-17")]
lemma countP_flatMap' (p : β → Bool) (l : List α) (f : α → List β) :
    countP p (l.flatMap f) = Nat.sum (map (countP p ∘ f) l)

Proof state:
α : Type u_1
β : Type u_2
p : β → Bool
l : List α
f : α → List β
⊢ countP p (flatMap f l) = Nat.sum (map (countP p ∘ f) l)

Tactic:
rw [List.flatMap, countP_flatten', map_map]

Result:
no goals
-- Mathlib/Topology/Algebra/MulAction.lean
theorem continuousSMul_sInf {ts : Set (TopologicalSpace X)}
    (h : ∀ t ∈ ts, @ContinuousSMul M X _ _ t) : @ContinuousSMul M X _ _ (sInf ts) :=
  -- Porting note: {} doesn't work because `sInf ts` isn't found by TC search. `(_)` finds it by
  -- unification instead.
  @ContinuousSMul.mk M X _ _ (_) <| by
      -- Porting note: needs `( :)`
      rw [← (@sInf_singleton _ _ ‹TopologicalSpace M›:)]
      exact
        continuous_sInf_rng.2 fun t ht =>
          continuous_sInf_dom₂ (Eq.refl _) ht
            (@ContinuousSMul.continuous_smul _ _ _ _ t (h t ht))

Proof state:
M : Type u_2
X : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ t ∈ ts, ContinuousSMul M X
⊢ Continuous fun p => p.1 • p.2

Tactic:
exact
  continuous_sInf_rng.2 fun t ht =>
    continuous_sInf_dom₂ (Eq.refl _) ht
      (@ContinuousSMul.continuous_smul _ _ _ _ t (h t ht))

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem fst_comp_prodAssoc :
    (LinearMap.fst R M₁ (M₂ × M₃)).comp (prodAssoc R M₁ M₂ M₃).toLinearMap =
    (LinearMap.fst R M₁ M₂).comp (LinearMap.fst R (M₁ × M₂) M₃)

Proof state:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
⊢ LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃) = LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
lemma idRel_subset_dynEntourage (T : X → X) {U : Set (X × X)} (h : idRel ⊆ U) (n : ℕ) :
    idRel ⊆ (dynEntourage T U n)

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
h : idRel ⊆ U
n : ℕ
⊢ ∀ i < n, ∀ (a : X), (T^[i] a, T^[i] a) ∈ U

Tactic:
exact fun _ _ _ ↦ h rfl

Result:
no goals

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
h : idRel ⊆ U
n : ℕ
⊢ idRel ⊆ dynEntourage T U n

Tactic:
simp only [dynEntourage, map_iterate, subset_iInter_iff, idRel_subset, mem_preimage, map_apply]

Result:
X : Type u_1
T : X → X
U : Set (X × X)
h : idRel ⊆ U
n : ℕ
⊢ ∀ i < n, ∀ (a : X), (T^[i] a, T^[i] a) ∈ U
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem orthonormal_subtype_range {v : ι → E} (hv : Function.Injective v) :
    Orthonormal 𝕜 (Subtype.val : Set.range v → E) ↔ Orthonormal 𝕜 v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : ι ≃ ↑(Set.range v) := Equiv.ofInjective v hv
⊢ Orthonormal 𝕜 Subtype.val ↔ Orthonormal 𝕜 v

Tactic:
refine ⟨fun h => h.comp f f.injective, fun h => ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : ι ≃ ↑(Set.range v) := Equiv.ofInjective v hv
h : Orthonormal 𝕜 v
⊢ Orthonormal 𝕜 Subtype.val

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : ι ≃ ↑(Set.range v) := Equiv.ofInjective v hv
h : Orthonormal 𝕜 v
⊢ Orthonormal 𝕜 Subtype.val

Tactic:
rw [← Equiv.self_comp_ofInjective_symm hv]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : ι ≃ ↑(Set.range v) := Equiv.ofInjective v hv
h : Orthonormal 𝕜 v
⊢ Orthonormal 𝕜 (v ∘ ⇑(Equiv.ofInjective v hv).symm)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : ι ≃ ↑(Set.range v) := Equiv.ofInjective v hv
h : Orthonormal 𝕜 v
⊢ Orthonormal 𝕜 (v ∘ ⇑(Equiv.ofInjective v hv).symm)

Tactic:
exact h.comp f.symm f.symm.injective

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
⊢ Orthonormal 𝕜 Subtype.val ↔ Orthonormal 𝕜 v

Tactic:
let f : ι ≃ Set.range v := Equiv.ofInjective v hv

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : ι ≃ ↑(Set.range v) := Equiv.ofInjective v hv
⊢ Orthonormal 𝕜 Subtype.val ↔ Orthonormal 𝕜 v
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
/-- A functor between preadditive categories that preserves (zero morphisms and) finite coproducts
    preserves finite biproducts. -/
lemma preservesBiproduct_of_preservesCoproduct {f : J → C}
    [PreservesColimit (Discrete.functor f) F] :
    PreservesBiproduct f F where
  preserves {b} hb :=
    ⟨isBilimitOfIsColimit _ <|
      IsColimit.ofIsoColimit
          ((IsColimit.precomposeInvEquiv (Discrete.compNatIsoDiscrete _ _)
                (F.mapCocone b.toCocone)).symm
            (isColimitOfPreserves F hb.isColimit)) <|
        Cocones.ext (Iso.refl _) (by rintro ⟨⟩; simp)⟩

Proof state:
case mk
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : PreservesColimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
as✝ : J
⊢ ((Cocones.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).ι.app { as := as✝ } ≫
      (Iso.refl ((Cocones.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).pt).hom =
    (F.mapBicone b).toCocone.ι.app { as := as✝ }

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : PreservesColimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
⊢ ∀ (j : Discrete J),
    ((Cocones.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).ι.app j ≫
        (Iso.refl ((Cocones.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).pt).hom =
      (F.mapBicone b).toCocone.ι.app j

Tactic:
rintro ⟨⟩

Result:
case mk
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : PreservesColimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
as✝ : J
⊢ ((Cocones.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).ι.app { as := as✝ } ≫
      (Iso.refl ((Cocones.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).pt).hom =
    (F.mapBicone b).toCocone.ι.app { as := as✝ }
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem Submodule.finrank_add_inf_finrank_orthogonal' {K₁ K₂ : Submodule 𝕜 E}
    [FiniteDimensional 𝕜 K₂] (h : K₁ ≤ K₂) {n : ℕ} (h_dim : finrank 𝕜 K₁ + n = finrank 𝕜 K₂) :
    finrank 𝕜 (K₁ᗮ ⊓ K₂ : Submodule 𝕜 E) = n

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
n : ℕ
h_dim : finrank 𝕜 ↥K₁ + n = finrank 𝕜 ↥K₂
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₁ + n

Tactic:
simp [Submodule.finrank_add_inf_finrank_orthogonal h, h_dim]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
n : ℕ
h_dim : finrank 𝕜 ↥K₁ + n = finrank 𝕜 ↥K₂
⊢ finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = n

Tactic:
rw [← add_right_inj (finrank 𝕜 K₁)]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K₂
h : K₁ ≤ K₂
n : ℕ
h_dim : finrank 𝕜 ↥K₁ + n = finrank 𝕜 ↥K₂
⊢ finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₁ + n
-- Mathlib/Data/Set/Countable.lean
theorem countable_iff_exists_subset_range [Nonempty α] {s : Set α} :
    s.Countable ↔ ∃ f : ℕ → α, s ⊆ range f :=
  ⟨fun h => by
    inhabit α
    exact ⟨enumerateCountable h default, subset_range_enumerate _ _⟩, fun ⟨f, hsf⟩ =>
    (countable_range f).mono hsf⟩

Proof state:
α : Type u
inst✝ : Nonempty α
s : Set α
h : s.Countable
inhabited_h : Inhabited α
⊢ ∃ f, s ⊆ range f

Tactic:
exact ⟨enumerateCountable h default, subset_range_enumerate _ _⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : Nonempty α
s : Set α
h : s.Countable
⊢ ∃ f, s ⊆ range f

Tactic:
inhabit α

Result:
α : Type u
inst✝ : Nonempty α
s : Set α
h : s.Countable
inhabited_h : Inhabited α
⊢ ∃ f, s ⊆ range f
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List α} {k : α} :
    (insertManyIfNewUnit m l).1.contains k = (m.contains k || l.contains k)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
k : α
⊢ (insertManyIfNewUnit m l).val.contains k = (m.contains k || l.contains k)

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.containsKey_insertListIfNewUnit

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem image_id [DecidableEq α] : s.image id = s :=
  ext fun _ => by simp only [mem_image, exists_prop, id, exists_eq_right]

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
x✝ : α
⊢ x✝ ∈ image id s ↔ x✝ ∈ s

Tactic:
simp only [mem_image, exists_prop, id, exists_eq_right]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
theorem divInt_eq_zero {a b : ℤ} (b0 : b ≠ 0) : a /. b = 0 ↔ a = 0

Proof state:
a b : ℤ
b0 : b ≠ 0
⊢ a /. b = 0 ↔ a = 0

Tactic:
rw [← zero_divInt b, divInt_eq_iff b0 b0, Int.zero_mul, Int.mul_eq_zero, or_iff_left b0]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderivWithin_sub_const (c : F) :
    fderivWithin 𝕜 (fun y => f y - c) s x = fderivWithin 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
c : F
⊢ fderivWithin 𝕜 (fun y => f y - c) s x = fderivWithin 𝕜 f s x

Tactic:
simp only [sub_eq_add_neg, fderivWithin_add_const]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapRange.zeroHom_comp (f : ZeroHom N P) (f₂ : ZeroHom M N) :
    (mapRange.zeroHom (f.comp f₂) : ZeroHom (α →₀ _) _) =
      (mapRange.zeroHom f).comp (mapRange.zeroHom f₂) :=
  ZeroHom.ext <| mapRange_comp f (map_zero f) f₂ (map_zero f₂) (by simp only [comp_apply, map_zero])

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : ZeroHom N P
f₂ : ZeroHom M N
⊢ (⇑f ∘ ⇑f₂) 0 = 0

Tactic:
simp only [comp_apply, map_zero]

Result:
no goals
-- Mathlib/Order/BoundedOrder/Basic.lean
theorem OrderTop.ext_top {α} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α}
    (B : OrderTop α) (H : ∀ x y : α, (haveI := hA; x ≤ y) ↔ x ≤ y) :
    (@Top.top α (@OrderTop.toTop α hA.toLE A)) = (@Top.top α (@OrderTop.toTop α hB.toLE B))

Proof state:
case refl
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤

Tactic:
apply top_unique

Result:
case refl.h
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ ≤ ⊤

Proof state:
case refl.h
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ ≤ ⊤

Tactic:
exact @le_top _ _ A _

Result:
no goals

Proof state:
α : Type u_1
hA : PartialOrder α
A : OrderTop α
hB : PartialOrder α
B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤

Tactic:
cases PartialOrder.ext H

Result:
case refl
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤
-- Mathlib/Data/Set/Lattice.lean
theorem sSup_iUnion (t : ι → Set β) : sSup (⋃ i, t i) = ⨆ i, sSup (t i)

Proof state:
β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
t : ι → Set β
⊢ sSup (⋃ i, t i) = ⨆ i, sSup (t i)

Tactic:
simp_rw [sSup_eq_iSup, iSup_iUnion]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem idxOf_cons_ne {a b : α} (l : List α) : b ≠ a → idxOf a (b :: l) = succ (idxOf a l)
  | h => by simp only [idxOf, findIdx_cons, Bool.cond_eq_ite, beq_iff_eq, h, ite_false]

Proof state:
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
x✝ : b ≠ a
h : b ≠ a := x✝
⊢ idxOf a (b :: l) = (idxOf a l).succ

Tactic:
simp only [idxOf, findIdx_cons, Bool.cond_eq_ite, beq_iff_eq, h, ite_false]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_pi_div_two : ((π / 2 : ℝ) : Angle).toReal = π / 2 :=
  toReal_coe_eq_self_iff.2 <| by constructor <;> linarith [pi_pos]

Proof state:
⊢ -π < π / 2 ∧ π / 2 ≤ π

Tactic:
constructor <;> linarith [pi_pos]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem pow_padicValNat_dvd {n : ℕ} : p ^ padicValNat p n ∣ n

Proof state:
case inr
p n : ℕ
hn : n > 0
⊢ p ^ padicValNat p n ∣ n

Tactic:
rcases eq_or_ne p 1 with (rfl | hp)

Result:
case inr.inl
n : ℕ
hn : n > 0
⊢ 1 ^ padicValNat 1 n ∣ n

case inr.inr
p n : ℕ
hn : n > 0
hp : p ≠ 1
⊢ p ^ padicValNat p n ∣ n

Proof state:
case inr.inr.hk
p n : ℕ
hn : n > 0
hp : p ≠ 1
⊢ padicValNat p n ≤ multiplicity p n

Tactic:
rw [padicValNat_def'] <;> assumption

Result:
no goals

Proof state:
case inl
p : ℕ
⊢ p ^ padicValNat p 0 ∣ 0

Tactic:
simp

Result:
no goals

Proof state:
case inr.inl
n : ℕ
hn : n > 0
⊢ 1 ^ padicValNat 1 n ∣ n

Tactic:
simp

Result:
no goals

Proof state:
p n : ℕ
⊢ p ^ padicValNat p n ∣ n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Result:
case inl
p : ℕ
⊢ p ^ padicValNat p 0 ∣ 0

case inr
p n : ℕ
hn : n > 0
⊢ p ^ padicValNat p n ∣ n

Proof state:
case inr.inr
p n : ℕ
hn : n > 0
hp : p ≠ 1
⊢ p ^ padicValNat p n ∣ n

Tactic:
apply pow_dvd_of_le_multiplicity

Result:
case inr.inr.hk
p n : ℕ
hn : n > 0
hp : p ≠ 1
⊢ padicValNat p n ≤ multiplicity p n
-- Mathlib/Order/Lattice.lean
theorem of_map_inf [SemilatticeInf α] [SemilatticeInf β]
    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊓ f y) : MonotoneOn f s := fun x hx y hy hxy =>
  inf_eq_left.1 <| by rw [← h _ hx _ hy, inf_eq_left.2 hxy]

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊓ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ f x ⊓ f y = f x

Tactic:
rw [← h _ hx _ hy, inf_eq_left.2 hxy]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem ofEq_symm (h : S₁ = S₂) : (ofEq S₁ S₂ h).symm = ofEq S₂ S₁ h.symm

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module k V₁
inst✝² : AffineSpace V₁ P₁
S₁ S₂ : AffineSubspace k P₁
inst✝¹ : Nonempty ↥S₁
inst✝ : Nonempty ↥S₂
h : S₁ = S₂
⊢ (ofEq S₁ S₂ h).symm = ofEq S₂ S₁ ⋯

Tactic:
ext

Result:
case h.a
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module k V₁
inst✝² : AffineSpace V₁ P₁
S₁ S₂ : AffineSubspace k P₁
inst✝¹ : Nonempty ↥S₁
inst✝ : Nonempty ↥S₂
h : S₁ = S₂
x✝ : ↥S₂
⊢ ↑((ofEq S₁ S₂ h).symm x✝) = ↑((ofEq S₂ S₁ ⋯) x✝)

Proof state:
case h.a
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module k V₁
inst✝² : AffineSpace V₁ P₁
S₁ S₂ : AffineSubspace k P₁
inst✝¹ : Nonempty ↥S₁
inst✝ : Nonempty ↥S₂
h : S₁ = S₂
x✝ : ↥S₂
⊢ ↑((ofEq S₁ S₂ h).symm x✝) = ↑((ofEq S₂ S₁ ⋯) x✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem aleph0_le_add_iff {a b : Cardinal} : ℵ₀ ≤ a + b ↔ ℵ₀ ≤ a ∨ ℵ₀ ≤ b

Proof state:
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a + b ↔ ℵ₀ ≤ a ∨ ℵ₀ ≤ b

Tactic:
simp only [← not_lt, add_lt_aleph0_iff, not_and_or]

Result:
no goals