harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.AffineSubspace.SSameSide.oangle_sign_eq {s : AffineSubspace ℝ P} {p₁ p₂ p₃ p₄ : P}
    (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃p₄ : s.SSameSide p₃ p₄) :
    (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign

Proof state:
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p => ∡ p.1 p.2.1 p.2.2) sp
hsp : ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ ↑π
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign

Tactic:
have hp₃ : (p₁, p₃, p₂) ∈ sp :=
  Set.mem_image_of_mem _ (sSameSide_self_iff.2 ⟨hp₃p₄.nonempty, hp₃p₄.2.1⟩)

Result:
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p => (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p => ∡ p.1 p.2.1 p.2.2) sp
hsp : ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ ↑π
hp₃ : (p₁, p₃, p₂) ∈ sp
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
-- Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
lemma tendsto_harmonic_sub_log :
    Tendsto (fun n : ℕ ↦ harmonic n - log n) atTop (𝓝 eulerMascheroniConstant)

Proof state:
⊢ eulerMascheroniSeq' =ᶠ[atTop] fun n => ↑(harmonic n) - log ↑n

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn

Result:
case h
n : ℕ
hn : n ≠ 0
⊢ eulerMascheroniSeq' n = ↑(harmonic n) - log ↑n

Proof state:
⊢ Tendsto (fun n => ↑(harmonic n) - log ↑n) atTop (𝓝 eulerMascheroniConstant)

Tactic:
apply tendsto_eulerMascheroniSeq'.congr'

Result:
⊢ eulerMascheroniSeq' =ᶠ[atTop] fun n => ↑(harmonic n) - log ↑n

Proof state:
case h
n : ℕ
hn : n ≠ 0
⊢ eulerMascheroniSeq' n = ↑(harmonic n) - log ↑n

