harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
/--
When `f : X ⟶ Y⟦m⟧`, `m + n = mn`, `n + a = a'` and `ha'' : m + a' = a''`, this lemma
relates the two morphisms `F.shiftMap f a' a'' ha''` and `(F.shift a).map (f⟦n⟧')`. Indeed,
via canonical isomorphisms, they both identity to morphisms
`(F.shift a').obj X ⟶ (F.shift a'').obj Y`.
-/
lemma shiftIso_hom_app_comp_shiftMap {X Y : C} {m : M} (f : X ⟶ Y⟦m⟧) (n mn : M) (hnm : m + n = mn)
    (a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') :
    (F.shiftIso n a a' ha').hom.app X ≫ F.shiftMap f a' a'' ha'' =
      (F.shift a).map (f⟦n⟧') ≫ (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).inv.app Y) ≫
        (F.shiftIso mn a a'' (by rw [← ha'', ← ha', ← hnm, add_assoc])).hom.app Y

Proof state:
C : Type u_1
A : Type u_2
inst✝⁶ : Category.{?u.81967, u_1} C
inst✝⁵ : Category.{?u.81971, u_2} A
F : C ⥤ A
M : Type u_3
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
G : Type u_4
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence M
X Y : C
m : M
f : X ⟶ (shiftFunctor C m).obj Y
n mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ mn + a = a''

Tactic:
rw [← ha'', ← ha', ← hnm, add_assoc]

Result:
no goals

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Category.{u_6, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
X Y : C
m : M
f : X ⟶ (shiftFunctor C m).obj Y
n mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ (F.shiftIso n a a' ha').hom.app X ≫ F.shiftMap f a' a'' ha'' =
    (F.shift a).map ((shiftFunctor C n).map f) ≫
      (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).inv.app Y) ≫ (F.shiftIso mn a a'' ⋯).hom.app Y

Tactic:
simp only [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'' Y,
  ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
  id_comp, comp_obj, shiftIso_hom_naturality_assoc, shiftMap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attachWith_reverse {P : α → Prop} {xs : Vector α n}
    {H : ∀ (a : α), a ∈ xs.reverse → P a} :
    xs.reverse.attachWith P H =
      (xs.attachWith P (fun a h => H a (by simpa using h))).reverse

Proof state:
α : Type ?u.58109
n : Nat
P : α → Prop
xs : Vector α n
H : ∀ (a : α), a ∈ xs.reverse → P a
a : α
h : a ∈ xs
⊢ a ∈ xs.reverse

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
P : α → Prop
xs : Vector α n
H : ∀ (a : α), a ∈ xs.reverse → P a
⊢ xs.reverse.attachWith P H = (xs.attachWith P ⋯).reverse

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : Nat
P : α → Prop
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse → P a
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse.attachWith P H =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith P ⋯).reverse

Proof state:
case mk
α : Type u_1
n : Nat
P : α → Prop
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse → P a
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse.attachWith P H =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith P ⋯).reverse

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
@[simp]
lemma objMap_id (f : Arrow C) : objMap I κ (𝟙 f) = 𝟙 _

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
⊢ (𝟙 ((iteration I κ).obj f)).left = 𝟙 (obj I κ f.hom)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
⊢ objMap I κ (𝟙 f) = 𝟙 (obj I κ f.hom)

Tactic:
simp only [objMap, Functor.map_id]

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
⊢ (𝟙 ((iteration I κ).obj f)).left = 𝟙 (obj I κ f.hom)
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
@[simp]
lemma snd_compProd (μ : Measure α) [SFinite μ] (κ : Kernel α β) [IsSFiniteKernel κ] :
    (μ ⊗ₘ κ).snd = κ ∘ₘ μ

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
exact measurable_snd hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ (μ ⊗ₘ κ).snd = ⇑κ ∘ₘ μ

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ (μ ⊗ₘ κ).snd s = (⇑κ ∘ₘ μ) s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' (Prod.snd ⁻¹' s)) ∂μ = ∫⁻ (a : α), (κ a) s ∂μ

Tactic:
rfl

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ (μ ⊗ₘ κ).snd s = (⇑κ ∘ₘ μ) s

Tactic:
rw [bind_apply hs κ.measurable, snd_apply hs, compProd_apply]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' (Prod.snd ⁻¹' s)) ∂μ = ∫⁻ (a : α), (κ a) s ∂μ

case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
theorem dvd_prod [CommMonoid M] {a} {l : List M} (ha : a ∈ l) : a ∣ l.prod

Proof state:
M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ a * (s.prod * t.prod)

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
⊢ a ∣ l.prod

Tactic:
let ⟨s, t, h⟩ := append_of_mem ha

Result:
M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ l.prod

Proof state:
M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ l.prod

Tactic:
rw [h, prod_append, prod_cons, mul_left_comm]

Result:
M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ a * (s.prod * t.prod)
-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem Inv_divided_by_X_pow_order_leftInv {f : k⟦X⟧} (hf : f ≠ 0) :
    (Inv_divided_by_X_pow_order hf) * (divided_by_X_pow_order hf) = 1

Proof state:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ divided_by_X_pow_order hf * Inv_divided_by_X_pow_order hf = 1

Tactic:
exact mul_invOfUnit (divided_by_X_pow_order hf) (firstUnitCoeff hf) rfl

Result:
no goals

Proof state:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ Inv_divided_by_X_pow_order hf * divided_by_X_pow_order hf = 1

Tactic:
rw [mul_comm]

Result:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ divided_by_X_pow_order hf * Inv_divided_by_X_pow_order hf = 1
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive]
lemma smul_iterate_apply (a : M) (n : ℕ) (x : α) : (a • ·)^[n] x = a ^ n • x

