harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem toList_zipIdx (a : Array α) (k : Nat) :
    (a.zipIdx k).toList = a.toList.zipIdx k

Proof state:
case mk
α : Type u_1
k : Nat
a : List α
⊢ ({ toList := a }.zipIdx k).toList = { toList := a }.toList.zipIdx k

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : Array α
k : Nat
⊢ (a.zipIdx k).toList = a.toList.zipIdx k

Tactic:
rcases a with ⟨a⟩

Result:
case mk
α : Type u_1
k : Nat
a : List α
⊢ ({ toList := a }.zipIdx k).toList = { toList := a }.toList.zipIdx k
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_congr {t : Finset β} {f g : β → α} (h₁ : s = t) (h₂ : ∀ x ∈ s, f x = g x) :
    s.sup' H f = t.sup' (h₁ ▸ H) g

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
t : Finset β
f g : β → α
H : t.Nonempty
h₂ : ∀ x ∈ t, f x = g x
c : α
⊢ t.sup' H f ≤ c ↔ t.sup' ⋯ g ≤ c

Tactic:
simp +contextual only [sup'_le_iff, h₂]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
t : Finset β
f g : β → α
H : t.Nonempty
h₂ : ∀ x ∈ t, f x = g x
⊢ t.sup' H f = t.sup' ⋯ g

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Result:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
t : Finset β
f g : β → α
H : t.Nonempty
h₂ : ∀ x ∈ t, f x = g x
c : α
⊢ t.sup' H f ≤ c ↔ t.sup' ⋯ g ≤ c

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
t : Finset β
f g : β → α
h₁ : s = t
h₂ : ∀ x ∈ s, f x = g x
⊢ s.sup' H f = t.sup' ⋯ g

Tactic:
subst s

Result:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
t : Finset β
f g : β → α
H : t.Nonempty
h₂ : ∀ x ∈ t, f x = g x
⊢ t.sup' H f = t.sup' ⋯ g
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem exists_measurable_nonneg {β} [Preorder β] [Zero β] {mβ : MeasurableSpace β} {f : α → β}
    (hf : AEMeasurable f μ) (f_nn : ∀ᵐ t ∂μ, 0 ≤ f t) : ∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᵐ[μ] g

Proof state:
case intro.intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝¹ : Preorder β
inst✝ : Zero β
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f μ
f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t
G : α → β
hG_meas : Measurable G
hG_mem : range G ⊆ Preorder.toLE.1 0
hG_ae_eq : f =ᶠ[ae μ] G
⊢ ∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g

Tactic:
exact ⟨G, hG_meas, fun x => hG_mem (mem_range_self x), hG_ae_eq⟩

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝¹ : Preorder β
inst✝ : Zero β
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f μ
f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t
⊢ ∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g

Tactic:
obtain ⟨G, hG_meas, hG_mem, hG_ae_eq⟩ := hf.exists_ae_eq_range_subset f_nn ⟨0, le_rfl⟩

Result:
case intro.intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝¹ : Preorder β
inst✝ : Zero β
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f μ
f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t
G : α → β
hG_meas : Measurable G
hG_mem : range G ⊆ Preorder.toLE.1 0
hG_ae_eq : f =ᶠ[ae μ] G
⊢ ∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g
-- Mathlib/Data/Bool/AllAny.lean
theorem all_iff_forall_prop : (all l fun a => p a) ↔ ∀ a ∈ l, p a

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ (l.all fun a => decide (p a)) = true ↔ ∀ (a : α), a ∈ l → p a

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem sq_one' {a : ℤ} (ha : (a : ZMod p) ≠ 0) : legendreSym p (a ^ 2) = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ (quadraticChar (ZMod p)) ↑(a ^ 2) = 1

Tactic:
rw [Int.cast_pow]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ (quadraticChar (ZMod p)) (↑a ^ 2) = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ (quadraticChar (ZMod p)) (↑a ^ 2) = 1

Tactic:
exact quadraticChar_sq_one' ha

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ legendreSym p (a ^ 2) = 1

Tactic:
dsimp only [legendreSym]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ (quadraticChar (ZMod p)) ↑(a ^ 2) = 1
-- Mathlib/Order/Filter/CardinalInter.lean
theorem cardinal_bInter_mem {S : Set ι} (hS : #S < c)
    {s : ∀ i ∈ S, Set α} :
    (⋂ i, ⋂ hi : i ∈ S, s i ‹_›) ∈ l ↔ ∀ i, ∀ hi : i ∈ S, s i ‹_› ∈ l

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
exact (cardinal_iInter_mem hS).trans Subtype.forall

Result:
no goals

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ i, ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

Tactic:
rw [biInter_eq_iInter]

Result:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s : (i : ι) → i ∈ S → Set α
⊢ ⋂ x, s ↑x ⋯ ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem support_rotate {u v : V} (c : G.Walk v v) (h : u ∈ c.support) :
    (c.rotate h).support.tail ~r c.support.tail

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.takeUntil u h).support.tail ++ (c.dropUntil u h).support.tail ~r c.support.tail

Tactic:
rw [← tail_support_append, take_spec]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.rotate h).support.tail ~r c.support.tail

