harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Perfect.lean
theorem AccPt.nhds_inter {x : α} {U : Set α} (h_acc : AccPt x (𝓟 C)) (hU : U ∈ 𝓝 x) :
    AccPt x (𝓟 (U ∩ C))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ 𝓝[≠] x ≤ 𝓟 U

Tactic:
rw [le_principal_iff]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ U ∈ 𝓝[≠] x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ AccPt x (𝓟 (U ∩ C))

Tactic:
rw [AccPt, ← inf_principal, ← inf_assoc, inf_of_le_left this]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ (𝓝[≠] x ⊓ 𝓟 C).NeBot

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ (𝓝[≠] x ⊓ 𝓟 C).NeBot

Tactic:
exact h_acc

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ U ∈ 𝓝[≠] x

Tactic:
exact mem_nhdsWithin_of_mem_nhds hU

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ AccPt x (𝓟 (U ∩ C))

Tactic:
have : 𝓝[≠] x ≤ 𝓟 U := by
  rw [le_principal_iff]
  exact mem_nhdsWithin_of_mem_nhds hU

Result:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ AccPt x (𝓟 (U ∩ C))
-- Mathlib/Data/List/Sort.lean
theorem erase_orderedInsert_of_not_mem [DecidableEq α]
    {x : α} {xs : List α} (hx : x ∉ xs) :
    (xs.orderedInsert r x).erase x = xs

Proof state:
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x : α
xs : List α
hx : x ∉ xs
⊢ (orderedInsert r x xs).erase x = xs

Tactic:
rw [orderedInsert_eq_take_drop, erase_append_right, List.erase_cons_head,
  takeWhile_append_dropWhile]

Result:
case h
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x : α
xs : List α
hx : x ∉ xs
⊢ x ∉ takeWhile (fun b => decide ¬r x b) xs
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
lemma isSplitEpi_toSimplexCategory_map_of_P_σ {x y : SimplexCategoryGenRel} {e : x ⟶ y}
    (he : P_σ e) : IsSplitEpi <| toSimplexCategory.map e

Proof state:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ IsSplitEpi (toSimplexCategory.map e)

Tactic:
constructor

Result:
case exists_splitEpi
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ Nonempty (SplitEpi (toSimplexCategory.map e))

Proof state:
case exists_splitEpi
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ Nonempty (SplitEpi (toSimplexCategory.map e))

Tactic:
constructor

Result:
case exists_splitEpi.val
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ SplitEpi (toSimplexCategory.map e)

Proof state:
case exists_splitEpi.val
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ SplitEpi (toSimplexCategory.map e)

Tactic:
apply SplitEpi.map

Result:
case exists_splitEpi.val.se
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ SplitEpi e

Proof state:
case exists_splitEpi.val.se
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ SplitEpi e

Tactic:
exact isSplitEpi_P_σ he |>.exists_splitEpi.some

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem exists_mem_image {f : α → β} {s : Set α} {p : β → Prop} :
    (∃ y ∈ f '' s, p y) ↔ ∃ x ∈ s, p (f x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : β → Prop
⊢ (∃ y ∈ f '' s, p y) ↔ ∃ x ∈ s, p (f x)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Wilson.lean
theorem wilsons_lemma : ((p - 1)! : ZMod p) = -1

Proof state:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => (↑a).val) a ha ∈ Ico 1 (p - 1).succ

Tactic:
rw [mem_Ico, ← Nat.succ_sub hp, Nat.add_one_sub_one]

Result:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ 1 ≤ (fun a x => (↑a).val) a ha ∧ (fun a x => (↑a).val) a ha < p

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∏ x : (ZMod p)ˣ, ↑x = ∏ x ∈ Ico 1 (p - 1).succ, ↑x

Tactic:
refine prod_bij (fun a _ => (a : ZMod p).val) ?_ ?_ ?_ ?_

Result:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (a : (ZMod p)ˣ) (ha : a ∈ univ), (fun a x => (↑a).val) a ha ∈ Ico 1 (p - 1).succ

case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (a₁ : (ZMod p)ˣ) (ha₁ : a₁ ∈ univ) (a₂ : (ZMod p)ˣ) (ha₂ : a₂ ∈ univ),
    (fun a x => (↑a).val) a₁ ha₁ = (fun a x => (↑a).val) a₂ ha₂ → a₁ = a₂

case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ b ∈ Ico 1 (p - 1).succ, ∃ a, ∃ (ha : a ∈ univ), (fun a x => (↑a).val) a ha = b

case refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (a : (ZMod p)ˣ) (ha : a ∈ univ), ↑a = ↑((fun a x => (↑a).val) a ha)

