harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Card.lean
theorem exists_ne_map_eq_of_ncard_lt_of_maps_to {t : Set β} (hc : t.ncard < s.ncard) {f : α → β}
    (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Finite

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hc : t.ncard < s.ncard
f : α → β
hf : ∀ a ∈ s, f a ∈ t
ht : autoParam t.Finite _auto✝
h' : ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1 → x = x_1
⊢ False

Tactic:
exact (ncard_le_ncard_of_injOn f hf h' ht).not_lt hc

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hc : t.ncard < s.ncard
f : α → β
hf : ∀ a ∈ s, f a ∈ t
ht : autoParam t.Finite _auto✝
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
by_contra h'

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hc : t.ncard < s.ncard
f : α → β
hf : ∀ a ∈ s, f a ∈ t
ht : autoParam t.Finite _auto✝
h' : ¬∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
⊢ False

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hc : t.ncard < s.ncard
f : α → β
hf : ∀ a ∈ s, f a ∈ t
ht : autoParam t.Finite _auto✝
h' : ¬∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
⊢ False

Tactic:
simp only [Ne, exists_prop, not_exists, not_and, not_imp_not] at h'

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hc : t.ncard < s.ncard
f : α → β
hf : ∀ a ∈ s, f a ∈ t
ht : autoParam t.Finite _auto✝
h' : ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1 → x = x_1
⊢ False
-- Mathlib/Data/Finset/Basic.lean
theorem erase_cons_of_ne {a b : α} {s : Finset α} (ha : a ∉ s) (hb : a ≠ b) :
    erase (cons a s ha) b = cons a (erase s b) fun h => ha <| erase_subset _ _ h

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
ha : a ∉ s
hb : a ≠ b
⊢ (cons a s ha).erase b = cons a (s.erase b) ⋯

Tactic:
simp only [cons_eq_insert, erase_insert_of_ne hb]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Opposites.lean
theorem natDegree_opRingEquiv (p : R[X]ᵐᵒᵖ) : (opRingEquiv R p).natDegree = (unop p).natDegree

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ ((opRingEquiv R) p).natDegree = (unop p).natDegree

Tactic:
by_cases p0 : p = 0

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : p = 0
⊢ ((opRingEquiv R) p).natDegree = (unop p).natDegree

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : ¬p = 0
⊢ ((opRingEquiv R) p).natDegree = (unop p).natDegree

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : ¬p = 0
⊢ ((opRingEquiv R) p).natDegree = (unop p).natDegree

Tactic:
simp only [p0, natDegree_eq_support_max', Ne, EmbeddingLike.map_eq_zero_iff, not_false_iff,
  support_opRingEquiv, unop_eq_zero_iff]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : p = 0
⊢ ((opRingEquiv R) p).natDegree = (unop p).natDegree

Tactic:
simp only [p0, _root_.map_zero, natDegree_zero, unop_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
    (x.sshiftRight y.toNat).getMsbD i =
      (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat))

Proof state:
w : Nat
x y : BitVec w
i : Nat
⊢ (x.sshiftRight y.toNat).getMsbD i = (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat))

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem nhds_false : 𝓝 False = ⊤ :=
  TopologicalSpace.nhds_generateFrom.trans <| by simp [@and_comm (_ ∈ _), iInter_and]

Proof state:
⊢ ⨅ s ∈ {s | False ∈ s ∧ s ∈ {{True}}}, 𝓟 s = ⊤

Tactic:
simp [@and_comm (_ ∈ _), iInter_and]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_add_intCast {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℤ) : x ^ (y + n) = x ^ y * x ^ n

Proof state:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
rw [rpow_def, rpow_def, Complex.ofReal_add,
  Complex.cpow_add _ _ (Complex.ofReal_ne_zero.mpr hx), Complex.ofReal_intCast,
  Complex.cpow_intCast, ← Complex.ofReal_zpow, mul_comm, Complex.re_ofReal_mul, mul_comm]

Result:
no goals
-- Mathlib/Dynamics/OmegaLimit.lean
theorem mem_omegaLimit_singleton_iff_map_cluster_point (x : α) (y : β) :
    y ∈ ω f ϕ {x} ↔ MapClusterPt y f fun t ↦ ϕ t x

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
x : α
y : β
⊢ y ∈ ω f ϕ {x} ↔ MapClusterPt y f fun t => ϕ t x

Tactic:
simp_rw [mem_omegaLimit_iff_frequently, mapClusterPt_iff, singleton_inter_nonempty, mem_preimage]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem cospherical_pair (p₁ p₂ : P) : Cospherical ({p₁, p₂} : Set P) :=
  ⟨midpoint ℝ p₁ p₂, ‖(2 : ℝ)‖⁻¹ * dist p₁ p₂, by
    rintro p (rfl | rfl | _)
    · rw [dist_comm, dist_midpoint_left (𝕜 := ℝ)]
    · rw [dist_comm, dist_midpoint_right (𝕜 := ℝ)]⟩

Proof state:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₂ p : P
⊢ dist p (midpoint ℝ p p₂) = ‖2‖⁻¹ * dist p p₂

Tactic:
rw [dist_comm, dist_midpoint_left (𝕜 := ℝ)]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ ∀ p ∈ {p₁, p₂}, dist p (midpoint ℝ p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
rintro p (rfl | rfl | _)

Result:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₂ p : P
⊢ dist p (midpoint ℝ p p₂) = ‖2‖⁻¹ * dist p p₂

case inr.refl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ dist p₂ (midpoint ℝ p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂

Proof state:
case inr.refl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ dist p₂ (midpoint ℝ p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
rw [dist_comm, dist_midpoint_right (𝕜 := ℝ)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addY_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ≠ Q x * P z) : W.addY P Q / W.addZ P Q =
      W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ W.addY P Q / W.addZ P Q =
    (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
      ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
erw [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hP hQ hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
  negAddY_of_Z_ne_zero hP hQ hPz hQz hx, Affine.addY]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
lemma leftHomologyMap'_congr (h : Homotopy φ₁ φ₂) (h₁ : S₁.LeftHomologyData)
    (h₂ : S₂.LeftHomologyData) : leftHomologyMap' φ₁ h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' φ₁ h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂

Tactic:
rw [h.eq_add_nullHomotopic, leftHomologyMap'_add, leftHomologyMap'_nullHomotopic, add_zero]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_subset_Ico_right (h : b₁ < b₂) : Icc a b₁ ⊆ Ico a b₂

Proof state:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Icc a b₁ ⊆ Ico a b₂

Tactic:
rw [← coe_subset, coe_Icc, coe_Ico]

Result:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Icc a b₁ ⊆ Set.Ico a b₂

Proof state:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Icc a b₁ ⊆ Set.Ico a b₂

Tactic:
exact Set.Icc_subset_Ico_right h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_map (f : α → β) (arr : Array α) : (arr.map f).size = arr.size

Proof state:
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
⊢ (map f arr).toList.length = arr.toList.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
⊢ (map f arr).size = arr.size

Tactic:
simp only [← length_toList]

Result:
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
⊢ (map f arr).toList.length = arr.toList.length
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
@[simp]
lemma measure_zero : StieltjesFunction.measure 0 = 0 :=
  Measure.ext_of_Ioc _ _ (by simp)

Proof state:
⊢ ∀ ⦃a b : ℝ⦄, a < b → (StieltjesFunction.measure 0) (Ioc a b) = 0 (Ioc a b)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/QuasiSeparated.lean
theorem isQuasiSeparated_univ_iff {α : Type*} [TopologicalSpace α] :
    IsQuasiSeparated (Set.univ : Set α) ↔ QuasiSeparatedSpace α

Proof state:
α : Type u_3
inst✝ : TopologicalSpace α
⊢ IsQuasiSeparated univ ↔ QuasiSeparatedSpace α

Tactic:
rw [quasiSeparatedSpace_iff]

Result:
α : Type u_3
inst✝ : TopologicalSpace α
⊢ IsQuasiSeparated univ ↔ ∀ (U V : Set α), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

Proof state:
α : Type u_3
inst✝ : TopologicalSpace α
⊢ IsQuasiSeparated univ ↔ ∀ (U V : Set α), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

Tactic:
simp [IsQuasiSeparated]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsRatCondKernelCDFAux.isRatStieltjesPoint_ae (hf : IsRatCondKernelCDFAux f κ ν)
    [IsFiniteKernel κ] [IsFiniteKernel ν] (a : α) :
    ∀ᵐ t ∂(ν a), IsRatStieltjesPoint f (a, t)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
t : β
ht_top : Tendsto (f (a, t)) atTop (𝓝 1)
ht_bot : Tendsto (f (a, t)) atBot (𝓝 0)
ht_iInf : ∀ (q : ℚ), ⨅ r, f (a, t) ↑r = f (a, t) q
h_mono : Monotone (f (a, t))
⊢ IsRatStieltjesPoint f (a, t)

Tactic:
exact ⟨h_mono, ht_top, ht_bot, ht_iInf⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, IsRatStieltjesPoint f (a, t)

Tactic:
filter_upwards [hf.tendsto_atTop_one a, hf.tendsto_atBot_zero a,
  hf.iInf_rat_gt_eq a, hf.mono a] with t ht_top ht_bot ht_iInf h_mono

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
t : β
ht_top : Tendsto (f (a, t)) atTop (𝓝 1)
ht_bot : Tendsto (f (a, t)) atBot (𝓝 0)
ht_iInf : ∀ (q : ℚ), ⨅ r, f (a, t) ↑r = f (a, t) q
h_mono : Monotone (f (a, t))
⊢ IsRatStieltjesPoint f (a, t)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma evalEval_polynomial (x y : R) : W'.polynomial.evalEval x y =
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) =
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆)

Tactic:
eval_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ y ^ 2 + (W'.a₁ * x + W'.a₃) * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆) =
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y W'.polynomial = y ^ 2 + W'.a₁ * x * y + W'.a₃ * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆)

Tactic:
simp only [polynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) =
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ y ^ 2 + (W'.a₁ * x + W'.a₃) * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆) =
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆)