Tactic:
simp only [rotate, tail_support_append]

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.dropUntil u h).support.tail ++ (c.takeUntil u h).support.tail ~r c.support.tail

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.dropUntil u h).support.tail ++ (c.takeUntil u h).support.tail ~r c.support.tail

Tactic:
apply List.IsRotated.trans List.isRotated_append

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.takeUntil u h).support.tail ++ (c.dropUntil u h).support.tail ~r c.support.tail
-- Mathlib/Data/Finset/Sups.lean
theorem disjSups_inter_subset_right : s ○ (t₁ ∩ t₂) ⊆ s ○ t₁ ∩ s ○ t₂

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t₁ t₂ : Finset α
⊢ s ○ (t₁ ∩ t₂) ⊆ s ○ t₁ ∩ s ○ t₂

Tactic:
simpa only [disjSups, product_inter, filter_inter_distrib] using image_inter_subset _ _ _

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem coe_T_inv : ↑(T⁻¹) = !![1, -1; 0, 1]

Proof state:
⊢ ↑T⁻¹ = !![1, -1; 0, 1]

Tactic:
simp [coe_inv, coe_T, adjugate_fin_two]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem getElem_tails (l : List α) (n : Nat) (h : n < (tails l).length) :
    (tails l)[n] = l.drop n

Proof state:
case nil
α : Type u_1
n : ℕ
h : n < [].tails.length
⊢ [].tails[n] = drop n []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.tails.length), l.tails[n] = drop n l
n : ℕ
h : n < (a :: l).tails.length
⊢ (a :: l).tails[n] = drop n (a :: l)

Tactic:
cases n with
| zero => simp
| succ n => simp [ihl]

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : ℕ
h : n < l.tails.length
⊢ l.tails[n] = drop n l

Tactic:
induction l generalizing n with
| nil => simp
| cons a l ihl =>
  cases n with
  | zero => simp
  | succ n => simp [ihl]

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.tails.length), l.tails[n] = drop n l
n : ℕ
h : n + 1 < (a :: l).tails.length
⊢ (a :: l).tails[n + 1] = drop (n + 1) (a :: l)

