harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive (attr := simp)] lemma mulEnergy_empty_right : Eₘ[s, ∅] = 0

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s : Finset α
⊢ Eₘ[s, ∅] = 0

Tactic:
simp [mulEnergy]

Result:
no goals
-- Mathlib/Data/Int/Interval.lean
theorem card_Ioc_of_le (h : a ≤ b) : (#(Ioc a b) : ℤ) = b - a

Proof state:
a b : ℤ
h : a ≤ b
⊢ ↑(#(Ioc a b)) = b - a

Tactic:
rw [card_Ioc, toNat_sub_of_le h]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
lemma hurwitzZetaOdd_eq (a : UnitAddCircle) (s : ℂ) :
    hurwitzZetaOdd a s = (hurwitzZeta a s - hurwitzZeta (-a) s) / 2

Proof state:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaOdd a s = (hurwitzZeta a s - hurwitzZeta (-a) s) / 2

Tactic:
simp only [hurwitzZeta, hurwitzZetaEven_neg, hurwitzZetaOdd_neg]

Result:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaOdd a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s - (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2

Proof state:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaOdd a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s - (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2

Tactic:
ring_nf

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem integralSum_biUnionTagged (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (π : Prepartition I)
    (πi : ∀ J, TaggedPrepartition J) :
    integralSum f vol (π.biUnionTagged πi) = ∑ J ∈ π.boxes, integralSum f vol (πi J)

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ integralSum f vol (π.biUnionTagged πi) = ∑ J ∈ π.boxes, integralSum f vol (πi J)

Tactic:
refine (π.sum_biUnion_boxes _ _).trans <| sum_congr rfl fun J hJ => sum_congr rfl fun J' hJ' => ?_

Result:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
J : Box ι
hJ : J ∈ π.boxes
J' : Box ι
hJ' : J' ∈ (πi J).boxes
⊢ (vol J') (f ((π.biUnionTagged πi).tag J')) = (vol J') (f ((πi J).tag J'))

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
J : Box ι
hJ : J ∈ π.boxes
J' : Box ι
hJ' : J' ∈ (πi J).boxes
⊢ (vol J') (f ((π.biUnionTagged πi).tag J')) = (vol J') (f ((πi J).tag J'))

Tactic:
rw [π.tag_biUnionTagged hJ hJ']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_insertListConst_of_mem [BEq α] [EquivBEq α] [Inhabited α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ toInsert.map Prod.fst) :
    getKey! k' (insertListConst l toInsert) = k

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : k ∈ List.map Prod.fst toInsert
⊢ getKey! k' (insertListConst l toInsert) = k

Tactic:
rw [getKey!_eq_getKey?, getKey?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem,
  Option.get!_some]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem isOpen_iff_of_not_mem (h : ∞ ∉ s) : IsOpen s ↔ IsOpen ((↑) ⁻¹' s : Set X)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∉ s
⊢ IsOpen s ↔ IsOpen (some ⁻¹' s)

Tactic:
simp [isOpen_def, h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_diff_le_iff_le_add (hs : NullMeasurableSet s μ) (hst : s ⊆ t) (hs' : μ s ≠ ∞)
    {ε : ℝ≥0∞} : μ (t \ s) ≤ ε ↔ μ t ≤ μ s + ε

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : μ s ≠ ⊤
ε : ℝ≥0∞
⊢ μ (t \ s) ≤ ε ↔ μ t ≤ μ s + ε

Tactic:
rw [measure_diff hst hs hs', tsub_le_iff_left]

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem totient_eq_zero : ∀ {n : ℕ}, φ n = 0 ↔ n = 0
  | 0 => by decide
  | n + 1 =>
    suffices ∃ x < n + 1, (n + 1).gcd x = 1 by simpa [totient, filter_eq_empty_iff]
    ⟨1 % (n + 1), mod_lt _ n.succ_pos, by rw [gcd_comm, ← gcd_rec, gcd_one_right]⟩

Proof state:
n : ℕ
⊢ (n + 1).gcd (1 % (n + 1)) = 1

Tactic:
rw [gcd_comm, ← gcd_rec, gcd_one_right]

Result:
no goals

Proof state:
n : ℕ
this : ∃ x < n + 1, (n + 1).gcd x = 1
⊢ φ (n + 1) = 0 ↔ n + 1 = 0

Tactic:
simpa [totient, filter_eq_empty_iff]

Result:
no goals

Proof state:
⊢ φ 0 = 0 ↔ 0 = 0

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem primeFactorsList_add_two (n : ℕ) :
    primeFactorsList (n + 2) = minFac (n + 2) :: primeFactorsList ((n + 2) / minFac (n + 2))

Proof state:
n : ℕ
⊢ (n + 2).primeFactorsList = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList

Tactic:
rw [primeFactorsList]

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ |X ω| ^ p` is
integrable for all nonnegative `p : ℝ`. -/
lemma integrable_rpow_abs_of_integrable_exp_mul (ht : t ≠ 0)
    (ht_int_pos : Integrable (fun ω ↦ exp (t * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp (- t * X ω)) μ) {p : ℝ} (hp : 0 ≤ p) :
    Integrable (fun ω ↦ |X ω| ^ p) μ

Proof state:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
h : Integrable (fun ω => |X ω| ^ p * rexp (0 * X ω)) μ
⊢ Integrable (fun ω => |X ω| ^ p) μ

Tactic:
simpa using h

Result:
no goals

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => rexp ((0 - t) * X ω)) μ

Tactic:
simpa using ht_int_neg

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => |X ω| ^ p) μ

Tactic:
have h := integrable_rpow_abs_mul_exp_of_integrable_exp_mul (μ := μ) (X := X) ht (v := 0) ?_ ?_ hp

Result:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
h : Integrable (fun ω => |X ω| ^ p * rexp (0 * X ω)) μ
⊢ Integrable (fun ω => |X ω| ^ p) μ

case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => rexp ((0 + t) * X ω)) μ

case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => rexp ((0 - t) * X ω)) μ

Proof state:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => rexp ((0 + t) * X ω)) μ

Tactic:
simpa using ht_int_pos

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_zsmul_eq_iff {ψ θ : Angle} : (2 : ℤ) • ψ = (2 : ℤ) • θ ↔ ψ = θ ∨ ψ = θ + ↑π

Proof state:
ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π

Tactic:
rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
  Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
  mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]

Result:
no goals

Proof state:
ψ θ : Angle
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π

Tactic:
have : Int.natAbs 2 = 2 := rfl

Result:
ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
-- Mathlib/Data/Set/Functor.lean
theorem image_val_subset : (γ : Set α) ⊆ β

Proof state:
α : Type u
β : Set α
γ : Set ↑β
⊢ Subtype.val '' γ ⊆ β

Tactic:
rintro _ ⟨⟨_, ha⟩, _, rfl⟩

Result:
case intro.mk.intro
α : Type u
β : Set α
γ : Set ↑β
val✝ : α
ha : val✝ ∈ β
left✝ : ⟨val✝, ha⟩ ∈ γ
⊢ ↑⟨val✝, ha⟩ ∈ β

Proof state:
case intro.mk.intro
α : Type u
β : Set α
γ : Set ↑β
val✝ : α
ha : val✝ ∈ β
left✝ : ⟨val✝, ha⟩ ∈ γ
⊢ ↑⟨val✝, ha⟩ ∈ β

Tactic:
exact ha

Result:
no goals
-- Mathlib/MeasureTheory/Group/Pointwise.lean
theorem MeasurableSet.const_smul_of_ne_zero {G₀ α : Type*} [GroupWithZero G₀] [MulAction G₀ α]
    [MeasurableSpace G₀] [MeasurableSpace α] [MeasurableSMul G₀ α] {s : Set α}
    (hs : MeasurableSet s) {a : G₀} (ha : a ≠ 0) : MeasurableSet (a • s)

Proof state:
G₀ : Type u_1
α : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulAction G₀ α
inst✝² : MeasurableSpace G₀
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G₀ α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (a • s)

Tactic:
rw [← preimage_smul_inv₀ ha]

Result:
G₀ : Type u_1
α : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulAction G₀ α
inst✝² : MeasurableSpace G₀
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G₀ α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet ((fun x => a⁻¹ • x) ⁻¹' s)

Proof state:
G₀ : Type u_1
α : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulAction G₀ α
inst✝² : MeasurableSpace G₀
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSMul G₀ α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet ((fun x => a⁻¹ • x) ⁻¹' s)

Tactic:
exact measurable_const_smul _ hs

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem sInf_image2 {f : β → γ → α} {s : Set β} {t : Set γ} :
    sInf (image2 f s t) = ⨅ (a ∈ s) (b ∈ t), f a b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β → γ → α
s : Set β
t : Set γ
⊢ sInf (image2 f s t) = ⨅ a ∈ s, ⨅ b ∈ t, f a b

Tactic:
rw [← image_prod, sInf_image, biInf_prod]

Result:
no goals
-- Mathlib/Algebra/Ring/InjSurj.lean
theorem leftDistribClass [Mul α] [Add α] [LeftDistribClass α] (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) : LeftDistribClass β where
  left_distrib := hf.forall₃.2 fun x y z => by simp only [← add, ← mul, left_distrib]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
add : ∀ (x y : α), f (x + y) = f x + f y
mul : ∀ (x y : α), f (x * y) = f x * f y
x y z : α
⊢ f x * (f y + f z) = f x * f y + f x * f z

Tactic:
simp only [← add, ← mul, left_distrib]

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem naturality {α β} (f : α → F β) (x : List α) :
    η (List.traverse f x) = List.traverse (@η _ ∘ f) x

Proof state:
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : List α
⊢ (fun {α} => η.app α) (List.traverse f x) = List.traverse ((fun {α} => η.app α) ∘ f) x

Tactic:
induction x <;> simp! [*, functor_norm, ApplicativeTransformation.preserves_map,
  ApplicativeTransformation.preserves_seq, ApplicativeTransformation.preserves_pure]

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is strictly positive, then
`f` is a strictly monotone function. -/
lemma strictMono_of_hasDerivAt_pos {f f' : ℝ → ℝ} (hf : ∀ x, HasDerivAt f (f' x) x)
    (hf' : ∀ x, 0 < f' x) : StrictMono f :=
  strictMono_of_deriv_pos fun x ↦ by rw [(hf _).deriv]; exact hf' _

Proof state:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), 0 < f' x
x : ℝ
⊢ 0 < deriv f x

Tactic:
rw [(hf _).deriv]

Result:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), 0 < f' x
x : ℝ
⊢ 0 < f' x

Proof state:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), 0 < f' x
x : ℝ
⊢ 0 < f' x

Tactic:
exact hf' _

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem add_moveRight_inr (x : PGame) {y : PGame} (i) :
    (x + y).moveRight (toRightMovesAdd (Sum.inr i)) = x + y.moveRight i

Proof state:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝).moveRight (toRightMovesAdd (Sum.inr i)) =
    mk α✝¹ β✝¹ a✝³ a✝² + (mk α✝ β✝ a✝¹ a✝).moveRight i

Tactic:
rfl

Result:
no goals

Proof state:
x y : PGame
i : y.RightMoves
⊢ (x + y).moveRight (toRightMovesAdd (Sum.inr i)) = x + y.moveRight i

Tactic:
cases x

Result:
case mk
y : PGame
i : y.RightMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (mk α✝ β✝ a✝¹ a✝ + y).moveRight (toRightMovesAdd (Sum.inr i)) = mk α✝ β✝ a✝¹ a✝ + y.moveRight i

Proof state:
case mk
y : PGame
i : y.RightMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (mk α✝ β✝ a✝¹ a✝ + y).moveRight (toRightMovesAdd (Sum.inr i)) = mk α✝ β✝ a✝¹ a✝ + y.moveRight i

Tactic:
cases y

Result:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝).moveRight (toRightMovesAdd (Sum.inr i)) =
    mk α✝¹ β✝¹ a✝³ a✝² + (mk α✝ β✝ a✝¹ a✝).moveRight i
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem mem_compl : a ∈ sᶜ ↔ a ∉ s

Proof state:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∈ sᶜ ↔ a ∉ s

Tactic:
simp [compl_eq_univ_sdiff]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem volumePreserving_toMixed :
    MeasurePreserving (toMixed K) where
  measurable := (toMixed K).continuous.measurable
  map_eq

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measure.map (⇑(toMixed K)) volume = volume

Tactic:
rw [← (OrthonormalBasis.addHaar_eq_volume (euclidean.stdOrthonormalBasis K)), Basis.map_addHaar,
  stdOrthonormalBasis_map_eq, Basis.addHaar_eq_iff, Basis.coe_parallelepiped,
  ← measure_congr (ZSpan.fundamentalDomain_ae_parallelepiped (stdBasis K) volume),
  volume_fundamentalDomain_stdBasis K]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isClosedMap_inl : IsClosedMap (@inl X Y) := fun u hu ↦ by
  simpa [isClosed_sum_iff, preimage_image_eq u Sum.inl_injective]

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
u : Set X
hu : IsClosed u
⊢ IsClosed (inl '' u)

Tactic:
simpa [isClosed_sum_iff, preimage_image_eq u Sum.inl_injective]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesAt.tendsto_partialSum
    (hf : HasFPowerSeriesAt f p x) :
    ∀ᶠ y in 𝓝 0, Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
⊢ ∀ᶠ (y : E) in 𝓝 0, Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))

Tactic:
rcases hf with ⟨r, hr⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
⊢ ∀ᶠ (y : E) in 𝓝 0, Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
⊢ ∀ᶠ (y : E) in 𝓝 0, Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))

Tactic:
filter_upwards [EMetric.ball_mem_nhds (0 : E) hr.r_pos] with y hy

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
y : E
hy : y ∈ EMetric.ball 0 r
⊢ Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
y : E
hy : y ∈ EMetric.ball 0 r
⊢ Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))

Tactic:
exact hr.tendsto_partialSum hy

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_eq_of_coprime_left {p a b : ℕ} (hab : Coprime a b)
    (hpa : p ∈ a.primeFactorsList) : (a * b).factorization p = a.factorization p

Proof state:
p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
⊢ (a * b).factorization p = a.factorization p

Tactic:
rw [factorization_mul_apply_of_coprime hab, ← primeFactorsList_count_eq,
  ← primeFactorsList_count_eq,
  count_eq_zero_of_not_mem (coprime_primeFactorsList_disjoint hab hpa), add_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_sqrt {x : ℝ} (hx : 0 ≤ x) : log (√x) = log x / 2

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ 2 ≠ 0

Tactic:
exact two_ne_zero

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ log √x = log x / 2

Tactic:
rw [eq_div_iff, mul_comm, ← Nat.cast_two, ← log_pow, sq_sqrt hx]

Result:
x : ℝ
hx : 0 ≤ x
⊢ 2 ≠ 0
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_mul_right_left (H : IsCoprime x (y * z)) : IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (y * z) x
⊢ IsCoprime y x

Tactic:
exact H.of_mul_left_left

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x (y * z)
⊢ IsCoprime x y

Tactic:
rw [isCoprime_comm] at H ⊢

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (y * z) x
⊢ IsCoprime y x
-- Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
theorem IsSRGWith.card_neighborFinset_union_of_not_adj {v w : V} (h : G.IsSRGWith n k ℓ μ)
    (hne : v ≠ w) (ha : ¬G.Adj v w) :
    #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - μ

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
hne : v ≠ w
ha : ¬G.Adj v w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card ↑(G.commonNeighbors v w)

Tactic:
apply h.card_neighborFinset_union_eq

Result:
no goals

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
hne : v ≠ w
ha : ¬G.Adj v w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - μ

Tactic:
rw [← h.of_not_adj hne ha]

Result:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
v w : V
h : G.IsSRGWith n k ℓ μ
hne : v ≠ w
ha : ¬G.Adj v w
⊢ #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card ↑(G.commonNeighbors v w)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma b₂_of_char_two : W.b₂ = W.a₁ ^ 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.a₁ ^ 2 + 4 * W.a₂ = W.a₁ ^ 2

Tactic:
linear_combination 2 * W.a₂ * CharP.cast_eq_zero R 2

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.b₂ = W.a₁ ^ 2

Tactic:
rw [b₂]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.a₁ ^ 2 + 4 * W.a₂ = W.a₁ ^ 2
-- Mathlib/Algebra/Ring/Parity.lean
lemma iterate_bit1 (hf : Involutive f) (n : ℕ) : f^[2 * n + 1] = f

Proof state:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ f^[2 * n + 1] = f

Tactic:
rw [← succ_eq_add_one, iterate_succ, hf.iterate_bit0, id_comp]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem isUnit_gcd_of_eq_mul_gcd {α : Type*} [CancelCommMonoidWithZero α] [GCDMonoid α]
    {x y x' y' : α} (ex : x = gcd x y * x') (ey : y = gcd x y * y') (h : gcd x y ≠ 0) :
    IsUnit (gcd x' y')

Proof state:
case h.e'_4
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ gcd x y * 1 = gcd (gcd x y * x') (gcd x y * y')

Tactic:
rw [← ex, ← ey, mul_one]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ Associated (gcd x' y') 1

Tactic:
refine Associated.of_mul_left ?_ (Associated.refl <| gcd x y) h

Result:
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ Associated (gcd x y * gcd x' y') (gcd x y * 1)

Proof state:
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ Associated (gcd x y * gcd x' y') (gcd x y * 1)

Tactic:
convert (gcd_mul_left' (gcd x y) x' y').symm using 1

Result:
case h.e'_4
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ gcd x y * 1 = gcd (gcd x y * x') (gcd x y * y')

Proof state:
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ IsUnit (gcd x' y')

Tactic:
rw [← associated_one_iff_isUnit]

Result:
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ Associated (gcd x' y') 1
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem t2_iff_isClosed_diagonal : T2Space X ↔ IsClosed (diagonal X)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ T2Space X ↔ IsClosed (diagonal X)

Tactic:
simp only [t2Space_iff_disjoint_nhds, ← isOpen_compl_iff, isOpen_iff_mem_nhds, Prod.forall,
  nhds_prod_eq, compl_diagonal_mem_prod, mem_compl_iff, mem_diagonal_iff, Pairwise]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_count' {f : α → ℝ≥0∞} (hf : Measurable f) : ∫⁻ a, f a ∂count = ∑' a, f a

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂count = ∑' (a : α), f a

Tactic:
rw [count, lintegral_sum_measure]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∑' (i : α), ∫⁻ (a : α), f a ∂dirac i = ∑' (a : α), f a

Proof state:
case e_f
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun i => ∫⁻ (a : α), f a ∂dirac i) = fun a => f a

Tactic:
exact funext fun a => lintegral_dirac' a hf

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∑' (i : α), ∫⁻ (a : α), f a ∂dirac i = ∑' (a : α), f a

Tactic:
congr

Result:
case e_f
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun i => ∫⁻ (a : α), f a ∂dirac i) = fun a => f a