harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem fderivWithin_comp_derivWithin {t : Set F} (hl : DifferentiableWithinAt 𝕜 l t (f x))
    (hf : DifferentiableWithinAt 𝕜 f s x) (hs : MapsTo f s t) :
    derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : F → E) (derivWithin f s x)

Proof state:
case inr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
case inl
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)

Tactic:
exact (hl.hasFDerivWithinAt.comp_hasDerivWithinAt x hf.hasDerivWithinAt hs).derivWithin hxs

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)

case inr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.span_iff_products [WellFoundedLT I] :
    ⊤ ≤ Submodule.span ℤ (Set.range (eval C)) ↔
      ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
this : Products.eval C '' {m | m < l} ⊆ ↑(Submodule.span ℤ (Set.range (eval C)))
⊢ L l

Tactic:
rw [← span_le] at this

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
this : Submodule.span ℤ (Products.eval C '' {m | m < l}) ≤ Submodule.span ℤ (Set.range (eval C))
⊢ L l

Proof state:
case intro.ind
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
⊢ L l

Tactic:
by_cases hl : l.isGood C

Result:
case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.isGood C l
⊢ L l

case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : ¬Products.isGood C l
⊢ L l

Proof state:
case pos.a
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.isGood C l
⊢ Products.eval C l ∈ Set.range (eval C)

Tactic:
exact ⟨⟨l, hl⟩, rfl⟩

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
⊢ Set.range (Products.eval C) ⊆ ↑(Submodule.span ℤ (Set.range (eval C)))

Tactic:
rintro f ⟨l, rfl⟩

Result:
case intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l : Products I
⊢ Products.eval C l ∈ ↑(Submodule.span ℤ (Set.range (eval C)))
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma injOn_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) (k : ℕ∞) :
    InjOn (f.genEigenspace · k) {μ | f.genEigenspace μ k ≠ ⊥}

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ : R
a✝ : μ₁ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
μ₂ : R
hμ₂ : μ₂ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
hμ₁₂ : (fun x => (f.genEigenspace x) k) μ₁ = (fun x => (f.genEigenspace x) k) μ₂
⊢ μ₁ = μ₂

Tactic:
by_contra contra

Result:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ : R
a✝ : μ₁ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
μ₂ : R
hμ₂ : μ₂ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
hμ₁₂ : (fun x => (f.genEigenspace x) k) μ₁ = (fun x => (f.genEigenspace x) k) μ₂
contra : ¬μ₁ = μ₂
⊢ False

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ : R
a✝ : μ₁ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
μ₂ : R
hμ₂ : μ₂ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
hμ₁₂ : (fun x => (f.genEigenspace x) k) μ₁ = (fun x => (f.genEigenspace x) k) μ₂
contra : ¬μ₁ = μ₂
⊢ False

Tactic:
apply hμ₂

Result:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ : R
a✝ : μ₁ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
μ₂ : R
hμ₂ : μ₂ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
hμ₁₂ : (fun x => (f.genEigenspace x) k) μ₁ = (fun x => (f.genEigenspace x) k) μ₂
contra : ¬μ₁ = μ₂
⊢ (f.genEigenspace μ₂) k = ⊥

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ : R
a✝ : μ₁ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
μ₂ : R
hμ₂ : μ₂ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
hμ₁₂ : (fun x => (f.genEigenspace x) k) μ₁ = (fun x => (f.genEigenspace x) k) μ₂
contra : ¬μ₁ = μ₂
⊢ (f.genEigenspace μ₂) k = ⊥

Tactic:
simpa only [hμ₁₂, disjoint_self] using f.disjoint_genEigenspace contra k k

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
⊢ InjOn (fun x => (f.genEigenspace x) k) {μ | (f.genEigenspace μ) k ≠ ⊥}

Tactic:
rintro μ₁ _ μ₂ hμ₂ hμ₁₂

Result:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ : R
a✝ : μ₁ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
μ₂ : R
hμ₂ : μ₂ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
hμ₁₂ : (fun x => (f.genEigenspace x) k) μ₁ = (fun x => (f.genEigenspace x) k) μ₂
⊢ μ₁ = μ₂
-- Mathlib/Order/Bounded.lean
theorem unbounded_lt_iff [LinearOrder α] : Unbounded (· < ·) s ↔ ∀ a, ∃ b ∈ s, a ≤ b

