harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.lift_map {f g : J → C} [HasBiproduct f] [HasBiproduct g] {P : C}
    (k : ∀ j, P ⟶ f j) (p : ∀ j, f j ⟶ g j) :
    biproduct.lift k ≫ biproduct.map p = biproduct.lift fun j => k j ≫ p j

Proof state:
case w
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
P : C
k : (j : J) → P ⟶ f j
p : (j : J) → f j ⟶ g j
j✝ : J
⊢ (lift k ≫ map p) ≫ π g j✝ = (lift fun j => k j ≫ p j) ≫ π g j✝

Tactic:
simp

Result:
no goals

Proof state:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
P : C
k : (j : J) → P ⟶ f j
p : (j : J) → f j ⟶ g j
⊢ lift k ≫ map p = lift fun j => k j ≫ p j

Tactic:
ext

Result:
case w
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
P : C
k : (j : J) → P ⟶ f j
p : (j : J) → f j ⟶ g j
j✝ : J
⊢ (lift k ≫ map p) ≫ π g j✝ = (lift fun j => k j ≫ p j) ≫ π g j✝
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem trunc_derivativeFun (f : R⟦X⟧) (n : ℕ) :
    trunc n f.derivativeFun = derivative (trunc (n + 1) f)

Proof state:
case pos
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
⊢ (coeff R d) f.derivativeFun = (derivative (trunc (n + 1) f)).coeff d

Tactic:
have : d + 1 < n + 1 := succ_lt_succ_iff.2 h

Result:
case pos
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
this : d + 1 < n + 1
⊢ (coeff R d) f.derivativeFun = (derivative (trunc (n + 1) f)).coeff d

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
⊢ (if d < n then (coeff R d) f.derivativeFun else 0) = (derivative (trunc (n + 1) f)).coeff d

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
⊢ (coeff R d) f.derivativeFun = (derivative (trunc (n + 1) f)).coeff d

case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
⊢ 0 = (derivative (trunc (n + 1) f)).coeff d

Proof state:
case pos
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
this : d + 1 < n + 1
⊢ (coeff R d) f.derivativeFun = (derivative (trunc (n + 1) f)).coeff d

Tactic:
rw [coeff_derivativeFun, coeff_derivative, coeff_trunc, if_pos this]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ trunc n f.derivativeFun = derivative (trunc (n + 1) f)

Tactic:
ext d

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
⊢ (trunc n f.derivativeFun).coeff d = (derivative (trunc (n + 1) f)).coeff d

Proof state:
case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
⊢ 0 = (derivative (trunc (n + 1) f)).coeff d

Tactic:
have : ¬d + 1 < n + 1 := by rwa [succ_lt_succ_iff]

Result:
case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
this : ¬d + 1 < n + 1
⊢ 0 = (derivative (trunc (n + 1) f)).coeff d

Proof state:
case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
this : ¬d + 1 < n + 1
⊢ 0 = (derivative (trunc (n + 1) f)).coeff d

Tactic:
rw [coeff_derivative, coeff_trunc, if_neg this, zero_mul]

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
⊢ (trunc n f.derivativeFun).coeff d = (derivative (trunc (n + 1) f)).coeff d

Tactic:
rw [coeff_trunc]

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
⊢ (if d < n then (coeff R d) f.derivativeFun else 0) = (derivative (trunc (n + 1) f)).coeff d

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
⊢ ¬d + 1 < n + 1