Tactic:
rw [add_mul, ← add_assoc]

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

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

Tactic:
assumption_mod_cast

Result:
no goals

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

Tactic:
rw [emultiplicity_eq_multiplicity hfin]

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b < n
⊢ ↑(multiplicity a b) < ↑n
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem mulETransformRight_inv : mulETransformRight e⁻¹ x = (mulETransformLeft e x.swap).swap

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulETransformRight e⁻¹ x = (mulETransformLeft e x.swap).swap

Tactic:
simp [-op_inv, op_smul_eq_smul, mulETransformLeft, mulETransformRight]

Result:
no goals
-- Mathlib/Order/Category/DistLat.lean
lemma hom_inv_apply {X Y : DistLat} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s

Proof state:
X Y : DistLat
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem Unit_of_divided_by_X_pow_order_zero : Unit_of_divided_by_X_pow_order (0 : k⟦X⟧) = 1

Proof state:
k : Type u_2
inst✝ : Field k
⊢ Unit_of_divided_by_X_pow_order 0 = 1

Tactic:
simp only [Unit_of_divided_by_X_pow_order, dif_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_extractLsb' {start len : Nat} {x : BitVec n} {i : Nat} (h : i < len) :
    (extractLsb' start len x)[i] = x.getLsbD (start+i)

Proof state:
n start len : Nat
x : BitVec n
i : Nat
h : i < len
⊢ (extractLsb' start len x)[i] = x.getLsbD (start + i)

Tactic:
simp [getElem_eq_testBit_toNat, getLsbD, h]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem _root_.Function.Injective.sSameSide_map_iff {s : AffineSubspace R P} {x y : P}
    {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
    (s.map f).SSameSide (f x) (f y) ↔ s.SSameSide x y

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
⊢ (map f s).SSameSide (f x) (f y) ↔ s.SSameSide x y

Tactic:
simp_rw [SSameSide, hf.wSameSide_map_iff, mem_map_iff_mem_of_injective hf]

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem HasBasis.nhds' {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) :
    HasBasis (𝓝 l) p fun i => { l' | s i ∈ l' }

Proof state:
ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (𝓝 l).HasBasis p fun i => {l' | s i ∈ l'}

Tactic:
simpa only [Iic_principal] using h.nhds

Result:
no goals
-- Mathlib/Tactic/Ring/RingNF.lean
theorem rat_rawCast_neg {R} [DivisionRing R] :
    (Rat.rawCast (.negOfNat n) d : R) = Int.rawCast (.negOfNat n) / Nat.rawCast d

Proof state:
n d : ℕ
R : Type u_2
inst✝ : DivisionRing R
⊢ Rat.rawCast (Int.negOfNat n) d = (Int.negOfNat n).rawCast / d.rawCast

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_union_le (s t : Set α) : (s ∪ t).encard ≤ s.encard + t.encard

Proof state:
α : Type u_1
s t : Set α
⊢ (s ∪ t).encard ≤ (s ∪ t).encard + (s ∩ t).encard

Tactic:
exact le_self_add

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
⊢ (s ∪ t).encard ≤ s.encard + t.encard

Tactic:
rw [← encard_union_add_encard_inter]

Result:
α : Type u_1
s t : Set α
⊢ (s ∪ t).encard ≤ (s ∪ t).encard + (s ∩ t).encard
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_of_singleton_coe (s : Set α) : ⋃ i : s, ({(i : α)} : Set α) = s

Proof state:
α : Type u_1
s : Set α
⊢ ⋃ i, {↑i} = s

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
lemma vecMul_conjTranspose_mul_self_eq_zero (A : Matrix m n R) (v : n → R) :
    v ᵥ* (Aᴴ * A) = 0 ↔ v ᵥ* Aᴴ = 0

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : n → R
⊢ v ᵥ* (Aᴴ * A) = 0 ↔ v ᵥ* Aᴴ = 0

Tactic:
simpa only [← Matrix.row_vecMul, row_eq_zero] using
  mul_conjTranspose_mul_self_eq_zero A (row (Fin 1) v)

Result:
no goals
-- Mathlib/Algebra/Exact.lean
lemma Exact.inr_fst : Function.Exact (LinearMap.inr R M N) (LinearMap.fst R M N)

Proof state:
case mk
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M
y : N
⊢ (LinearMap.fst R M N) (x, y) = 0 ↔ (x, y) ∈ Set.range ⇑(LinearMap.inr R M N)

Tactic:
simp only [LinearMap.fst_apply, @eq_comm _ x, LinearMap.coe_inr, Set.mem_range, Prod.mk.injEq,
  exists_eq_right]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ Exact ⇑(LinearMap.inr R M N) ⇑(LinearMap.fst R M N)

Tactic:
rintro ⟨x, y⟩

Result:
case mk
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M
y : N
⊢ (LinearMap.fst R M N) (x, y) = 0 ↔ (x, y) ∈ Set.range ⇑(LinearMap.inr R M N)
-- Mathlib/Topology/ContinuousMap/T0Sierpinski.lean
theorem eq_induced_by_maps_to_sierpinski (X : Type*) [t : TopologicalSpace X] :
    t = ⨅ u : Opens X, sierpinskiSpace.induced (· ∈ u)

Proof state:
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ (fun x => x ∈ { carrier := u, is_open' := h }) ⁻¹' {True} = u

Tactic:
simp [Set.preimage]

Result:
no goals

Proof state:
case a
X : Type u_1
t : TopologicalSpace X
⊢ ∀ (i : Opens X), t ≤ induced (fun x => x ∈ i) sierpinskiSpace

Tactic:
exact fun u => Continuous.le_induced (isOpen_iff_continuous_mem.mp u.2)

Result:
no goals

Proof state:
case a
X : Type u_1
t : TopologicalSpace X
⊢ t ≤ ⨅ u, induced (fun x => x ∈ u) sierpinskiSpace

Tactic:
rw [le_iInf_iff]

Result:
case a
X : Type u_1
t : TopologicalSpace X
⊢ ∀ (i : Opens X), t ≤ induced (fun x => x ∈ i) sierpinskiSpace

Proof state:
case a.hs
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ ∃ i t_1, IsOpen t_1 ∧ (fun x => x ∈ i) ⁻¹' t_1 = u

Tactic:
exact ⟨⟨u, h⟩, {True}, isOpen_singleton_true, by simp [Set.preimage]⟩

Result:
no goals

Proof state:
X : Type u_1
t : TopologicalSpace X
⊢ t = ⨅ u, induced (fun x => x ∈ u) sierpinskiSpace

Tactic:
apply le_antisymm

Result:
case a
X : Type u_1
t : TopologicalSpace X
⊢ t ≤ ⨅ u, induced (fun x => x ∈ u) sierpinskiSpace

case a
X : Type u_1
t : TopologicalSpace X
⊢ ⨅ u, induced (fun x => x ∈ u) sierpinskiSpace ≤ t

Proof state:
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ IsOpen u

Tactic:
apply isOpen_generateFrom_of_mem

Result:
case a.hs
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ u ∈ ⋃ i, {s | IsOpen s}

Proof state:
case a.hs
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ u ∈ ⋃ i, {s | IsOpen s}

Tactic:
simp only [Set.mem_iUnion, Set.mem_setOf_eq, isOpen_induced_iff]

Result:
case a.hs
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ ∃ i t_1, IsOpen t_1 ∧ (fun x => x ∈ i) ⁻¹' t_1 = u

Proof state:
case a
X : Type u_1
t : TopologicalSpace X
⊢ ⨅ u, induced (fun x => x ∈ u) sierpinskiSpace ≤ t

Tactic:
intro u h

Result:
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ IsOpen u
-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem limitUncurryIsoLimitCompLim_inv_π {j} {k} :
    (limitUncurryIsoLimitCompLim F).inv ≫ limit.π _ (j, k) =
      (limit.π _ j ≫ limit.π _ k : limit (_ ⋙ lim) ⟶ _)

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_5, u_1} J
inst✝⁴ : Category.{u_6, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).hom ≫ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) =
    (limitUncurryIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k

Tactic:
simp

Result:
no goals

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_5, u_1} J
inst✝⁴ : Category.{u_6, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) = limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k

Tactic:
rw [← cancel_epi (limitUncurryIsoLimitCompLim F).hom]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_5, u_1} J
inst✝⁴ : Category.{u_6, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).hom ≫ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) =
    (limitUncurryIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k
-- Mathlib/Combinatorics/SimpleGraph/LineGraph.lean
lemma lineGraph_adj_iff_exists {e₁ e₂ : G.edgeSet} :
    (G.lineGraph).Adj e₁ e₂ ↔ e₁ ≠ e₂ ∧ ∃ v, v ∈ (e₁ : Sym2 V) ∧ v ∈ (e₂ : Sym2 V)

Proof state:
V : Type u_1
G : SimpleGraph V
e₁ e₂ : ↑G.edgeSet
⊢ G.lineGraph.Adj e₁ e₂ ↔ e₁ ≠ e₂ ∧ ∃ v ∈ ↑e₁, v ∈ ↑e₂

Tactic:
simp [Set.Nonempty, lineGraph]

Result:
no goals