Proof state:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
⊢ Unbounded (fun x1 x2 => x1 < x2) s ↔ ∀ (a : α), ∃ b ∈ s, a ≤ b

Tactic:
simp only [Unbounded, not_lt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_le_size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} :
    m.size ≤ (insertMany m l).size

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
⊢ m.size ≤ (insertMany m l).size

Tactic:
simp_to_raw using Raw₀.Const.size_le_size_insertMany_list ⟨m, _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_insertList_of_mem [BEq α] [LawfulBEq α]
    {l toInsert : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k') {v : β k}
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ toInsert) :
    getValueCast? k' (insertList l toInsert) =
    some (cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys toInsert
mem : ⟨k, v⟩ ∈ toInsert
this : getEntry? k' (insertList l toInsert) = getEntry? k' toInsert
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? k' (insertList l toInsert)) fun p h => cast ⋯ p.snd) =
    some (cast ⋯ v)

Tactic:
rw [getEntry?_of_mem distinct_toInsert k_beq mem] at this

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : DistinctKeys toInsert
mem : ⟨k, v⟩ ∈ toInsert
this : getEntry? k' (insertList l toInsert) = some ⟨k, v⟩
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? k' (insertList l toInsert)) fun p h => cast ⋯ p.snd) =
    some (cast ⋯ v)
-- Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
theorem rootsOfUnity.integer_power_of_ringEquiv (g : L ≃+* L) :
    ∃ m : ℤ, ∀ t : rootsOfUnity n L, g (t : Lˣ) = (t ^ m : Lˣ)

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
⊢ ∃ m, ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ m)

Tactic:
obtain ⟨m, hm⟩ := MonoidHom.map_cyclic ((g : L ≃* L).restrictRootsOfUnity n).toMonoidHom

Result:
case intro
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
m : ℤ
hm : ∀ (g_1 : ↥(rootsOfUnity n L)), ((↑g).restrictRootsOfUnity n).toMonoidHom g_1 = g_1 ^ m
⊢ ∃ m, ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ m)

Proof state:
case intro
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
m : ℤ
hm : ∀ (g_1 : ↥(rootsOfUnity n L)), ((↑g).restrictRootsOfUnity n).toMonoidHom g_1 = g_1 ^ m
⊢ ∃ m, ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ m)

Tactic:
exact ⟨m, fun t ↦ Units.ext_iff.1 <| SetCoe.ext_iff.2 <| hm t⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem modifyKey_eq_alterKey (k : α) (f : β → β) (l : List ((_ : α) × β)) :
    modifyKey k f l = alterKey k (·.map f) l

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
l : List ((_ : α) × β)
⊢ (match getValue? k l with
    | none => l
    | some v => replaceEntry k (f v) l) =
    match
      match getValue? k l with
      | some x => some (f x)
      | none => none with
    | none => eraseKey k l
    | some v => insertEntry k v l

Tactic:
split <;> next h =>
  simp [h, insertEntry, containsKey_eq_isSome_getValue?, eraseKey_of_containsKey_eq_false]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
l : List ((_ : α) × β)
x✝ : Option β
v✝ : β
h : getValue? k l = some v✝
⊢ replaceEntry k (f v✝) l =
    match
      match getValue? k l with
      | some x => some (f x)
      | none => none with
    | none => eraseKey k l
    | some v => insertEntry k v l

Tactic:
simp [h, insertEntry, containsKey_eq_isSome_getValue?, eraseKey_of_containsKey_eq_false]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
l : List ((_ : α) × β)
⊢ modifyKey k f l = alterKey k (fun x => Option.map f x) l

Tactic:
rw [modifyKey, alterKey, Option.map.eq_def]

Result:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
l : List ((_ : α) × β)
⊢ (match getValue? k l with
    | none => l
    | some v => replaceEntry k (f v) l) =
    match
      match getValue? k l with
      | some x => some (f x)
      | none => none with
    | none => eraseKey k l
    | some v => insertEntry k v l
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.pentagon (W X Y Z : C) :
    coprod.map (coprod.associator W X Y).hom (𝟙 Z) ≫
        (coprod.associator W (X ⨿ Y) Z).hom ≫ coprod.map (𝟙 W) (coprod.associator X Y Z).hom =
      (coprod.associator (W ⨿ X) Y Z).hom ≫ (coprod.associator W X (Y ⨿ Z)).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