Tactic:
simp_rw [eulerMascheroniSeq', hn, if_false]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean
theorem aux1 {a b c : Nat} (h : b < a * c) : 0 < a

Proof state:
a b c : Nat
h : b < a * c
⊢ 0 < a

Tactic:
by_cases a = 0

Result:
case pos
a b c : Nat
h : b < a * c
h✝ : a = 0
⊢ 0 < a

case neg
a b c : Nat
h : b < a * c
h✝ : ¬a = 0
⊢ 0 < a

Proof state:
case pos
a b c : Nat
h : b < a * c
h✝ : a = 0
⊢ 0 < a

Tactic:
simp_all

Result:
no goals

Proof state:
case neg
a b c : Nat
h : b < a * c
h✝ : ¬a = 0
⊢ 0 < a

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean
@[reassoc]
lemma homologySequence_comp  :
    (F.shift n₀).map T.mor₁ ≫ (F.shift n₀).map T.mor₂ = 0

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ : ℤ
⊢ (F.shift n₀).map T.mor₁ ≫ (F.shift n₀).map T.mor₂ = 0

Tactic:
rw [← Functor.map_comp, comp_distTriang_mor_zero₁₂ _ hT, Functor.map_zero]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
@[simp] lemma support_div (f g : ι → G₀) : support (fun a ↦ f a / g a) = support f ∩ support g

Proof state:
ι : Type u_1
G₀ : Type u_3
inst✝ : GroupWithZero G₀
f g : ι → G₀
⊢ (support fun a => f a / g a) = support f ∩ support g

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_map_left (f : α → β) (F : Filter α) (G : Filter γ) :
    map f F ×ˢ G = map (Prod.map f id) (F ×ˢ G)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
F : Filter α
G : Filter γ
⊢ map f F ×ˢ G = map (Prod.map f id) (F ×ˢ G)

Tactic:
rw [← prod_map_map_eq', map_id]

Result:
no goals
-- Mathlib/Order/PFilter.lean
theorem sInf_gc :
    GaloisConnection (fun x => toDual (principal x)) fun F => sInf (ofDual F : PFilter P) :=
  fun x F => by simp only [le_sInf_iff, SetLike.mem_coe, toDual_le, SetLike.le_def, mem_principal]

Proof state:
P : Type u_1
inst✝ : CompleteSemilatticeInf P
x : P
F : (PFilter P)ᵒᵈ
⊢ (fun x => toDual (principal x)) x ≤ F ↔ x ≤ (fun F => sInf ↑(ofDual F)) F

Tactic:
simp only [le_sInf_iff, SetLike.mem_coe, toDual_le, SetLike.le_def, mem_principal]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem vector_ofFn {n} {f : Fin n → α → σ} (hf : ∀ i, Primrec (f i)) :
    Primrec fun a => List.Vector.ofFn fun i => f i a :=
  vector_toList_iff.1 <| by simp [list_ofFn hf]

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Primrec (f i)
⊢ Primrec fun a => (List.Vector.ofFn fun i => f i a).toList

Tactic:
simp [list_ofFn hf]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem exists_maximal_linearIndepOn' (v : ι → M) :
    ∃ s : Set ι, (LinearIndepOn R v s) ∧ ∀ t : Set ι, s ⊆ t → (LinearIndepOn R v t) → s = t

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s => LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J => ↑I ⊆ ↑J
f g : ι →₀ R
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hc : IsChain r ∅
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
hgsupp : g ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
⊢ g = 0

Tactic:
simpa using hgsupp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem continuousAt_oangle {x : P × P × P} (hx12 : x.1 ≠ x.2.1) (hx32 : x.2.2 ≠ x.2.1) :
    ContinuousAt (fun y : P × P × P => ∡ y.1 y.2.1 y.2.2) x

Proof state:
case funProp.discharger
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
⊢ (x.1 -ᵥ x.2.1, x.2.2 -ᵥ x.2.1).2 ≠ 0

Tactic:
simp [*]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
⊢ ContinuousAt (fun y => o.oangle (y.1 -ᵥ y.2.1) (y.2.2 -ᵥ y.2.1)) x

Tactic:
fun_prop (disch := simp [*])

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
⊢ ContinuousAt (fun y => ∡ y.1 y.2.1 y.2.2) x

Tactic:
unfold oangle

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
⊢ ContinuousAt (fun y => o.oangle (y.1 -ᵥ y.2.1) (y.2.2 -ᵥ y.2.1)) x
-- Mathlib/Data/Rat/Cast/Defs.lean
@[norm_cast] lemma cast_sub_of_ne_zero (hp : (p.den : α) ≠ 0) (hq : (q.den : α) ≠ 0) :
    ↑(p - q) = (p - q : α)

Proof state:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p - q) = ↑p - ↑q

Tactic:
simp [sub_eq_add_neg, cast_add_of_ne_zero, hp, hq]

Result:
no goals
-- Mathlib/Data/List/Dedup.lean
theorem dedup_append (l₁ l₂ : List α) : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = a :: l₁ ∪ l₂.dedup

Tactic:
simp only [cons_union] at *

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = List.insert a (l₁ ∪ l₂.dedup)

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∉ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
rw [dedup_cons_of_not_mem' h, insert_of_not_mem h]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = List.insert a (l₁ ∪ l₂.dedup)

Tactic:
rw [← IH, cons_append]

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∈ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
rw [dedup_cons_of_mem' h, insert_of_mem h]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
by_cases h : a ∈ dedup (l₁ ++ l₂)

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∈ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

case neg
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∉ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ ([] ++ l₂).dedup = [] ∪ l₂.dedup

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup

Tactic:
induction' l₁ with a l₁ IH

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ ([] ++ l₂).dedup = [] ∪ l₂.dedup

case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = a :: l₁ ∪ l₂.dedup
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem leftCoset_assoc (s : Set α) (a b : α) : a • (b • s) = (a * b) • s

Proof state:
α : Type u_1
inst✝ : Semigroup α
s : Set α
a b : α
⊢ a • b • s = (a * b) • s

Tactic:
simp [← image_smul, (image_comp _ _ _).symm, Function.comp, mul_assoc]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem Nontrivial.image_of_injOn (hs : s.Nontrivial) (hf : s.InjOn f) :
    (f '' s).Nontrivial

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Nontrivial
hf : InjOn f s
⊢ (f '' s).Nontrivial

Tactic:
obtain ⟨x, hx, y, hy, hxy⟩ := hs

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ (f '' s).Nontrivial
-- Mathlib/Order/KrullDimension.lean
lemma height_le_krullDim (a : α) : height a ≤ krullDim α

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
this : Nonempty α
⊢ ↑(height a) ≤ krullDim α

Tactic:
rw [krullDim_eq_iSup_length]

Result:
α : Type u_1
inst✝ : Preorder α
a : α
this : Nonempty α
⊢ ↑(height a) ≤ ↑(⨆ p, ↑p.length)

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ↑(height a) ≤ krullDim α

Tactic:
have : Nonempty α := ⟨a⟩

Result:
α : Type u_1
inst✝ : Preorder α
a : α
this : Nonempty α
⊢ ↑(height a) ≤ krullDim α

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
this : Nonempty α
⊢ ↑(height a) ≤ ↑(⨆ p, ↑p.length)

Tactic:
simp only [WithBot.coe_le_coe, iSup_le_iff]

Result:
α : Type u_1
inst✝ : Preorder α
a : α
this : Nonempty α
⊢ height a ≤ ⨆ p, ↑p.length

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
this : Nonempty α
⊢ height a ≤ ⨆ p, ↑p.length

Tactic:
exact height_le fun p _ ↦ le_iSup_of_le p le_rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
theorem coequalizer_preimage_image_eq_of_preimage_eq (π : Y ⟶ Z) (e : f ≫ π = g ≫ π)
    (h : IsColimit (Cofork.ofπ π e)) (U : Set Y) (H : f ⁻¹' U = g ⁻¹' U) : π ⁻¹' (π '' U) = U

Proof state:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), Function.Coequalizer.Rel f g x y → (x ∈ U ↔ y ∈ U)
⊢ ∀ {x y : Y}, (x ∈ U ↔ y ∈ U) → (y ∈ U ↔ x ∈ U)

Tactic:
tauto

Result:
no goals

Proof state:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
⊢ ∀ (x y : Y), Function.Coequalizer.Rel f g x y → (x ∈ U ↔ y ∈ U)

Tactic:
rintro _ _ ⟨x⟩

Result:
case intro
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
x : X
⊢ f x ∈ U ↔ g x ∈ U

Proof state:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
⊢ π ⁻¹' (π '' U) = U

Tactic:
have lem : ∀ x y, Function.Coequalizer.Rel f g x y → (x ∈ U ↔ y ∈ U) := by
  rintro _ _ ⟨x⟩
  change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
  rw [H]

Result:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), Function.Coequalizer.Rel f g x y → (x ∈ U ↔ y ∈ U)
⊢ π ⁻¹' (π '' U) = U

Proof state:
case h.mp.intro.intro
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), Function.Coequalizer.Rel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ y : Y
hy : y ∈ U
e' : Cofork.π (coequalizerColimit f g).cocone y = Cofork.π (coequalizerColimit f g).cocone x✝
⊢ x✝ ∈ U

