harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem _root_.MeasureTheory.AEStronglyMeasurable.comp {δ : Type*} [TopologicalSpace δ]
    {f : γ → δ} (hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)) :
    ∀ᵐ x ∂κ a, AEStronglyMeasurable f (η x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel β γ
δ : Type u_5
inst✝ : TopologicalSpace δ
f : γ → δ
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ ∀ᵐ (x : β) ∂κ a, AEStronglyMeasurable f (η x)

Tactic:
filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk] with x hx using
  ⟨hf.mk f, hf.stronglyMeasurable_mk, hx⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma coe_map_Δ' : (W.map φ).Δ' = φ W.Δ'

Proof state:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ ↑(W.map φ).Δ' = φ ↑W.Δ'

Tactic:
rw [coe_Δ', map_Δ, coe_Δ']

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Mat.lean
theorem additiveObjIsoBiproduct_naturality' (F : Mat_ C ⥤ D) [Functor.Additive F] {M N : Mat_ C}
    (f : M ⟶ N) :
    (additiveObjIsoBiproduct F M).inv ≫ F.map f =
      biproduct.matrix (fun i j => F.map ((embedding C).map (f i j)) :) ≫
        (additiveObjIsoBiproduct F N).inv

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
⊢ (additiveObjIsoBiproduct F M).inv ≫ F.map f =
    (biproduct.matrix fun i j => F.map ((embedding C).map (f i j))) ≫ (additiveObjIsoBiproduct F N).inv

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, additiveObjIsoBiproduct_naturality]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- Functional equation for the even Hurwitz zeta function with poles removed (alternative form). -/
lemma completedCosZeta₀_one_sub (a : UnitAddCircle) (s : ℂ) :
    completedCosZeta₀ a (1 - s) = completedHurwitzZetaEven₀ a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedCosZeta₀ a (1 - s) = completedHurwitzZetaEven₀ a s

Tactic:
rw [← completedHurwitzZetaEven₀_one_sub, sub_sub_cancel]

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem div : ∀ {w x y z}, c w x → c y z → c (w / y) (x / z) := @fun w x y z h1 h2 => by
  simpa only [div_eq_mul_inv] using c.mul h1 (c.inv h2)

Proof state:
M : Type u_1
inst✝ : Group M
c : Con M
w x y z : M
h1 : c w x
h2 : c y z
⊢ c (w / y) (x / z)

Tactic:
simpa only [div_eq_mul_inv] using c.mul h1 (c.inv h2)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get?_set_of_lt (a : α) {m n} (l : List α) (h : n < length l) :
    (set l m a).get? n = if m = n then some a else l.get? n

Proof state:
α : Type u_1
a : α
m n : Nat
l : List α
h : n < l.length
⊢ (l.set m a).get? n = if m = n then some a else l.get? n