W X Y Z : C
⊢ map (associator W X Y).hom (𝟙 Z) ≫ (associator W (X ⨿ Y) Z).hom ≫ map (𝟙 W) (associator X Y Z).hom =
    (associator (W ⨿ X) Y Z).hom ≫ (associator W X (Y ⨿ Z)).hom

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CoversTop.lean
lemma coversTop_iff_of_isTerminal (X : C) (hX : IsTerminal X)
    {I : Type*} (Y : I → C) :
    J.CoversTop Y ↔ Sieve.ofObjects Y X ∈ J X

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ J.CoversTop Y ↔ Sieve.ofObjects Y X ∈ J X

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ J.CoversTop Y → Sieve.ofObjects Y X ∈ J X

case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ Sieve.ofObjects Y X ∈ J X → J.CoversTop Y

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ Sieve.ofObjects Y X ∈ J X → J.CoversTop Y

Tactic:
intro h W

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
h : Sieve.ofObjects Y X ∈ J X
W : C
⊢ Sieve.ofObjects Y W ∈ J W

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
h : Sieve.ofObjects Y X ∈ J X
W : C
⊢ Sieve.pullback (hX.from W) (Sieve.ofObjects Y X) ≤ Sieve.ofObjects Y W

Tactic:
rintro T a ⟨i, ⟨b⟩⟩

Result:
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
h : Sieve.ofObjects Y X ∈ J X
W T : C
a : T ⟶ W
i : I
b : T ⟶ Y i
⊢ (Sieve.ofObjects Y W).arrows a

Proof state:
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
h : Sieve.ofObjects Y X ∈ J X
W T : C
a : T ⟶ W
i : I
b : T ⟶ Y i
⊢ (Sieve.ofObjects Y W).arrows a

Tactic:
exact ⟨i, ⟨b⟩⟩

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ J.CoversTop Y → Sieve.ofObjects Y X ∈ J X

Tactic:
tauto

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
h : Sieve.ofObjects Y X ∈ J X
W : C
⊢ Sieve.ofObjects Y W ∈ J W

Tactic:
apply J.superset_covering _ (J.pullback_stable (hX.from W) h)

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
h : Sieve.ofObjects Y X ∈ J X
W : C
⊢ Sieve.pullback (hX.from W) (Sieve.ofObjects Y X) ≤ Sieve.ofObjects Y W
-- Mathlib/Algebra/BigOperators/Finsupp.lean
lemma indicator_eq_sum_attach_single [AddCommMonoid M] {s : Finset α} (f : ∀ a ∈ s, M) :
    indicator s f = ∑ x ∈ s.attach, single ↑x (f x x.2)

Proof state:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ ∑ x ∈ s.attach, single (↑x) ((indicator s f) ↑x) = ∑ x ∈ s.attach, single (↑x) (f ↑x ⋯)

Tactic:
refine Finset.sum_congr rfl (fun _ _ => ?_)

