harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem MemBaseSet.unionComplToSubordinate (hπ₁ : l.MemBaseSet I c r₁ π₁)
    (hle : ∀ x ∈ Box.Icc I, r₂ x ≤ r₁ x) {π₂ : Prepartition I} (hU : π₂.iUnion = ↑I \ π₁.iUnion)
    (hc : l.bDistortion → π₂.distortion ≤ c) :
    l.MemBaseSet I c r₁ (π₁.unionComplToSubordinate π₂ hU r₂) :=
  ⟨hπ₁.1.disjUnion ((π₂.isSubordinate_toSubordinate r₂).mono hle) _,
    fun h => (hπ₁.2 h).disjUnion (π₂.isHenstock_toSubordinate _) _,
    fun h => (distortion_unionComplToSubordinate _ _ _ _).trans_le (max_le (hπ₁.3 h) (hc h)),
    fun _ => ⟨⊥, by simp⟩⟩

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)
π₁ : TaggedPrepartition I
hπ₁ : l.MemBaseSet I c r₁ π₁
hle : ∀ x ∈ Box.Icc I, r₂ x ≤ r₁ x
π₂ : Prepartition I
hU : π₂.iUnion = ↑I \ π₁.iUnion
hc : l.bDistortion = true → π₂.distortion ≤ c
x✝ : l.bDistortion = true
⊢ ⊥.iUnion = ↑I \ (π₁.unionComplToSubordinate π₂ hU r₂).iUnion ∧ ⊥.distortion ≤ c

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem coord_reindex (i : ι') : (b.reindex e).coord i = b.coord (e.symm i)

Proof state:
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i : ι'
⊢ (b.reindex e).coord i = b.coord (e.symm i)

Tactic:
ext

Result:
case h
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i : ι'
p✝ : P
⊢ ((b.reindex e).coord i) p✝ = (b.coord (e.symm i)) p✝

Proof state:
case h
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i : ι'
p✝ : P
⊢ ((b.reindex e).coord i) p✝ = (b.coord (e.symm i)) p✝

Tactic:
classical simp [AffineBasis.coord]

Result:
no goals

Proof state:
case h
ι : Type u_1
ι' : Type u_2
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
e : ι ≃ ι'
i : ι'
p✝ : P
⊢ ((b.reindex e).coord i) p✝ = (b.coord (e.symm i)) p✝

Tactic:
simp [AffineBasis.coord]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_div_mul_self_add_zsmul_eq (a b : k) (ha : a ≠ 0) :
    fract (b / a) * a + ⌊b / a⌋ • a = b

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a b : k
ha : a ≠ 0
⊢ fract (b / a) * a + ⌊b / a⌋ • a = b

Tactic:
rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel₀ b ha]

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem inf_le_centerMass {s : Finset ι} {f : ι → α} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i)
    (hw₁ : 0 < ∑ i ∈ s, w i) :
    s.inf' (nonempty_of_ne_empty <| by rintro rfl; simp at hw₁) f ≤ s.centerMass w f :=
  @centerMass_le_sup R _ αᵒᵈ _ _ _ _ _ _ _ hw₀ hw₁

Proof state:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
ι : Type u_5
ι' : Type u_6
α : Type u_7
inst✝⁸ : LinearOrderedField R
inst✝⁷ : LinearOrderedField R'
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ ∅, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ ∅, w i
⊢ False

Tactic:
simp at hw₁

Result:
no goals

Proof state:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
ι : Type u_5
ι' : Type u_6
α : Type u_7
inst✝⁸ : LinearOrderedField R
inst✝⁷ : LinearOrderedField R'
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ s, w i
⊢ s ≠ ∅

Tactic:
rintro rfl

Result:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
ι : Type u_5
ι' : Type u_6
α : Type u_7
inst✝⁸ : LinearOrderedField R
inst✝⁷ : LinearOrderedField R'
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z : ι → E
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ ∅, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ ∅, w i
⊢ False
-- Mathlib/Data/PEquiv.lean
theorem refl_trans (f : α ≃. β) : (PEquiv.refl α).trans f = f