Tactic:
rwa [succ_lt_succ_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean
theorem integral_mulExpNegMulSq_comp_eq {P' : Measure E} [IsFiniteMeasure P']
    {A : Subalgebra ℝ C(E, ℝ)} (hε : 0 < ε)
    (hbound : ∀ g ∈ A, ∃ C, ∀ x y : E, dist (g x) (g y) ≤ C)
    (heq : ∀ g ∈ A, ∫ x, (g : E → ℝ) x ∂P = ∫ x, (g : E → ℝ) x ∂P') {g : C(E, ℝ)} (hgA : g ∈ A) :
    ∫ x, mulExpNegMulSq ε (g x) ∂P = ∫ x, mulExpNegMulSq ε (g x) ∂P'

Proof state:
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
n : ℕ
⊢ 1 + (↑n)⁻¹ • -(ε • g * g) ∈ A

Tactic:
apply Subalgebra.add_mem A (Subalgebra.one_mem A) (Subalgebra.smul_mem A _ n⁻¹)

Result:
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
n : ℕ
⊢ -(ε • g * g) ∈ A

Proof state:
case intro
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
one_plus_inv_mul_mem : ∀ (n : ℕ), g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n ∈ A
⊢ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P = ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'

Tactic:
have limP : Tendsto (fun n : ℕ => ∫ x, (g * (1 + (n : ℝ)⁻¹ • -(ε • g * g)) ^ n) x ∂P) atTop
    (𝓝 (∫ x, mulExpNegMulSq ε (g x) ∂P')) := by
  rw [funext fun n => heq _ (one_plus_inv_mul_mem n)]
  exact tendsto_integral_mul_one_plus_inv_smul_sq_pow (mkOfBound g C h) hε

Result:
case intro
E : Type u_1
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
P : Measure E
inst✝¹ : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ C(E, ℝ)
hε : 0 < ε
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : C(E, ℝ)
hgA : g ∈ A
C : ℝ
h : ∀ (x y : E), dist (g x) (g y) ≤ C
one_plus_inv_mul_mem : ∀ (n : ℕ), g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n ∈ A
limP :
  Tendsto (fun n => ∫ (x : E), (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x ∂P) atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'))
⊢ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P = ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem functorPushforward_id (R : Sieve X) : R.functorPushforward (𝟭 _) = R

Proof state:
case h.mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ R.arrows f → (functorPushforward (𝟭 C) R).arrows f

Tactic:
intro hf

Result:
case h.mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
hf : R.arrows f
⊢ (functorPushforward (𝟭 C) R).arrows f

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ (functorPushforward (𝟭 C) R).arrows f ↔ R.arrows f

Tactic:
constructor

Result:
case h.mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ (functorPushforward (𝟭 C) R).arrows f → R.arrows f

case h.mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ R.arrows f → (functorPushforward (𝟭 C) R).arrows f

Proof state:
case h.mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
hf : R.arrows f
⊢ (functorPushforward (𝟭 C) R).arrows f

Tactic:
exact ⟨X, f, 𝟙 _, hf, by simp⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
hf : R.arrows f
⊢ f = 𝟙 X ≫ (𝟭 C).map f

Tactic:
simp

Result:
no goals

Proof state:
case h.mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
hf : (functorPushforward (𝟭 C) R).arrows f
⊢ R.arrows f

Tactic:
obtain ⟨X, g, h, hg, rfl⟩ := hf

Result:
case h.mp.intro.intro.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝¹ : C
R : Sieve X✝¹
X✝ X : C
g : X ⟶ X✝¹
h : X✝ ⟶ (𝟭 C).obj X
hg : R.arrows g
⊢ R.arrows (h ≫ (𝟭 C).map g)

Proof state:
case h.mp.intro.intro.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝¹ : C
R : Sieve X✝¹
X✝ X : C
g : X ⟶ X✝¹
h : X✝ ⟶ (𝟭 C).obj X
hg : R.arrows g
⊢ R.arrows (h ≫ (𝟭 C).map g)

Tactic:
exact R.downward_closed hg h

Result:
no goals

Proof state:
case h.mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ (functorPushforward (𝟭 C) R).arrows f → R.arrows f

Tactic:
intro hf

Result:
case h.mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
hf : (functorPushforward (𝟭 C) R).arrows f
⊢ R.arrows f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Sieve X
⊢ functorPushforward (𝟭 C) R = R

Tactic:
ext X f

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ (functorPushforward (𝟭 C) R).arrows f ↔ R.arrows f
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem Int.ModEq.pow_card_sub_one_eq_one {p : ℕ} (hp : Nat.Prime p) {n : ℤ} (hpn : IsCoprime n p) :
    n ^ (p - 1) ≡ 1 [ZMOD p]

Proof state:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
⊢ n ^ (p - 1) ≡ 1 [ZMOD ↑p]

Tactic:
haveI : Fact p.Prime := ⟨hp⟩

Result:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ n ^ (p - 1) ≡ 1 [ZMOD ↑p]

Proof state:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ IsCoprime (↑p) n

Tactic:
exact hpn.symm

Result:
no goals

Proof state:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ ¬↑n = 0

Tactic:
rw [CharP.intCast_eq_zero_iff _ p, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd]

Result:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ IsCoprime (↑p) n

Proof state:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1) ≡ 1 [ZMOD ↑p]

Tactic:
simpa [← ZMod.intCast_eq_intCast_iff] using ZMod.pow_card_sub_one_eq_one this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_map_hom (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : Vector α n)
    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
    (l.map g).foldl f' (g a) = g (l.foldl f a)

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
l : Array α
⊢ Array.foldl f' (g a) (Array.map g l) 0 l.size = g (Array.foldl f a l)

Tactic:
rw [Array.foldl_map_hom' _ _ _ _ _ h rfl]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : Vector α n
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
⊢ foldl f' (g a) (map g l) = g (foldl f a l)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
l : Array α
⊢ foldl f' (g a) (map g { toArray := l, size_toArray := ⋯ }) = g (foldl f a { toArray := l, size_toArray := ⋯ })

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
l : Array α
⊢ foldl f' (g a) (map g { toArray := l, size_toArray := ⋯ }) = g (foldl f a { toArray := l, size_toArray := ⋯ })

Tactic:
simp

Result:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
l : Array α
⊢ Array.foldl f' (g a) (Array.map g l) 0 l.size = g (Array.foldl f a l)
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
protected lemma Connected.preconnected {H : G.Subgraph} (h : H.Connected) : H.Preconnected

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.Preconnected

Tactic:
exact h.1

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ H.Preconnected

Tactic:
rw [H.connected_iff] at h

Result:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.Preconnected
-- Mathlib/Data/Set/Function.lean
theorem range_piecewise (f g : α → β) : range (s.piecewise f g) = f '' s ∪ g '' sᶜ

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ range (s.piecewise f g) = f '' s ∪ g '' sᶜ

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (s.piecewise f g) ↔ y ∈ f '' s ∪ g '' sᶜ

Proof state:
case h.mp.intro
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
⊢ s.piecewise f g x ∈ f '' s ∪ g '' sᶜ

Tactic:
by_cases h : x ∈ s <;> [left; right] <;> use x <;> simp [h]

Result:
no goals

Proof state:
case h.mp
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (s.piecewise f g) → y ∈ f '' s ∪ g '' sᶜ

Tactic:
rintro ⟨x, rfl⟩

Result:
case h.mp.intro
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
⊢ s.piecewise f g x ∈ f '' s ∪ g '' sᶜ

Proof state:
case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (s.piecewise f g) ↔ y ∈ f '' s ∪ g '' sᶜ

Tactic:
constructor

Result:
case h.mp
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (s.piecewise f g) → y ∈ f '' s ∪ g '' sᶜ

case h.mpr
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ f '' s ∪ g '' sᶜ → y ∈ range (s.piecewise f g)

Proof state:
case h.mpr
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ f '' s ∪ g '' sᶜ → y ∈ range (s.piecewise f g)

Tactic:
rintro (⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩) <;> use x <;> simp_all

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem moebius_apply_isPrimePow_not_prime {n : ℕ} (hn : IsPrimePow n) (hn' : ¬n.Prime) :
    μ n = 0

Proof state:
p : ℕ
hp : Nat.Prime p
hk : 0 < 1
hn : IsPrimePow (p ^ 1)
hn' : ¬Nat.Prime (p ^ 1)
⊢ Nat.Prime (p ^ 1)

Tactic:
simpa

Result:
no goals

Proof state:
n : ℕ
hn : IsPrimePow n
hn' : ¬Nat.Prime n
⊢ μ n = 0

Tactic:
obtain ⟨p, k, hp, hk, rfl⟩ := (isPrimePow_nat_iff _).1 hn

Result:
case intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ μ (p ^ k) = 0

Proof state:
case intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ μ (p ^ k) = 0

Tactic:
rw [moebius_apply_prime_pow hp hk.ne', if_neg]

Result:
case intro.intro.intro.intro.hnc
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ ¬k = 1

Proof state:
case intro.intro.intro.intro.hnc
p : ℕ
hp : Nat.Prime p
hk : 0 < 1
hn : IsPrimePow (p ^ 1)
hn' : ¬Nat.Prime (p ^ 1)
⊢ False

Tactic:
exact hn' (by simpa)

Result:
no goals

Proof state:
case intro.intro.intro.intro.hnc
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ ¬k = 1

Tactic:
rintro rfl

Result:
case intro.intro.intro.intro.hnc
p : ℕ
hp : Nat.Prime p
hk : 0 < 1
hn : IsPrimePow (p ^ 1)
hn' : ¬Nat.Prime (p ^ 1)
⊢ False
-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma llr_tilted_left [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν)
    (hf : Integrable (fun x ↦ exp (f x)) μ) (hfν : AEMeasurable f ν) :
    (llr (μ.tilted f) ν) =ᵐ[μ] fun x ↦ f x - log (∫ z, exp (f z) ∂μ) + llr μ ν x

Proof state:
case h.hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ⊤
⊢ rexp (f x) ≠ 0 ∧ ∫ (x : α), rexp (f x) ∂μ ≠ 0

Tactic:
exact ⟨(exp_pos _).ne', (integral_exp_pos hf).ne'⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
lemma of_iSup_eq_top {ι} (U : ι → X.Opens) (hU : iSup U = ⊤)
    (H : ∀ i, P ((U i).ι ≫ f)) : P f

Proof state:
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
i : (X.openCoverOfISupEqTop Subtype.val ⋯).J
⊢ P ((X.openCoverOfISupEqTop Subtype.val ⋯).map i ≫ f)

Tactic:
obtain ⟨_, i, rfl⟩ := i

Result:
case mk.intro
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
i : ι
⊢ P ((X.openCoverOfISupEqTop Subtype.val ⋯).map ⟨U i, ⋯⟩ ≫ f)

Proof state:
case h.h
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑(⨆ i, ↑i) ↔ x✝ ∈ ↑⊤

Tactic:
simp [← hU]

Result:
no goals

Proof state:
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
⊢ P f

Tactic:
refine (iff_of_openCover' f
  (X.openCoverOfISupEqTop (s := Set.range U) Subtype.val (by ext; simp [← hU]))).mpr fun i ↦ ?_

Result:
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
i : (X.openCoverOfISupEqTop Subtype.val ⋯).J
⊢ P ((X.openCoverOfISupEqTop Subtype.val ⋯).map i ≫ f)

Proof state:
case mk.intro
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
i : ι
⊢ P ((X.openCoverOfISupEqTop Subtype.val ⋯).map ⟨U i, ⋯⟩ ≫ f)

Tactic:
exact H i

Result:
no goals

Proof state:
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
⊢ ⨆ i, ↑i = ⊤

Tactic:
ext

Result:
case h.h
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → X.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P ((U i).ι ≫ f)
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ↑(⨆ i, ↑i) ↔ x✝ ∈ ↑⊤
-- Mathlib/Data/Multiset/Lattice.lean
theorem inf_ndinsert (a : α) (s : Multiset α) : (ndinsert a s).inf = a ⊓ s.inf

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).inf = a ⊓ s.inf

Tactic:
rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_cons]

Result:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
/-- If two vectors `x` and `y` are linearly independent, so are their linear combinations
`a x + b y` and `c x + d y` provided the determinant `a * d - b * c` is nonzero. -/
lemma LinearIndependent.linear_combination_pair_of_det_ne_zero {R M : Type*} [CommRing R]
    [NoZeroDivisors R] [AddCommGroup M] [Module R M]
    {x y : M} (h : LinearIndependent R ![x, y])
    {a b c d : R} (h' : a * d - b * c ≠ 0) :
    LinearIndependent R ![a • x + b • y, c • x + d • y]

Proof state:
R : Type u_6
M : Type u_7
inst✝³ : CommRing R
inst✝² : NoZeroDivisors R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
a b c d : R
h' : a * d - b * c ≠ 0
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
H : (s * a + t * c) • x + (s * b + t * d) • y = 0
I1 : s * a + t * c = 0
I2 : s * b + t * d = 0
⊢ (a * d - b * c) * s = 0

Tactic:
linear_combination d * I1 - c * I2

Result:
no goals

Proof state:
R : Type u_6
M : Type u_7
inst✝³ : CommRing R
inst✝² : NoZeroDivisors R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
a b c d : R
h' : a * d - b * c ≠ 0
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
H : (s * a + t * c) • x + (s * b + t * d) • y = 0
I1 : s * a + t * c = 0
I2 : s * b + t * d = 0
J1 : (a * d - b * c) * s = 0
J2 : (a * d - b * c) * t = 0
⊢ s = 0 ∧ t = 0

Tactic:
exact ⟨by simpa [h'] using mul_eq_zero.1 J1, by simpa [h'] using mul_eq_zero.1 J2⟩

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/FloorPow.lean
theorem sum_div_pow_sq_le_div_sq (N : ℕ) {j : ℝ} (hj : 0 < j) {c : ℝ} (hc : 1 < c) :
    (∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (c ^ i) ^ 2) ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2

Proof state:
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ 0 < 1 / j ^ 2

Tactic:
positivity

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem prod_image_image_eq {m₁ : α → γ} {m₂ : β → δ} :
    (m₁ '' s) ×ˢ (m₂ '' t) = (fun p : α × β => (m₁ p.1, m₂ p.2)) '' s ×ˢ t :=
  ext <| by
    simp [-exists_and_right, exists_and_right.symm, and_left_comm, and_assoc, and_comm]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
m₁ : α → γ
m₂ : β → δ
⊢ ∀ (x : γ × δ), x ∈ (m₁ '' s) ×ˢ (m₂ '' t) ↔ x ∈ (fun p => (m₁ p.1, m₂ p.2)) '' s ×ˢ t

Tactic:
simp [-exists_and_right, exists_and_right.symm, and_left_comm, and_assoc, and_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem map_empty_eq_zero {β} [AddCancelMonoid β] {T : Set α → β} (hT : FinMeasAdditive μ T) :
    T ∅ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : AddCancelMonoid β
T : Set α → β
h_empty : μ ∅ ≠ ⊤
hT : T ∅ = T ∅ + T ∅
⊢ T ∅ = 0

Tactic:
nth_rw 1 [← add_zero (T ∅)] at hT

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : AddCancelMonoid β
T : Set α → β
h_empty : μ ∅ ≠ ⊤
hT : T ∅ + 0 = T ∅ + T ∅
⊢ T ∅ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : AddCancelMonoid β
T : Set α → β
hT : FinMeasAdditive μ T
⊢ T ∅ = 0

Tactic:
have h_empty : μ ∅ ≠ ∞ := (measure_empty.le.trans_lt ENNReal.coe_lt_top).ne

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : AddCancelMonoid β
T : Set α → β
hT : FinMeasAdditive μ T
h_empty : μ ∅ ≠ ⊤
⊢ T ∅ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : AddCancelMonoid β
T : Set α → β
hT : FinMeasAdditive μ T
h_empty : μ ∅ ≠ ⊤
⊢ T ∅ = 0

Tactic:
specialize hT ∅ ∅ MeasurableSet.empty MeasurableSet.empty h_empty h_empty (disjoint_empty _)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : AddCancelMonoid β
T : Set α → β
h_empty : μ ∅ ≠ ⊤
hT : T (∅ ∪ ∅) = T ∅ + T ∅
⊢ T ∅ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : AddCancelMonoid β
T : Set α → β
h_empty : μ ∅ ≠ ⊤
hT : T ∅ + 0 = T ∅ + T ∅
⊢ T ∅ = 0

Tactic:
exact (add_left_cancel hT).symm

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : AddCancelMonoid β
T : Set α → β
h_empty : μ ∅ ≠ ⊤
hT : T (∅ ∪ ∅) = T ∅ + T ∅
⊢ T ∅ = 0

Tactic:
rw [Set.union_empty] at hT

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : AddCancelMonoid β
T : Set α → β
h_empty : μ ∅ ≠ ⊤
hT : T ∅ = T ∅ + T ∅
⊢ T ∅ = 0
-- Mathlib/Algebra/Group/Int/Even.lean
@[parity_simps]
lemma even_sub : Even (m - n) ↔ (Even m ↔ Even n)

Proof state:
m n : ℤ
⊢ Even (m - n) ↔ (Even m ↔ Even n)

Tactic:
simp [sub_eq_add_neg, parity_simps]

Result:
no goals