Proof state:
M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
n : ℕ
x : α
⊢ (fun x => a • x)^[n] x = a ^ n • x

Tactic:
rw [smul_iterate]

Result:
no goals
-- Mathlib/Probability/Moments/ComplexMGF.lean
/-- For `z : ℂ` with `z.re ∈ interior (integrableExpSet X μ)`, the n-th derivative of the function
`complexMGF X μ` at `z` is `μ[X ^ n * cexp (z * X)]`. -/
lemma iteratedDeriv_complexMGF (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    iteratedDeriv n (complexMGF X μ) z = μ[fun ω ↦ X ω ^ n * cexp (z * X ω)]

Proof state:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      iteratedDeriv n (complexMGF X μ) z = ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv (n + 1) (complexMGF X μ) z = ∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ

Tactic:
rw [iteratedDeriv_succ]

Result:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      iteratedDeriv n (complexMGF X μ) z = ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (complexMGF X μ)) z = ∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ

Proof state:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      iteratedDeriv n (complexMGF X μ) z = ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (complexMGF X μ)) z = ∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ

Tactic:
exact (hasDerivAt_iteratedDeriv_complexMGF hz n).deriv

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ iteratedDeriv n (complexMGF X μ) z = ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ

Tactic:
induction n generalizing z with
| zero => simp [complexMGF]
| succ n hn =>
  rw [iteratedDeriv_succ]
  exact (hasDerivAt_iteratedDeriv_complexMGF hz n).deriv

Result:
no goals

Proof state:
case zero
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv 0 (complexMGF X μ) z = ∫ (x : Ω), (fun ω => ↑(X ω) ^ 0 * cexp (z * ↑(X ω))) x ∂μ

Tactic:
simp [complexMGF]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem iSup_mul (S : ι → AddSubmonoid R) (T : AddSubmonoid R) : (⨆ i, S i) * T = ⨆ i, S i * T :=
  le_antisymm (mul_le.mpr fun s hs t ht ↦ iSup_induction _ (C := (· * t ∈ _)) hs
      (fun i s hs ↦ mem_iSup_of_mem i <| mul_mem_mul hs ht) (by simp_rw [zero_mul]; apply zero_mem)
      fun _ _ ↦ by simp_rw [right_distrib]; apply add_mem) <|
    iSup_le fun i ↦ mul_le_mul_left (le_iSup _ i)

Proof state:
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_7
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
⊢ (fun x => x * t ∈ ⨆ i, S i * T) 0

Tactic:
simp_rw [zero_mul]

Result:
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_7
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
⊢ 0 ∈ ⨆ i, S i * T

Proof state:
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_7
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
x✝¹ x✝ : R
⊢ (fun x => x * t ∈ ⨆ i, S i * T) x✝¹ → (fun x => x * t ∈ ⨆ i, S i * T) x✝ → (fun x => x * t ∈ ⨆ i, S i * T) (x✝¹ + x✝)

Tactic:
simp_rw [right_distrib]

Result:
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_7
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
x✝¹ x✝ : R
⊢ x✝¹ * t ∈ ⨆ i, S i * T → x✝ * t ∈ ⨆ i, S i * T → x✝¹ * t + x✝ * t ∈ ⨆ i, S i * T

Proof state:
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_7
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
x✝¹ x✝ : R
⊢ x✝¹ * t ∈ ⨆ i, S i * T → x✝ * t ∈ ⨆ i, S i * T → x✝¹ * t + x✝ * t ∈ ⨆ i, S i * T

Tactic:
apply add_mem

Result:
no goals