Proof state:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ f x✝ ↔ a✝ ∈ f x✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α ≃. β
⊢ (PEquiv.refl α).trans f = f

Tactic:
ext

Result:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ ((PEquiv.refl α).trans f) x✝ ↔ a✝ ∈ f x✝

Proof state:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ ((PEquiv.refl α).trans f) x✝ ↔ a✝ ∈ f x✝

Tactic:
dsimp [PEquiv.trans]

Result:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ f x✝ ↔ a✝ ∈ f x✝
-- Mathlib/Logic/Equiv/Basic.lean
theorem eq_or_eq_of_swap_apply_ne_self {a b x : α} (h : swap a b x ≠ x) : x = a ∨ x = b

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
h : (swap a b) x ≠ x
⊢ x = a ∨ x = b

Tactic:
contrapose! h

Result:
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
h : x ≠ a ∧ x ≠ b
⊢ (swap a b) x = x

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
h : x ≠ a ∧ x ≠ b
⊢ (swap a b) x = x

Tactic:
exact swap_apply_of_ne_of_ne h.1 h.2

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
theorem mapMono_δ₀ {n : ℕ} : mapMono K (δ (0 : Fin (n + 2))) = K.d (n + 1) n :=
  mapMono_δ₀' K _ (by rw [Isδ₀.iff])

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
K : ChainComplex C ℕ
n : ℕ
⊢ Isδ₀ (SimplexCategory.δ 0)

Tactic:
rw [Isδ₀.iff]

Result:
no goals
-- Mathlib/Data/PNat/Basic.lean
theorem modDivAux_spec :
    ∀ (k : ℕ+) (r q : ℕ) (_ : ¬(r = 0 ∧ q = 0)),
      ((modDivAux k r q).1 : ℕ) + k * (modDivAux k r q).2 = r + k * q
  | _, 0, 0, h => (h ⟨rfl, rfl⟩).elim
  | k, 0, q + 1, _ => by
    change (k : ℕ) + (k : ℕ) * (q + 1).pred = 0 + (k : ℕ) * (q + 1)
    rw [Nat.pred_succ, Nat.mul_succ, zero_add, add_comm]
  | _, _ + 1, _, _ => rfl

Proof state:
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑(k.modDivAux 0 (q + 1)).1 + ↑k * (k.modDivAux 0 (q + 1)).2 = 0 + ↑k * (q + 1)

Tactic:
change (k : ℕ) + (k : ℕ) * (q + 1).pred = 0 + (k : ℕ) * (q + 1)

Result:
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * (q + 1).pred = 0 + ↑k * (q + 1)

Proof state:
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * (q + 1).pred = 0 + ↑k * (q + 1)