Tactic:
exact (eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem (Quot.eqvGen_exact e'))).mp hy

Result:
no goals

Proof state:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), Function.Coequalizer.Rel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
⊢ π ⁻¹' (π '' U) = U

Tactic:
ext

Result:
case h
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : f ⁻¹' U = g ⁻¹' U
lem : ∀ (x y : Y), Function.Coequalizer.Rel f g x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U
x✝ : Y
⊢ x✝ ∈ π ⁻¹' (π '' U) ↔ x✝ ∈ U
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_flatten (f : α → β) (L : Array (Array α)) :
    (flatten L).map f = (map (map f) L).flatten

Proof state:
case of
α : Type u_1
β : Type u_2
f : α → β
xss : List (List α)
⊢ (List.map (List.map f) xss).flatten.toArray = (List.map (fun x => (List.map f x).toArray) xss).toArray.flatten

Tactic:
rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]

Result:
no goals

Proof state:
case of
α : Type u_1
β : Type u_2
f : α → β
xss : List (List α)
⊢ map f (List.map List.toArray xss).toArray.flatten = (map (map f) (List.map List.toArray xss).toArray).flatten

Tactic:
simp only [flatten_toArray_map, List.map_toArray, List.map_flatten, List.map_map,
  Function.comp_def]

Result:
case of
α : Type u_1
β : Type u_2
f : α → β
xss : List (List α)
⊢ (List.map (List.map f) xss).flatten.toArray = (List.map (fun x => (List.map f x).toArray) xss).toArray.flatten

Proof state:
α : Type u_1
β : Type u_2
f : α → β
L : Array (Array α)
⊢ map f L.flatten = (map (map f) L).flatten

Tactic:
induction L using array₂_induction with
| of xss =>
  simp only [flatten_toArray_map, List.map_toArray, List.map_flatten, List.map_map,
    Function.comp_def]
  rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/Measure.lean
theorem setOf_liouvilleWith_subset_aux :
    { x : ℝ | ∃ p > 2, LiouvilleWith p x } ⊆
      ⋃ m : ℤ, (· + (m : ℝ)) ⁻¹' ⋃ n > (0 : ℕ),
        { x : ℝ | ∃ᶠ b : ℕ in atTop, ∃ a ∈ Finset.Icc (0 : ℤ) b,
          |x - (a : ℤ) / b| < 1 / (b : ℝ) ^ (2 + 1 / n : ℝ) }

Proof state:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
⊢ x ∈
    ⋃ m,
      (fun x => x + ↑m) ⁻¹'
        ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}

Tactic:
simp only [mem_iUnion, mem_preimage]

