harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem card_interedges_add_card_interedges_compl (s : Finset α) (t : Finset β) :
    #(interedges r s t) + #(interedges (fun x y ↦ ¬r x y) s t) = #s * #t

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ #(interedges r s t) + #(interedges (fun x y => ¬r x y) s t) = #s * #t

Tactic:
classical
rw [← card_product, interedges, interedges, ← card_union_of_disjoint, filter_union_filter_neg_eq]
exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ #(interedges r s t) + #(interedges (fun x y => ¬r x y) s t) = #s * #t

Tactic:
rw [← card_product, interedges, interedges, ← card_union_of_disjoint, filter_union_filter_neg_eq]

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ Disjoint (filter (fun e => r e.1 e.2) (s ×ˢ t)) (filter (fun e => ¬r e.1 e.2) (s ×ˢ t))

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ Disjoint (filter (fun e => r e.1 e.2) (s ×ˢ t)) (filter (fun e => ¬r e.1 e.2) (s ×ˢ t))

Tactic:
exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem Arrows.pullbackCompatible_iff (x : (i : I) → P.obj (op (X i))) :
    Compatible P π x ↔ PullbackCompatible P π x

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
⊢ Compatible P π x ↔ PullbackCompatible P π x

Tactic:
refine ⟨fun t i j ↦ ?_, fun t i j Z gi gj comm ↦ ?_⟩

Result:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
t : Compatible P π x
i j : I
⊢ P.map (pullback.fst (π i) (π j)).op (x i) = P.map (pullback.snd (π i) (π j)).op (x j)

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
t : PullbackCompatible P π x
i j : I
Z : C
gi : Z ⟶ X i
gj : Z ⟶ X j
comm : gi ≫ π i = gj ≫ π j
⊢ P.map gi.op (x i) = P.map gj.op (x j)

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
t : PullbackCompatible P π x
i j : I
Z : C
gi : Z ⟶ X i
gj : Z ⟶ X j
comm : gi ≫ π i = gj ≫ π j
⊢ P.map gi.op (x i) = P.map gj.op (x j)

Tactic:
rw [← pullback.lift_fst _ _ comm, op_comp, FunctorToTypes.map_comp_apply, t i j,
  ← FunctorToTypes.map_comp_apply, ← op_comp, pullback.lift_snd]

Result:
no goals

Proof state:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
t : Compatible P π x
i j : I
⊢ P.map (pullback.fst (π i) (π j)).op (x i) = P.map (pullback.snd (π i) (π j)).op (x j)

Tactic:
apply t

Result:
case refine_1.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
t : Compatible P π x
i j : I
⊢ pullback.fst (π i) (π j) ≫ π i = pullback.snd (π i) (π j) ≫ π j

Proof state:
case refine_1.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
t : Compatible P π x
i j : I
⊢ pullback.fst (π i) (π j) ≫ π i = pullback.snd (π i) (π j) ≫ π j

Tactic:
exact pullback.condition

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem exists_pow_ne_one_of_isCyclic [G_cyclic : IsCyclic G]
    {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Nat.card G) : ∃ a : G, a ^ k ≠ 1

Proof state:
case h.e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x => a ^ x
k_lt_card_G : a ^ k = 1
⊢ Nat.card G = orderOf a

Tactic:
rw [← Nat.card_zpowers, eq_comm, card_eq_iff_eq_top, eq_top_iff]

Result:
case h.e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x => a ^ x
k_lt_card_G : a ^ k = 1
⊢ ⊤ ≤ zpowers a

Proof state:
G : Type u_2
inst✝ : Group G
G_cyclic : IsCyclic G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
⊢ ∃ a, a ^ k ≠ 1

Tactic:
rcases G_cyclic with ⟨a, ha⟩

Result:
case mk.intro
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
a : G
ha : Function.Surjective fun x => a ^ x
⊢ ∃ a, a ^ k ≠ 1

Proof state:
case mk.intro
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
a : G
ha : Function.Surjective fun x => a ^ x
⊢ ∃ a, a ^ k ≠ 1

Tactic:
use a

Result:
case h
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
a : G
ha : Function.Surjective fun x => a ^ x
⊢ a ^ k ≠ 1

Proof state:
G : Type u_2
inst✝ : Group G
G_cyclic : IsCyclic G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
⊢ ∃ a, a ^ k ≠ 1

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero (Nat.not_eq_zero_of_lt k_lt_card_G)

Result:
G : Type u_2
inst✝ : Group G
G_cyclic : IsCyclic G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
⊢ ∃ a, a ^ k ≠ 1

