harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/HashSet/Lemmas.lean
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).contains k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : HashSet α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
⊢ (m.insert k).contains k = true

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Curry.lean
theorem frequently_curry_prod_iff :
    (∃ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ (∃ᶠ x in l, x ∈ s) ∧ ∃ᶠ y in m, y ∈ t

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
s : Set α
t : Set β
⊢ (∃ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ (∃ᶠ (x : α) in l, x ∈ s) ∧ ∃ᶠ (y : β) in m, y ∈ t

Tactic:
simp [frequently_curry_iff]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
@[simp]
protected lemma bot_mem : ⊥ ∈ f.invtSubmodule

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
⊢ ⊥ ∈ f.invtSubmodule

Tactic:
simp [invtSubmodule]

Result:
no goals
-- Mathlib/CategoryTheory/Enriched/HomCongr.lean
lemma eHomCongr_refl (X Y : C) :
    eHomCongr V (Iso.refl X) (Iso.refl Y) = Iso.refl (X ⟶[V] Y)

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y : C
⊢ eHomCongr V (refl X) (refl Y) = refl (EnrichedCategory.Hom X Y)

Tactic:
aesop

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem lift_mul_right (z) : f.lift hg z * g (f.sec z).2 = g (f.sec z).1

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
⊢ (f.lift hg) z * g ↑(f.sec z).2 = g (f.sec z).1

Tactic:
erw [mul_assoc, IsUnit.liftRight_inv_mul, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_abs {i : Nat} {x : BitVec w} :
    getMsbD (x.abs) i = if x.msb then getMsbD (-x) i else getMsbD x i

Proof state:
w i : Nat
x : BitVec w
⊢ x.abs.getMsbD i = if x.msb = true then (-x).getMsbD i else x.getMsbD i

Tactic:
by_cases h : x.msb <;> simp [BitVec.abs, h]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem relindex_ker (f : G →* G') : f.ker.relindex K = Nat.card (K.map f)

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
K : Subgroup G
f : G →* G'
⊢ f.ker.relindex K = Nat.card ↥(map f K)

Tactic:
rw [← MonoidHom.comap_bot, relindex_comap, relindex_bot_left]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem comap_coe_nhds_infty : comap ((↑) : X → OnePoint X) (𝓝 ∞) = coclosedCompact X

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ comap some (𝓝 ∞) = coclosedCompact X

Tactic:
simp [nhds_infty_eq, comap_sup, comap_map coe_injective]

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem top_prod (s : NonUnitalSubring S) :
    (⊤ : NonUnitalSubring R).prod s = s.comap (NonUnitalRingHom.snd R S) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_snd]

Proof state:
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
s : NonUnitalSubring S
x : R × S
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (NonUnitalRingHom.snd R S) s

Tactic:
simp [mem_prod, MonoidHom.coe_snd]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem spanNorm_bot :
    spanNorm R (⊥ : Ideal S) = ⊥ := span_eq_bot.mpr fun x hx => by simpa using hx

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
x : R
hx : x ∈ ⇑(Algebra.intNorm R S) '' ↑⊥
⊢ x = 0

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem leadingCoeff_of_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) :
    P.toPoly.leadingCoeff = P.d

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ P.toPoly.leadingCoeff = P.d

Tactic:
rw [of_c_eq_zero ha hb hc, leadingCoeff_C]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma φ_three : W.φ 3 = C X * C W.Ψ₃ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 3 - 1 = 2

Tactic:
rfl

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.φ 3 = C X * C W.Ψ₃ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 2

Tactic:
rw [φ, ψ_three, three_add_one_eq_four, ψ_four, mul_assoc, show (3 - 1 : ℤ) = 2 by rfl, ψ_two,
  ← sq]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourierCoeff.const_smul (f : AddCircle T → E) (c : ℂ) (n : ℤ) :
    fourierCoeff (c • f :) n = c • fourierCoeff f n

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
c : ℂ
n : ℤ
⊢ fourierCoeff (c • f) n = c • fourierCoeff f n

Tactic:
simp_rw [fourierCoeff, Pi.smul_apply, ← smul_assoc, smul_eq_mul, mul_comm, ← smul_eq_mul,
  smul_assoc, integral_smul]

Result:
no goals
-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem of_finrank_sup [FiniteDimensional F A] [FiniteDimensional F B]
    (H : finrank F ↥(A ⊔ B) = finrank F A * finrank F B) : A.LinearDisjoint B :=
  linearDisjoint_iff'.2 <| .of_finrank_sup_of_free (by rwa [← sup_toSubalgebra_of_left])

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : FiniteDimensional F ↥A
inst✝ : FiniteDimensional F ↥B
H : finrank F ↥(A ⊔ B) = finrank F ↥A * finrank F ↥B
⊢ finrank F ↥(A.toSubalgebra ⊔ B.toSubalgebra) = finrank F ↥A.toSubalgebra * finrank F ↥B.toSubalgebra

Tactic:
rwa [← sup_toSubalgebra_of_left]

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem range_IciExtend (f : Ici a → β) : range (IciExtend f) = range f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a : α
f : ↑(Ici a) → β
⊢ range (IciExtend f) = range f

Tactic:
simp only [IciExtend, range_comp f, range_projIci, range_id', image_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_insertMany_list_of_contains_eq_false [LawfulBEq α] (h : m.WF)
    {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (m.insertMany l).get! k = m.get! k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k : α
inst✝ : Inhabited (β k)
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (m.insertMany l).get! k = m.get! k

Tactic:
simp_to_raw using Raw₀.get!_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/ModelTheory/Algebra/Ring/Basic.lean
theorem realize_zero (v : α → R) : Term.realize v (0 : ring.Term α) = 0

Proof state:
α : Type u_1
R : Type u_2
inst✝⁵ : Add R
inst✝⁴ : Mul R
inst✝³ : Neg R
inst✝² : One R
inst✝¹ : Zero R
inst✝ : CompatibleRing R
v : α → R
⊢ Term.realize v 0 = 0

Tactic:
simp [zero_def, funMap_zero, constantMap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem dvd_refl (a : Nat) : a ∣ a := ⟨1, by simp⟩

Proof state:
a : Nat
⊢ a = a * 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem eq_0_of_lt_one (x : Nat) : x < 1 ↔ x = 0 :=
  Iff.intro
    (fun p =>
      match x with
      | 0 => Eq.refl 0
      | _+1 => False.elim (not_lt_zero _ (Nat.lt_of_succ_lt_succ p)))
    (fun p => by simp [p])

Proof state:
x : Nat
p : x = 0
⊢ x < 1

Tactic:
simp [p]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_le_size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List ((a : α) × β a)} :
    m.1.size ≤ (m.insertMany l).1.1.size

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List ((a : α) × β a)
⊢ m.val.size ≤ (m.insertMany l).val.val.size

Tactic:
simp_to_model [insertMany] using List.length_le_length_insertList

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Integral.lean
lemma cfcL_integral (a : A) (f : X → C(spectrum 𝕜 a, 𝕜)) (hf₁ : Integrable f μ)
    (ha : p a

Proof state:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace X
μ : Measure X
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : CompleteSpace A
inst✝ : ContinuousFunctionalCalculus 𝕜 p
a : A
f : X → C(↑(spectrum 𝕜 a), 𝕜)
hf₁ : Integrable f μ
ha : autoParam (p a) _auto✝
⊢ ∫ (x : X), (cfcL ha) (f x) ∂μ = (cfcL ha) (∫ (x : X), f x ∂μ)

Tactic:
rw [ContinuousLinearMap.integral_comp_comm _ hf₁]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_univ : volume (univ : Set ℝ) = ∞ :=
  ENNReal.eq_top_of_forall_nnreal_le fun r =>
    calc
      (r : ℝ≥0∞) = volume (Icc (0 : ℝ) r)

Proof state:
r : ℝ≥0
⊢ ↑r = volume (Icc 0 ↑r)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem MonoFactorisation.kernel_ι_comp [HasKernel f] (F : MonoFactorisation f) :
    kernel.ι f ≫ F.e = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
F : MonoFactorisation f
⊢ kernel.ι f ≫ F.e = 0

Tactic:
rw [← cancel_mono F.m, zero_comp, Category.assoc, F.fac, kernel.condition]

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Iio_eq_univ_iff : ⋃ i, Iio (f i) = univ ↔ (¬ BddAbove (range f))

Proof state:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
⊢ ⋃ i, Iio (f i) = univ ↔ ¬BddAbove (range f)

Tactic:
simp [not_bddAbove_iff, Set.eq_univ_iff_forall]

Result:
no goals
-- Mathlib/Data/Int/ConditionallyCompleteOrder.lean
theorem csInf_empty : sInf (∅ : Set ℤ) = 0 :=
  dif_neg (by simp)

Proof state:
⊢ ¬(∅.Nonempty ∧ BddBelow ∅)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_mul_eq_div_div_swap : a / (b * c) = a / c / b

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b c : α
⊢ a / (b * c) = a / c / b

Tactic:
simp only [mul_assoc, mul_inv_rev, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Order/Filter/Interval.lean
theorem tendstoIxxClass_principal {s t : Set α} {Ixx : α → α → Set α} :
    TendstoIxxClass Ixx (𝓟 s) (𝓟 t) ↔ ∀ᵉ (x ∈ s) (y ∈ s), Ixx x y ⊆ t :=
  Iff.trans ⟨fun h => h.1, fun h => ⟨h⟩⟩ <| by
    simp only [smallSets_principal, prod_principal_principal, tendsto_principal_principal,
      forall_prod_set, mem_powerset_iff, mem_principal]

Proof state:
α : Type u_1
s t : Set α
Ixx : α → α → Set α
⊢ Tendsto (fun p => Ixx p.1 p.2) (𝓟 s ×ˢ 𝓟 s) (𝓟 t).smallSets ↔ ∀ x ∈ s, ∀ y ∈ s, Ixx x y ⊆ t

Tactic:
simp only [smallSets_principal, prod_principal_principal, tendsto_principal_principal,
  forall_prod_set, mem_powerset_iff, mem_principal]

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem map_eq_zero {s : Multiset α} {f : α → β} : s.map f = 0 ↔ s = 0

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ map f s = 0 ↔ s = 0

Tactic:
rw [← Multiset.card_eq_zero, Multiset.card_map, Multiset.card_eq_zero]

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ioc_pred_left_eq_Icc (a b : α) : Ioc (pred a) b = Icc a b := coe_injective <| by simp

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a b : α
⊢ ↑(Ioc (pred a) b) = ↑(Icc a b)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.emultiplicity_self {a : α} (hfin : FiniteMultiplicity a a) :
    emultiplicity a a = 1

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
hfin : FiniteMultiplicity a a
⊢ emultiplicity a a = 1

Tactic:
simp [hfin.emultiplicity_eq_multiplicity]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_neg_one : S R (-1) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ S R (-1) = 0

Tactic:
simpa using S_sub_one R 0

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
lemma inv_sub_one : p⁻¹ - 1 = -q⁻¹

Proof state:
p q : ℝ
h : p.IsConjExponent q
⊢ p⁻¹ - 1 = -q⁻¹

Tactic:
rw [← h.inv_add_inv_conj, sub_add_cancel_left]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem map_matrix_mul (M : Matrix m n α) (N : Matrix n o α) (i : m) (j : o) (f : α →+* β) :
    f ((M * N) i j) = (M.map f * N.map f) i j

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring α
inst✝ : NonAssocSemiring β
M : Matrix m n α
N : Matrix n o α
i : m
j : o
f : α →+* β
⊢ f ((M * N) i j) = (M.map ⇑f * N.map ⇑f) i j

Tactic:
simp [Matrix.mul_apply, map_sum]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_comap_comap_eq_relrank_inf
    {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) :
    relrank (A.comap f) (B.comap f) = relrank A (B ⊓ f.fieldRange)

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
⊢ (comap f A).relrank (comap f B) = A.relrank (B ⊓ f.fieldRange)

Tactic:
simpa only [lift_id] using lift_relrank_comap_comap_eq_lift_relrank_inf A B f

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimon_.lean
theorem hom_counit_hom {M N : Bimon_ C} (f : M ⟶ N) :
    f.hom.hom ≫ N.counit.hom = M.counit.hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Bimon_ C
f : M ⟶ N
⊢ f.hom.hom ≫ N.counit.hom = M.counit.hom

Tactic:
simpa [- Comon_.Hom.hom_counit] using congr_arg Mon_.Hom.hom f.hom_counit

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
theorem self_act_act_eq {x y : R} : (x ◃ x) ◃ y = x ◃ y

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃ x) ◃ y = x ◃ y

Tactic:
rw [← right_inv x y, ← self_distrib]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
theorem riemannZeta_zero : riemannZeta 0 = -1 / 2

Proof state:
⊢ riemannZeta 0 = -1 / 2

Tactic:
simp_rw [riemannZeta, hurwitzZetaEven, Function.update_self, if_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem xor_zero (x : Nat) : x ^^^ 0 = x

Proof state:
x : Nat
⊢ x ^^^ 0 = x

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x : Nat
⊢ ∀ (i : Nat), (x ^^^ 0).testBit i = x.testBit i

Proof state:
case pred
x : Nat
⊢ ∀ (i : Nat), (x ^^^ 0).testBit i = x.testBit i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_mulIndicator (s t : Set α) (f : α → M) :
    mulIndicator s (mulIndicator t f) = mulIndicator (s ∩ t) f :=
  funext fun x => by
    simp only [mulIndicator]
    split_ifs <;> simp_all +contextual

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
⊢ s.mulIndicator (t.mulIndicator f) x = (s ∩ t).mulIndicator f x

Tactic:
simp only [mulIndicator]

Result:
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
⊢ (if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
x : α
⊢ (if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1

Tactic:
split_ifs <;> simp_all +contextual

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem eqOn_closure₂' [T2Space Z] {s : Set X} {t : Set Y} {f g : X → Y → Z}
    (h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y) (hf₁ : ∀ x, Continuous (f x))
    (hf₂ : ∀ y, Continuous fun x => f x y) (hg₁ : ∀ x, Continuous (g x))
    (hg₂ : ∀ y, Continuous fun x => g x y) : ∀ x ∈ closure s, ∀ y ∈ closure t, f x y = g x y :=
  suffices closure s ⊆ ⋂ y ∈ closure t, { x | f x y = g x y } by simpa only [subset_def, mem_iInter]
  (closure_minimal fun x hx => mem_iInter₂.2 <| Set.EqOn.closure (h x hx) (hf₁ _) (hg₁ _)) <|
    isClosed_biInter fun _ _ => isClosed_eq (hf₂ _) (hg₂ _)

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
Z : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : T2Space Z
s : Set X
t : Set Y
f g : X → Y → Z
h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y
hf₁ : ∀ (x : X), Continuous (f x)
hf₂ : ∀ (y : Y), Continuous fun x => f x y
hg₁ : ∀ (x : X), Continuous (g x)
hg₂ : ∀ (y : Y), Continuous fun x => g x y
this : closure s ⊆ ⋂ y ∈ closure t, {x | f x y = g x y}
⊢ ∀ x ∈ closure s, ∀ y ∈ closure t, f x y = g x y

Tactic:
simpa only [subset_def, mem_iInter]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompMap.lean
@[simp]
lemma swap_swap : (swap α β) ∘ₖ (swap β α) = Kernel.id

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ swap α β ∘ₖ swap β α = Kernel.id

Tactic:
simp_rw [swap, Kernel.deterministic_comp_deterministic, Prod.swap_swap_eq, Kernel.id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_modifyKey [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l):
    getValueCast? k' (modifyKey k f l) =
      if h : k == k' then
        (cast (congrArg (Option ∘ β) (eq_of_beq h)) ((getValueCast? k l).map f))
      else
        getValueCast? k' l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getValueCast? k' (modifyKey k f l) =
    if h : (k == k') = true then cast ⋯ (Option.map f (getValueCast? k l)) else getValueCast? k' l

Tactic:
simp [modifyKey_eq_alterKey, getValueCast?_alterKey, hl]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
lemma nhds_subtype_eq_comap_nhdsWithin (s : Set X) (x : { x // x ∈ s }) :
    𝓝 x = comap (↑) (𝓝[s] (x : X))

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : { x // x ∈ s }
⊢ 𝓝 x = comap Subtype.val (𝓝[s] ↑x)

Tactic:
rw [nhds_subtype, ← comap_nhdsWithin_range, Subtype.range_val]

Result:
no goals
-- Mathlib/Algebra/Group/Prod.lean
theorem comp_coprod {Q : Type*} [CommMonoid Q] (h : P →* Q) (f : M →* P) (g : N →* P) :
    h.comp (f.coprod g) = (h.comp f).coprod (h.comp g) :=
  ext fun x => by simp

Proof state:
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommMonoid P
Q : Type u_6
inst✝ : CommMonoid Q
h : P →* Q
f : M →* P
g : N →* P
x : M × N
⊢ (h.comp (f.coprod g)) x = ((h.comp f).coprod (h.comp g)) x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem le_card_sdiff (s t : Finset α) : #t - #s ≤ #(t \ s) :=
  calc
    #t - #s ≤ #t - #(s ∩ t) :=
      Nat.sub_le_sub_left (card_le_card inter_subset_left) _
    _ = #(t \ (s ∩ t)) := (card_sdiff inter_subset_right).symm
    _ ≤ #(t \ s)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(t \ (s ∩ t)) ≤ #(t \ s)

Tactic:
rw [sdiff_inter_self_right t s]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem basicOpen_mul_le_left (f g : A) : basicOpen 𝒜 (f * g) ≤ basicOpen 𝒜 f

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 f

Tactic:
exact inf_le_left

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
⊢ basicOpen 𝒜 (f * g) ≤ basicOpen 𝒜 f

Tactic:
rw [basicOpen_mul 𝒜 f g]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
⊢ basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 f
-- Mathlib/Deprecated/Cardinal/Finite.lean
theorem _root_.Cardinal.natCast_le_toPartENat_iff {n : ℕ} {c : Cardinal} :
    ↑n ≤ toPartENat c ↔ ↑n ≤ c

Proof state:
n : ℕ
c : Cardinal.{u_1}
⊢ ↑n ≤ toPartENat c ↔ ↑n ≤ c

Tactic:
rw [← toPartENat_natCast n, toPartENat_le_iff_of_le_aleph0 (le_of_lt (nat_lt_aleph0 n))]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg {b : ℝ} (hb : 0 < b) (s : ℝ) :
    (fun x : ℝ => x ^ s * exp (-b * x ^ 2)) =o[atTop] fun x : ℝ => exp (-(1 / 2) * x)

Proof state:
b : ℝ
hb : 0 < b
s : ℝ
⊢ (fun x => x ^ s * rexp (-b * x ^ 2)) =o[atTop] fun x => rexp (-(1 / 2) * x)

Tactic:
exact rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg s one_lt_two hb

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Order.lean
theorem mabs_mem_iff {S G} [Group G] [LinearOrder G] {_ : SetLike S G}
    [InvMemClass S G] {H : S} {x : G} : |x|ₘ ∈ H ↔ x ∈ H

Proof state:
S : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : LinearOrder G
x✝ : SetLike S G
inst✝ : InvMemClass S G
H : S
x : G
⊢ mabs x ∈ H ↔ x ∈ H

Tactic:
cases mabs_choice x <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem length_modify (f : α → α) : ∀ n l, length (modify f n l) = length l :=
  length_modifyTailIdx _ fun l => by cases l <;> rfl

Proof state:
α : Type u_1
f : α → α
l : List α
⊢ (modifyHead f l).length = l.length

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem ciSup_unique [Unique ι] {s : ι → α} : ⨆ i, s i = s default

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Unique ι
s : ι → α
⊢ ⨆ i, s i = s default

Tactic:
have : ∀ i, s i = s default := fun i => congr_arg s (Unique.eq_default i)

Result:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Unique ι
s : ι → α
this : ∀ (i : ι), s i = s default
⊢ ⨆ i, s i = s default

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Unique ι
s : ι → α
this : ∀ (i : ι), s i = s default
⊢ ⨆ i, s i = s default

Tactic:
simp only [this, ciSup_const]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem unzip_snd : (unzip l).snd = l.map Prod.snd

Proof state:
α✝ : Type u_1
β✝ : Type u_2
l : List (α✝ × β✝)
⊢ l.unzip.snd = map Prod.snd l

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_flatten (l : Vector (Vector β m) n) (i : Nat) :
    l.flatten[i]? =
      if hi : i < n * m then
        haveI : i / m < n

Proof state:
β : Type u_1
m n : Nat
l : Vector (Vector β m) n
i : Nat
⊢ l.flatten[i]? = if hi : i < n * m then some l[i / m][i % m] else none

Tactic:
simp [getElem?_def]

Result:
no goals

Proof state:
β : Type ?u.289146
m n : Nat
l : Vector (Vector β m) n
i : Nat
hi : i < n * m
⊢ i / m < n

Tactic:
rwa [Nat.div_lt_iff_lt_mul (Nat.pos_of_lt_mul_left hi)]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem leftCoset_mem_leftCoset {a : α} (ha : a ∈ s) : a • (s : Set α) = s :=
  Set.ext <| by simp [mem_leftCoset_iff, mul_mem_cancel_left (s.inv_mem ha)]

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ a • ↑s ↔ x ∈ ↑s

Tactic:
simp [mem_leftCoset_iff, mul_mem_cancel_left (s.inv_mem ha)]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem biInf_apply' {ι} (I : Set ι) (m : ι → OuterMeasure α) {s : Set α} (hs : s.Nonempty) :
    (⨅ i ∈ I, m i) s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨅ i ∈ I, m i (t n)

Proof state:
α : Type u_1
ι : Type u_2
I : Set ι
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
⊢ (⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)

Tactic:
simp only [← iInf_subtype'', iInf_apply' _ hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl

Proof state:
α : Type ?u.5071
β : Type ?u.5070
P : α → Prop
f : (a : α) → P a → β
⊢ ∀ (a : α), a ∈ #[] → P a

Tactic:
simp

Result:
no goals