Result:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
⊢ ∃ i i_1,
    ∃ (_ : i_1 > 0), x + ↑i ∈ {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑i_1)}
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem self_eq_mass_mul_normalize (s : Set Ω) : μ s = μ.mass * μ.normalize s

Proof state:
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
⊢ μ s = μ.mass * μ.normalize s

Tactic:
have mass_nonzero : μ.mass ≠ 0 := by rwa [μ.mass_nonzero_iff]

Result:
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : μ.mass ≠ 0
⊢ μ s = μ.mass * μ.normalize s

Proof state:
case inl
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
s : Set Ω
⊢ 0 s = mass 0 * (normalize 0) s

Tactic:
simp

Result:
no goals

Proof state:
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : μ.mass ≠ 0
⊢ μ s = μ.mass * ⟨↑(μ.mass⁻¹ • μ), ⋯⟩ s

Tactic:
simp [ProbabilityMeasure.coe_mk, toMeasure_smul, mul_inv_cancel_left₀ mass_nonzero, coeFn_def]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
⊢ μ.mass ≠ 0

Tactic:
rwa [μ.mass_nonzero_iff]

Result:
no goals

Proof state:
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : μ.mass ≠ 0
⊢ μ s = μ.mass * μ.normalize s

Tactic:
simp only [normalize, dif_neg mass_nonzero]

Result:
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : μ.mass ≠ 0
⊢ μ s = μ.mass * ⟨↑(μ.mass⁻¹ • μ), ⋯⟩ s

Proof state:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
⊢ μ s = μ.mass * μ.normalize s

Tactic:
obtain rfl | h := eq_or_ne μ 0

Result:
case inl
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
s : Set Ω
⊢ 0 s = mass 0 * (normalize 0) s

case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
⊢ μ s = μ.mass * μ.normalize s
-- Mathlib/MeasureTheory/Measure/Haar/Quotient.lean
theorem MeasureTheory.Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set {s : Set G}
    (fund_dom_s : IsFundamentalDomain Γ.op s ν) {V : Set (G ⧸ Γ)}
    (meas_V : MeasurableSet V) (neZeroV : μ V ≠ 0) (hV : μ V = ν (π ⁻¹' V ∩ s))
    (neTopV : μ V ≠ ⊤) : QuotientMeasureEqMeasurePreimage ν μ

Proof state:
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ⊤
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
has_fund : HasFundamentalDomain (↥Γ.op) G ν
i : QuotientMeasureEqMeasurePreimage ν μ'
this✝ : μ'.IsMulLeftInvariant
this : μ = μ'
⊢ μ' U = (map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)) U

Tactic:
rfl

Result:
no goals

Proof state:
case h.convert_3
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ⊤
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
has_fund : HasFundamentalDomain (↥Γ.op) G ν
i : QuotientMeasureEqMeasurePreimage ν μ'
this✝ : μ'.IsMulLeftInvariant
this : SigmaFinite μ'
⊢ ν (QuotientGroup.mk ⁻¹' V ∩ s) ≠ ⊤

Tactic:
exact trans hV.symm neTopV

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem rnDeriv_lt_top (μ ν : Measure α) [SigmaFinite μ] : ∀ᵐ x ∂ν, μ.rnDeriv ν x < ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x < ⊤

Tactic:
suffices ∀ n, ∀ᵐ x ∂ν, x ∈ spanningSets μ n → μ.rnDeriv ν x < ∞ by
  filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → μ.rnDeriv ν x < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → μ.rnDeriv ν x < ⊤
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x < ⊤

Tactic:
filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ μ (spanningSets μ n) ≠ ⊤

Tactic:
exact (measure_spanningSets_lt_top _ _).ne

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∫⁻ (x : α) in spanningSets μ n, μ.rnDeriv ν x ∂ν ≠ ⊤

Tactic:
refine (lintegral_rnDeriv_lt_top_of_measure_ne_top _ ?_).ne

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ μ (spanningSets μ n) ≠ ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → μ.rnDeriv ν x < ⊤

Tactic:
intro n

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → μ.rnDeriv ν x < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → μ.rnDeriv ν x < ⊤

Tactic:
rw [← ae_restrict_iff' (measurableSet_spanningSets _ _)]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂ν.restrict (spanningSets μ n), μ.rnDeriv ν x < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂ν.restrict (spanningSets μ n), μ.rnDeriv ν x < ⊤

Tactic:
apply ae_lt_top (measurable_rnDeriv _ _)

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∫⁻ (x : α) in spanningSets μ n, μ.rnDeriv ν x ∂ν ≠ ⊤
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsCompact.isLindelof (hs : IsCompact s) :
    IsLindelof s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
⊢ IsLindelof s

Tactic:
tauto

Result:
no goals