harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Condensed/Epi.lean
lemma epi_iff_locallySurjective_on_compHaus : Epi f ↔
    ∀ (S : CompHaus) (y : ToType (Y.val.obj ⟨S⟩)),
      (∃ (S' : CompHaus) (φ : S' ⟶ S) (_ : Function.Surjective φ) (x : ToType (X.val.obj ⟨S'⟩)),
        f.val.app ⟨S'⟩ x = Y.val.map ⟨φ⟩ y)

Proof state:
A : Type u'
inst✝⁸ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁷ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁶ : ConcreteCategory A FA
inst✝⁵ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁴ : (coherentTopology CompHaus).WEqualsLocallyBijective A
inst✝³ : HasSheafify (coherentTopology CompHaus) A
inst✝² : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)
inst✝¹ : Balanced (Sheaf (coherentTopology CompHaus) A)
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
⊢ Epi f ↔
    ∀ (S : CompHaus) (y : ToType (Y.val.obj (op S))),
      ∃ S' φ, ∃ (_ : Function.Surjective ⇑(hom φ)), ∃ x, (hom (f.val.app (op S'))) x = (hom (Y.val.map (op φ))) y

Tactic:
rw [← isLocallySurjective_iff_epi', coherentTopology.isLocallySurjective_iff,
  regularTopology.isLocallySurjective_iff]

Result:
A : Type u'
inst✝⁸ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁷ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁶ : ConcreteCategory A FA
inst✝⁵ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁴ : (coherentTopology CompHaus).WEqualsLocallyBijective A
inst✝³ : HasSheafify (coherentTopology CompHaus) A
inst✝² : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)
inst✝¹ : Balanced (Sheaf (coherentTopology CompHaus) A)
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
⊢ (∀ (X_1 : CompHaus) (y : ToType (Y.val.obj (op X_1))),
      ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (hom (f.val.app (op X'))) x = (hom (Y.val.map (op φ))) y) ↔
    ∀ (S : CompHaus) (y : ToType (Y.val.obj (op S))),
      ∃ S' φ, ∃ (_ : Function.Surjective ⇑(hom φ)), ∃ x, (hom (f.val.app (op S'))) x = (hom (Y.val.map (op φ))) y

Proof state:
A : Type u'
inst✝⁸ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁷ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁶ : ConcreteCategory A FA
inst✝⁵ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁴ : (coherentTopology CompHaus).WEqualsLocallyBijective A
inst✝³ : HasSheafify (coherentTopology CompHaus) A
inst✝² : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)
inst✝¹ : Balanced (Sheaf (coherentTopology CompHaus) A)
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
⊢ (∀ (X_1 : CompHaus) (y : ToType (Y.val.obj (op X_1))),
      ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (hom (f.val.app (op X'))) x = (hom (Y.val.map (op φ))) y) ↔
    ∀ (S : CompHaus) (y : ToType (Y.val.obj (op S))),
      ∃ S' φ, ∃ (_ : Function.Surjective ⇑(hom φ)), ∃ x, (hom (f.val.app (op S'))) x = (hom (Y.val.map (op φ))) y

Tactic:
simp_rw [((CompHaus.effectiveEpi_tfae _).out 0 2 :)]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
lemma monotone_of_sub_one_le : (∀ a, ¬ IsMin a → f (a - 1) ≤ f a) → Monotone f

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f (a - 1) ≤ f a) → Monotone f

Tactic:
simpa [Order.pred_eq_sub_one] using monotone_of_pred_le (f := f)

Result:
no goals
-- Mathlib/Order/Hom/Bounded.lean
theorem cancel_left {g : BotHom β γ} {f₁ f₂ : BotHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => BotHom.ext fun a => hg <| by rw [← BotHom.comp_apply, h, BotHom.comp_apply],
    congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Bot α
inst✝¹ : Bot β
inst✝ : Bot γ
g : BotHom β γ
f₁ f₂ : BotHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← BotHom.comp_apply, h, BotHom.comp_apply]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem lifts_iff_set_range (p : S[X]) : p ∈ lifts f ↔ p ∈ Set.range (map f)

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ p ∈ Set.range (map f)

