harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/IndicatorConstPointwise.lean
/-- The indicator functions of `Asᵢ` tend to the indicator function of `A` pointwise if and only if
for every `x`, we eventually have the equivalence `x ∈ Asᵢ ↔ x ∈ A`. -/
@[simp] lemma tendsto_indicator_const_iff_forall_eventually [T1Space β] (b : β) [NeZero b] :
    Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b)) L (𝓝 (A.indicator (fun (_ : α) ↦ b)))
      ↔ ∀ x, ∀ᶠ i in L, (x ∈ As i ↔ x ∈ A)

Proof state:
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ Tendsto (fun i => (As i).indicator fun x => b) L (𝓝 (A.indicator fun x => b)) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
apply tendsto_indicator_const_iff_forall_eventually' _ b

Result:
case nhd_b
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ {0}ᶜ ∈ 𝓝 b

case nhd_o
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ {b}ᶜ ∈ 𝓝 0

Proof state:
case nhd_o
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ {b}ᶜ ∈ 𝓝 0

Tactic:
simp only [compl_singleton_mem_nhds_iff, ne_eq, (NeZero.ne b).symm, not_false_eq_true]

Result:
no goals

Proof state:
case nhd_b
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ {0}ᶜ ∈ 𝓝 b

Tactic:
simp only [compl_singleton_mem_nhds_iff, ne_eq, NeZero.ne, not_false_eq_true]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem map.injective {f : α → β} (hinj : Injective f) : Injective (map f)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
z z' : Sym2 α
⊢ map f z = map f z' → z = z'

Tactic:
refine Sym2.inductionOn₂ z z' (fun x y x' y' => ?_)

Result:
α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ map f s(x, y) = map f s(x', y') → s(x, y) = s(x', y')

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ map f s(x, y) = map f s(x', y') → s(x, y) = s(x', y')

Tactic:
simp [hinj.eq_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
⊢ Injective (map f)

Tactic:
intro z z'

Result:
α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
z z' : Sym2 α
⊢ map f z = map f z' → z = z'
-- Mathlib/Data/Num/Lemmas.lean
theorem ofNat'_one : Num.ofNat' 1 = 1

Proof state:
⊢ ofNat' 1 = 1

Tactic:
erw [ofNat'_bit true 0, cond, ofNat'_zero]

Result:
⊢ Num.bit1 0 = 1

Proof state:
⊢ Num.bit1 0 = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem sInf_coe (S : Set (LieSubmodule R L M)) : (↑(sInf S) : Set M) = ⋂ s ∈ S, (s : Set M)

Proof state:
case h
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
S : Set (LieSubmodule R L M)
m : M
⊢ m ∈ ⋂ p ∈ {x | ∃ s ∈ S, ↑s = x}, ↑p ↔ m ∈ ⋂ s ∈ S, ↑s

Tactic:
simp only [mem_iInter, mem_setOf_eq, forall_apply_eq_imp_iff₂, exists_imp,
  and_imp, SetLike.mem_coe, mem_toSubmodule]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
S : Set (LieSubmodule R L M)
⊢ ↑(sInf S) = ⋂ s ∈ S, ↑s

Tactic:
rw [← LieSubmodule.coe_toSubmodule, sInf_toSubmodule, Submodule.sInf_coe]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
S : Set (LieSubmodule R L M)
⊢ ⋂ p ∈ {x | ∃ s ∈ S, ↑s = x}, ↑p = ⋂ s ∈ S, ↑s

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
S : Set (LieSubmodule R L M)
⊢ ⋂ p ∈ {x | ∃ s ∈ S, ↑s = x}, ↑p = ⋂ s ∈ S, ↑s

Tactic:
ext m

Result:
case h
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
S : Set (LieSubmodule R L M)
m : M
⊢ m ∈ ⋂ p ∈ {x | ∃ s ∈ S, ↑s = x}, ↑p ↔ m ∈ ⋂ s ∈ S, ↑s
-- Mathlib/Analysis/Matrix.lean
theorem nnnorm_row (v : n → α) : ‖row ι v‖₊ = ‖v‖₊

Proof state:
n : Type u_4
α : Type u_5
ι : Type u_7
inst✝² : Fintype n
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ ‖row ι v‖₊ = ‖v‖₊

Tactic:
simp [nnnorm_def, Pi.nnnorm_def]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem union_distrib_iInter₂_right (s : ∀ i, κ i → Set α) (t : Set α) :
    (⋂ (i) (j), s i j) ∪ t = ⋂ (i) (j), s i j ∪ t

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ i, ⋂ j, s i j) ∪ t = ⋂ i, ⋂ j, s i j ∪ t