Tactic:
simp [ihl]

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.tails.length), l.tails[n] = drop n l
h : 0 < (a :: l).tails.length
⊢ (a :: l).tails[0] = drop 0 (a :: l)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Bases.lean
protected lemma IsTopologicalBasis.isInducing {β} [TopologicalSpace β] {f : α → β} {T : Set (Set β)}
    (hf : IsInducing f) (h : IsTopologicalBasis T) : IsTopologicalBasis ((preimage f) '' T) :=
  .of_hasBasis_nhds fun a ↦ by
    convert (hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id with s
    aesop

Proof state:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : IsInducing f
h : IsTopologicalBasis T
a : α
⊢ (𝓝 a).HasBasis (fun t => t ∈ preimage f '' T ∧ a ∈ t) id

Tactic:
convert (hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id with s

Result:
case h.e'_4.h.a
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : IsInducing f
h : IsTopologicalBasis T
a : α
s : Set α
⊢ s ∈ preimage f '' T ∧ a ∈ s ↔ s ∈ (preimage f ∘ fun t => t) '' {i | i ∈ T ∧ f a ∈ i}

Proof state:
case h.e'_4.h.a
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : IsInducing f
h : IsTopologicalBasis T
a : α
s : Set α
⊢ s ∈ preimage f '' T ∧ a ∈ s ↔ s ∈ (preimage f ∘ fun t => t) '' {i | i ∈ T ∧ f a ∈ i}

Tactic:
aesop

Result:
no goals
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.cellFrontier_union_openCell_eq_closedCell [RelCWComplex C D] (n : ℕ)
    (i : cell C n) : cellFrontier n i ∪ openCell n i = closedCell n i

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ cellFrontier n i ∪ openCell n i = closedCell n i

Tactic:
rw [cellFrontier, openCell, closedCell, ← image_union]

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ ↑(map n i) '' (sphere 0 1 ∪ ball 0 1) = ↑(map n i) '' closedBall 0 1

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ ↑(map n i) '' (sphere 0 1 ∪ ball 0 1) = ↑(map n i) '' closedBall 0 1

Tactic:
congrm map n i '' ?_

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ sphere 0 1 ∪ ball 0 1 = closedBall 0 1

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ sphere 0 1 ∪ ball 0 1 = closedBall 0 1

Tactic:
exact sphere_union_ball

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem support_ofMultiset : (ofMultiset s hs).support = s.toFinset :=
  Set.ext (by simp [mem_support_iff, hs])

Proof state:
α : Type u_1
s : Multiset α
hs : s ≠ 0
⊢ ∀ (x : α), x ∈ (ofMultiset s hs).support ↔ x ∈ ↑s.toFinset

Tactic:
simp [mem_support_iff, hs]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem mem_bot {x : A} : x ∈ (⊥ : NonUnitalStarSubalgebra R A) ↔ x = 0 :=
  show x ∈ NonUnitalAlgebra.adjoin R (∅ ∪ star ∅ : Set A) ↔ x = 0 by
    rw [Set.star_empty, Set.union_empty, NonUnitalAlgebra.adjoin_empty, NonUnitalAlgebra.mem_bot]

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
x : A
⊢ x ∈ NonUnitalAlgebra.adjoin R (∅ ∪ star ∅) ↔ x = 0

Tactic:
rw [Set.star_empty, Set.union_empty, NonUnitalAlgebra.adjoin_empty, NonUnitalAlgebra.mem_bot]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
/-- See also `map_yonedaEquiv'` for a more general version. -/
lemma map_yonedaEquiv {X Y : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj X ⟶ F)
    (g : Y ⟶ X) : F.map g.op (yonedaEquiv f) = f.app (op Y) g

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ F.map g.op (yonedaEquiv f) = f.app (op Y) g

Tactic:
rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Result:
no goals
-- Mathlib/Topology/Order/Lattice.lean
lemma ContinuousAt.finset_sup (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
    ContinuousAt (s.sup f) x

Proof state:
L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
x : X
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.sup f) x

Tactic:
simpa only [← Finset.sup_apply] using finset_sup_apply hs

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
theorem TensorProduct.map_surjective : Function.Surjective (TensorProduct.map g g')

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R N
inst✝⁴ : Module R P
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
N' : Type u_6
P' : Type u_7
inst✝³ : AddCommMonoid N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module R N'
inst✝ : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective ⇑g'
⊢ Function.Surjective (⇑(lTensor P g') ∘ ⇑(rTensor N' g))

Tactic:
exact Function.Surjective.comp (lTensor_surjective _ hg') (rTensor_surjective _ hg)

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R N
inst✝⁴ : Module R P
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
N' : Type u_6
P' : Type u_7
inst✝³ : AddCommMonoid N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module R N'
inst✝ : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective ⇑g'
⊢ Function.Surjective ⇑(map g g')

Tactic:
rw [← lTensor_comp_rTensor, coe_comp]

Result:
R : Type u_1
inst✝⁸ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R N
inst✝⁴ : Module R P
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
N' : Type u_6
P' : Type u_7
inst✝³ : AddCommMonoid N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module R N'
inst✝ : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective ⇑g'
⊢ Function.Surjective (⇑(lTensor P g') ∘ ⇑(rTensor N' g))
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem tendsto_Lp_iff_tendsto_eLpNorm' {ι} {fi : Filter ι} [Fact (1 ≤ p)] (f : ι → Lp E p μ)
    (f_lim : Lp E p μ) :
    fi.Tendsto f (𝓝 f_lim) ↔ fi.Tendsto (fun n => eLpNorm (⇑(f n) - ⇑f_lim) p μ) (𝓝 0)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
n : ι
⊢ eLpNorm (↑↑(f n - f_lim)) p μ ≠ ⊤

Tactic:
exact Lp.eLpNorm_ne_top _

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
⊢ Tendsto (fun b => dist (f b) f_lim) fi (𝓝 0) ↔ Tendsto (fun n => eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)

Tactic:
simp_rw [dist_def]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
⊢ Tendsto (fun b => (eLpNorm (↑↑(f b) - ↑↑f_lim) p μ).toReal) fi (𝓝 0) ↔
    Tendsto (fun n => eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
n : ι
⊢ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ ≠ ⊤

Tactic:
rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
n : ι
⊢ eLpNorm (↑↑(f n - f_lim)) p μ ≠ ⊤

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
⊢ Tendsto (fun b => (eLpNorm (↑↑(f b) - ↑↑f_lim) p μ).toReal) fi (𝓝 0) ↔
    Tendsto (fun n => eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)

Tactic:
rw [← ENNReal.zero_toReal, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
n : ι
⊢ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ ≠ ⊤

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
⊢ Tendsto f fi (𝓝 f_lim) ↔ Tendsto (fun n => eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)

Tactic:
rw [tendsto_iff_dist_tendsto_zero]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
⊢ Tendsto (fun b => dist (f b) f_lim) fi (𝓝 0) ↔ Tendsto (fun n => eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)
-- Mathlib/MeasureTheory/Measure/Prod.lean
lemma snd_sum {ι : Type*} (μ : ι → Measure (α × β)) : (sum μ).snd = sum (fun n ↦ (μ n).snd)

Proof state:
case h.hs
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
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
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
⊢ (sum μ).snd = sum fun n => (μ n).snd

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ (sum μ).snd s = (sum fun n => (μ n).snd) s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ι), (μ i) (Prod.snd ⁻¹' s) = ∑' (i : ι), (μ i).snd s

Tactic:
simp_rw [snd_apply hs]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ (sum μ).snd s = (sum fun n => (μ n).snd) s

Tactic:
rw [snd_apply hs, sum_apply, sum_apply _ hs]

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ι), (μ i) (Prod.snd ⁻¹' s) = ∑' (i : ι), (μ i).snd s

case h.hs
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem one_le_rpow_of_pos_of_le_one_of_nonpos (hx1 : 0 < x) (hx2 : x ≤ 1) (hz : z ≤ 0) :
    1 ≤ x ^ z

Proof state:
x z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 ≤ x ^ z

Tactic:
convert rpow_le_rpow_of_exponent_ge hx1 hx2 hz

Result:
case h.e'_3
x z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 = x ^ 0

Proof state:
case h.e'_3
x z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 = x ^ 0

Tactic:
exact (rpow_zero x).symm

Result:
no goals
-- Mathlib/Control/Fold.lean
theorem foldl_toList (f : α → β → α) (xs : t β) (x : α) :
    foldl f x xs = List.foldl f x (toList xs)

Proof state:
α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = unop ((Foldl.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))) x

Tactic:
simp only [foldl, toList_spec, foldMap_hom_free, foldl.ofFreeMonoid_comp_of, Foldl.get,
  FreeMonoid.ofList_toList]

Result:
no goals

Proof state:
α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = List.foldl f x (toList xs)

Tactic:
rw [← FreeMonoid.toList_ofList (toList xs), ← foldl.unop_ofFreeMonoid]

Result:
α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = unop ((Foldl.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))) x
-- Mathlib/RingTheory/Localization/Module.lean
theorem Basis.ofIsLocalizedModule_apply (i : ι) : b.ofIsLocalizedModule Rₛ S f i = f (b i)

Proof state:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
i : ι
⊢ (ofIsLocalizedModule Rₛ S f b) i = f (b i)

Tactic:
rw [ofIsLocalizedModule, coe_mk, Function.comp_apply]

Result:
no goals
-- Mathlib/Topology/Order/Lattice.lean
lemma ContinuousWithinAt.finset_inf
    (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) : ContinuousWithinAt (s.inf f) t x

Proof state:
L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeInf L
inst✝¹ : OrderTop L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.inf f) t x

Tactic:
simpa only [← Finset.inf_apply] using finset_inf_apply hs

Result:
no goals
-- Mathlib/Order/PropInstances.lean
theorem disjoint_iff [∀ i, OrderBot (α' i)] {f g : ∀ i, α' i} :
    Disjoint f g ↔ ∀ i, Disjoint (f i) (g i)

Proof state:
case mpr
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
x : (i : ι) → α' i
hf : x ≤ f
hg : x ≤ g
i : ι
⊢ x i ≤ ⊥ i

Tactic:
apply h i (hf i) (hg i)

Result:
no goals

Proof state:
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)

Tactic:
constructor

Result:
case mp
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)

case mpr
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g

Proof state:
case mpr
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g

Tactic:
intro h x hf hg i

Result:
case mpr
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : ∀ (i : ι), Disjoint (f i) (g i)
x : (i : ι) → α' i
hf : x ≤ f
hg : x ≤ g
i : ι
⊢ x i ≤ ⊥ i

Proof state:
case mp
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
⊢ x ≤ ⊥

Tactic:
exact (update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => bot_le⟩)
  (update_le_iff.mpr ⟨hg, fun _ _ => bot_le⟩)).1

Result:
no goals

Proof state:
case mp
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)

Tactic:
intro h i x hf hg

Result:
case mp
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
h : Disjoint f g
i : ι
x : α' i
hf : x ≤ f i
hg : x ≤ g i
⊢ x ≤ ⊥