harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobjectMap_comp {X'' Y'' : C} {f'' : X'' ⟶ Y''} [HasKernel f'']
    (sq : Arrow.mk f ⟶ Arrow.mk f') (sq' : Arrow.mk f' ⟶ Arrow.mk f'') :
    kernelSubobjectMap (sq ≫ sq') = kernelSubobjectMap sq ≫ kernelSubobjectMap sq'

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
inst✝³ : HasZeroMorphisms C
f : X ⟶ Y
inst✝² : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝¹ : HasKernel f'
X'' Y'' : C
f'' : X'' ⟶ Y''
inst✝ : HasKernel f''
sq : Arrow.mk f ⟶ Arrow.mk f'
sq' : Arrow.mk f' ⟶ Arrow.mk f''
⊢ kernelSubobjectMap (sq ≫ sq') = kernelSubobjectMap sq ≫ kernelSubobjectMap sq'

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem prod_mk_fst_snd (x : M ∗ N) : (fst x, snd x) = toProd x

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (fst x, snd x) = toProd x

Tactic:
rw [← fst_prod_snd, MonoidHom.prod_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/EverywherePos.lean
lemma IsEverywherePos.smul_measure (hs : IsEverywherePos μ s) {c : ℝ≥0∞} (hc : c ≠ 0) :
    IsEverywherePos (c • μ) s :=
  fun x hx n hn ↦ by simpa [hc.bot_lt, hs x hx n hn] using hc.bot_lt

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ.IsEverywherePos s
c : ℝ≥0∞
hc : c ≠ 0
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
⊢ 0 < (c • μ) n

Tactic:
simpa [hc.bot_lt, hs x hx n hn] using hc.bot_lt

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
theorem prod_extend_by_one [CommMonoid α] (s : Finset ι) (f : ι → α) :
    ∏ i, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i

Proof state:
α : Type u_1
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommMonoid α
s : Finset ι
f : ι → α
⊢ (∏ i : ι, if i ∈ s then f i else 1) = ∏ i ∈ s, f i

Tactic:
rw [← prod_filter, filter_mem_eq_inter, univ_inter]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sup_typein_limit {o : Ordinal} (ho : ∀ a, a < o → succ a < o) :
    sup.{u, u} (typein ((· < ·) : o.toType → o.toType → Prop)) = o

Proof state:
o : Ordinal.{u}
ho : ∀ a < o, succ a < o
⊢ ∀ a < o, succ a < o

Tactic:
assumption

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem mclosure_range (f : F) : closure (Set.range f) = mrange f

Proof state:
M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ closure (Set.range ⇑f) = mrange f

Tactic:
rw [← Set.image_univ, ← map_mclosure, mrange_eq_map, closure_univ]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem modEq_zero : a ≡ b [PMOD 0] ↔ a = b

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
a b : α
⊢ a ≡ b [PMOD 0] ↔ a = b

Tactic:
simp [ModEq, sub_eq_zero, eq_comm]

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
lemma schnirelmannDensity_nonneg : 0 ≤ schnirelmannDensity A :=
  Real.iInf_nonneg (fun _ => by positivity)

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
x✝ : { n // 0 < n }
⊢ 0 ≤ ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑x✝))) / ↑↑x✝

Tactic:
positivity

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem cons_subset {a : α} {s t : Multiset α} : a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Proof state:
α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Tactic:
simp [subset_iff, or_imp, forall_and]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem mem_lifts (p : S[X]) : p ∈ lifts f ↔ ∃ q : R[X], map f q = p

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ ∃ q, map f q = p

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

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem comp_C : p.comp (C a) = C (p.eval a)

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
⊢ p.comp (C a) = C (eval a p)

Tactic:
simp [comp, map_sum (C : R →+* _)]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
theorem PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap (X : SimplicialObject A) :
    PInftyToNormalizedMooreComplex X ≫ inclusionOfMooreComplexMap X = PInfty

Proof state:
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ PInftyToNormalizedMooreComplex X ≫ inclusionOfMooreComplexMap X = PInfty

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attach_map_coe (o : Option α) (f : α → β) :
    (o.attach.map fun (i : {i // i ∈ o}) => f i) = o.map f

Proof state:
α : Type u_1
β : Type u_2
o : Option α
f : α → β
⊢ Option.map (fun i => f i.val) o.attach = Option.map f o

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem map_nhds_subtype_val {s : Set X} (x : s) : map ((↑) : s → X) (𝓝 x) = 𝓝[s] ↑x

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : ↑s
⊢ map Subtype.val (𝓝 x) = 𝓝[s] ↑x

Tactic:
rw [IsInducing.subtypeVal.map_nhds_eq, Subtype.range_val]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_setWidth' (x : BitVec w) (i : Nat) (h : w ≤ v) (hi : i < v) :
    (setWidth' h x)[i] = x.getLsbD i

Proof state:
w v : Nat
x : BitVec w
i : Nat
h : w ≤ v
hi : i < v
⊢ (setWidth' h x)[i] = x.getLsbD i

Tactic:
rw [getElem_eq_testBit_toNat, toNat_setWidth', getLsbD]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addXYZ_smul (P Q : Fin 3 → R) (u v : R) :
    W'.addXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.addXYZ P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ W'.addXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.addXYZ P Q

Tactic:
rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_push_self (a : α) (l : Array α) : count a (l.push a) = count a l + 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ count a (l.push a) = count a l + 1

Tactic:
simp [count_push]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem getLeft_eq_iff (h : x.isLeft) : x.getLeft h = a ↔ x = inl a

Proof state:
α✝ : Type u_1
a : α✝
β✝ : Type u_2
x : α✝ ⊕ β✝
h : x.isLeft = true
⊢ x.getLeft h = a ↔ x = inl a

Tactic:
cases x <;> simp at h ⊢

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_add_cos : cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) :=
  ofReal_injective <| by simp [cos_add_cos]

Proof state:
x y : ℝ
⊢ ↑(cos x + cos y) = ↑(2 * cos ((x + y) / 2) * cos ((x - y) / 2))

Tactic:
simp [cos_add_cos]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem single_injective (a : Γ) : Function.Injective (single a : R → HahnSeries Γ R) :=
  fun r s rs => by rw [← coeff_single_same a r, ← coeff_single_same a s, rs]

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r s : R
rs : (single a) r = (single a) s
⊢ r = s

Tactic:
rw [← coeff_single_same a r, ← coeff_single_same a s, rs]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem mem_closedBall_self (hr : 0 ≤ r) : x ∈ closedBall p x r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : 0 ≤ r
⊢ x ∈ p.closedBall x r

Tactic:
simp [hr]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@[to_additive (attr := simp)]
lemma mulLECancellable_prod :
    MulLECancellable (∏ i ∈ s, f i) ↔ ∀ ⦃i⦄, i ∈ s → MulLECancellable (f i)

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LE α
inst✝ : MulLeftMono α
s : Finset ι
f : ι → α
⊢ MulLECancellable (∏ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → MulLECancellable (f i)

Tactic:
induction' s using Finset.cons_induction with i s hi ih <;> simp [*]

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
@[simp] lemma mem_disjiUnion {b : β} {h} : b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
b : β
h : (↑s).PairwiseDisjoint t
⊢ b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a

Tactic:
simp only [mem_def, disjiUnion_val, Multiset.mem_bind, exists_prop]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem norm_integral_le_integral_norm (h : a ≤ b) :
    ‖∫ x in a..b, f x ∂μ‖ ≤ ∫ x in a..b, ‖f x‖ ∂μ :=
  norm_integral_le_integral_norm_Ioc.trans_eq <| by rw [uIoc_of_le h, integral_of_le h]

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : a ≤ b
⊢ ∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ = ∫ (x : ℝ) in a..b, ‖f x‖ ∂μ

Tactic:
rw [uIoc_of_le h, integral_of_le h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
    {k a : α} {v : β} : getValue? a (insertEntryIfNew k v l) =
      if k == a ∧ containsKey k l = false then some v else getValue? a l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
⊢ getValue? a (insertEntryIfNew k v l) = if (k == a) = true ∧ containsKey k l = false then some v else getValue? a l

Tactic:
simp [getValue?_eq_getEntry?, getEntry?_insertEntryIfNew,
    apply_ite (Option.map (fun (y : ((_ : α) × β)) => y.2))]

Result:
no goals
-- Mathlib/RingTheory/Localization/LocalizationLocalization.lean
theorem mk'_eq_algebraMap_mk'_of_submonoid_le {M N : Submonoid R} (h : M ≤ N) [IsLocalization M S]
    [IsLocalization N T] [Algebra S T] [IsScalarTower R S T] (x : R) (y : {a : R // a ∈ M}) :
    mk' T x ⟨y.1, h y.2⟩ = algebraMap S T (mk' S x y) :=
  mk'_eq_iff_eq_mul.mpr (by simp only [IsScalarTower.algebraMap_apply R S T, ← map_mul, mk'_spec])

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
y : ↥M
⊢ (algebraMap R T) x = (algebraMap S T) (mk' S x y) * (algebraMap R T) ↑⟨↑y, ⋯⟩

Tactic:
simp only [IsScalarTower.algebraMap_apply R S T, ← map_mul, mk'_spec]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
lemma box.upper_sub_lower (ν : ι → ℤ) (i : ι) :
    (box n ν ).upper i - (box n ν).lower i = 1 / n

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
i : ι
⊢ (box n ν).upper i - (box n ν).lower i = 1 / ↑n

Tactic:
simp_rw [box, add_div, add_sub_cancel_left]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/Compact.lean
theorem IsCompactOperator.image_subset_compact_of_bounded [ContinuousConstSMul 𝕜₂ M₂]
    {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f) {S : Set M₁} (hS : Bornology.IsBounded S) :
    ∃ K : Set M₂, IsCompact K ∧ f '' S ⊆ K :=
  hf.image_subset_compact_of_isVonNBounded <| by rwa [NormedSpace.isVonNBounded_iff]

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜₁
inst✝⁶ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁵ : SeminormedAddCommGroup M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : NormedSpace 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
S : Set M₁
hS : Bornology.IsBounded S
⊢ IsVonNBounded 𝕜₁ S

Tactic:
rwa [NormedSpace.isVonNBounded_iff]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem specializes_pi {f g : ∀ i, π i} : f ⤳ g ↔ ∀ i, f i ⤳ g i

Proof state:
ι : Type u_5
π : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (π i)
f g : (i : ι) → π i
⊢ f ⤳ g ↔ ∀ (i : ι), f i ⤳ g i

Tactic:
simp only [Specializes, nhds_pi, pi_le_pi]

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem preimage_mul_right_closedBall [IsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ) :
    (fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r

Proof state:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x => x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r

Tactic:
exact preimage_smul_closedBall (MulOpposite.op a) b r

Result:
no goals

Proof state:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r

Tactic:
rw [div_eq_mul_inv]

Result:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x => x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_empty (a : α) : 𝓝[∅] a = ⊥

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[∅] a = ⊥

Tactic:
rw [nhdsWithin, principal_empty, inf_bot_eq]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/CocompactMap.lean
theorem tendsto_of_forall_preimage {f : α → β} (h : ∀ s, IsCompact s → IsCompact (f ⁻¹' s)) :
    Tendsto f (cocompact α) (cocompact β) := fun s hs =>
  match mem_cocompact.mp hs with
  | ⟨t, ht, hts⟩ =>
    mem_map.mpr (mem_cocompact.mpr ⟨f ⁻¹' t, h t ht, by simpa using preimage_mono hts⟩)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : ∀ (s : Set β), IsCompact s → IsCompact (f ⁻¹' s)
s : Set β
hs : s ∈ cocompact β
t : Set β
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ (f ⁻¹' t)ᶜ ⊆ f ⁻¹' s

Tactic:
simpa using preimage_mono hts

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
@[simp] lemma add_halves (a : K) : a / 2 + a / 2 = a

Proof state:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : NeZero 2
a : K
⊢ a / 2 + a / 2 = a

Tactic:
rw [← add_div, add_self_div_two]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma map_id : M.map id (injOn_id M.E) = M

Proof state:
α : Type u_1
M : Matroid α
⊢ M.map id ⋯ = M

Tactic:
simp [ext_iff_indep]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
private lemma lower_aux [DecidableEq α] :
    a ∈ lowerClosure ↑(s ∪ t) ↔ a ∈ lowerClosure s ∨ a ∈ lowerClosure t

Proof state:
α : Type u_1
inst✝¹ : SemilatticeSup α
s t : Finset α
a : α
inst✝ : DecidableEq α
⊢ a ∈ lowerClosure ↑(s ∪ t) ↔ a ∈ lowerClosure ↑s ∨ a ∈ lowerClosure ↑t

Tactic:
rw [coe_union, lowerClosure_union, LowerSet.mem_sup_iff]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_sdiff_add_card (s t : Finset α) : #(s \ t) + #t = #(s ∪ t)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s \ t) + #t = #(s ∪ t)

Tactic:
rw [← card_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem constantCoeff_wittSub (n : ℕ) : constantCoeff (wittSub p n) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (X 0 - X 1) = 0

Tactic:
simp only [sub_zero, RingHom.map_sub, constantCoeff_X]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittSub p n) = 0

Tactic:
apply constantCoeff_wittStructureInt p _ _ n

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (X 0 - X 1) = 0
-- Mathlib/Probability/Kernel/Defs.lean
theorem ext_fun_iff : κ = η ↔ ∀ a f, Measurable f → ∫⁻ b, f b ∂κ a = ∫⁻ b, f b ∂η a :=
  ⟨fun h a f _ => by rw [h], ext_fun⟩

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : κ = η
a : α
f : β → ℝ≥0∞
x✝ : Measurable f
⊢ ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a

Tactic:
rw [h]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem map_inv_hom (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [IsIso f] :
    F.map (inv f) ≫ F.map f = 𝟙 (F.obj Y)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map (inv f) ≫ F.map f = 𝟙 (F.obj Y)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Image.lean
lemma sigma_mk_preimage_image_eq_self : Sigma.mk i ⁻¹' (Sigma.mk i '' s) = s

Proof state:
α : Type u_1
β : α → Type u_2
i : α
s : Set (β i)
⊢ Sigma.mk i ⁻¹' (Sigma.mk i '' s) = s

Tactic:
simp [image]

Result:
no goals
-- Mathlib/Data/Vector/Mem.lean
theorem mem_cons_iff (v : Vector α n) : a' ∈ (a ::ᵥ v).toList ↔ a' = a ∨ a' ∈ v.toList

Proof state:
α : Type u_1
n : ℕ
a a' : α
v : Vector α n
⊢ a' ∈ (a ::ᵥ v).toList ↔ a' = a ∨ a' ∈ v.toList

Tactic:
rw [Vector.toList_cons, List.mem_cons]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
theorem N₁Γ₀_inv_app_f_f (K : ChainComplex C ℕ) (n : ℕ) :
    (N₁Γ₀.inv.app K).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ((toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom).f.f
      n =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n

Tactic:
apply id_comp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ (N₁Γ₀.inv.app K).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n

Tactic:
rw [N₁Γ₀_inv_app]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ((toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom).f.f
      n =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem find?_range'_eq_none {s n : Nat} {p : Nat → Bool} :
    (range' s n).find? p = none ↔ ∀ i, s ≤ i → i < s + n → !p i

Proof state:
s n : Nat
p : Nat → Bool
⊢ find? p (range' s n) = none ↔ ∀ (i : Nat), s ≤ i → i < s + n → (!p i) = true

Tactic:
simp [range'_eq_mk_range']

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem Prime.properDivisors {p : ℕ} (pp : p.Prime) : properDivisors p = {1}

Proof state:
p : ℕ
pp : Prime p
⊢ p.properDivisors = {1}

Tactic:
rw [← erase_insert properDivisors.not_self_mem, insert_self_properDivisors pp.ne_zero,
  pp.divisors, pair_comm, erase_insert fun con => pp.ne_one (mem_singleton.1 con)]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Control/ForInStep/Lemmas.lean
theorem ForInStep.bind_yield_bindList [Monad m]
    (f : α → β → m (ForInStep β)) (s : ForInStep β) (l) :
    (s.bind fun a => (yield a).bindList f l) = s.bindList f l

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m (ForInStep β)
s : ForInStep β
l : List α
⊢ (s.bind fun a => bindList f l (yield a)) = bindList f l s

Tactic:
cases s <;> simp

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_mul_relfinrank_eq_inf_relfinrank (h : B ≤ C) :
    relfinrank A B * relfinrank B C = (A ⊓ B).relfinrank C

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h : B ≤ C
⊢ A.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
simpa using congr(toNat $(relrank_mul_relrank_eq_inf_relrank A h))

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_univ_pi (ι : Type*) [Fintype ι] : dimH (univ : Set (ι → ℝ)) = Fintype.card ι

Proof state:
ι : Type u_5
inst✝ : Fintype ι
⊢ dimH univ = ↑(Fintype.card ι)

Tactic:
simp only [← Metric.iUnion_ball_nat_succ (0 : ι → ℝ), dimH_iUnion,
  dimH_ball_pi _ (Nat.cast_add_one_pos _), iSup_const]

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem coprodᵢ_neBot_iff [∀ i, Nonempty (α i)] : NeBot (Filter.coprodᵢ f) ↔ ∃ d, NeBot (f d)

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ (Filter.coprodᵢ f).NeBot ↔ ∃ d, (f d).NeBot

Tactic:
simp [coprodᵢ_neBot_iff', *]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem linearIndependent_le_span_finset {ι : Type*} (v : ι → M) (i : LinearIndependent R v)
    (w : Finset M) (s : span R (w : Set M) = ⊤) : #ι ≤ w.card

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Finset M
s : span R ↑w = ⊤
⊢ #ι ≤ ↑w.card

Tactic:
simpa only [Finset.coe_sort_coe, Fintype.card_coe] using linearIndependent_le_span v i w s

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
@[simp] lemma indep_zero_left {m₁ m₂ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} :
    Indep m₁ m₂ (0 : Kernel α Ω) μ

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
μ : Measure α
m₁ m₂ _mΩ : MeasurableSpace Ω
⊢ Indep m₁ m₂ 0 μ

Tactic:
simp [Indep]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem image_Icc (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) :
    e '' Icc x y = Icc (e x) (e y)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Icc x y = Icc (e x) (e y)

Tactic:
rw [← e.preimage_Icc, image_preimage_eq_inter_range, inter_eq_left.2 (he.out ⟨_, rfl⟩ ⟨_, rfl⟩)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem Fin.circulant_injective : ∀ n, Injective fun v : Fin n → α => circulant v
  | 0 => by simp [Injective]
  | _ + 1 => Matrix.circulant_injective

Proof state:
α : Type u_1
⊢ Injective fun v => circulant v

Tactic:
simp [Injective]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem lipschitzWith_iff_norm_div_le {f : E → F} {C : ℝ≥0} :
    LipschitzWith C f ↔ ∀ x y, ‖f x / f y‖ ≤ C * ‖x / y‖

Proof state:
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
C : ℝ≥0
⊢ LipschitzWith C f ↔ ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖

Tactic:
simp only [lipschitzWith_iff_dist_le_mul, dist_eq_norm_div]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem iInter_of_antitone_of_frequently
    {ι : Type*} [Preorder ι] [(atTop : Filter ι).IsCountablyGenerated] {s : ι → Set α}
    (hsm : Antitone s) (hs : ∃ᶠ i in atTop, MeasurableSet (s i)) : MeasurableSet (⋂ i, s i)

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_6
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet (⋂ i, s i)

Tactic:
rw [← compl_iff, compl_iInter]

Result:
α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_6
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet (⋃ i, (s i)ᶜ)

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_6
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet (⋃ i, (s i)ᶜ)

Tactic:
exact .iUnion_of_monotone_of_frequently (compl_anti.comp hsm) <| hs.mono fun _ ↦ .compl

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma unitForward_naturality₂ {F : Cᵒᵖ ⥤ Type v} (η : F ⟶ A) (X Y : C) (f : X ⟶ Y)
    (p : YonedaCollection (restrictedYonedaObj η) Y) :
    unitForward η X (YonedaCollection.map₂ (restrictedYonedaObj η) f p) =
      F.map f.op (unitForward η Y p)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X Y : C
f : X ⟶ Y
p : YonedaCollection (restrictedYonedaObj η) Y
⊢ unitForward η X (YonedaCollection.map₂ (restrictedYonedaObj η) f p) = F.map f.op (unitForward η Y p)

Tactic:
simp [unitForward]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem dist_zero_of_empty [IsEmpty α] : dist f g = 0

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
inst✝ : IsEmpty α
⊢ dist f g = 0

Tactic:
rw [(ext isEmptyElim : f = g), dist_self]

Result:
no goals