Proof state:
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_7
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
⊢ 0 ∈ ⨆ i, S i * T

Tactic:
apply zero_mem

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma germ_eq_zero_of_pow_mul_eq_zero {X : Scheme.{u}} {U : Opens X} (x : U) {f s : Γ(X, U)}
    (hx : x.val ∈ X.basicOpen s) {n : ℕ} (hf : s ^ n * f = 0) : X.presheaf.germ U x x.2 f = 0

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↥U
f s : ↑Γ(X, U)
hx✝ : ↑x ∈ X.basicOpen s
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ?hx)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

case hx
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↥U
f s : ↑Γ(X, U)
hx : ↑x ∈ X.basicOpen s
n : ℕ
hf : s ^ n * f = 0
⊢ ↑x ∈ U

Tactic:
have hu : IsUnit (X.presheaf.germ _ x x.2 (s ^ n)) := by
  rw [map_pow]
  exact IsUnit.pow n hx

Result:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↥U
f s : ↑Γ(X, U)
hx✝ : ↑x ∈ X.basicOpen s
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
hu : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n))
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↥U
f s : ↑Γ(X, U)
hx✝ : ↑x ∈ X.basicOpen s
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ?hx)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s ^ n)

Tactic:
exact IsUnit.pow n hx

Result:
no goals

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↥U
f s : ↑Γ(X, U)
hx✝ : ↑x ∈ X.basicOpen s
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ?hx)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n))

Tactic:
rw [map_pow]

Result:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↥U
f s : ↑Γ(X, U)
hx✝ : ↑x ∈ X.basicOpen s
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ?hx)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s ^ n)

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↥U
f s : ↑Γ(X, U)
hx✝ : ↑x ∈ X.basicOpen s
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
hu : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n))
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

Tactic:
rw [← hu.mul_right_eq_zero, ← map_mul, hf, map_zero]

Result:
no goals

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↥U
f s : ↑Γ(X, U)
hx : ↑x ∈ X.basicOpen s
n : ℕ
hf : s ^ n * f = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

Tactic:
rw [Scheme.mem_basicOpen] at hx

Result:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↥U
f s : ↑Γ(X, U)
hx✝ : ↑x ∈ X.basicOpen s
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ?hx)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

case hx
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↥U
f s : ↑Γ(X, U)
hx : ↑x ∈ X.basicOpen s
n : ℕ
hf : s ^ n * f = 0
⊢ ↑x ∈ U
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem ordProj_dvd_ordProj_iff_dvd {a b : ℕ} (ha0 : a ≠ 0) (hb0 : b ≠ 0) :
    (∀ p : ℕ, ordProj[p] a ∣ ordProj[p] b) ↔ a ∣ b

Proof state:
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ (∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ a ∣ b

Tactic:
refine ⟨fun h => ?_, fun hab p => ordProj_dvd_ordProj_of_dvd hb0 hab p⟩

Result:
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p
⊢ a ∣ b

Proof state:
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p
⊢ a ∣ b

Tactic:
rw [← factorization_le_iff_dvd ha0 hb0]

Result:
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p
⊢ a.factorization ≤ b.factorization

Proof state:
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p
⊢ a.factorization ≤ b.factorization

Tactic:
intro q

Result:
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p
q : ℕ
⊢ a.factorization q ≤ b.factorization q

Proof state:
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p
q : ℕ
⊢ a.factorization q ≤ b.factorization q

Tactic:
rcases le_or_lt q 1 with (hq_le | hq1)

Result:
case inl
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p
q : ℕ
hq_le : q ≤ 1
⊢ a.factorization q ≤ b.factorization q

case inr
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p
q : ℕ
hq1 : 1 < q
⊢ a.factorization q ≤ b.factorization q

Proof state:
case inr
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p
q : ℕ
hq1 : 1 < q
⊢ a.factorization q ≤ b.factorization q

Tactic:
exact (pow_dvd_pow_iff_le_right hq1).1 (h q)

Result:
no goals

Proof state:
case inl
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p
q : ℕ
hq_le : q ≤ 1
⊢ a.factorization q ≤ b.factorization q

Tactic:
interval_cases q <;> simp

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
/-- A row partitioned matrix multiplied by a column partitioned matrix gives a 2 by 2 block
matrix. -/
lemma fromRows_mul_fromCols [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R)
    (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
    (fromRows A₁ A₂) * (fromCols B₁ B₂) =
      fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
⊢ A₁.fromRows A₂ * B₁.fromCols B₂ = fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)

Tactic:
ext (_ | _) (_ | _) <;> simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.HasBasis.equicontinuousWithinAt_iff_right {p : κ → Prop}
    {s : κ → Set (α × α)} {F : ι → X → α} {S : Set X} {x₀ : X} (hα : (𝓤 α).HasBasis p s) :
    EquicontinuousWithinAt F S x₀ ↔ ∀ k, p k → ∀ᶠ x in 𝓝[S] x₀, ∀ i, (F i x₀, F i x) ∈ s k

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i → ∀ᶠ (x : X) in 𝓝[S] x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s i)}) ↔
    ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k

