harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsBigO.eq_zero_of_norm_pow_within {f : E'' → F''} {s : Set E''} {x₀ : E''} {n : ℕ}
    (h : f =O[𝓝[s] x₀] fun x => ‖x - x₀‖ ^ n) (hx₀ : x₀ ∈ s) (hn : n ≠ 0) : f x₀ = 0 :=
  mem_of_mem_nhdsWithin hx₀ h.eq_zero_imp <| by simp_rw [sub_self, norm_zero, zero_pow hn]

Proof state:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : E'' → F''
s : Set E''
x₀ : E''
n : ℕ
h : f =O[𝓝[s] x₀] fun x => ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : n ≠ 0
⊢ ‖x₀ - x₀‖ ^ n = 0

Tactic:
simp_rw [sub_self, norm_zero, zero_pow hn]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
lemma isLocallySurjective_of_isLocallySurjective
    {F₁ F₂ F₃ : Cᵒᵖ ⥤ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃)
    [IsLocallySurjective J (f₁ ≫ f₂)] :
    IsLocallySurjective J f₂ where
  imageSieve_mem {X} x

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
X : C
x : ToType (F₃.obj (op X))
⊢ imageSieve f₂ x ∈ J X

Tactic:
refine J.superset_covering ?_ (imageSieve_mem J (f₁ ≫ f₂) x)

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
X : C
x : ToType (F₃.obj (op X))
⊢ imageSieve (f₁ ≫ f₂) x ≤ imageSieve f₂ x

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
X : C
x : ToType (F₃.obj (op X))
⊢ imageSieve (f₁ ≫ f₂) x ≤ imageSieve f₂ x

Tactic:
intro Y g hg

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
X : C
x : ToType (F₃.obj (op X))
Y : C
g : Y ⟶ X
hg : (imageSieve (f₁ ≫ f₂) x).arrows g
⊢ (imageSieve f₂ x).arrows g

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
X : C
x : ToType (F₃.obj (op X))
Y : C
g : Y ⟶ X
hg : (imageSieve (f₁ ≫ f₂) x).arrows g
⊢ (imageSieve f₂ x).arrows g

Tactic:
exact ⟨f₁.app _ (localPreimage (f₁ ≫ f₂) x g hg),
  by simpa using app_localPreimage (f₁ ≫ f₂) x g hg⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
X : C
x : ToType (F₃.obj (op X))
Y : C
g : Y ⟶ X
hg : (imageSieve (f₁ ≫ f₂) x).arrows g
⊢ (ConcreteCategory.hom (f₂.app (op Y))) ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) x g hg)) =
    (ConcreteCategory.hom (F₃.map g.op)) x

Tactic:
simpa using app_localPreimage (f₁ ≫ f₂) x g hg

Result:
no goals
-- Mathlib/Algebra/Colimit/Module.lean
theorem of.zero_exact {i x} (H : of R ι G f i x = 0) :
    ∃ j hij, f i j hij x = (0 : G j)

Proof state:
case h.e'_2.h.h.e'_2.h.h.e'_3
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x : G i
H : (of R ι G f i) x = 0
x✝¹ : ι
x✝ : i ≤ x✝¹
⊢ 0 = (f i x✝¹ x✝) 0

Tactic:
rw [map_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x : G i
H : (of R ι G f i) x = 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = 0

Tactic:
convert exists_eq_of_of_eq (H.trans (map_zero <| _).symm)

Result:
case h.e'_2.h.h.e'_2.h.h.e'_3
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝¹ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i : ι
x : G i
H : (of R ι G f i) x = 0
x✝¹ : ι
x✝ : i ≤ x✝¹
⊢ 0 = (f i x✝¹ x✝) 0
-- Mathlib/Data/Nat/Factorization/PrimePow.lean
theorem isPrimePow_pow_iff {n k : ℕ} (hk : k ≠ 0) : IsPrimePow (n ^ k) ↔ IsPrimePow n

Proof state:
case h
n k : ℕ
hk : k ≠ 0
p : ℕ
hp : Nat.Prime p
⊢ p ∣ n ^ k ↔ p ∣ n

Tactic:
exact ⟨hp.dvd_of_dvd_pow, fun t => t.trans (dvd_pow_self _ hk)⟩

Result:
no goals

Proof state:
case h
n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a → (a ∣ n ^ k ↔ a ∣ n)

Tactic:
intro p hp

Result:
case h
n k : ℕ
hk : k ≠ 0
p : ℕ
hp : Nat.Prime p
⊢ p ∣ n ^ k ↔ p ∣ n

Proof state:
case h
n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a ∧ a ∣ n ^ k ↔ Nat.Prime a ∧ a ∣ n

Tactic:
simp only [and_congr_right_iff]

Result:
case h
n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a → (a ∣ n ^ k ↔ a ∣ n)

Proof state:
n k : ℕ
hk : k ≠ 0
⊢ (∃! p, Nat.Prime p ∧ p ∣ n ^ k) ↔ ∃! p, Nat.Prime p ∧ p ∣ n

Tactic:
apply existsUnique_congr

Result:
case h
n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a ∧ a ∣ n ^ k ↔ Nat.Prime a ∧ a ∣ n

Proof state:
n k : ℕ
hk : k ≠ 0
⊢ IsPrimePow (n ^ k) ↔ IsPrimePow n

Tactic:
simp only [isPrimePow_iff_unique_prime_dvd]

Result:
n k : ℕ
hk : k ≠ 0
⊢ (∃! p, Nat.Prime p ∧ p ∣ n ^ k) ↔ ∃! p, Nat.Prime p ∧ p ∣ n
-- Mathlib/Data/Finset/Card.lean
theorem card_eq_three : #s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Proof state:
case mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ #{x, y, z} = 3

Tactic:
simp only [xy, xz, yz, mem_insert, card_insert_of_not_mem, not_false_iff, mem_singleton,
  or_self_iff, card_singleton]

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
a b c : α
bc : b ≠ c
abc : ¬a = b ∧ ¬a = c
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {a, b, c} = {x, y, z}

Tactic:
exact ⟨a, b, c, abc.1, abc.2, bc, rfl⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 2) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
simp_rw [card_eq_two]