Tactic:
simp only [coe_mapRingHom, lifts, Set.mem_range, RingHom.mem_rangeS]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem support_C_mul_T (a : R) (n : ℤ) : Finsupp.support (C a * T n) ⊆ {n}

Proof state:
R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (Finsupp.single n a).support ⊆ {n}

Tactic:
exact support_single_subset

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (C a * T n).support ⊆ {n}

Tactic:
rw [← single_eq_C_mul_T]

Result:
R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (Finsupp.single n a).support ⊆ {n}
-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma Scheme.Opens.ι_image_basicOpen (r : Γ(U, ⊤)) :
    U.ι ''ᵁ U.toScheme.basicOpen r = X.basicOpen r

Proof state:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen r

Tactic:
rw [Scheme.map_basicOpen, Scheme.basicOpen_res_eq]

Result:
no goals
-- Mathlib/Data/DFinsupp/Order.lean
theorem support_tsub : (f - g).support ⊆ f.support

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (α i)
inst✝⁵ : (i : ι) → PartialOrder (α i)
inst✝⁴ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝³ : (i : ι) → Sub (α i)
inst✝² : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ (f - g).support ⊆ f.support

Tactic:
simp +contextual only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff,
  Ne, coe_tsub, Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)

Proof state:
w : Nat
⊢ 0 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem Disjoint.le_symmDiff_sup_symmDiff_right (h : Disjoint b c) : a ≤ a ∆ b ⊔ a ∆ c

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint b c
⊢ a ≤ b ∆ a ⊔ c ∆ a

Tactic:
exact h.le_symmDiff_sup_symmDiff_left

Result:
no goals

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint b c
⊢ a ≤ a ∆ b ⊔ a ∆ c

Tactic:
simp_rw [symmDiff_comm a]

Result:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint b c
⊢ a ≤ b ∆ a ⊔ c ∆ a
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem UniformGroup.uniformity_countably_generated [(𝓝 (1 : α)).IsCountablyGenerated] :
    (𝓤 α).IsCountablyGenerated

Proof state:
α : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : (𝓝 1).IsCountablyGenerated
⊢ (𝓤 α).IsCountablyGenerated

Tactic:
rw [uniformity_eq_comap_nhds_one]

Result:
α : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : (𝓝 1).IsCountablyGenerated
⊢ (comap (fun x => x.2 / x.1) (𝓝 1)).IsCountablyGenerated

Proof state:
α : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : (𝓝 1).IsCountablyGenerated
⊢ (comap (fun x => x.2 / x.1) (𝓝 1)).IsCountablyGenerated