Tactic:
simp [getElem?_set', getElem?_eq_getElem h]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem toList_get_zero (h : x ∈ p.support) :
    (toList p x).get ⟨0, (length_toList_pos_of_mem_support _ _ h)⟩ = x

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
h : x ∈ p.support
⊢ (p.toList x).get ⟨0, ⋯⟩ = x

Tactic:
simp [toList]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma pow_self_pos : 0 < n ^ n

Proof state:
n : ℕ
⊢ 0 < n ^ n

Tactic:
simp [Nat.pow_pos_iff, n.eq_zero_or_pos.symm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_setIfInBounds_ne (a : Vector α n) (i : Nat) (x : α) (j : Nat)
    (h : i ≠ j) : (a.setIfInBounds i x)[j]? = a[j]?

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
x : α
j : Nat
h : i ≠ j
⊢ (a.setIfInBounds i x)[j]? = a[j]?

Tactic:
simp [getElem?_setIfInBounds, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_allOnes (i : Nat) (h : i < v) : (allOnes v)[i] = true

Proof state:
v i : Nat
h : i < v
⊢ (allOnes v)[i] = true

Tactic:
simp [getElem_eq_testBit_toNat, h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem tendsto_pre (m : Set X → ℝ≥0∞) (s : Set X) :
    Tendsto (fun r => pre m r s) (𝓝[>] 0) (𝓝 <| mkMetric' m s)

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto ((fun r => (pre m r) s) ∘ Subtype.val) atBot (𝓝 ((mkMetric' m) s))

Tactic:
simp only [mkMetric', OuterMeasure.iSup_apply, iSup_subtype']

Result:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto ((fun r => (pre m r) s) ∘ Subtype.val) atBot (𝓝 (⨆ i, (pre m ↑i) s))

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun r => (pre m r) s) (𝓝[>] 0) (𝓝 ((mkMetric' m) s))

Tactic:
rw [← map_coe_Ioi_atBot, tendsto_map'_iff]

Result:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto ((fun r => (pre m r) s) ∘ Subtype.val) atBot (𝓝 ((mkMetric' m) s))

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto ((fun r => (pre m r) s) ∘ Subtype.val) atBot (𝓝 (⨆ i, (pre m ↑i) s))

Tactic:
exact tendsto_atBot_iSup fun r r' hr => mono_pre _ hr _

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem card_support_le_one {f : Perm α} : #f.support ≤ 1 ↔ f = 1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ #f.support ≤ 1 ↔ f = 1

Tactic:
rw [le_iff_lt_or_eq, Nat.lt_succ_iff, Nat.le_zero, card_support_eq_zero, or_iff_not_imp_right,
  imp_iff_right f.card_support_ne_one]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ioi_sub_one_eq_Ici (a : α) : Ioi (a - 1) = Ici a

Proof state:
α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrderTop α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a : α
⊢ Ioi (a - 1) = Ici a

Tactic:
simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici a

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem uIcc_self : [[a, a]] = {a}

Proof state:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a : α
⊢ [[a, a]] = {a}

Tactic:
simp [uIcc]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem map_leftUnitor_inv (X : C) :
    F.map (λ_ X).inv = (λ_ (F.obj X)).inv ≫ ε F ▷ F.obj X ≫ μ F (𝟙_ C) X

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X : C
⊢ F.map (λ_ X).inv = (λ_ (F.obj X)).inv ≫ ε F ▷ F.obj X ≫ μ F (𝟙_ C) X

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.beq_to_eq (a b : Bool) : (a == b) = (a = b)

Proof state:
a b : Bool
⊢ ((a == b) = true) = (a = b)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem one_le_pi_div_two : (1 : ℝ) ≤ π / 2

Proof state:
⊢ 1 ≤ π / 2

Tactic:
rw [Real.pi, mul_div_cancel_left₀ _ (two_ne_zero' ℝ)]

Result:
⊢ 1 ≤ Classical.choose exists_cos_eq_zero

Proof state:
⊢ 1 ≤ Classical.choose exists_cos_eq_zero

Tactic:
exact (Classical.choose_spec exists_cos_eq_zero).1.1

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem rat_add_iff : LiouvilleWith p (r + x) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
r : ℚ
⊢ LiouvilleWith p (↑r + x) ↔ LiouvilleWith p x

Tactic:
rw [add_comm, add_rat_iff]

Result:
no goals
-- Mathlib/RingTheory/QuotSMulTop.lean
lemma map_comp_mkQ (f : M →ₗ[R] M') :
    map r f ∘ₗ mkQ (r • ⊤) = mkQ (r • ⊤) ∘ₗ f

Proof state:
R : Type u_2
inst✝⁴ : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ (map r) f ∘ₗ (r • ⊤).mkQ = (r • ⊤).mkQ ∘ₗ f

Tactic:
ext

Result:
case h
R : Type u_2
inst✝⁴ : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x✝ : M
⊢ ((map r) f ∘ₗ (r • ⊤).mkQ) x✝ = ((r • ⊤).mkQ ∘ₗ f) x✝

Proof state:
case h
R : Type u_2
inst✝⁴ : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x✝ : M
⊢ ((map r) f ∘ₗ (r • ⊤).mkQ) x✝ = ((r • ⊤).mkQ ∘ₗ f) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_preimage_mem_nhdsWithin {x : M} (h : x ∈ f.source) (ht : t ∈ 𝓝[s] x) :
    (f.extend I).symm ⁻¹' t ∈ 𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I x

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝[s] x
⊢ ↑(f.extend I).symm ⁻¹' t ∈ 𝓝[↑(f.extend I).symm ⁻¹' s ∩ range ↑I] ↑(f.extend I) x

Tactic:
rwa [← map_extend_symm_nhdsWithin f (I := I) h, mem_map] at ht

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_ball [Nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) :
    μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)

Tactic:
rw [← addHaar_ball_mul μ x hr, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_dif {f : α → β} [Decidable c] {a : c → α} :
     (if h : c then some (a h) else none).map f = if h : c then some (f (a h)) else none

Proof state:
α : Type u_1
β : Type u_2
c : Prop
f : α → β
inst✝ : Decidable c
a : c → α
⊢ Option.map f (if h : c then some (a h) else none) = if h : c then some (f (a h)) else none

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem pop_range' : (range' s n step).pop = range' s (n - 1) step

Proof state:
s n step : Nat
⊢ (range' s n step).pop = range' s (n - 1) step

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
/-- The product over `univ` of a sum can be written as a sum over the product of sets,
`Fintype.piFinset`. `Finset.prod_sum` is an alternative statement when the product is not
over `univ`. -/
lemma prod_univ_sum [Fintype ι] (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → α) :
    ∏ i, ∑ j ∈ t i, f i j = ∑ x ∈ piFinset t, ∏ i, f i (x i)

Proof state:
ι : Type u_1
α : Type u_3
κ : ι → Type u_6
inst✝² : CommSemiring α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
⊢ ∏ i : ι, ∑ j ∈ t i, f i j = ∑ x ∈ piFinset t, ∏ i : ι, f i (x i)

Tactic:
simp only [prod_attach_univ, prod_sum, Finset.sum_univ_pi]

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem zero_lt_one : (0 : ℝ) < 1

Proof state:
⊢ 0 < 1

Tactic:
convert ratCast_lt.2 zero_lt_one <;> simp [← ofCauchy_ratCast, ofCauchy_one, ofCauchy_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem epi_image_of_epi {X Y : C} (f : X ⟶ Y) [HasImage f] [E : Epi f] : Epi (image.ι f)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
E : Epi (factorThruImage f ≫ image.ι f)
⊢ Epi (image.ι f)

Tactic:
exact epi_of_epi (factorThruImage f) (image.ι f)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
E : Epi f
⊢ Epi (image.ι f)

Tactic:
rw [← image.fac f] at E

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
E : Epi (factorThruImage f ≫ image.ι f)
⊢ Epi (image.ι f)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@[simp]
lemma evalEval_polynomialY_zero : W'.polynomialY.evalEval 0 0 = W'.a₃

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ evalEval 0 0 W'.polynomialY = W'.a₃

Tactic:
simp only [evalEval_polynomialY, zero_add, mul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem ushiftRightRec_succ (x : BitVec w₁) (y : BitVec w₂) :
    ushiftRightRec x y (n + 1) = (ushiftRightRec x y n) >>> (y &&& twoPow w₂ (n + 1))

Proof state:
w₁ w₂ n : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.ushiftRightRec y (n + 1) = x.ushiftRightRec y n >>> (y &&& twoPow w₂ (n + 1))

Tactic:
simp [ushiftRightRec]

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upperCrossingTime_succ : upperCrossingTime a b f N (n + 1) ω =
    hitting f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : OrderBot ι
inst✝ : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ upperCrossingTime a b f N (n + 1) ω =
    hitting f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω

Tactic:
rw [upperCrossingTime]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem map_map (f₁ : β → γ) (f₂ : α → β) :
    map f₁ (map f₂ xs) = map (fun x => f₁ <| f₂ x) xs

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
f₁ : β → γ
f₂ : α → β
⊢ map f₁ (map f₂ xs) = map (fun x => f₁ (f₂ x)) xs

Tactic:
induction xs <;> simp_all

Result:
no goals
-- Mathlib/Data/Fin/SuccPred.lean
@[simp]
lemma orderSucc_last (n : ℕ)  :
    Order.succ (Fin.last n) = Fin.last n

Proof state:
n : ℕ
⊢ Order.succ (last n) = last n

Tactic:
simp [orderSucc_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_zero (f_zero : f 0 = 0) : seminormFromBounded' f (0 : R) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_zero : f 0 = 0
⊢ seminormFromBounded' f 0 = 0

Tactic:
simp_rw [seminormFromBounded', zero_mul, f_zero, zero_div, ciSup_const]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem nnnorm_def (x : tsze R M) : ‖x‖₊ = ‖fst x‖₊ + ‖snd x‖₊

Proof state:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ ‖x‖₊ = ‖x.fst‖₊ + ‖x.snd‖₊

Tactic:
ext

Result:
case a
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ ↑‖x‖₊ = ↑(‖x.fst‖₊ + ‖x.snd‖₊)

Proof state:
case a
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ ↑‖x‖₊ = ↑(‖x.fst‖₊ + ‖x.snd‖₊)

Tactic:
simp [norm_def]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Minpoly.lean
theorem coeff_zero_minpoly (x : K) : v ((minpoly K (algebraMap K L x)).coeff 0) = v x

Proof state:
K : Type u_1
inst✝³ : Field K
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : K
⊢ v ((minpoly K ((algebraMap K L) x)).coeff 0) = v x

Tactic:
rw [minpoly.eq_X_sub_C, coeff_sub, coeff_X_zero, coeff_C_zero, zero_sub, Valuation.map_neg]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma WithTop.lt_ofDual_iff {x : WithBot α} {y : WithTop αᵒᵈ} :
    x < WithTop.ofDual y ↔ y < WithBot.toDual x

Proof state:
α : Type u_1
inst✝ : LT α
x : WithBot α
y : WithTop αᵒᵈ
⊢ x < WithTop.ofDual y ↔ y < WithBot.toDual x

Tactic:
cases x <;> cases y <;> simp [lt_toDual]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean
lemma Nonempty.div_zero (hs : s.Nonempty) : s / 0 = 0 :=
  s.div_zero_subset.antisymm <| by simpa [mem_div] using hs

Proof state:
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ s / 0

Tactic:
simpa [mem_div] using hs

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem hasBasis_nhdsSet (s : Set X) : (𝓝ˢ s).HasBasis (fun U => IsOpen U ∧ s ⊆ U) fun U => U :=
  ⟨fun t => by simp [mem_nhdsSet_iff_exists, and_assoc]⟩

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ t ∈ 𝓝ˢ s ↔ ∃ i, (IsOpen i ∧ s ⊆ i) ∧ i ⊆ t

Tactic:
simp [mem_nhdsSet_iff_exists, and_assoc]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem length_mul_ge_length_sub_length (w₁ w₂ : W) :
    ℓ w₁ - ℓ w₂ ≤ ℓ (w₁ * w₂)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₁ - cs.length w₂ ≤ cs.length (w₁ * w₂)

Tactic:
simpa [Nat.sub_le_of_le_add] using cs.length_mul_le (w₁ * w₂) w₂⁻¹

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem RingHom.map_geom_sum₂ [Semiring α] [Semiring β] (x y : α) (n : ℕ) (f : α →+* β) :
    f (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ range n, f x ^ i * f y ^ (n - 1 - i)

Proof state:
α : Type u
β : Type u_1
inst✝¹ : Semiring α
inst✝ : Semiring β
x y : α
n : ℕ
f : α →+* β
⊢ f (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ range n, f x ^ i * f y ^ (n - 1 - i)

Tactic:
simp [map_sum f]

Result:
no goals
-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem vandermonde_transpose_mul_vandermonde {n : ℕ} (v : Fin n → R) (i j) :
    ((vandermonde v)ᵀ * vandermonde v) i j = ∑ k : Fin n, v k ^ (i + j : ℕ)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
i j : Fin n
⊢ ((vandermonde v)ᵀ * vandermonde v) i j = ∑ k : Fin n, v k ^ (↑i + ↑j)

Tactic:
simp only [vandermonde_apply, Matrix.mul_apply, Matrix.transpose_apply, pow_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem tail_append_of_ne_nil {xs ys : List α} (h : xs ≠ []) :
    (xs ++ ys).tail = xs.tail ++ ys

Proof state:
α : Type u_1
xs ys : List α
h : xs ≠ []
⊢ (xs ++ ys).tail = xs.tail ++ ys

Tactic:
simp_all [tail_append]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma mem_genEigenspace {f : End R M} {μ : R} {k : ℕ∞} {x : M} :
    x ∈ f.genEigenspace μ k ↔ ∃ l : ℕ, l ≤ k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this : Nonempty { l // ↑l ≤ k }
m n : { i // ↑i ≤ k }
h : m ≤ n
⊢ LinearMap.ker ((f - μ • 1) ^ ↑m) ≤ LinearMap.ker ((f - μ • 1) ^ ↑n)

Tactic:
simpa using (f - μ • 1).iterateKer.monotone h

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
⊢ x ∈ (f.genEigenspace μ) k ↔ ∃ l, ↑l ≤ k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)

Tactic:
have : Nonempty {l : ℕ // l ≤ k} := ⟨⟨0, zero_le _⟩⟩

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this : Nonempty { l // ↑l ≤ k }
⊢ x ∈ (f.genEigenspace μ) k ↔ ∃ l, ↑l ≤ k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 => x1 ≤ x2) fun i => LinearMap.ker ((f - μ • 1) ^ ↑i)
⊢ x ∈ (f.genEigenspace μ) k ↔ ∃ l, ↑l ≤ k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)

Tactic:
simp_rw [genEigenspace, OrderHom.coe_mk, LinearMap.mem_ker, iSup_subtype',
  Submodule.mem_iSup_of_directed _ this, LinearMap.mem_ker, Subtype.exists, exists_prop]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem splits_iff_roots_eq_three (ha : P.a ≠ 0) :
    Splits φ P.toPoly ↔ ∃ x y z : K, (map φ P).roots = {x, y, z}

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : P.a ≠ 0
⊢ Splits φ P.toPoly ↔ ∃ x y z, (map φ P).roots = {x, y, z}

Tactic:
rw [splits_iff_card_roots ha, card_eq_three]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma zeroLocus_mono {U : X.Opens} {s t : Set Γ(X, U)} (h : s ⊆ t) :
    X.zeroLocus t ⊆ X.zeroLocus s

Proof state:
X : Scheme
U : X.Opens
s t : Set ↑Γ(X, U)
h : s ⊆ t
⊢ ∀ (x : ↑↑X.toPresheafedSpace), (∀ f ∈ t, x ∉ X.basicOpen f) → ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
exact fun x H f hf hxf ↦ H f (h hf) hxf

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
s t : Set ↑Γ(X, U)
h : s ⊆ t
⊢ X.zeroLocus t ⊆ X.zeroLocus s

Tactic:
simp only [Set.subset_def, Scheme.mem_zeroLocus_iff]

Result:
X : Scheme
U : X.Opens
s t : Set ↑Γ(X, U)
h : s ⊆ t
⊢ ∀ (x : ↑↑X.toPresheafedSpace), (∀ f ∈ t, x ∉ X.basicOpen f) → ∀ f ∈ s, x ∉ X.basicOpen f
-- Mathlib/Order/Sublattice.lean
@[simp] lemma pi_top (s : Set κ) : (pi s fun _ ↦ ⊤ : Sublattice (∀ i, π i)) = ⊤ :=
  ext fun a ↦ by simp [mem_pi]

Proof state:
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
a : (i : κ) → π i
⊢ (a ∈ pi s fun x => ⊤) ↔ a ∈ ⊤

Tactic:
simp [mem_pi]

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
lemma sub_sq_comm (a b : R) : (a - b) ^ 2 = (b - a) ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = (b - a) ^ 2

Tactic:
rw [sub_sq', mul_right_comm, add_comm, sub_sq']

Result:
no goals
-- Mathlib/Topology/Baire/Lemmas.lean
theorem IsGδ.dense_biUnion_interior_of_closed {t : Set α} {s : Set X} (hs : IsGδ s) (hd : Dense s)
    (ht : t.Countable) {f : α → Set X} (hc : ∀ i ∈ t, IsClosed (f i)) (hU : s ⊆ ⋃ i ∈ t, f i) :
    Dense (⋃ i ∈ t, interior (f i))

Proof state:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
t : Set α
s : Set X
hs : IsGδ s
hd : Dense s
ht : t.Countable
f : α → Set X
this : Countable ↑t
hc : ∀ (x : ↑t), IsClosed (f ↑x)
hU : s ⊆ ⋃ x, f ↑x
⊢ Dense (⋃ x, interior (f ↑x))

Tactic:
exact hs.dense_iUnion_interior_of_closed hd hc hU

Result:
no goals

Proof state:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
t : Set α
s : Set X
hs : IsGδ s
hd : Dense s
ht : t.Countable
f : α → Set X
hc : ∀ i ∈ t, IsClosed (f i)
hU : s ⊆ ⋃ i ∈ t, f i
⊢ Dense (⋃ i ∈ t, interior (f i))

Tactic:
haveI := ht.to_subtype

Result:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
t : Set α
s : Set X
hs : IsGδ s
hd : Dense s
ht : t.Countable
f : α → Set X
hc : ∀ i ∈ t, IsClosed (f i)
hU : s ⊆ ⋃ i ∈ t, f i
this : Countable ↑t
⊢ Dense (⋃ i ∈ t, interior (f i))

Proof state:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
t : Set α
s : Set X
hs : IsGδ s
hd : Dense s
ht : t.Countable
f : α → Set X
hc : ∀ i ∈ t, IsClosed (f i)
hU : s ⊆ ⋃ i ∈ t, f i
this : Countable ↑t
⊢ Dense (⋃ i ∈ t, interior (f i))

Tactic:
simp only [biUnion_eq_iUnion, SetCoe.forall'] at *

Result:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
t : Set α
s : Set X
hs : IsGδ s
hd : Dense s
ht : t.Countable
f : α → Set X
this : Countable ↑t
hc : ∀ (x : ↑t), IsClosed (f ↑x)
hU : s ⊆ ⋃ x, f ↑x
⊢ Dense (⋃ x, interior (f ↑x))
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_succ_iff_fderiv :
    ContDiff 𝕜 (n + 1) f ↔ Differentiable 𝕜 f ∧ (n = ω → AnalyticOnNhd 𝕜 f univ) ∧
      ContDiff 𝕜 n (fderiv 𝕜 f)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
⊢ ContDiff 𝕜 (n + 1) f ↔ Differentiable 𝕜 f ∧ (n = ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 n (fderiv 𝕜 f)

Tactic:
simp only [← contDiffOn_univ, ← differentiableOn_univ, ← fderivWithin_univ,
  contDiffOn_succ_iff_fderivWithin uniqueDiffOn_univ, analyticOn_univ]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Defs.lean
theorem prod_one_cons : (1 :: l).prod = l.prod

Proof state:
M : Type u_4
inst✝ : MulOneClass M
l : List M
⊢ (1 :: l).prod = l.prod

Tactic:
rw [prod, foldr, one_mul]

Result:
no goals