Tactic:
rw [Nat.pred_succ, Nat.mul_succ, zero_add, add_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem id_of_comp_right_id (f : X ⟶ X) (w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g) : f = 𝟙 X

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g
⊢ f = 𝟙 X

Tactic:
convert w (𝟙 X)

Result:
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g
⊢ f = 𝟙 X ≫ f

Proof state:
case h.e'_2
C : Type u
inst✝ : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g
⊢ f = 𝟙 X ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
lemma neg_one_sq : (-1 : R) ^ 2 = 1

Proof state:
R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
⊢ (-1) ^ 2 = 1

Tactic:
simp [neg_sq, one_pow]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem image.mk (f : ZFSet.{u} → ZFSet.{u}) [Definable₁ f] (x) {y} : y ∈ x → f y ∈ image f x :=
  Quotient.inductionOn₂ x y fun ⟨_, _⟩ _ ⟨a, ya⟩ => by
    simp only [mk_eq, ← Definable₁.mk_out (f := f)]
    exact ⟨a, Definable₁.out_equiv f ya⟩

Proof state:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
x✝² x✝¹ : PSet.{u}
α✝ : Type u
A✝ : α✝ → PSet.{u}
x✝ : ⟦x✝¹⟧ ∈ ⟦PSet.mk α✝ A✝⟧
a : (PSet.mk α✝ A✝).Type
ya : x✝¹.Equiv ((PSet.mk α✝ A✝).Func a)
⊢ f ⟦x✝¹⟧ ∈ image f ⟦PSet.mk α✝ A✝⟧

Tactic:
simp only [mk_eq, ← Definable₁.mk_out (f := f)]

Result:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
x✝² x✝¹ : PSet.{u}
α✝ : Type u
A✝ : α✝ → PSet.{u}
x✝ : ⟦x✝¹⟧ ∈ ⟦PSet.mk α✝ A✝⟧
a : (PSet.mk α✝ A✝).Type
ya : x✝¹.Equiv ((PSet.mk α✝ A✝).Func a)
⊢ ZFSet.mk (Definable₁.out f x✝¹) ∈ image f (ZFSet.mk (PSet.mk α✝ A✝))

Proof state:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
x✝² x✝¹ : PSet.{u}
α✝ : Type u
A✝ : α✝ → PSet.{u}
x✝ : ⟦x✝¹⟧ ∈ ⟦PSet.mk α✝ A✝⟧
a : (PSet.mk α✝ A✝).Type
ya : x✝¹.Equiv ((PSet.mk α✝ A✝).Func a)
⊢ ZFSet.mk (Definable₁.out f x✝¹) ∈ image f (ZFSet.mk (PSet.mk α✝ A✝))

Tactic:
exact ⟨a, Definable₁.out_equiv f ya⟩

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem inf_left_le_of_le_sup_right (h : IsCompl x y) (hle : a ≤ b ⊔ y) : a ⊓ x ≤ b :=
  calc
    a ⊓ x ≤ (b ⊔ y) ⊓ x := inf_le_inf hle le_rfl
    _ = b ⊓ x ⊔ y ⊓ x := inf_sup_right _ _ _
    _ = b ⊓ x

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y : α
h : IsCompl x y
hle : a ≤ b ⊔ y
⊢ b ⊓ x ⊔ y ⊓ x = b ⊓ x

Tactic:
rw [h.symm.inf_eq_bot, sup_bot_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem or_assoc : or (or o₁ o₂) o₃ = or o₁ (or o₂ o₃)

Proof state:
α✝ : Type u_1
o₁ o₂ o₃ : Option α✝
⊢ (o₁.or o₂).or o₃ = o₁.or (o₂.or o₃)

Tactic:
cases o₁ <;> cases o₂ <;> rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_addU {K : Type v} [Field K] (f : F →+* K) (P Q : Fin 3 → F) :
    addU (f ∘ P) (f ∘ Q) = f (addU P Q)

Proof state:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ -(((⇑f ∘ P) y * (⇑f ∘ Q) z ^ 3 - (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 3) / ((⇑f ∘ P) z * (⇑f ∘ Q) z)) =
    f (-((P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z)))

Tactic:
map_simp

Result:
no goals

Proof state:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ addU (⇑f ∘ P) (⇑f ∘ Q) = f (addU P Q)

Tactic:
simp only [addU]

Result:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ -(((⇑f ∘ P) y * (⇑f ∘ Q) z ^ 3 - (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 3) / ((⇑f ∘ P) z * (⇑f ∘ Q) z)) =
    f (-((P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z)))
-- Mathlib/ModelTheory/Basic.lean
theorem card_functions_sum (i : ℕ) :
    #((L.sum L').Functions i)
      = (Cardinal.lift.{u'} #(L.Functions i) + Cardinal.lift.{u} #(L'.Functions i) : Cardinal)

Proof state:
L : Language
L' : Language
i : ℕ
⊢ #((L.sum L').Functions i) = lift.{u', u} #(L.Functions i) + lift.{u, u'} #(L'.Functions i)

Tactic:
simp [Language.sum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
    l.toArray.anyM p = l.anyM p

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
l : List α
⊢ anyM p l.toArray = List.anyM p l

Tactic:
rw [← anyM_toList]

Result:
no goals
-- Mathlib/Topology/Sheaves/SheafCondition/Sites.lean
theorem TopCat.Presheaf.isSheaf_of_isOpenEmbedding (h : IsOpenEmbedding f) (hF : F.IsSheaf) :
    IsSheaf (h.isOpenMap.functor.op ⋙ F)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
hF : F.IsSheaf
⊢ IsSheaf (⋯.functor.op ⋙ F)

Tactic:
have := h.functor_isContinuous

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
hF : F.IsSheaf
this : ⋯.functor.IsContinuous (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y)
⊢ IsSheaf (⋯.functor.op ⋙ F)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
hF : F.IsSheaf
this : ⋯.functor.IsContinuous (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y)
⊢ IsSheaf (⋯.functor.op ⋙ F)

Tactic:
exact Functor.op_comp_isSheaf _ _ _ ⟨_, hF⟩

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem map_id : map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁)

Proof state:
R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
⊢ map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁)

Tactic:
ext m

Result:
case a.h
R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
m : M₁
⊢ ((map (QuadraticMap.Isometry.id Q₁)).toLinearMap ∘ₗ ι Q₁) m =
    ((AlgHom.id R (CliffordAlgebra Q₁)).toLinearMap ∘ₗ ι Q₁) m

Proof state:
case a.h
R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
m : M₁
⊢ ((map (QuadraticMap.Isometry.id Q₁)).toLinearMap ∘ₗ ι Q₁) m =
    ((AlgHom.id R (CliffordAlgebra Q₁)).toLinearMap ∘ₗ ι Q₁) m

Tactic:
exact map_apply_ι _ m

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem isCobounded_iff_closedBall_compl_subset {s : Set α} (c : α) :
    IsCobounded s ↔ ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
⊢ Bornology.IsCobounded s ↔ ∃ r, (closedBall c r)ᶜ ⊆ s

Tactic:
rw [← isBounded_compl_iff, isBounded_iff_subset_closedBall c]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
⊢ (∃ r, sᶜ ⊆ closedBall c r) ↔ ∃ r, (closedBall c r)ᶜ ⊆ s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
⊢ (∃ r, sᶜ ⊆ closedBall c r) ↔ ∃ r, (closedBall c r)ᶜ ⊆ s

Tactic:
apply exists_congr

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
⊢ ∀ (a : ℝ), sᶜ ⊆ closedBall c a ↔ (closedBall c a)ᶜ ⊆ s

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
r : ℝ
⊢ sᶜ ⊆ closedBall c r ↔ (closedBall c r)ᶜ ⊆ s

Tactic:
rw [compl_subset_comm]

Result:
no goals

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
⊢ ∀ (a : ℝ), sᶜ ⊆ closedBall c a ↔ (closedBall c a)ᶜ ⊆ s

Tactic:
intro r

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
r : ℝ
⊢ sᶜ ⊆ closedBall c r ↔ (closedBall c r)ᶜ ⊆ s
-- Mathlib/Topology/Separation/Regular.lean
/-- In a regular space, if a compact set and a closed set are disjoint, then they have disjoint
neighborhoods. -/
lemma SeparatedNhds.of_isCompact_isClosed {s t : Set X}
    (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) : SeparatedNhds s t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
hst : Disjoint s t
⊢ SeparatedNhds s t

Tactic:
simpa only [separatedNhds_iff_disjoint, hs.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet,
  ht.closure_eq, disjoint_left] using hst

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem toSpanSingleton_eq_zero_iff {x : M} : toSpanSingleton R M x = 0 ↔ x = 0

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ toSpanSingleton R M x = 0 ↔ x = 0

Tactic:
rw [← toSpanSingleton_zero, (toSpanSingleton_injective R M).eq_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem cylinder_univ (s : Finset ι) : cylinder s (univ : Set (∀ i : s, α i)) = univ

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
⊢ cylinder s univ = univ

Tactic:
rw [cylinder, preimage_univ]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
theorem jacobiTheta_eq_tsum_nat {τ : ℂ} (hτ : 0 < im τ) :
    jacobiTheta τ = ↑1 + ↑2 * ∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)

Proof state:
τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta τ = 1 + 2 * ∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)

Tactic:
rw [(hasSum_nat_jacobiTheta hτ).tsum_eq, mul_div_cancel₀ _ (two_ne_zero' ℂ), ← add_sub_assoc,
  add_sub_cancel_left]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma BoundaryLE.not_mem {j : ι} (hj : e.BoundaryLE j) {k' : ι'} (hk' : c'.Rel (e.f j) k')
    (a : ι) : e.f a ≠ k' := fun ha =>
  hj.2 a (by simpa only [ha] using hk')

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryLE j
k' : ι'
hk' : c'.Rel (e.f j) k'
a : ι
ha : e.f a = k'
⊢ c'.Rel (e.f j) (e.f a)

Tactic:
simpa only [ha] using hk'

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_biUnion_finset₀ {s : Finset ι} {f : ι → Set α}
    (hd : Set.Pairwise (↑s) (AEDisjoint μ on f)) (hm : ∀ b ∈ s, NullMeasurableSet (f b) μ) :
    μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ μ (⋃ b ∈ s, f b) = ∑' (b : { x // x ∈ s }), μ (f ↑b)

Tactic:
exact measure_biUnion₀ s.countable_toSet hd hm

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p)

Tactic:
rw [← Finset.sum_attach, Finset.attach_eq_univ, ← tsum_fintype]

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ μ (⋃ b ∈ s, f b) = ∑' (b : { x // x ∈ s }), μ (f ↑b)
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem cauchySeq_of_edist_le_geometric_two : CauchySeq f

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ 2⁻¹ < 1

Tactic:
simp [ENNReal.one_lt_two]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ CauchySeq f

Tactic:
refine cauchySeq_of_edist_le_geometric 2⁻¹ C ?_ hC hu

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ 2⁻¹ < 1

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n
⊢ CauchySeq f

Tactic:
simp only [div_eq_mul_inv, ENNReal.inv_pow] at hu

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ CauchySeq f
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
/-- If `terminalComparison F` is an Iso, then `F` preserves terminal objects. -/
lemma preservesLimit_empty_of_isIso_terminalComparison [IsIso (terminalComparison F)] :
    PreservesLimit (Functor.empty.{0} C) F

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : IsIso (terminalComparison F)
⊢ IsLimit (F.mapCone terminal.cone)

Tactic:
apply isLimitChangeEmptyCone D terminal.isLimit

Result:
case hi
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : IsIso (terminalComparison F)
⊢ terminal.cone.pt ≅ (F.mapCone terminal.cone).pt

Proof state:
case hi
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : IsIso (terminalComparison F)
⊢ terminal.cone.pt ≅ (F.mapCone terminal.cone).pt

Tactic:
exact asIso (terminalComparison F)|>.symm

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : IsIso (terminalComparison F)
⊢ PreservesLimit (Functor.empty C) F

Tactic:
apply preservesLimit_of_preserves_limit_cone terminal.isLimit

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : IsIso (terminalComparison F)
⊢ IsLimit (F.mapCone terminal.cone)
-- Mathlib/Data/Set/Card.lean
theorem ncard_coe {α : Type*} (s : Set α) :
    Set.ncard (Set.univ : Set (Set.Elem s)) = s.ncard :=
  Set.ncard_congr (fun a ha ↦ ↑a) (fun a ha ↦ a.prop) (by simp) (by simp)

Proof state:
α : Type u_3
s : Set α
⊢ ∀ (a b : ↑s) (ha : a ∈ univ) (hb : b ∈ univ), (fun a ha => ↑a) a ha = (fun a ha => ↑a) b hb → a = b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
s : Set α
⊢ ∀ b ∈ s, ∃ a, ∃ (ha : a ∈ univ), (fun a ha => ↑a) a ha = b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.pow {m n : ℕ+} (k l : ℕ) (h : m.Coprime n) : (m ^ k : ℕ).Coprime (n ^ l)

Proof state:
m n : ℕ+
k l : ℕ
h : m.Coprime n
⊢ (↑m ^ k).Coprime (↑n ^ l)

Tactic:
rw [← coprime_coe] at *

Result:
m n : ℕ+
k l : ℕ
h : (↑m).Coprime ↑n
⊢ (↑m ^ k).Coprime (↑n ^ l)

Proof state:
m n : ℕ+
k l : ℕ
h : (↑m).Coprime ↑n
⊢ (↑m ^ k).Coprime (↑n ^ l)

Tactic:
apply Nat.Coprime.pow

Result:
case H1
m n : ℕ+
k l : ℕ
h : (↑m).Coprime ↑n
⊢ (↑m).Coprime ↑n

Proof state:
case H1
m n : ℕ+
k l : ℕ
h : (↑m).Coprime ↑n
⊢ (↑m).Coprime ↑n

Tactic:
apply h

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/OverClass.lean
lemma homIsOver_of_isOverTower [OverClass X S] [OverClass X S'] [OverClass Y S]
    [OverClass Y S'] [OverClass S S']
    [IsOverTower X S S'] [IsOverTower Y S S'] [HomIsOver f S] : HomIsOver f S'

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : C
f : X ⟶ Y
S S' : C
inst✝⁷ : OverClass X S
inst✝⁶ : OverClass X S'
inst✝⁵ : OverClass Y S
inst✝⁴ : OverClass Y S'
inst✝³ : OverClass S S'
inst✝² : IsOverTower X S S'
inst✝¹ : IsOverTower Y S S'
inst✝ : HomIsOver f S
⊢ HomIsOver f S'

Tactic:
constructor

Result:
case comp_over
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : C
f : X ⟶ Y
S S' : C
inst✝⁷ : OverClass X S
inst✝⁶ : OverClass X S'
inst✝⁵ : OverClass Y S
inst✝⁴ : OverClass Y S'
inst✝³ : OverClass S S'
inst✝² : IsOverTower X S S'
inst✝¹ : IsOverTower Y S S'
inst✝ : HomIsOver f S
⊢ autoParam (f ≫ Y ↘ S' = X ↘ S') _auto✝

Proof state:
case comp_over
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : C
f : X ⟶ Y
S S' : C
inst✝⁷ : OverClass X S
inst✝⁶ : OverClass X S'
inst✝⁵ : OverClass Y S
inst✝⁴ : OverClass Y S'
inst✝³ : OverClass S S'
inst✝² : IsOverTower X S S'
inst✝¹ : IsOverTower Y S S'
inst✝ : HomIsOver f S
⊢ autoParam (f ≫ Y ↘ S' = X ↘ S') _auto✝

Tactic:
rw [← comp_over (Y ↘ S), comp_over_assoc f, comp_over]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem closure_compl : closure sᶜ = (interior s)ᶜ

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ closure sᶜ = (interior s)ᶜ

Tactic:
simp [closure_eq_compl_interior_compl]

Result:
no goals
-- Mathlib/Data/List/TakeWhile.lean
theorem dropWhile_eq_nil_iff : dropWhile p l = [] ↔ ∀ x ∈ l, p x

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
induction' l with x xs IH

Result:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p [] = [] ↔ ∀ (x : α), x ∈ [] → p x = true

case cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Proof state:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p [] = [] ↔ ∀ (x : α), x ∈ [] → p x = true

Tactic:
simp [dropWhile]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : dropWhile p xs = [] ↔ ∀ (x : α), x ∈ xs → p x = true
⊢ dropWhile p (x :: xs) = [] ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Tactic:
by_cases hp : p x <;> simp [hp, IH]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/Normed.lean
theorem normed_sub (x : E) : f.normed μ (c - x) = f.normed μ (c + x)

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : HasContDiffBump E
inst✝ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
x : E
⊢ f.normed μ (c - x) = f.normed μ (c + x)

Tactic:
simp_rw [f.normed_def, f.sub]

Result:
no goals