Proof state:
case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ b ∈ Ico 1 (p - 1).succ, ∃ a, ∃ (ha : a ∈ univ), (fun a x => (↑a).val) a ha = b

Tactic:
intro b hb

Result:
case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ∈ Ico 1 (p - 1).succ
⊢ ∃ a, ∃ (ha : a ∈ univ), (fun a x => (↑a).val) a ha = b

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x : (ZMod p)ˣ, ↑x = -1

Tactic:
simp_rw [← Units.coeHom_apply]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x : (ZMod p)ˣ, (Units.coeHom (ZMod p)) x = -1
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma netMaxcard_zero (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) :
    netMaxcard T F U 0 = 1

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
⊢ netMaxcard T F U 0 = 1

Tactic:
apply (iSup₂_le _).antisymm ((one_le_netMaxcard_iff T F U 0).2 h)

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
⊢ ∀ (i : Finset X), IsDynNetIn T F U 0 ↑i → ↑i.card ≤ 1

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => univ
x : X
x_s : x ∈ s
y : X
y_s : y ∈ s
⊢ x = y

Tactic:
exact PairwiseDisjoint.elim_set s_net x_s y_s x (mem_univ x) (mem_univ x)

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => univ
⊢ ↑s.card ≤ 1

Tactic:
norm_cast

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => univ
⊢ s.card ≤ 1

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => univ
⊢ s.card ≤ 1

Tactic:
refine Finset.card_le_one.2 (fun x x_s y y_s ↦ ?_)

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => univ
x : X
x_s : x ∈ s
y : X
y_s : y ∈ s
⊢ x = y

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
⊢ ∀ (i : Finset X), IsDynNetIn T F U 0 ↑i → ↑i.card ≤ 1

Tactic:
intro s ⟨_, s_net⟩

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => ball x (dynEntourage T U 0)
⊢ ↑s.card ≤ 1

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => ball x (dynEntourage T U 0)
⊢ ↑s.card ≤ 1

Tactic:
simp only [ball, dynEntourage_zero, preimage_univ] at s_net

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => univ
⊢ ↑s.card ≤ 1
-- Mathlib/Topology/Algebra/Indicator.lean
theorem ContinuousOn.continuousAt_mulIndicator (hf : ContinuousOn f (interior s)) {x : α}
    (hx : x ∉ frontier s) :
    ContinuousAt (s.mulIndicator f) x

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior s
hs : interior s ∈ 𝓝 x
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
exact ContinuousAt.congr (hf.continuousAt hs) <| Filter.eventuallyEq_iff_exists_mem.mpr
  ⟨interior s, hs, Set.eqOn_mulIndicator.symm.mono interior_subset⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior s
⊢ x ∈ interior (interior s)

Tactic:
rwa [interior_interior]

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior s
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
have hs : interior s ∈ 𝓝 x := mem_interior_iff_mem_nhds.mp (by rwa [interior_interior])

Result:
case inl
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior s
hs : interior s ∈ 𝓝 x
⊢ ContinuousAt (s.mulIndicator f) x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∈ interior s ∪ interior sᶜ
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
obtain h | h := hx

Result:
case inl
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior s
⊢ ContinuousAt (s.mulIndicator f) x

case inr
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior sᶜ
⊢ ContinuousAt (s.mulIndicator f) x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∉ frontier s
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
rw [← Set.mem_compl_iff, compl_frontier_eq_union_interior] at hx

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∈ interior s ∪ interior sᶜ
⊢ ContinuousAt (s.mulIndicator f) x

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior sᶜ
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
exact ContinuousAt.congr continuousAt_const <| Filter.eventuallyEq_iff_exists_mem.mpr
  ⟨sᶜ, mem_interior_iff_mem_nhds.mp h, Set.eqOn_mulIndicator'.symm⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem Monic.isPrimitive {p : R[X]} (hp : p.Monic) : p.IsPrimitive

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Monic
⊢ p.IsPrimitive

Tactic:
rintro r ⟨q, h⟩

Result:
case intro
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Monic
r : R
q : R[X]
h : p = C r * q
⊢ IsUnit r

Proof state:
case intro
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Monic
r : R
q : R[X]
h : p = C r * q
⊢ IsUnit r

Tactic:
exact isUnit_of_mul_eq_one r (q.coeff p.natDegree) (by rwa [← coeff_C_mul, ← h])

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Monic
r : R
q : R[X]
h : p = C r * q
⊢ r * q.coeff p.natDegree = 1