Proof state:
case h
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
a : G
ha : Function.Surjective fun x => a ^ x
⊢ a ^ k ≠ 1

Tactic:
contrapose! k_lt_card_G

Result:
case h
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x => a ^ x
k_lt_card_G : a ^ k = 1
⊢ Nat.card G ≤ k

Proof state:
case h
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x => a ^ x
k_lt_card_G : a ^ k = 1
⊢ Nat.card G ≤ k

Tactic:
convert orderOf_le_of_pow_eq_one k_pos.bot_lt k_lt_card_G

Result:
case h.e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x => a ^ x
k_lt_card_G : a ^ k = 1
⊢ Nat.card G = orderOf a

Proof state:
case h.e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x => a ^ x
k_lt_card_G : a ^ k = 1
⊢ ⊤ ≤ zpowers a

Tactic:
exact fun x _ ↦ ha x

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
/-- The lower part of the first column of the snake diagram is exact. -/
lemma exact_C₁_down : (ShortComplex.mk S.v₁₂.τ₁ S.v₂₃.τ₁
    (by rw [← comp_τ₁, S.w₁₃, zero_τ₁])).Exact :=
  exact_of_g_is_cokernel _ S.h₃τ₁

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.45520, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₁₂.τ₁ ≫ S.v₂₃.τ₁ = 0

Tactic:
rw [← comp_τ₁, S.w₁₃, zero_τ₁]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
lemma toInteger_isPrimitiveRoot {k : ℕ+} (hζ : IsPrimitiveRoot ζ k) :
    IsPrimitiveRoot hζ.toInteger k :=
  IsPrimitiveRoot.of_map_of_injective (by exact hζ) RingOfIntegers.coe_injective

Proof state:
K : Type u
inst✝ : Field K
ζ : K
k : ℕ+
hζ : IsPrimitiveRoot ζ ↑k
⊢ IsPrimitiveRoot ((algebraMap (𝓞 K) K) hζ.toInteger) ↑k

Tactic:
exact hζ

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_bot : comap m ⊥ = ⊥ :=
  bot_unique fun s _ => ⟨∅, mem_bot, by simp only [empty_subset, preimage_empty]⟩

Proof state:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
x✝ : s ∈ ⊥
⊢ m ⁻¹' ∅ ⊆ s

Tactic:
simp only [empty_subset, preimage_empty]

Result:
no goals
-- Mathlib/Data/Matroid/Dual.lean
theorem dual_dep_iff_forall : (M✶.Dep I) ↔ (∀ B, M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I : Set α
⊢ M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E

Tactic:
simp_rw [dep_iff, dual_indep_iff_exists', dual_ground, and_congr_left_iff, not_and,
  not_exists, not_and, not_disjoint_iff_nonempty_inter, Classical.imp_iff_right_iff,
  iff_true_intro Or.inl]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/Int.lean
/-- The 2-adic norm of the n-th harmonic number is 2 raised to the logarithm of n in base 2. -/
lemma padicNorm_two_harmonic {n : ℕ} (hn : n ≠ 0) :
    ‖(harmonic n : ℚ_[2])‖ = 2 ^ (Nat.log 2 n)

Proof state:
n : ℕ
hn : n ≠ 0
⊢ ‖↑(harmonic n)‖ = 2 ^ Nat.log 2 n

Tactic:
rw [padicNormE.eq_padicNorm, padicNorm.eq_zpow_of_nonzero (harmonic_pos hn).ne',
  padicValRat_two_harmonic, neg_neg, zpow_natCast, Rat.cast_pow, Rat.cast_natCast, Nat.cast_ofNat]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoLocallyUniformlyOn.congr {G : ι → α → β} (hf : TendstoLocallyUniformlyOn F f p s)
    (hg : ∀ n, s.EqOn (F n) (G n)) : TendstoLocallyUniformlyOn G f p s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ (n : ι), EqOn (F n) (G n) s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, G n y) ∈ u

Tactic:
obtain ⟨t, ht, h⟩ := hf u hu x hx

Result:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ (n : ι), EqOn (F n) (G n) s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
h : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, G n y) ∈ u

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ (n : ι), EqOn (F n) (G n) s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
h : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, G n y) ∈ u

Tactic:
refine ⟨s ∩ t, inter_mem self_mem_nhdsWithin ht, ?_⟩

Result:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ (n : ι), EqOn (F n) (G n) s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
h : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ s ∩ t, (f y, G n y) ∈ u

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ (n : ι), EqOn (F n) (G n) s
⊢ TendstoLocallyUniformlyOn G f p s