Tactic:
simp_rw [union_distrib_iInter_right]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
@[simp] lemma finsetEquivSet_symm_apply (s : Set α) [Fintype s] :
    finsetEquivSet.symm s = s.toFinset

Proof state:
α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ finsetEquivSet.symm s = s.toFinset

Tactic:
simp [finsetEquivSet]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem coeFn_add (μ ν : FiniteMeasure Ω) : (⇑(μ + ν) : Set Ω → ℝ≥0) = (⇑μ + ⇑ν : Set Ω → ℝ≥0)

Proof state:
case h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
x✝ : Set Ω
⊢ ↑(μ + ν) x✝ = ↑μ x✝ + ↑ν x✝

Tactic:
norm_cast

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
⊢ ⇑(μ + ν) = ⇑μ + ⇑ν

Tactic:
funext

Result:
case h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
x✝ : Set Ω
⊢ (μ + ν) x✝ = (⇑μ + ⇑ν) x✝

Proof state:
case h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
x✝ : Set Ω
⊢ (μ + ν) x✝ = (⇑μ + ⇑ν) x✝

Tactic:
simp only [Pi.add_apply, ← ENNReal.coe_inj, ne_eq, ennreal_coeFn_eq_coeFn_toMeasure,
  ENNReal.coe_add]

Result:
case h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
x✝ : Set Ω
⊢ ↑(μ + ν) x✝ = ↑μ x✝ + ↑ν x✝
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem ftaylorSeriesWithin_univ : ftaylorSeriesWithin 𝕜 f univ = ftaylorSeries 𝕜 f

Proof state:
case h.h
𝕜 : 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
x : E
n : ℕ
⊢ ftaylorSeriesWithin 𝕜 f univ x n = ftaylorSeries 𝕜 f x n

Tactic:
change iteratedFDerivWithin 𝕜 n f univ x = iteratedFDeriv 𝕜 n f x

Result:
case h.h
𝕜 : 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
x : E
n : ℕ
⊢ iteratedFDerivWithin 𝕜 n f univ x = iteratedFDeriv 𝕜 n f x

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
⊢ ftaylorSeriesWithin 𝕜 f univ = ftaylorSeries 𝕜 f

Tactic:
ext1 x

Result:
case h
𝕜 : 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
x : E
⊢ ftaylorSeriesWithin 𝕜 f univ x = ftaylorSeries 𝕜 f x

Proof state:
case h
𝕜 : 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
x : E
⊢ ftaylorSeriesWithin 𝕜 f univ x = ftaylorSeries 𝕜 f x

Tactic:
ext1 n

Result:
case h.h
𝕜 : 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
x : E
n : ℕ
⊢ ftaylorSeriesWithin 𝕜 f univ x n = ftaylorSeries 𝕜 f x n

Proof state:
case h.h
𝕜 : 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
x : E
n : ℕ
⊢ iteratedFDerivWithin 𝕜 n f univ x = iteratedFDeriv 𝕜 n f x

Tactic:
rw [iteratedFDerivWithin_univ]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
lemma ae_le_trim_of_stronglyMeasurable (hm : m ≤ m₀) (hf : StronglyMeasurable[m] f)
    (hg : StronglyMeasurable[m] g) (hfg : f ≤ᵐ[μ] g) : f ≤ᵐ[μ.trim hm] g