Result:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
x✝¹ : { x // x ∈ s }
x✝ : x✝¹ ∈ s.attach
⊢ single (↑x✝¹) ((indicator s f) ↑x✝¹) = single (↑x✝¹) (f ↑x✝¹ ⋯)

Proof state:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ ∀ x ∈ s, x ∉ (indicator s f).support → single x ((indicator s f) x) = 0

Tactic:
intro i _ hi

Result:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
a✝ : i ∈ s
hi : i ∉ (indicator s f).support
⊢ single i ((indicator s f) i) = 0

Proof state:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
a✝ : i ∈ s
hi : i ∉ (indicator s f).support
⊢ single i ((indicator s f) i) = 0

Tactic:
rw [not_mem_support_iff.mp hi, single_zero]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ indicator s f = ∑ x ∈ s.attach, single (↑x) (f ↑x ⋯)

Tactic:
rw [← sum_single (indicator s f), sum, sum_subset (support_indicator_subset _ _), ← sum_attach]

Result:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ ∑ x ∈ s.attach, single (↑x) ((indicator s f) ↑x) = ∑ x ∈ s.attach, single (↑x) (f ↑x ⋯)

α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ ∀ x ∈ s, x ∉ (indicator s f).support → single x ((indicator s f) x) = 0

Proof state:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
x✝¹ : { x // x ∈ s }
x✝ : x✝¹ ∈ s.attach
⊢ single (↑x✝¹) ((indicator s f) ↑x✝¹) = single (↑x✝¹) (f ↑x✝¹ ⋯)

Tactic:
rw [indicator_of_mem]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem tendsto_nhdsWithin_iff_subtype {s : Set α} {a : α} (h : a ∈ s) (f : α → β) (l : Filter β) :
    Tendsto f (𝓝[s] a) l ↔ Tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto f (𝓝[s] a) l ↔ Tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l

Tactic:
rw [nhdsWithin_eq_map_subtype_coe h, tendsto_map'_iff]

Result:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto (f ∘ Subtype.val) (𝓝 ⟨a, h⟩) l ↔ Tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto (f ∘ Subtype.val) (𝓝 ⟨a, h⟩) l ↔ Tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNormEssSup_indicator_const_eq (s : Set α) (c : G) (hμs : μ s ≠ 0) :
    eLpNormEssSup (s.indicator fun _ : α => c) μ = ‖c‖ₑ

Proof state:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμs : μ s ≠ 0
⊢ eLpNormEssSup (s.indicator fun x => c) μ = ‖c‖ₑ

Tactic:
refine le_antisymm (eLpNormEssSup_indicator_const_le s c) ?_

Result:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμs : μ s ≠ 0
⊢ ‖c‖ₑ ≤ eLpNormEssSup (s.indicator fun x => c) μ

Proof state:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμs : μ s ≠ 0
h : eLpNormEssSup (s.indicator fun x => c) μ < ‖c‖ₑ
h' : μ {a | ‖c‖ₑ ≤ ‖s.indicator (fun x => c) a‖ₑ} = 0
⊢ False

Tactic:
refine hμs (measure_mono_null (fun x hx_mem => ?_) h')

Result:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμs : μ s ≠ 0
h : eLpNormEssSup (s.indicator fun x => c) μ < ‖c‖ₑ
h' : μ {a | ‖c‖ₑ ≤ ‖s.indicator (fun x => c) a‖ₑ} = 0
x : α
hx_mem : x ∈ s
⊢ x ∈ {a | ‖c‖ₑ ≤ ‖s.indicator (fun x => c) a‖ₑ}

Proof state:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμs : μ s ≠ 0
h : eLpNormEssSup (s.indicator fun x => c) μ < ‖c‖ₑ
⊢ False

Tactic:
have h' := ae_iff.mp (ae_lt_of_essSup_lt h)

Result:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμs : μ s ≠ 0
h : eLpNormEssSup (s.indicator fun x => c) μ < ‖c‖ₑ
h' : μ {a | ¬‖s.indicator (fun x => c) a‖ₑ < ‖c‖ₑ} = 0
⊢ False

Proof state:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμs : μ s ≠ 0
h : eLpNormEssSup (s.indicator fun x => c) μ < ‖c‖ₑ
h' : μ {a | ¬‖s.indicator (fun x => c) a‖ₑ < ‖c‖ₑ} = 0
⊢ False

Tactic:
push_neg at h'

Result:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμs : μ s ≠ 0
h : eLpNormEssSup (s.indicator fun x => c) μ < ‖c‖ₑ
h' : μ {a | ‖c‖ₑ ≤ ‖s.indicator (fun x => c) a‖ₑ} = 0
⊢ False

Proof state:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμs : μ s ≠ 0
⊢ ‖c‖ₑ ≤ eLpNormEssSup (s.indicator fun x => c) μ

Tactic:
by_contra! h

Result:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμs : μ s ≠ 0
h : eLpNormEssSup (s.indicator fun x => c) μ < ‖c‖ₑ
⊢ False

Proof state:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμs : μ s ≠ 0
h : eLpNormEssSup (s.indicator fun x => c) μ < ‖c‖ₑ
h' : μ {a | ‖c‖ₑ ≤ ‖s.indicator (fun x => c) a‖ₑ} = 0
x : α
hx_mem : x ∈ s
⊢ x ∈ {a | ‖c‖ₑ ≤ ‖s.indicator (fun x => c) a‖ₑ}

Tactic:
rw [Set.mem_setOf_eq, Set.indicator_of_mem hx_mem, enorm_eq_nnnorm]

Result:
no goals
-- Mathlib/Data/DFinsupp/Interval.lean
lemma card_Ioc : #(Ioc f g) = (∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i))) - 1

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ioc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Tactic:
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]

Result:
no goals