Tactic:
rintro u hu x hx

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ (n : ι), EqOn (F n) (G n) s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, G n y) ∈ u

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ (n : ι), EqOn (F n) (G n) s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
h : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ s ∩ t, (f y, G n y) ∈ u

Tactic:
filter_upwards [h] with i hi y hy using hg i hy.1 ▸ hi y hy.2

Result:
no goals
-- Mathlib/Topology/Sheaves/Stalks.lean
theorem germ_eq (F : X.Presheaf C) {U V : Opens X} (x : X) (mU : x ∈ U) (mV : x ∈ V)
    (s : ToType (F.obj (op U))) (t : ToType (F.obj (op V)))
    (h : F.germ U x mU s = F.germ V x mV t) :
    ∃ (W : Opens X) (_m : x ∈ W) (iU : W ⟶ U) (iV : W ⟶ V), F.map iU.op s = F.map iV.op t

Proof state:
case intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
U V : Opens ↑X
x : ↑X
mU : x ∈ U
mV : x ∈ V
s : ToType (F.obj (op U))
t : ToType (F.obj (op V))
h : (ConcreteCategory.hom (F.germ U x mU)) s = (ConcreteCategory.hom (F.germ V x mV)) t
W : (OpenNhds x)ᵒᵖ
iU : op { obj := U, property := mU } ⟶ W
iV : op { obj := V, property := mV } ⟶ W
e : (((OpenNhds.inclusion x).op ⋙ F) ⋙ forget C).map iU s = (((OpenNhds.inclusion x).op ⋙ F) ⋙ forget C).map iV t
⊢ ∃ W, ∃ (_ : x ∈ W), ∃ iU iV, (ConcreteCategory.hom (F.map iU.op)) s = (ConcreteCategory.hom (F.map iV.op)) t

Tactic:
exact ⟨(unop W).1, (unop W).2, iU.unop, iV.unop, e⟩

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
U V : Opens ↑X
x : ↑X
mU : x ∈ U
mV : x ∈ V
s : ToType (F.obj (op U))
t : ToType (F.obj (op V))
h : (ConcreteCategory.hom (F.germ U x mU)) s = (ConcreteCategory.hom (F.germ V x mV)) t
⊢ ∃ W, ∃ (_ : x ∈ W), ∃ iU iV, (ConcreteCategory.hom (F.map iU.op)) s = (ConcreteCategory.hom (F.map iV.op)) t

Tactic:
obtain ⟨W, iU, iV, e⟩ :=
  (Types.FilteredColimit.isColimit_eq_iff.{v, v} _
        (isColimitOfPreserves (forget C) (colimit.isColimit ((OpenNhds.inclusion x).op ⋙ F)))).mp
      h

Result:
case intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
U V : Opens ↑X
x : ↑X
mU : x ∈ U
mV : x ∈ V
s : ToType (F.obj (op U))
t : ToType (F.obj (op V))
h : (ConcreteCategory.hom (F.germ U x mU)) s = (ConcreteCategory.hom (F.germ V x mV)) t
W : (OpenNhds x)ᵒᵖ
iU : op { obj := U, property := mU } ⟶ W
iV : op { obj := V, property := mV } ⟶ W
e : (((OpenNhds.inclusion x).op ⋙ F) ⋙ forget C).map iU s = (((OpenNhds.inclusion x).op ⋙ F) ⋙ forget C).map iV t
⊢ ∃ W, ∃ (_ : x ∈ W), ∃ iU iV, (ConcreteCategory.hom (F.map iU.op)) s = (ConcreteCategory.hom (F.map iV.op)) t
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive (attr := simp)] lemma mul_inv_cancel_comm_assoc (a b : G) : a * (b * a⁻¹) = b

Proof state:
G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a * (b * a⁻¹) = b

Tactic:
rw [mul_comm, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass {γ : Type*}
    {F : Filter γ} {μs : γ → FiniteMeasure Ω}
    (μs_lim : Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize))
    (mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)) (f : Ω →ᵇ ℝ≥0) :
    Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Proof state:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
by_cases h_mass : μ.mass = 0

Result:
case pos
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)
f : Ω →ᵇ ℝ≥0
h_mass : μ.mass = 0
⊢ Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

case neg
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)
f : Ω →ᵇ ℝ≥0
h_mass : ¬μ.mass = 0
⊢ Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
-- Mathlib/Order/Filter/Pointwise.lean
theorem pure_vsub_pure : (pure a : Filter β) -ᵥ pure b = (pure (a -ᵥ b) : Filter α)

