harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem toList_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) :
    (a.mapFinIdx f).toList = a.toList.mapFinIdx (fun i a h => f i a (by simpa))

Proof state:
α : Type ?u.33232
β : Type ?u.33254
a✝ : Array α
f : (i : Nat) → α → i < a✝.size → β
i : Nat
a : α
h : i < a✝.toList.length
⊢ i < a✝.size

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : Array α
f : (i : Nat) → α → i < a.size → β
⊢ (a.mapFinIdx f).toList = a.toList.mapFinIdx fun i a_1 h => f i a_1 h

Tactic:
apply List.ext_getElem <;> simp

Result:
no goals
-- Mathlib/Topology/Order/MonotoneConvergence.lean
theorem tendsto_atBot_isLUB (h_anti : Antitone f) (ha : IsLUB (Set.range f) a) :
    Tendsto f atBot (𝓝 a)

Proof state:
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsLUB (range f) a
⊢ Tendsto f atBot (𝓝 a)

Tactic:
convert tendsto_atTop_isLUB h_anti.dual_left ha using 1

Result:
no goals
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_lt_four : π < 4

Proof state:
⊢ π < 4

Tactic:
pi_upper_bound [4 / 3]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem mem_chart_source_iff (p q : TM) :
    p ∈ (chartAt (ModelProd H E) q).source ↔ p.1 ∈ (chartAt H q.1).source

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
p q : TM
⊢ p ∈ (chartAt (ModelProd H E) q).source ↔ p.proj ∈ (chartAt H q.proj).source

Tactic:
simp only [FiberBundle.chartedSpace_chartAt, mfld_simps]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem surjOn_image (h : Semiconj f fa fb) (ha : SurjOn fa s t) : SurjOn fb (f '' s) (f '' t)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ fb (f x) ∈ fb '' (f '' s)

Tactic:
exact mem_image_of_mem _ (mem_image_of_mem _ hxs)

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ f (fa x) ∈ fb '' (f '' s)

Tactic:
rw [h x]

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ fb (f x) ∈ fb '' (f '' s)

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
⊢ SurjOn fb (f '' s) (f '' t)

Tactic:
rintro y ⟨x, hxt, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxt : x ∈ t
⊢ f x ∈ fb '' (f '' s)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxt : x ∈ t
⊢ f x ∈ fb '' (f '' s)

Tactic:
rcases ha hxt with ⟨x, hxs, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ f (fa x) ∈ fb '' (f '' s)
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_le_of_dvd (g : F[X]) (h1 : f ∣ g) (h2 : g ≠ 0) :
    f.natSepDegree ≤ g.natSepDegree

Proof state:
F : Type u
inst✝ : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
⊢ f.natSepDegree ≤ g.natSepDegree

Tactic:
classical
simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F)]
exact Finset.card_le_card <| Multiset.toFinset_subset.mpr <|
  Multiset.Le.subset <| roots.le_of_dvd (map_ne_zero h2) <| map_dvd _ h1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
⊢ f.natSepDegree ≤ g.natSepDegree

Tactic:
simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F)]

Result:
F : Type u
inst✝ : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
⊢ (f.aroots (AlgebraicClosure F)).toFinset.card ≤ (g.aroots (AlgebraicClosure F)).toFinset.card

Proof state:
F : Type u
inst✝ : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
⊢ (f.aroots (AlgebraicClosure F)).toFinset.card ≤ (g.aroots (AlgebraicClosure F)).toFinset.card

Tactic:
exact Finset.card_le_card <| Multiset.toFinset_subset.mpr <|
  Multiset.Le.subset <| roots.le_of_dvd (map_ne_zero h2) <| map_dvd _ h1

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean
@[simp] lemma smul_top (ha : IsUnit a) : a • (⊤ : AffineSubspace k V) = ⊤

Proof state:
M : Type u_1
k : Type u_2
V : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : Monoid M
inst✝¹ : DistribMulAction M V
inst✝ : SMulCommClass M k V
a : M
ha : IsUnit a
⊢ a • ⊤ = ⊤

Tactic:
ext x

Result:
case h
M : Type u_1
k : Type u_2
V : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : Monoid M
inst✝¹ : DistribMulAction M V
inst✝ : SMulCommClass M k V
a : M
ha : IsUnit a
x : V
⊢ x ∈ a • ⊤ ↔ x ∈ ⊤