Result:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Proof state:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
rintro ⟨a, _, abc, rfl, b, c, bc, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
a b c : α
bc : b ≠ c
abc : a ∉ {b, c}
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {a, b, c} = {x, y, z}

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
a b c : α
bc : b ≠ c
abc : a ∉ {b, c}
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {a, b, c} = {x, y, z}

Tactic:
rw [mem_insert, mem_singleton, not_or] at abc

Result:
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
a b c : α
bc : b ≠ c
abc : ¬a = b ∧ ¬a = c
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {a, b, c} = {x, y, z}

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
constructor

Result:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 3 → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → #s = 3

Proof state:
case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → #s = 3

Tactic:
rintro ⟨x, y, z, xy, xz, yz, rfl⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ #{x, y, z} = 3

Proof state:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 3 → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
rw [card_eq_succ]

Result:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 2) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma IsOfFinOrder.mem_powers_iff_mem_zpowers (hx : IsOfFinOrder x) :
    y ∈ powers x ↔ y ∈ zpowers x :=
  ⟨fun ⟨n, hn⟩ ↦ ⟨n, by simp_all⟩, fun ⟨i, hi⟩ ↦ ⟨(i % orderOf x).natAbs, by
    dsimp only
    rwa [← zpow_natCast, Int.natAbs_of_nonneg <| Int.emod_nonneg _ <|
      Int.natCast_ne_zero_iff_pos.2 <| hx.orderOf_pos, zpow_mod_orderOf]⟩⟩

Proof state:
G : Type u_1
inst✝ : Group G
x y : G
hx : IsOfFinOrder x
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
⊢ (fun x_1 => x ^ x_1) (i % ↑(orderOf x)).natAbs = y

Tactic:
dsimp only

Result:
G : Type u_1
inst✝ : Group G
x y : G
hx : IsOfFinOrder x
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
⊢ x ^ (i % ↑(orderOf x)).natAbs = y

Proof state:
G : Type u_1
inst✝ : Group G
x y : G
hx : IsOfFinOrder x
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
⊢ x ^ (i % ↑(orderOf x)).natAbs = y

Tactic:
rwa [← zpow_natCast, Int.natAbs_of_nonneg <| Int.emod_nonneg _ <|
  Int.natCast_ne_zero_iff_pos.2 <| hx.orderOf_pos, zpow_mod_orderOf]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
x y : G
hx : IsOfFinOrder x
x✝ : y ∈ powers x
n : ℕ
hn : (fun x_1 => x ^ x_1) n = y
⊢ (fun x_1 => x ^ x_1) ↑n = y

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem mul_right' (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n * c]

Proof state:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
exact h.mul_left'

Result:
no goals

Proof state:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ a * c ≡ b * c [ZMOD n * c]

Tactic:
rw [mul_comm a, mul_comm b, mul_comm n]

Result:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]
-- Mathlib/Probability/Martingale/Basic.lean
theorem submartingale_nat [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f)
    (hint : ∀ i, Integrable (f i) μ) (hf : ∀ i, f i ≤ᵐ[μ] μ[f (i + 1)|𝒢 i]) :
    Submartingale f 𝒢 μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]
i : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ

Tactic:
have : ∫ ω in s, f (i + 1) ω ∂μ = ∫ ω in s, (μ[f (i + 1)|𝒢 i]) ω ∂μ :=
  (setIntegral_condExp (𝒢.le i) (hint _) hs).symm

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]
i : ℕ
s : Set Ω
hs : MeasurableSet s
this : ∫ (ω : Ω) in s, f (i + 1) ω ∂μ = ∫ (ω : Ω) in s, (μ[f (i + 1)|↑𝒢 i]) ω ∂μ
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]
i : ℕ
s : Set Ω
hs : MeasurableSet s
this : ∫ (ω : Ω) in s, f (i + 1) ω ∂μ = ∫ (ω : Ω) in s, (μ[f (i + 1)|↑𝒢 i]) ω ∂μ
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ

Tactic:
rw [this]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]
i : ℕ
s : Set Ω
hs : MeasurableSet s
this : ∫ (ω : Ω) in s, f (i + 1) ω ∂μ = ∫ (ω : Ω) in s, (μ[f (i + 1)|↑𝒢 i]) ω ∂μ
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, (μ[f (i + 1)|↑𝒢 i]) ω ∂μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]
⊢ Submartingale f 𝒢 μ

Tactic:
refine submartingale_of_setIntegral_le_succ hadp hint fun i s hs => ?_

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]
i : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]
i : ℕ
s : Set Ω
hs : MeasurableSet s
this : ∫ (ω : Ω) in s, f (i + 1) ω ∂μ = ∫ (ω : Ω) in s, (μ[f (i + 1)|↑𝒢 i]) ω ∂μ
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, (μ[f (i + 1)|↑𝒢 i]) ω ∂μ

Tactic:
exact setIntegral_mono_ae (hint i).integrableOn integrable_condExp.integrableOn (hf i)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findSome?_mkVector : findSome? f (mkVector n a) = if n = 0 then none else f a

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
⊢ findSome? f (mkVector n a) = if n = 0 then none else f a

Tactic:
rw [mkVector_eq_mk_mkArray, findSome?_mk, Array.findSome?_mkArray]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem head?_filter (p : α → Bool) (l : List α) : (l.filter p).head? = l.find? p

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ (filter p l).head? = find? p l

Tactic:
rw [← filterMap_eq_filter, head?_filterMap, findSome?_guard]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
/-- A finite-dimensional manifold modelled on a locally compact field
(such as ℝ, ℂ or the `p`-adic numbers) is locally compact. -/
lemma Manifold.locallyCompact_of_finiteDimensional
    (I : ModelWithCorners 𝕜 E H) [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E] :
    LocallyCompactSpace M

Proof state:
E : Type u_8
𝕜 : Type u_9
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_10
inst✝⁴ : TopologicalSpace H
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
this✝ : ProperSpace E
this : LocallyCompactSpace H
⊢ LocallyCompactSpace M

Tactic:
exact ChartedSpace.locallyCompactSpace H M

Result:
no goals

Proof state:
E : Type u_8
𝕜 : Type u_9
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_10
inst✝⁴ : TopologicalSpace H
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
this : ProperSpace E
⊢ LocallyCompactSpace M

Tactic:
have : LocallyCompactSpace H := I.locallyCompactSpace

Result:
E : Type u_8
𝕜 : Type u_9
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_10
inst✝⁴ : TopologicalSpace H
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
this✝ : ProperSpace E
this : LocallyCompactSpace H
⊢ LocallyCompactSpace M

Proof state:
E : Type u_8
𝕜 : Type u_9
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_10
inst✝⁴ : TopologicalSpace H
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
⊢ LocallyCompactSpace M

Tactic:
have : ProperSpace E := FiniteDimensional.proper 𝕜 E

Result:
E : Type u_8
𝕜 : Type u_9
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_10
inst✝⁴ : TopologicalSpace H
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
this : ProperSpace E
⊢ LocallyCompactSpace M
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[simp]
lemma HomologyData.leftRightHomologyComparison'_eq (h : S.HomologyData) :
    leftRightHomologyComparison' h.left h.right = h.iso.hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
⊢ leftRightHomologyComparison' h.left h.right = h.iso.hom

Tactic:
simp only [← cancel_epi h.left.π, ← cancel_mono h.right.ι, assoc,
  π_leftRightHomologyComparison'_ι, comm]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem inits_eq (s : Stream' α) :
    inits s = [head s]::map (List.cons (head s)) (inits (tail s))

Proof state:
case a
α : Type u
s : Stream' α
n : ℕ
⊢ s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n

Tactic:
cases n

Result:
case a.zero
α : Type u
s : Stream' α
⊢ s.inits.get 0 = ([s.head] :: map (List.cons s.head) s.tail.inits).get 0

case a.succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ s.inits.get (n✝ + 1) = ([s.head] :: map (List.cons s.head) s.tail.inits).get (n✝ + 1)

Proof state:
case a
α : Type u
s : Stream' α
⊢ ∀ (n : ℕ), s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n

Tactic:
intro n