Tactic:
rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
  (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]

Result:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i → ∀ᶠ (x : X) in 𝓝[S] x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s i)}) ↔
    ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isPrefixOf_iff_prefix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
    l₁.isPrefixOf l₂ ↔ l₁ <+: l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
⊢ l₁.isPrefixOf l₂ = true ↔ l₁ <+: l₂

Tactic:
induction l₁ generalizing l₂ with
| nil => simp
| cons a l₁ ih =>
  cases l₂ with
  | nil => simp
  | cons a' l₂ => simp [isPrefixOf, ih]

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, l₁.isPrefixOf l₂ = true ↔ l₁ <+: l₂
a' : α
l₂ : List α
⊢ (a :: l₁).isPrefixOf (a' :: l₂) = true ↔ a :: l₁ <+: a' :: l₂

Tactic:
simp [isPrefixOf, ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₂ : List α
⊢ [].isPrefixOf l₂ = true ↔ [] <+: l₂

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, l₁.isPrefixOf l₂ = true ↔ l₁ <+: l₂
l₂ : List α
⊢ (a :: l₁).isPrefixOf l₂ = true ↔ a :: l₁ <+: l₂

Tactic:
cases l₂ with
| nil => simp
| cons a' l₂ => simp [isPrefixOf, ih]

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, l₁.isPrefixOf l₂ = true ↔ l₁ <+: l₂
⊢ (a :: l₁).isPrefixOf [] = true ↔ a :: l₁ <+: []

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Int/Cast/Basic.lean
theorem cast_negOfNat (n : ℕ) : ((negOfNat n : ℤ) : R) = -n

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(negOfNat n) = -↑n

Tactic:
simp [Int.cast_neg, negOfNat_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
@[simp]
lemma vectorSpan_add_self (s : Set V) : (vectorSpan k s : Set V) + s = affineSpan k s

Proof state:
case h
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x✝ : V
⊢ (∃ x ∈ vectorSpan k s, ∃ y ∈ s, x + y = x✝) ↔ ∃ p₁ ∈ s, ∃ v ∈ vectorSpan k s, x✝ = v + p₁

Tactic:
aesop

Result:
no goals

Proof state:
case h
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x✝ : V
⊢ x✝ ∈ ↑(vectorSpan k s) + s ↔ x✝ ∈ ↑(affineSpan k s)

Tactic:
simp [mem_add, spanPoints]

Result:
case h
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x✝ : V
⊢ (∃ x ∈ vectorSpan k s, ∃ y ∈ s, x + y = x✝) ↔ ∃ p₁ ∈ s, ∃ v ∈ vectorSpan k s, x✝ = v + p₁

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(vectorSpan k s) + s = ↑(affineSpan k s)

Tactic:
ext

Result:
case h
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x✝ : V
⊢ x✝ ∈ ↑(vectorSpan k s) + s ↔ x✝ ∈ ↑(affineSpan k s)
-- Mathlib/Data/Fintype/Card.lean
theorem Fintype.card_fin_lt_of_le {m n : ℕ} (h : m ≤ n) :
    Fintype.card {i : Fin n // i < m} = m

Proof state:
case f
m n : ℕ
h : m ≤ n
⊢ { i // ↑i < m } ≃ Fin m

Tactic:
exact { toFun := fun ⟨⟨i, _⟩, hi⟩ ↦ ⟨i, hi⟩
        invFun := fun ⟨i, hi⟩ ↦ ⟨⟨i, lt_of_lt_of_le hi h⟩, hi⟩
        left_inv := fun i ↦ rfl
        right_inv := fun i ↦ rfl }

Result:
no goals

Proof state:
m n : ℕ
h : m ≤ n
⊢ card { i // ↑i < m } = m

Tactic:
conv_rhs => rw [← Fintype.card_fin m]

Result:
m n : ℕ
h : m ≤ n
⊢ card { i // ↑i < m } = card (Fin m)

Proof state:
m n : ℕ
h : m ≤ n
⊢ card { i // ↑i < m } = card (Fin m)

Tactic:
apply Fintype.card_congr

Result:
case f
m n : ℕ
h : m ≤ n
⊢ { i // ↑i < m } ≃ Fin m