Proof state:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᶠ[ae μ] g
⊢ f ≤ᶠ[ae (μ.trim hm)] g

Tactic:
rwa [EventuallyLE, ae_iff, trim_measurableSet_eq hm]

Result:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᶠ[ae μ] g
⊢ MeasurableSet {a | ¬f a ≤ g a}

Proof state:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᶠ[ae μ] g
⊢ MeasurableSet {a | ¬f a ≤ g a}

Tactic:
exact (hf.measurableSet_le hg).compl

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.of_pow {n : ℕ} {f : α → 𝕜} {g : α → R} (h : IsBigOWith c l (f ^ n) (g ^ n))
    (hn : n ≠ 0) (hc : c ≤ c' ^ n) (hc' : 0 ≤ c') : IsBigOWith c' l f g :=
  IsBigOWith.of_bound <| (h.weaken hc).bound.mono fun x hx ↦
    le_of_pow_le_pow_left₀ hn (by positivity) <|
      calc
        ‖f x‖ ^ n = ‖f x ^ n‖ := (norm_pow _ _).symm
        _ ≤ c' ^ n * ‖g x ^ n‖ := hx
        _ ≤ c' ^ n * ‖g x‖ ^ n

Proof state:
case h
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
c c' : ℝ
l : Filter α
n : ℕ
f : α → 𝕜
g : α → R
h : IsBigOWith c l (f ^ n) (g ^ n)
hn : n ≠ 0
hc : c ≤ c' ^ n
hc' : 0 ≤ c'
x : α
hx : ‖(f ^ n) x‖ ≤ c' ^ n * ‖(g ^ n) x‖
⊢ ‖g x ^ n‖ ≤ ‖g x‖ ^ n

Tactic:
exact norm_pow_le' _ hn.bot_lt

Result:
no goals

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
c c' : ℝ
l : Filter α
n : ℕ
f : α → 𝕜
g : α → R
h : IsBigOWith c l (f ^ n) (g ^ n)
hn : n ≠ 0
hc : c ≤ c' ^ n
hc' : 0 ≤ c'
x : α
hx : ‖(f ^ n) x‖ ≤ c' ^ n * ‖(g ^ n) x‖
⊢ 0 ≤ c' * ‖g x‖

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
c c' : ℝ
l : Filter α
n : ℕ
f : α → 𝕜
g : α → R
h : IsBigOWith c l (f ^ n) (g ^ n)
hn : n ≠ 0
hc : c ≤ c' ^ n
hc' : 0 ≤ c'
x : α
hx : ‖(f ^ n) x‖ ≤ c' ^ n * ‖(g ^ n) x‖
⊢ c' ^ n * ‖g x ^ n‖ ≤ c' ^ n * ‖g x‖ ^ n

Tactic:
gcongr

Result:
case h
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
c c' : ℝ
l : Filter α
n : ℕ
f : α → 𝕜
g : α → R
h : IsBigOWith c l (f ^ n) (g ^ n)
hn : n ≠ 0
hc : c ≤ c' ^ n
hc' : 0 ≤ c'
x : α
hx : ‖(f ^ n) x‖ ≤ c' ^ n * ‖(g ^ n) x‖
⊢ ‖g x ^ n‖ ≤ ‖g x‖ ^ n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem map_zipIdx (f : α → β) (l : Vector α n) (k : Nat) :
    map (Prod.map f id) (zipIdx l k) = zipIdx (l.map f) k

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
l : Vector α n
k : Nat
⊢ map (Prod.map f id) (l.zipIdx k) = (map f l).zipIdx k

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
k : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map (Prod.map f id) ({ toArray := toArray✝, size_toArray := size_toArray✝ }.zipIdx k) =
    (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).zipIdx k

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
k : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map (Prod.map f id) ({ toArray := toArray✝, size_toArray := size_toArray✝ }.zipIdx k) =
    (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).zipIdx k

Tactic:
simp [Array.map_zipIdx]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem of'_mul_modOf (g : G) (x : k[G]) : of' k G g * x %ᵒᶠ g = 0

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : k[G]
⊢ of' k G g * x %ᵒᶠ g = 0

Tactic:
ext g'

Result:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : k[G]
g' : G
⊢ (of' k G g * x %ᵒᶠ g) g' = 0 g'

Proof state:
case H.inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : k[G]
d : G
⊢ (of' k G g * x %ᵒᶠ g) (g + d) = 0

Tactic:
rw [modOf_apply_self_add]

Result:
no goals

Proof state:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : k[G]
g' : G
⊢ (of' k G g * x %ᵒᶠ g) g' = 0

Tactic:
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)

Result:
case H.inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : k[G]
d : G
⊢ (of' k G g * x %ᵒᶠ g) (g + d) = 0

case H.inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ (of' k G g * x %ᵒᶠ g) g' = 0

Proof state:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : k[G]
g' : G
⊢ (of' k G g * x %ᵒᶠ g) g' = 0 g'

Tactic:
rw [Finsupp.zero_apply]

Result:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : k[G]
g' : G
⊢ (of' k G g * x %ᵒᶠ g) g' = 0

Proof state:
case H.inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ (of' k G g * x %ᵒᶠ g) g' = 0

Tactic:
rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem restrict_of_measure_ne_top [BorelSpace α] [WeaklyRegular μ] {A : Set α}
    (h'A : μ A ≠ ∞) : WeaklyRegular (μ.restrict A)

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
inst✝ : μ.WeaklyRegular
A : Set α
h'A : μ A ≠ ⊤
⊢ (μ.restrict A).WeaklyRegular

Tactic:
haveI : Fact (μ A < ∞) := ⟨h'A.lt_top⟩

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
inst✝ : μ.WeaklyRegular
A : Set α
h'A : μ A ≠ ⊤
this : Fact (μ A < ⊤)
⊢ (μ.restrict A).WeaklyRegular

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
inst✝ : μ.WeaklyRegular
A : Set α
h'A : μ A ≠ ⊤
this✝ : Fact (μ A < ⊤)
V : Set α
V_open : IsOpen V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
this : (μ.restrict A).InnerRegularWRT IsClosed fun s => MeasurableSet s
⊢ ∃ K ⊆ V, IsClosed K ∧ r < (μ.restrict A) K

Tactic:
exact this V_open.measurableSet r hr

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
inst✝ : μ.WeaklyRegular
A : Set α
h'A : μ A ≠ ⊤
this : Fact (μ A < ⊤)
⊢ (μ.restrict A).WeaklyRegular

Tactic:
refine InnerRegularWRT.weaklyRegular_of_finite (μ.restrict A) (fun V V_open r hr ↦ ?_)

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
inst✝ : μ.WeaklyRegular
A : Set α
h'A : μ A ≠ ⊤
this : Fact (μ A < ⊤)
V : Set α
V_open : IsOpen V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
⊢ ∃ K ⊆ V, IsClosed K ∧ r < (μ.restrict A) K

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
inst✝ : μ.WeaklyRegular
A : Set α
h'A : μ A ≠ ⊤
this : Fact (μ A < ⊤)
V : Set α
V_open : IsOpen V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
⊢ ∃ K ⊆ V, IsClosed K ∧ r < (μ.restrict A) K

Tactic:
have : InnerRegularWRT (μ.restrict A) IsClosed (fun s ↦ MeasurableSet s) :=
  InnerRegularWRT.restrict_of_measure_ne_top innerRegular_measurable h'A

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
inst✝ : μ.WeaklyRegular
A : Set α
h'A : μ A ≠ ⊤
this✝ : Fact (μ A < ⊤)
V : Set α
V_open : IsOpen V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
this : (μ.restrict A).InnerRegularWRT IsClosed fun s => MeasurableSet s
⊢ ∃ K ⊆ V, IsClosed K ∧ r < (μ.restrict A) K
-- Mathlib/Order/Cover.lean
theorem covBy_iff_le_iff_lt_left {x y : α} : x ⋖ y ↔ ∀ {z}, z ≤ x ↔ z < y

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ x ⋖ y ↔ ∀ {z : α}, z ≤ x ↔ z < y

Tactic:
simp_rw [covBy_iff_lt_iff_le_left, iff_comm]

Result:
no goals
-- Mathlib/Data/Matroid/Loop.lean
lemma IsRestriction.isLoop_iff (hNM : N ≤r M) : N.IsLoop e ↔ e ∈ N.E ∧ M.IsLoop e

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
e : α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsLoop e ↔ e ∈ (M ↾ R).E ∧ M.IsLoop e

Tactic:
simp only [restrict_isLoop_iff, restrict_ground_eq, and_congr_right_iff, or_iff_left_iff_imp]

Result:
case intro.intro
α : Type u_1
M : Matroid α
e : α
R : Set α
hR : R ⊆ M.E
⊢ e ∈ R → e ∉ M.E → M.IsLoop e

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
e : α
R : Set α
hR : R ⊆ M.E
⊢ e ∈ R → e ∉ M.E → M.IsLoop e

Tactic:
exact fun heR heE ↦ (heE (hR heR)).elim

Result:
no goals

Proof state:
α : Type u_1
M N : Matroid α
e : α
hNM : N ≤r M
⊢ N.IsLoop e ↔ e ∈ N.E ∧ M.IsLoop e

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Result:
case intro.intro
α : Type u_1
M : Matroid α
e : α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsLoop e ↔ e ∈ (M ↾ R).E ∧ M.IsLoop e
-- Mathlib/GroupTheory/ArchimedeanDensely.lean
lemma LinearOrderedAddCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete
    {G : Type*} [LinearOrderedAddCommGroup G] [Nontrivial G] (g : G) :
    Set.WellFoundedOn {x : G | x ≤ g} (· > ·) ↔ Nonempty (G ≃+o ℤ)

Proof state:
case refine_4
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : {x | -g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
a✝ : G
⊢ a✝ ∈ {x | x ≤ g} → ∀ b ∈ {x | x ≤ g}, a✝ > b → Function.onFun (fun x1 x2 => x1 < x2) (fun x => -x) a✝ b

Tactic:
simp [Function.onFun, neg_le]

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 => x1 > x2) ↔ Nonempty (G ≃+o ℤ)

Tactic:
rw [← wellFoundedOn_setOf_le_lt_iff_nonempty_discrete (g := -g)]

Result:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 => x1 > x2) ↔ {x | -g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2

Proof state:
case refine_4
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : {x | -g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ ∀ a ∈ {x | x ≤ g}, ∀ b ∈ {x | x ≤ g}, a > b → Function.onFun (fun x1 x2 => x1 < x2) (fun x => -x) a b

Tactic:
intro

Result:
case refine_4
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
h : {x | -g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
a✝ : G
⊢ a✝ ∈ {x | x ≤ g} → ∀ b ∈ {x | x ≤ g}, a✝ > b → Function.onFun (fun x1 x2 => x1 < x2) (fun x => -x) a✝ b
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem left_ne_zero_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : x ≠ 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y ≠ 0
⊢ x ≠ 0

Tactic:
rintro rfl

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
y : V
h : o.oangle 0 y ≠ 0
⊢ False

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
y : V
h : o.oangle 0 y ≠ 0
⊢ False

Tactic:
simp at h

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem get_tail (x : Vector α n) (i) : x.tail.get i = x.get ⟨i.1 + 1, by omega⟩

Proof state:
case mk.mk.nil
α : Type u_1
n i : ℕ
ih : i < n - 1
h : [].length = n
⊢ (tail ⟨[], h⟩).get ⟨i, ih⟩ = get ⟨[], h⟩ ⟨i + 1, ⋯⟩

Tactic:
rw [List.length] at h

Result:
case mk.mk.nil
α : Type u_1
n i : ℕ
ih : i < n - 1
h✝ : [].length = n
h : 0 = n
⊢ (tail ⟨[], h✝⟩).get ⟨i, ih⟩ = get ⟨[], h✝⟩ ⟨i + 1, ⋯⟩

Proof state:
case mk.mk.nil
α : Type u_1
n i : ℕ
ih✝ : i < n - 1
ih : i < 0 - 1
h✝ : [].length = n
h : 0 = n
⊢ (tail ⟨[], h✝⟩).get ⟨i, ih✝⟩ = get ⟨[], h✝⟩ ⟨i + 1, ⋯⟩

Tactic:
contradiction

Result:
no goals

Proof state:
case mk
α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ x.tail.get ⟨i, ih⟩ = x.get ⟨↑⟨i, ih⟩ + 1, ⋯⟩

Tactic:
dsimp

Result:
case mk
α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ x.tail.get ⟨i, ih⟩ = x.get ⟨i + 1, ⋯⟩

Proof state:
α : Type u_1
n : ℕ
x : Vector α n
i : Fin (n - 1)
⊢ x.tail.get i = x.get ⟨↑i + 1, ⋯⟩

Tactic:
obtain ⟨i, ih⟩ := i

Result:
case mk
α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ x.tail.get ⟨i, ih⟩ = x.get ⟨↑⟨i, ih⟩ + 1, ⋯⟩

Proof state:
case mk.mk.nil
α : Type u_1
n i : ℕ
ih : i < n - 1
h✝ : [].length = n
h : 0 = n
⊢ (tail ⟨[], h✝⟩).get ⟨i, ih⟩ = get ⟨[], h✝⟩ ⟨i + 1, ⋯⟩

Tactic:
rw [← h] at ih

Result:
case mk.mk.nil
α : Type u_1
n i : ℕ
ih✝ : i < n - 1
ih : i < 0 - 1
h✝ : [].length = n
h : 0 = n
⊢ (tail ⟨[], h✝⟩).get ⟨i, ih✝⟩ = get ⟨[], h✝⟩ ⟨i + 1, ⋯⟩

Proof state:
case mk
α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ x.tail.get ⟨i, ih⟩ = x.get ⟨i + 1, ⋯⟩

Tactic:
rcases x with ⟨_ | _, h⟩ <;> try rfl

Result:
case mk.mk.nil
α : Type u_1
n i : ℕ
ih : i < n - 1
h : [].length = n
⊢ (tail ⟨[], h⟩).get ⟨i, ih⟩ = get ⟨[], h⟩ ⟨i + 1, ⋯⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
x : Vector α n
i : Fin (n - 1)
⊢ ↑i + 1 < n

Tactic:
omega

Result:
no goals

Proof state:
case mk.mk.cons
α : Type u_1
n i : ℕ
ih : i < n - 1
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length = n
⊢ (tail ⟨head✝ :: tail✝, h⟩).get ⟨i, ih⟩ = get ⟨head✝ :: tail✝, h⟩ ⟨i + 1, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_sq_pi_over_two_pow (n : ℕ) :
    sin (π / 2 ^ (n + 1)) ^ 2 = 1 - (sqrtTwoAddSeries 0 n / 2) ^ 2

Proof state:
n : ℕ
⊢ sin (π / 2 ^ (n + 1)) ^ 2 = 1 - (sqrtTwoAddSeries 0 n / 2) ^ 2

Tactic:
rw [sin_sq, cos_pi_over_two_pow]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma comp_add (α : Ext X Y n) {m : ℕ} (β₁ β₂ : Ext Y Z m) {p : ℕ} (h : n + m = p) :
    α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β₁ β₂ : Ext Y Z m
p : ℕ
h : n + m = p
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β₁ β₂ : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β₁ β₂ : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (α.comp (β₁ + β₂) h).hom = (α.comp β₁ h + α.comp β₂ h).hom

Tactic:
simp [this, add_hom']

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β₁ β₂ : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β₁ β₂ : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (α.comp (β₁ + β₂) h).hom = (α.comp β₁ h + α.comp β₂ h).hom