Proof state:
case h
M : Type u_1
k : Type u_2
V : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : Monoid M
inst✝¹ : DistribMulAction M V
inst✝ : SMulCommClass M k V
a : M
ha : IsUnit a
x : V
⊢ x ∈ a • ⊤ ↔ x ∈ ⊤

Tactic:
simpa [smul_eq_map, map_top] using ⟨ha.unit⁻¹ • x, smul_inv_smul ha.unit _⟩

Result:
no goals
-- Mathlib/Order/Partition/Equipartition.lean
theorem indiscrete_isEquipartition {hs : s ≠ ∅} : (indiscrete hs).IsEquipartition

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
hs : s ≠ ∅
⊢ (indiscrete hs).IsEquipartition

Tactic:
rw [IsEquipartition, indiscrete_parts, coe_singleton]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
hs : s ≠ ∅
⊢ {s}.EquitableOn Finset.card

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
hs : s ≠ ∅
⊢ {s}.EquitableOn Finset.card

Tactic:
exact Set.equitableOn_singleton s _

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem head!_append [Inhabited α] (t : List α) {s : List α} (h : s ≠ []) :
    head! (s ++ t) = head! s

Proof state:
α : Type u
inst✝ : Inhabited α
t s : List α
h : s ≠ []
⊢ (s ++ t).head! = s.head!

Tactic:
induction s

Result:
case nil
α : Type u
inst✝ : Inhabited α
t : List α
h : [] ≠ []
⊢ ([] ++ t).head! = [].head!

case cons
α : Type u
inst✝ : Inhabited α
t : List α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → (tail✝ ++ t).head! = tail✝.head!
h : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝ ++ t).head! = (head✝ :: tail✝).head!

Proof state:
case cons
α : Type u
inst✝ : Inhabited α
t : List α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → (tail✝ ++ t).head! = tail✝.head!
h : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝ ++ t).head! = (head✝ :: tail✝).head!

Tactic:
rfl

Result:
no goals

Proof state:
case nil
α : Type u
inst✝ : Inhabited α
t : List α
h : [] ≠ []
⊢ ([] ++ t).head! = [].head!

Tactic:
contradiction

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
lemma isFiniteMeasure_restrict : IsFiniteMeasure (μ.restrict s) ↔ μ s ≠ ∞

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ IsFiniteMeasure (μ.restrict s) ↔ μ s ≠ ⊤

Tactic:
simp [isFiniteMeasure_iff, lt_top_iff_ne_top]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity (hfin : FiniteMultiplicity a b)
    {n : ℕ} (h : n < emultiplicity a b) : n < multiplicity a b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n < emultiplicity a b
⊢ n < multiplicity a b

Tactic:
rw [emultiplicity_eq_multiplicity hfin] at h

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n < ↑(multiplicity a b)
⊢ n < multiplicity a b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n < ↑(multiplicity a b)
⊢ n < multiplicity a b

Tactic:
assumption_mod_cast

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem map_orderEmbOfFin_univ (s : Finset α) {k : ℕ} (h : s.card = k) :
    Finset.map (s.orderEmbOfFin h).toEmbedding Finset.univ = s

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ map (s.orderEmbOfFin h).toEmbedding univ = s

Tactic:
simp [map_eq_image]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem disjoint_principal_nhdsSet : Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure s) t

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure s) t

Tactic:
rw [disjoint_principal_left, ← subset_interior_iff_mem_nhdsSet, interior_compl,
  subset_compl_iff_disjoint_left]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem findSome?_succ_of_isSome {f : Fin (n+1) → Option α} (h : (f 0).isSome) :
    findSome? f = f 0

Proof state:
n : Nat
α : Type u_1
f : Fin (n + 1) → Option α
h : (f 0).isSome = true
⊢ findSome? f = f 0

Tactic:
cases _h : f 0 <;> simp_all [findSome?_succ_of_some]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
@[simp]
lemma height_orderIso (f : α ≃o β) (x : α) : height (f x) = height x

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height x ≤ height (f x)

Tactic:
exact height_le_height_apply_of_strictMono _ f.strictMono x

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height (f x) = height x

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height (f x) ≤ height x

case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height x ≤ height (f x)

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height (f x) ≤ height x