Tactic:
rwa [← coeff_C_mul, ← h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
theorem colimit_eq {j j' : J} {x : F.obj j} {x' : F.obj j'}
    (w : colimit.ι F j x = colimit.ι F j' x') :
      Relation.EqvGen (Quot.Rel F) ⟨j, x⟩ ⟨j', x'⟩

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
w : colimit.ι F j x = colimit.ι F j' x'
⊢ Relation.EqvGen (Quot.Rel F) ⟨j, x⟩ ⟨j', x'⟩

Tactic:
apply Quot.eq.1

Result:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
w : colimit.ι F j x = colimit.ι F j' x'
⊢ Quot.mk (Quot.Rel F) ⟨j, x⟩ = Quot.mk (Quot.Rel F) ⟨j', x'⟩

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
w : colimit.ι F j x = colimit.ι F j' x'
⊢ Quot.mk (Quot.Rel F) ⟨j, x⟩ = Quot.mk (Quot.Rel F) ⟨j', x'⟩

Tactic:
simpa using congr_arg (colimitEquivQuot F) w

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.centerMass_insert (ha : i ∉ t) (hw : ∑ j ∈ t, w j ≠ 0) :
    (insert i t).centerMass w z =
      (w i / (w i + ∑ j ∈ t, w j)) • z i +
        ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z

Proof state:
case e_a.e_a
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (w i + ∑ i ∈ t, w i)⁻¹ = (∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹

Tactic:
rw [div_mul_eq_mul_div, mul_inv_cancel₀ hw, one_div]

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
i : ι
t : Finset ι
w : ι → R
z : ι → E
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (insert i t).centerMass w z =
    (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z

Tactic:
simp only [centerMass, sum_insert ha, smul_add, (mul_smul _ _ _).symm, ← div_eq_inv_mul]

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (w i / (w i + ∑ i ∈ t, w i)) • z i + (w i + ∑ i ∈ t, w i)⁻¹ • ∑ i ∈ t, w i • z i =
    (w i / (w i + ∑ i ∈ t, w i)) • z i + ((∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹) • ∑ i ∈ t, w i • z i

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (w i / (w i + ∑ i ∈ t, w i)) • z i + (w i + ∑ i ∈ t, w i)⁻¹ • ∑ i ∈ t, w i • z i =
    (w i / (w i + ∑ i ∈ t, w i)) • z i + ((∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹) • ∑ i ∈ t, w i • z i

Tactic:
congr 2

Result:
case e_a.e_a
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (w i + ∑ i ∈ t, w i)⁻¹ = (∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
@[simp]
lemma one_rpow {x : ℝ} : (1 : A) ^ x = (1 : A)

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
x : ℝ
⊢ 1 ^ x = 1

Tactic:
simp [rpow_def]

Result:
no goals
-- Mathlib/Data/Finset/SDiff.lean
theorem Nontrivial.sdiff_singleton_nonempty {c : α} {s : Finset α} (hS : s.Nontrivial) :
    (s \ {c}).Nonempty

Proof state:
α : Type u_1
inst✝ : DecidableEq α
c : α
s : Finset α
hS : s.Nontrivial
⊢ ¬(s = ∅ ∨ s = {c})

Tactic:
push_neg

Result:
α : Type u_1
inst✝ : DecidableEq α
c : α
s : Finset α
hS : s.Nontrivial
⊢ s ≠ ∅ ∧ s ≠ {c}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
c : α
hS : ∅.Nontrivial
⊢ False

Tactic:
exact Finset.not_nontrivial_empty hS

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
c : α
s : Finset α
hS : s.Nontrivial
⊢ (s \ {c}).Nonempty

Tactic:
rw [Finset.sdiff_nonempty, Finset.subset_singleton_iff]

Result:
α : Type u_1
inst✝ : DecidableEq α
c : α
s : Finset α
hS : s.Nontrivial
⊢ ¬(s = ∅ ∨ s = {c})

Proof state:
α : Type u_1
inst✝ : DecidableEq α
c : α
s : Finset α
hS : s.Nontrivial
⊢ s ≠ ∅ ∧ s ≠ {c}

Tactic:
exact ⟨by rintro rfl; exact Finset.not_nontrivial_empty hS, hS.ne_singleton⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
c : α
s : Finset α
hS : s.Nontrivial
⊢ s ≠ ∅

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : DecidableEq α
c : α
hS : ∅.Nontrivial
⊢ False
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.union : range C = ⋃ (e : {o' // o' < o}), (smaller C e.val)

Proof state:
case h.refine_2.intro.intro.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
o' : Ordinal.{u}
h : o' < o
l : Products I
hl : Products.isGood (π C fun x => ord I x < o') l
⊢ Products.isGood C l

Tactic:
rw [contained_eq_proj C o hsC]

Result:
case h.refine_2.intro.intro.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o.IsLimit
hsC : contained C o
o' : Ordinal.{u}
h : o' < o
l : Products I
hl : Products.isGood (π C fun x => ord I x < o') l
⊢ Products.isGood (π C fun x => ord I x < o) l
-- Mathlib/Probability/StrongLaw.lean
theorem tsum_prob_mem_Ioi_lt_top {X : Ω → ℝ} (hint : Integrable X) (hnonneg : 0 ≤ X) :
    (∑' j : ℕ, ℙ {ω | X ω ∈ Set.Ioi (j : ℝ)}) < ∞

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
⊢ Tendsto (fun N => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))

Tactic:
refine tendsto_finset_sum _ fun i _ => ?_

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ Tendsto (fun N => ℙ {ω | X ω ∈ Set.Ioc ↑i ↑N}) atTop (𝓝 (ℙ {ω | X ω ∈ Set.Ioi ↑i}))

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N} ⊆ {ω | X ω ∈ Set.Ioi ↑i}

Tactic:
simp (config := {contextual := true}) only [Set.mem_Ioc, Set.mem_Ioi,
  Set.iUnion_subset_iff, Set.setOf_subset_setOf, imp_true_iff]

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem transEquiv_transEquiv (e : PartialEquiv α β) (f' : β ≃ γ) (f'' : γ ≃ δ) :
    (e.transEquiv f').transEquiv f'' = e.transEquiv (f'.trans f'')

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
f' : β ≃ γ
f'' : γ ≃ δ
⊢ (e.transEquiv f').transEquiv f'' = e.transEquiv (f'.trans f'')

Tactic:
simp only [transEquiv_eq_trans, trans_assoc, Equiv.trans_toPartialEquiv]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem differentiableAt_apply (i : ι) (f : ∀ i, F' i) :
    DifferentiableAt (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i) f

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
⊢ DifferentiableAt 𝕜 (fun f => f i) f

Tactic:
have h := ((differentiableAt_pi (𝕜 := 𝕜)
           (Φ := fun (f : ∀ i, F' i) (i' : ι) => f i') (x := f))).1

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
h : DifferentiableAt 𝕜 (fun f i' => f i') f → ∀ (i : ι), DifferentiableAt 𝕜 (fun x => x i) f
⊢ DifferentiableAt 𝕜 (fun f => f i) f

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
h : DifferentiableAt 𝕜 (fun f i' => f i') f → ∀ (i : ι), DifferentiableAt 𝕜 (fun x => x i) f
⊢ DifferentiableAt 𝕜 (fun f => f i) f

Tactic:
apply h

Result:
case a
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
h : DifferentiableAt 𝕜 (fun f i' => f i') f → ∀ (i : ι), DifferentiableAt 𝕜 (fun x => x i) f
⊢ DifferentiableAt 𝕜 (fun f i' => f i') f

Proof state:
case a
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
h : DifferentiableAt 𝕜 (fun f i' => f i') f → ∀ (i : ι), DifferentiableAt 𝕜 (fun x => x i) f
⊢ DifferentiableAt 𝕜 (fun f i' => f i') f

Tactic:
apply differentiableAt_id

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
    m.1.isEmpty = true → get? m a = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ m.val.isEmpty = true → get? m a = none

Tactic:
simp_to_model

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ (toListModel m.val.buckets).isEmpty = true → getValue? a (toListModel m.val.buckets) = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ (toListModel m.val.buckets).isEmpty = true → getValue? a (toListModel m.val.buckets) = none

Tactic:
empty

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem totallyBounded_of_finite_discretization {s : Set α}
    (H : ∀ ε > (0 : ℝ),
        ∃ (β : Type u) (_ : Fintype β) (F : s → β), ∀ x y, F x = F y → dist (x : α) y < ε) :
    TotallyBounded s

Proof state:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s = ∅
⊢ TotallyBounded s

Tactic:
rw [hs]

Result:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s = ∅
⊢ TotallyBounded ∅
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₈_of_isCharTwoJEqZeroNF : W.b₈ = -W.a₄ ^ 2

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 0 ^ 2 * W.a₆ + 4 * 0 * W.a₆ - 0 * W.a₃ * W.a₄ + 0 * W.a₃ ^ 2 - W.a₄ ^ 2 = -W.a₄ ^ 2

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.b₈ = -W.a₄ ^ 2

Tactic:
rw [b₈, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 0 ^ 2 * W.a₆ + 4 * 0 * W.a₆ - 0 * W.a₃ * W.a₄ + 0 * W.a₃ ^ 2 - W.a₄ ^ 2 = -W.a₄ ^ 2