Tactic:
exact Filter.comap.isCountablyGenerated _ _

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_union_mul_inter_apply (f : α → M) (s t : Set α) (a : α) :
    mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a
      = mulIndicator s f a * mulIndicator t f a

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
f : α → M
s t : Set α
a : α
⊢ (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Tactic:
by_cases hs : a ∈ s <;> by_cases ht : a ∈ t <;> simp [*]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem piecewise_same : s.piecewise f f = f

Proof state:
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
⊢ s.piecewise f f = f

Tactic:
ext x

Result:
case h
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
⊢ s.piecewise f f x = f x

Proof state:
case h
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
⊢ s.piecewise f f x = f x

Tactic:
by_cases hx : x ∈ s <;> simp [hx]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem sup_join {f₁ f₂ : Filter (Filter α)} : join f₁ ⊔ join f₂ = join (f₁ ⊔ f₂) :=
  Filter.ext fun x => by simp only [mem_sup, mem_join]

Proof state:
α : Type u
f₁ f₂ : Filter (Filter α)
x : Set α
⊢ x ∈ f₁.join ⊔ f₂.join ↔ x ∈ (f₁ ⊔ f₂).join

Tactic:
simp only [mem_sup, mem_join]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Hasse.lean
theorem pathGraph_adj {n : ℕ} {u v : Fin n} :
    (pathGraph n).Adj u v ↔ u.val + 1 = v.val ∨ v.val + 1 = u.val

Proof state:
n : ℕ
u v : Fin n
⊢ (pathGraph n).Adj u v ↔ ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u

Tactic:
simp only [pathGraph, hasse]

Result:
n : ℕ
u v : Fin n
⊢ u ⋖ v ∨ v ⋖ u ↔ ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u

Proof state:
n : ℕ
u v : Fin n
⊢ u ⋖ v ∨ v ⋖ u ↔ ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u

Tactic:
simp_rw [← Fin.coe_covBy_iff, covBy_iff_add_one_eq]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem irreducible_of_irreducible_absNorm {I : Ideal S} (hI : Irreducible (Ideal.absNorm I)) :
    Irreducible I :=
  irreducible_iff.mpr
    ⟨fun h =>
      hI.not_unit (by simpa only [Ideal.isUnit_iff, Nat.isUnit_iff, absNorm_eq_one_iff] using h),
      by
      rintro a b rfl
      simpa only [Ideal.isUnit_iff, Nat.isUnit_iff, absNorm_eq_one_iff] using
        hI.isUnit_or_isUnit (_root_.map_mul absNorm a b)⟩

Proof state:
S : Type u_1
inst✝³ : CommRing S
inst✝² : Nontrivial S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
hI : Irreducible (absNorm I)
h : IsUnit I
⊢ IsUnit (absNorm I)

Tactic:
simpa only [Ideal.isUnit_iff, Nat.isUnit_iff, absNorm_eq_one_iff] using h

Result:
no goals

Proof state:
S : Type u_1
inst✝³ : CommRing S
inst✝² : Nontrivial S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
hI : Irreducible (absNorm I)
⊢ ∀ (a b : Ideal S), I = a * b → IsUnit a ∨ IsUnit b

Tactic:
rintro a b rfl

Result:
S : Type u_1
inst✝³ : CommRing S
inst✝² : Nontrivial S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
a b : Ideal S
hI : Irreducible (absNorm (a * b))
⊢ IsUnit a ∨ IsUnit b

Proof state:
S : Type u_1
inst✝³ : CommRing S
inst✝² : Nontrivial S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
a b : Ideal S
hI : Irreducible (absNorm (a * b))
⊢ IsUnit a ∨ IsUnit b

Tactic:
simpa only [Ideal.isUnit_iff, Nat.isUnit_iff, absNorm_eq_one_iff] using
  hI.isUnit_or_isUnit (_root_.map_mul absNorm a b)

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma comapOn_preimage_eq (N : Matroid β) (f : α → β) : N.comapOn (f ⁻¹' N.E) f = N.comap f

Proof state:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
⊢ f ⁻¹' N.E = (N.comap f).E

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
⊢ N.comapOn (f ⁻¹' N.E) f = N.comap f

Tactic:
rw [comapOn, restrict_eq_self_iff]

Result:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
⊢ f ⁻¹' N.E = (N.comap f).E
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem eq_zero_of_tdiv_eq_zero {d n : Int} (h : d ∣ n) (H : n.tdiv d = 0) : n = 0

Proof state:
d n : Int
h : d ∣ n
H : n.tdiv d = 0
⊢ n = 0

Tactic:
rw [← Int.mul_tdiv_cancel' h, H, Int.mul_zero]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem isMulTwoCoboundary_of_mem_twoCoboundaries
    (f : G × G → M) (hf : f ∈ twoCoboundaries (Rep.ofMulDistribMulAction G M)) :
    IsMulTwoCoboundary (M := M) (Additive.toMul ∘ f)

Proof state:
case intro
G M : Type
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulDistribMulAction G M
x : G → ↑(Rep.ofMulDistribMulAction G M).V
⊢ IsMulTwoCoboundary (⇑Additive.toMul ∘ (dOne (Rep.ofMulDistribMulAction G M)) x)

Tactic:
exact ⟨x, fun _ _ => rfl⟩

Result:
no goals

Proof state:
G M : Type
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulDistribMulAction G M
f : G × G → M
hf : f ∈ twoCoboundaries (Rep.ofMulDistribMulAction G M)
⊢ IsMulTwoCoboundary (⇑Additive.toMul ∘ f)

Tactic:
rcases hf with ⟨x, rfl⟩

Result:
case intro
G M : Type
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulDistribMulAction G M
x : G → ↑(Rep.ofMulDistribMulAction G M).V
⊢ IsMulTwoCoboundary (⇑Additive.toMul ∘ (dOne (Rep.ofMulDistribMulAction G M)) x)
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_succ_iff_hasFDerivAt {n : ℕ} :
    ContDiff 𝕜 (n + 1) f ↔
      ∃ f' : E → E →L[𝕜] F, ContDiff 𝕜 n f' ∧ ∀ x, HasFDerivAt f (f' x) x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
⊢ ContDiff 𝕜 (↑n + 1) f ↔ ∃ f', ContDiff 𝕜 (↑n) f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x

Tactic:
simp only [← contDiffOn_univ, ← hasFDerivWithinAt_univ, Set.mem_univ, forall_true_left,
  contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn uniqueDiffOn_univ,
  WithTop.natCast_ne_top, analyticOn_univ, false_implies, true_and]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem mul_inv_lt_inv_mul_iff : a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b c d : α
inst✝ : MulRightStrictMono α
⊢ a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b

Tactic:
rw [← mul_lt_mul_iff_left d, ← mul_lt_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
  inv_mul_cancel_right]

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem updateCol_submatrix_equiv [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : o)
    (c : l → α) (e : l ≃ m) (f : o ≃ n) : updateCol (A.submatrix e f) j c =
    (A.updateCol (f j) fun i => c (e.symm i)).submatrix e f

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq o
inst✝ : DecidableEq n
A : Matrix m n α
j : o
c : l → α
e : l ≃ m
f : o ≃ n
⊢ (A.submatrix ⇑e ⇑f).updateCol j c = (A.updateCol (f j) fun i => c (e.symm i)).submatrix ⇑e ⇑f

Tactic:
simpa only [← transpose_submatrix, updateRow_transpose] using
  congr_arg transpose (updateRow_submatrix_equiv Aᵀ j c f e)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem tendsto_exp_nhds_zero_iff {α : Type*} {l : Filter α} {f : α → ℂ} :
    Tendsto (fun x => exp (f x)) l (𝓝 0) ↔ Tendsto (fun x => re (f x)) l atBot

Proof state:
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (fun x => cexp (f x)) l (𝓝 0) ↔ Tendsto (fun x => (f x).re) l atBot

Tactic:
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero, tendsto_comap_iff]

Result:
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (re ∘ f) l atBot ↔ Tendsto (fun x => (f x).re) l atBot

Proof state:
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (re ∘ f) l atBot ↔ Tendsto (fun x => (f x).re) l atBot

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
/-- A vector is in the same ray as a nonnegative multiple of one it is in the same ray as. -/
lemma nonneg_smul_right (h : SameRay R x y) (ha : 0 ≤ a) : SameRay R x (a • y) :=
  h.trans (sameRay_nonneg_smul_right y ha) fun hy => Or.inr <| by rw [hy, smul_zero]

Proof state:
R : Type u_1
inst✝⁷ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
x y : M
S : Type u_5
inst✝⁴ : OrderedCommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
h : SameRay R x y
ha : 0 ≤ a
hy : y = 0
⊢ a • y = 0

Tactic:
rw [hy, smul_zero]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem frontier_prod_univ_eq (s : Set X) :
    frontier (s ×ˢ (univ : Set Y)) = frontier s ×ˢ univ

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
⊢ frontier (s ×ˢ univ) = frontier s ×ˢ univ

Tactic:
simp [frontier_prod_eq]

Result:
no goals
-- Mathlib/RingTheory/Artinian/Module.lean
theorem eventuallyConst_of_isArtinian (f : ℕ →o (Submodule R M)ᵒᵈ) :
    atTop.EventuallyConst f

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ →o (Submodule R M)ᵒᵈ
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → f i = f j

Tactic:
exact monotone_stabilizes f

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ →o (Submodule R M)ᵒᵈ
⊢ EventuallyConst (⇑f) atTop

Tactic:
simp_rw [eventuallyConst_atTop, eq_comm]

Result:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ →o (Submodule R M)ᵒᵈ
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → f i = f j
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem eq_one_of_mul_right (h : a * b = 1) : a = 1 :=
  congr_arg Units.inv <| Subsingleton.elim (Units.mk _ _ (by
    rw [← mul_left_cancel_iff (a := a), ← mul_assoc, h, one_mul, mul_one]) h) 1

Proof state:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
rw [← mul_left_cancel_iff (a := a), ← mul_assoc, h, one_mul, mul_one]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
lemma FractionalIdeal.inv_le_comm {I J : FractionalIdeal A⁰ K} (hI : I ≠ 0) (hJ : J ≠ 0) :
    I⁻¹ ≤ J ↔ J⁻¹ ≤ I

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
⊢ I⁻¹ ≤ J ↔ J⁻¹ ≤ I

Tactic:
simpa using le_inv_comm (A := A) (K := K) (inv_ne_zero hI) (inv_ne_zero hJ)

Result:
no goals
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.qr₁' (a b : ℕ) (r : ℤ) (ha : a % 2 = 1) (hb : b % 4 = 1)
    (hr : jacobiSymNat b a = r) : jacobiSymNat a b = r

Proof state:
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 4 = 1
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = r

Tactic:
rwa [jacobiSymNat, ← jacobiSym.quadratic_reciprocity_one_mod_four hb (Nat.odd_iff.mpr ha)]

Result:
no goals
-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem ae_tendsto_rnDeriv (ρ μ : Measure β) [IsLocallyFiniteMeasure μ] [IsLocallyFiniteMeasure ρ] :
    ∀ᵐ x ∂μ,
      Tendsto (fun r => ρ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (ρ.rnDeriv μ x))

Proof state:
case h
β : Type u
inst✝⁶ : MetricSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : SecondCountableTopology β
inst✝² : HasBesicovitchCovering β
ρ μ : Measure β
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsLocallyFiniteMeasure ρ
x : β
hx : Tendsto (fun a => ρ a / μ a) ((Besicovitch.vitaliFamily μ).filterAt x) (𝓝 (ρ.rnDeriv μ x))
⊢ Tendsto (fun r => ρ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (ρ.rnDeriv μ x))

Tactic:
exact hx.comp (tendsto_filterAt μ x)

Result:
no goals

Proof state:
β : Type u
inst✝⁶ : MetricSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : SecondCountableTopology β
inst✝² : HasBesicovitchCovering β
ρ μ : Measure β
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsLocallyFiniteMeasure ρ
⊢ ∀ᵐ (x : β) ∂μ, Tendsto (fun r => ρ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (ρ.rnDeriv μ x))

Tactic:
filter_upwards [VitaliFamily.ae_tendsto_rnDeriv (Besicovitch.vitaliFamily μ) ρ] with x hx

Result:
case h
β : Type u
inst✝⁶ : MetricSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : SecondCountableTopology β
inst✝² : HasBesicovitchCovering β
ρ μ : Measure β
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsLocallyFiniteMeasure ρ
x : β
hx : Tendsto (fun a => ρ a / μ a) ((Besicovitch.vitaliFamily μ).filterAt x) (𝓝 (ρ.rnDeriv μ x))
⊢ Tendsto (fun r => ρ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (ρ.rnDeriv μ x))
-- Mathlib/LinearAlgebra/Dimension/Finrank.lean
theorem finrank_le_of_rank_le {n : ℕ} (h : Module.rank R M ≤ ↑n) : finrank R M ≤ n

Proof state:
case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ Module.rank R M < ℵ₀

Tactic:
exact h.trans_lt (nat_lt_aleph0 n)

Result:
no goals

Proof state:
case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ ↑n < ℵ₀

Tactic:
exact nat_lt_aleph0 n

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ finrank R M ≤ n

Tactic:
rwa [← Cardinal.toNat_le_iff_le_of_lt_aleph0, toNat_natCast] at h

Result:
case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ Module.rank R M < ℵ₀

case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ ↑n < ℵ₀
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem isBoundedBilinearMap_mul : IsBoundedBilinearMap 𝕜 fun p : 𝕜 × 𝕜 => p.1 * p.2

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
⊢ IsBoundedBilinearMap 𝕜 fun p => p.1 * p.2

Tactic:
simp_rw [← smul_eq_mul]

Result:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
⊢ IsBoundedBilinearMap 𝕜 fun p => p.1 • p.2

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
⊢ IsBoundedBilinearMap 𝕜 fun p => p.1 • p.2

Tactic:
exact isBoundedBilinearMap_smul

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma Nonempty.zero_mul (hs : s.Nonempty) : 0 * s = 0 :=
  s.zero_mul_subset.antisymm <| by simpa [mem_mul] using hs

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ 0 * s

Tactic:
simpa [mem_mul] using hs

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
lemma strictAnti_of_lt_sub_one : (∀ a, ¬ IsMin a → f a < f (a - 1)) → StrictAnti f

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f a < f (a - 1)) → StrictAnti f

Tactic:
simpa [Order.pred_eq_sub_one] using strictAnti_of_lt_pred (f := f)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem self_le_rpow_of_one_le (h₁ : 1 ≤ x) (h₂ : 1 ≤ y) : x ≤ x ^ y

Proof state:
x y : ℝ
h₁ : 1 ≤ x
h₂ : 1 ≤ y
⊢ x ≤ x ^ y

Tactic:
simpa only [rpow_one] using rpow_le_rpow_of_exponent_le h₁ h₂

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem append_cons (as : List α) (b : α) (bs : List α) : as ++ b :: bs = as ++ [b] ++ bs

Proof state:
α : Type u
as : List α
b : α
bs : List α
⊢ as ++ b :: bs = as ++ b :: nil ++ bs

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem lowerBoundP?_exists {t : RBSet α cmp} [TransCmp cmp] [IsCut cmp cut] :
    (∃ x, t.lowerBoundP? cut = some x) ↔ ∃ x ∈ t, cut x ≠ .lt

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBSet α cmp
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
⊢ (∃ x, x ∈ t.val ∧ ¬cut x = Ordering.lt) ↔ ∃ x, (∃ y, y ∈ t.val ∧ cmp x y = Ordering.eq) ∧ ¬cut x = Ordering.lt

Tactic:
exact ⟨
  fun ⟨x, h1, h2⟩ => ⟨x, ⟨x, h1, OrientedCmp.cmp_refl⟩, h2⟩,
  fun ⟨x, ⟨y, h1, h2⟩, eq⟩ => ⟨y, h1, IsCut.congr (cut := cut) h2 ▸ eq⟩⟩

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBSet α cmp
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
⊢ (∃ x, t.lowerBoundP? cut = some x) ↔ ∃ x, x ∈ t ∧ cut x ≠ Ordering.lt

Tactic:
simp [lowerBoundP?, t.2.out.1.lowerBound?_exists, mem_toList, mem_iff_mem_toList]

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBSet α cmp
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
⊢ (∃ x, x ∈ t.val ∧ ¬cut x = Ordering.lt) ↔ ∃ x, (∃ y, y ∈ t.val ∧ cmp x y = Ordering.eq) ∧ ¬cut x = Ordering.lt
-- Mathlib/Topology/UnitInterval.lean
lemma addNSMul_zero : addNSMul h δ 0 = a

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
h : a ≤ b
δ : α
⊢ ↑(addNSMul h δ 0) = a

Tactic:
rw [addNSMul, zero_smul, add_zero, projIcc_left]

Result:
no goals