Tactic:
simpa using height_le_height_apply_of_strictMono _ f.symm.strictMono (f x)

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem sum_tensor {P Q R S : C} {J : Type*} (s : Finset J) (f : P ⟶ Q) (g : J → (R ⟶ S)) :
    (∑ j ∈ s, g j) ⊗ f = ∑ j ∈ s, g j ⊗ f

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ (∑ j ∈ s, g j) ⊗ f = ∑ j ∈ s, g j ⊗ f

Tactic:
simp only [tensorHom_def, sum_whiskerRight, Preadditive.sum_comp]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem isEmpty_of_colorable_zero (h : G.Colorable 0) : IsEmpty V

Proof state:
case false
V : Type u
G : SimpleGraph V
h : G.Colorable 0
⊢ V → False

Tactic:
intro v

Result:
case false
V : Type u
G : SimpleGraph V
h : G.Colorable 0
v : V
⊢ False

Proof state:
case false
V : Type u
G : SimpleGraph V
h : G.Colorable 0
v : V
⊢ False

Tactic:
obtain ⟨i, hi⟩ := h.some v

Result:
case false.mk
V : Type u
G : SimpleGraph V
h : G.Colorable 0
v : V
i : ℕ
hi : i < 0
⊢ False

Proof state:
case false.mk
V : Type u
G : SimpleGraph V
h : G.Colorable 0
v : V
i : ℕ
hi : i < 0
⊢ False

Tactic:
exact Nat.not_lt_zero _ hi

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
h : G.Colorable 0
⊢ IsEmpty V

Tactic:
constructor

Result:
case false
V : Type u
G : SimpleGraph V
h : G.Colorable 0
⊢ V → False
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_transpose [Field R] [Fintype m] (A : Matrix m n R) : Aᵀ.rank = A.rank

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
A : Matrix m n R
⊢ Aᵀ.rank = A.rank

Tactic:
rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
    toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
    toLin_eq_toLin', toLin'_apply', rank]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
A : Matrix m n R
⊢ Aᵀ.rank = A.rank