Proof state:
α : Type u_2
β : Type u_3
inst✝ : VSub α β
a b : β
⊢ pure a -ᵥ pure b = pure (a -ᵥ b)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
theorem Fix.dest_mk (x : F (append1 α (Fix F α))) : Fix.dest (Fix.mk x) = x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ mk ∘ dest = _root_.id

Tactic:
ext (x : Fix F α)

Result:
case h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : F (α ::: Fix F α)
x : Fix F α
⊢ (mk ∘ dest) x = _root_.id x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = x

Tactic:
conv =>
  rhs
  rw [← MvFunctor.id_map x]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = TypeVec.id <$$> x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ rec (MvFunctor.map (TypeVec.id ::: mk)) (mk x) = x

Tactic:
rw [Fix.rec_eq, ← Fix.dest, ← comp_map]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ (mk x).dest = x

Tactic:
unfold Fix.dest

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ rec (MvFunctor.map (TypeVec.id ::: mk)) (mk x) = x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x

Tactic:
rw [this, appendFun_id_id]

Result:
no goals

Proof state:
case h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : F (α ::: Fix F α)
x : Fix F α
⊢ (mk ∘ dest) x = _root_.id x

Tactic:
apply Fix.mk_dest

Result:
no goals

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = TypeVec.id <$$> x

Tactic:
rw [← appendFun_comp, id_comp]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x

Tactic:
have : Fix.mk ∘ Fix.dest (F := F) (α := α) = _root_.id := by
  ext (x : Fix F α)
  apply Fix.mk_dest

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Fix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive]
lemma prod_min_le [LinearOrderedCommMonoid α] {s : Multiset ι} {f g : ι → α} :
    (s.map fun i ↦ min (f i) (g i)).prod ≤ min (s.map f).prod (s.map g).prod

Proof state:
case mk
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedCommMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (map (fun i => f i ⊓ g i) (Quot.mk (⇑(List.isSetoid ι)) l)).prod ≤
    (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod ⊓ (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]

Result:
case mk
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedCommMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (List.map (fun i => f i ⊓ g i) l).prod ≤ (List.map f l).prod ⊓ (List.map g l).prod

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedCommMonoid α
s : Multiset ι
f g : ι → α
⊢ (map (fun i => f i ⊓ g i) s).prod ≤ (map f s).prod ⊓ (map g s).prod

Tactic:
obtain ⟨l⟩ := s

Result:
case mk
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedCommMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (map (fun i => f i ⊓ g i) (Quot.mk (⇑(List.isSetoid ι)) l)).prod ≤
    (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod ⊓ (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Proof state:
case mk
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedCommMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (List.map (fun i => f i ⊓ g i) l).prod ≤ (List.map f l).prod ⊓ (List.map g l).prod

Tactic:
apply List.prod_min_le

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean
theorem measurable_limit_of_tendsto_metrizable_ae {ι} [Countable ι] [Nonempty ι] {μ : Measure α}
    {f : ι → α → β} {L : Filter ι} [L.IsCountablyGenerated] (hf : ∀ n, AEMeasurable (f n) μ)
    (h_ae_tendsto : ∀ᵐ x ∂μ, ∃ l : β, Tendsto (fun n => f n x) L (𝓝 l)) :
    ∃ f_lim : α → β, Measurable f_lim ∧ ∀ᵐ x ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
ι : Type u_3
inst✝² : Countable ι
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)
hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x
h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x
f_lim : α → β := fun x => if h : x ∈ aeSeqSet hf p then Exists.choose ⋯ else ⋯.some
hf_lim : ∀ (x : α), Tendsto (fun n => aeSeq hf p n x) L (𝓝 (f_lim x))
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))
⊢ ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))

Tactic:
have h_f_lim_meas : Measurable f_lim :=
  measurable_of_tendsto_metrizable' L (aeSeq.measurable hf p)
    (tendsto_pi_nhds.mpr fun x => hf_lim x)

Result:
case inr
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
ι : Type u_3
inst✝² : Countable ι
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)
hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x
h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x
f_lim : α → β := fun x => if h : x ∈ aeSeqSet hf p then Exists.choose ⋯ else ⋯.some
hf_lim : ∀ (x : α), Tendsto (fun n => aeSeq hf p n x) L (𝓝 (f_lim x))
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))
h_f_lim_meas : Measurable f_lim
⊢ ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))
-- Mathlib/Data/Nat/Init.lean
lemma div_lt_one_iff (hb : 0 < b) : a / b < 1 ↔ a < b

Proof state:
a b : ℕ
hb : 0 < b
⊢ a / b < 1 ↔ a < b

Tactic:
simp only [← Nat.not_le, one_le_div_iff hb]

Result:
no goals