Result:
case a
α : Type u
s : Stream' α
n : ℕ
⊢ s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n

Proof state:
case a.succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ take (n✝ + 1).succ s = s.head :: take n✝.succ s.tail

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
s : Stream' α
⊢ s.inits = [s.head] :: map (List.cons s.head) s.tail.inits

Tactic:
apply Stream'.ext

Result:
case a
α : Type u
s : Stream' α
⊢ ∀ (n : ℕ), s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n

Proof state:
case a.succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ s.inits.get (n✝ + 1) = ([s.head] :: map (List.cons s.head) s.tail.inits).get (n✝ + 1)

Tactic:
rw [get_inits, get_succ, tail_cons, get_map, get_inits]

Result:
case a.succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ take (n✝ + 1).succ s = s.head :: take n✝.succ s.tail

Proof state:
case a.zero
α : Type u
s : Stream' α
⊢ s.inits.get 0 = ([s.head] :: map (List.cons s.head) s.tail.inits).get 0

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
/-- See also `orderOf_eq_card_powers`. -/
@[to_additive "See also `addOrder_eq_card_multiples`."]
lemma Nat.card_submonoidPowers : Nat.card (powers a) = orderOf a

Proof state:
case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
have := (infinite_powers.2 ha).to_subtype

Result:
case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
this : Infinite ↑↑(powers a)
⊢ Nat.card ↥(powers a) = orderOf a

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
by_cases ha : IsOfFinOrder a

Result:
case pos
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Proof state:
case pos
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
exact (Nat.card_congr (finEquivPowers _ ha).symm).trans <| by simp

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card (Fin (orderOf a)) = orderOf a

Tactic:
simp

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
this : Infinite ↑↑(powers a)
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem mem_lift_of_splits_of_roots_mem_range [Algebra R K] {f : K[X]}
    (hs : f.Splits (RingHom.id K)) (hm : f.Monic) (hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range) :
    f ∈ Polynomial.lifts (algebraMap R K)

Proof state:
R : Type u_1
K : Type v
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : f.Monic
hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range
⊢ (Multiset.map (fun a => X - C a) f.roots).prod ∈ liftsRing (algebraMap R K)

Tactic:
refine Subring.multiset_prod_mem _ _ fun P hP => ?_

Result:
R : Type u_1
K : Type v
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : f.Monic
hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range
P : K[X]
hP : P ∈ Multiset.map (fun a => X - C a) f.roots
⊢ P ∈ liftsRing (algebraMap R K)

Proof state:
case intro.intro
R : Type u_1
K : Type v
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : f.Monic
hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range
b : K
hb : b ∈ f.roots
hP : X - C b ∈ Multiset.map (fun a => X - C a) f.roots
⊢ X - C b ∈ liftsRing (algebraMap R K)

Tactic:
exact Subring.sub_mem _ (X_mem_lifts _) (C'_mem_lifts (hr _ hb))

Result:
no goals

Proof state:
R : Type u_1
K : Type v
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : f.Monic
hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range
P : K[X]
hP : P ∈ Multiset.map (fun a => X - C a) f.roots
⊢ P ∈ liftsRing (algebraMap R K)

Tactic:
obtain ⟨b, hb, rfl⟩ := Multiset.mem_map.1 hP

Result:
case intro.intro
R : Type u_1
K : Type v
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : f.Monic
hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range
b : K
hb : b ∈ f.roots
hP : X - C b ∈ Multiset.map (fun a => X - C a) f.roots
⊢ X - C b ∈ liftsRing (algebraMap R K)

Proof state:
R : Type u_1
K : Type v
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : f.Monic
hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range
⊢ f ∈ lifts (algebraMap R K)

Tactic:
rw [eq_prod_roots_of_monic_of_splits_id hm hs, lifts_iff_liftsRing]

Result:
R : Type u_1
K : Type v
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : f.Monic
hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range
⊢ (Multiset.map (fun a => X - C a) f.roots).prod ∈ liftsRing (algebraMap R K)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Impl.lean
theorem mergeSort_eq_mergeSortTR : @mergeSort = @mergeSortTR

Proof state:
case h.h.h
x✝² : Type u_1
x✝¹ : List x✝²
x✝ : autoParam (x✝² → x✝² → Bool) _auto✝
⊢ x✝¹.mergeSort x✝ = mergeSortTR x✝¹ x✝

Tactic:
rw [mergeSortTR, mergeSortTR_run_eq_mergeSort]

Result:
no goals

Proof state:
⊢ @mergeSort = @mergeSortTR

Tactic:
funext

Result:
case h.h.h
x✝² : Type u_1
x✝¹ : List x✝²
x✝ : autoParam (x✝² → x✝² → Bool) _auto✝
⊢ x✝¹.mergeSort x✝ = mergeSortTR x✝¹ x✝