Tactic:
classical
rw [Aᵀ.rank_eq_finrank_range_toLin (Pi.basisFun R n).dualBasis (Pi.basisFun R m).dualBasis,
    toLin_transpose, ← LinearMap.dualMap_def, LinearMap.finrank_range_dualMap_eq_finrank_range,
    toLin_eq_toLin', toLin'_apply', rank]

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma disjSum_inj {α β : Type*} {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} :
    s₁.disjSum t₁ = s₂.disjSum t₂ ↔ s₁ = s₂ ∧ t₁ = t₂

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
t₁ t₂ : Finset β
⊢ s₁.disjSum t₁ = s₂.disjSum t₂ ↔ s₁ = s₂ ∧ t₁ = t₂

Tactic:
simp [Finset.ext_iff]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem natCast_re (n : ℕ) : re (n : K) = n

Proof state:
K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ re ↑n = ↑n

Tactic:
rw [← ofReal_natCast, ofReal_re]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
lemma isIso_of_isIso_apply (f : X ⟶ Y) [hf : ∀ i, IsIso (f i)] :
    IsIso f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f : X ⟶ Y
hf : ∀ (i : β), IsIso (f i)
⊢ IsIso f

Tactic:
change IsIso (isoMk X Y (fun i => asIso (f i))).hom

Result:
C : Type u
inst✝ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f : X ⟶ Y
hf : ∀ (i : β), IsIso (f i)
⊢ IsIso (X.isoMk Y fun i => asIso (f i)).hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f : X ⟶ Y
hf : ∀ (i : β), IsIso (f i)
⊢ IsIso (X.isoMk Y fun i => asIso (f i)).hom

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ioc_pred_right_of_not_isMin (ha : ¬IsMin b) : Ioc a (pred b) = Ioo a b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin b
⊢ Ioc a (pred b) = Ioo a b

Tactic:
rw [← Ioi_inter_Iic, Iic_pred_of_not_isMin ha, Ioi_inter_Iio]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem pentagon_hom_inv_inv_inv_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv =
      (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv = (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i

Tactic:
simp [← cancel_epi (f ◁ (α_ g h i).inv)]

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Basic.lean
theorem right_vsub_pointReflection (x y : P) : y -ᵥ pointReflection x y = 2 • (y -ᵥ x) :=
  neg_injective <| by simp [← neg_nsmul]

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ -(y -ᵥ (pointReflection x) y) = -(2 • (y -ᵥ x))

Tactic:
simp [← neg_nsmul]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_eq_of_norm_add_lt_right {z1 z2 : ℤ_[p]} (h : ‖z1 + z2‖ < ‖z2‖) : ‖z1‖ = ‖z2‖ :=
  by_contra fun hne =>
    not_lt_of_ge (by rw [norm_add_eq_max_of_ne hne]; apply le_max_right) h

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1 + z2‖ ≥ ‖z2‖

Tactic:
rw [norm_add_eq_max_of_ne hne]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ⊔ ‖z2‖ ≥ ‖z2‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ⊔ ‖z2‖ ≥ ‖z2‖

Tactic:
apply le_max_right

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem const_mul_rev (f g : R) (U hu₁ hu₂) : const R f g U hu₁ * const R g f U hu₂ = 1

Proof state:
R : Type u
inst✝ : CommRing R
f g : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl
hu₂ : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl
⊢ const R f g U hu₁ * const R g f U hu₂ = 1

Tactic:
rw [const_mul, const_congr R rfl (mul_comm g f), const_self]

Result:
no goals
-- Mathlib/Data/Nat/PrimeFin.lean
lemma primeFactors_pow (n : ℕ) (hk : k ≠ 0) : (n ^ k).primeFactors = n.primeFactors

Proof state:
case zero
n : ℕ
hk : 0 ≠ 0
⊢ (n ^ 0).primeFactors = n.primeFactors

Tactic:
simp at hk

Result:
no goals

Proof state:
case succ
n n✝ : ℕ
hk : n✝ + 1 ≠ 0
⊢ (n ^ (n✝ + 1)).primeFactors = n.primeFactors

Tactic:
rw [primeFactors_pow_succ]

Result:
no goals

Proof state:
k n : ℕ
hk : k ≠ 0
⊢ (n ^ k).primeFactors = n.primeFactors

Tactic:
cases k

Result:
case zero
n : ℕ
hk : 0 ≠ 0
⊢ (n ^ 0).primeFactors = n.primeFactors

case succ
n n✝ : ℕ
hk : n✝ + 1 ≠ 0
⊢ (n ^ (n✝ + 1)).primeFactors = n.primeFactors
-- Mathlib/ModelTheory/Definability.lean
theorem definable_finset_biUnion {ι : Type*} {f : ι → Set (α → M)}
    (hf : ∀ i, A.Definable L (f i)) (s : Finset ι) : A.Definable L (⋃ i ∈ s, f i)

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.sup f)

Tactic:
exact definable_finset_sup hf s

Result:
no goals

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (⋃ i ∈ s, f i)

Tactic:
rw [← Finset.sup_set_eq_biUnion]

Result:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.sup f)
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem intervalIntegrable_const_iff {c : E} :
    IntervalIntegrable (fun _ => c) μ a b ↔ c = 0 ∨ μ (Ι a b) < ∞

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
c : E
⊢ IntervalIntegrable (fun x => c) μ a b ↔ c = 0 ∨ μ (Ι a b) < ⊤

Tactic:
simp only [intervalIntegrable_iff, integrableOn_const]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem alternatingProd_cons' :
    ∀ (a : α) (l : List α), alternatingProd (a :: l) = a * (alternatingProd l)⁻¹
  | a, [] => by rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]
  | a, b :: l => by
    rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]

Proof state:
α : Type u_2
inst✝ : CommGroup α
a b : α
l : List α
⊢ (a :: b :: l).alternatingProd = a * (b :: l).alternatingProd⁻¹

Tactic:
rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CommGroup α
a : α
⊢ [a].alternatingProd = a * [].alternatingProd⁻¹

Tactic:
rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]

Result:
no goals
-- Mathlib/Topology/DiscreteSubset.lean
lemma tendsto_cofinite_cocompact_of_discrete [DiscreteTopology X]
    (hf : Tendsto f (cocompact _) (cocompact _)) :
    Tendsto f cofinite (cocompact _)

Proof state:
case h.e'_4
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ cofinite = cocompact X

Tactic:
rw [cocompact_eq_cofinite X]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ Tendsto f cofinite (cocompact Y)

Tactic:
convert hf

Result:
case h.e'_4
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ cofinite = cocompact X
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.tendsto_left_iff (hla : la.HasBasis pa sa) :
    Tendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
f : α → β
hla : la.HasBasis pa sa
⊢ (∀ t ∈ lb, ∃ i, pa i ∧ sa i ⊆ f ⁻¹' t) ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
f : α → β
hla : la.HasBasis pa sa
⊢ Tendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t

Tactic:
simp only [Tendsto, (hla.map f).le_iff, image_subset_iff]

Result:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
f : α → β
hla : la.HasBasis pa sa
⊢ (∀ t ∈ lb, ∃ i, pa i ∧ sa i ⊆ f ⁻¹' t) ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t
-- Mathlib/Data/Option/NAry.lean
/-- If `a` is a left identity for a binary operation `f`, then `some a` is a left identity for
`Option.map₂ f`. -/
lemma map₂_left_identity {f : α → β → β} {a : α} (h : ∀ b, f a b = b) (o : Option β) :
    map₂ f (some a) o = o

Proof state:
case none
α : Type u_1
β : Type u_2
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
⊢ map₂ f (some a) none = none

case some
α : Type u_1
β : Type u_2
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
val✝ : β
⊢ map₂ f (some a) (some val✝) = some val✝

Tactic:
exacts [rfl, congr_arg some (h _)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
o : Option β
⊢ map₂ f (some a) o = o

Tactic:
cases o

Result:
case none
α : Type u_1
β : Type u_2
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
⊢ map₂ f (some a) none = none

case some
α : Type u_1
β : Type u_2
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
val✝ : β
⊢ map₂ f (some a) (some val✝) = some val✝
-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem catalan_three : catalan 3 = 5

Proof state:
⊢ catalan 3 = 5

Tactic:
norm_num [catalan_eq_centralBinom_div, Nat.centralBinom, Nat.choose]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biprod.map_eq [HasBinaryBiproducts C] {W X Y Z : C} {f : W ⟶ Y} {g : X ⟶ Z} :
    biprod.map f g = biprod.fst ≫ f ≫ biprod.inl + biprod.snd ≫ g ≫ biprod.inr

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ map f g = fst ≫ f ≫ inl + snd ≫ g ≫ inr

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
/-- A version of `Finset.centerMass_mem_convexHull` for when the weights are nonpositive. -/
lemma Finset.centerMass_mem_convexHull_of_nonpos (t : Finset ι) (hw₀ : ∀ i ∈ t, w i ≤ 0)
    (hws : ∑ i ∈ t, w i < 0) (hz : ∀ i ∈ t, z i ∈ s) : t.centerMass w z ∈ convexHull R s

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
w : ι → R
z : ι → E
t : Finset ι
hw₀ : ∀ i ∈ t, w i ≤ 0
hws : ∑ i ∈ t, w i < 0
hz : ∀ i ∈ t, z i ∈ s
⊢ 0 < ∑ i ∈ t, -w i

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
w : ι → R
z : ι → E
t : Finset ι
hw₀ : ∀ i ∈ t, w i ≤ 0
hws : ∑ i ∈ t, w i < 0
hz : ∀ i ∈ t, z i ∈ s
⊢ t.centerMass w z ∈ (convexHull R) s

Tactic:
rw [← centerMass_neg_left]

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
w : ι → R
z : ι → E
t : Finset ι
hw₀ : ∀ i ∈ t, w i ≤ 0
hws : ∑ i ∈ t, w i < 0
hz : ∀ i ∈ t, z i ∈ s
⊢ t.centerMass (-w) z ∈ (convexHull R) s

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
w : ι → R
z : ι → E
t : Finset ι
hw₀ : ∀ i ∈ t, w i ≤ 0
hws : ∑ i ∈ t, w i < 0
hz : ∀ i ∈ t, z i ∈ s
⊢ t.centerMass (-w) z ∈ (convexHull R) s

Tactic:
exact Finset.centerMass_mem_convexHull _ (fun _i hi ↦ neg_nonneg.2 <| hw₀ _ hi) (by simpa) hz

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_pair {a b : α} : Pairwise R [a, b] ↔ R a b

Proof state:
α : Type u_1
R : α → α → Prop
a b : α
⊢ Pairwise R [a, b] ↔ R a b

Tactic:
simp

Result:
no goals