harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/RingedSpace/Basic.lean
theorem basicOpen_of_isUnit {U : Opens X} {f : X.presheaf.obj (op U)} (hf : IsUnit f) :
    X.basicOpen f = U

Proof state:
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ X.basicOpen f ≤ U

Tactic:
exact X.basicOpen_le f

Result:
no goals

Proof state:
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ x ∈ ↑(X.basicOpen f)

Tactic:
rw [SetLike.mem_coe, X.mem_basicOpen f x hx]

Result:
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)

Proof state:
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ U ≤ X.basicOpen f

Tactic:
intro x hx

Result:
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ x ∈ ↑(X.basicOpen f)

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ X.basicOpen f = U

Tactic:
apply le_antisymm

Result:
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ X.basicOpen f ≤ U

case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ U ≤ X.basicOpen f

Proof state:
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)

Tactic:
exact RingHom.isUnit_map _ hf

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.smul [Add α] [SMul γ β] (h : Periodic f c) (a : γ) :
    Periodic (a • f) c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝¹ : Add α
inst✝ : SMul γ β
h : Periodic f c
a : γ
⊢ Periodic (a • f) c

Tactic:
simp_all

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_eq_coe {n : ℕ} :
    emultiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Proof state:
case mp.left.hk
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ↑n ≤ emultiplicity a b

Tactic:
simp [h]

Result:
no goals

Proof state:
case mp.right.hm
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ n < n + 1

Tactic:
simp

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
constructor

Result:
case mp.left
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ a ^ n ∣ b

case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ¬a ^ (n + 1) ∣ b

Proof state:
case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b → ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n

Tactic:
apply emultiplicity_eq_of_dvd_of_not_dvd

Result:
no goals

Proof state:
case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ¬a ^ (n + 1) ∣ b

Tactic:
apply not_pow_dvd_of_emultiplicity_lt

Result:
case mp.right.hm
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ emultiplicity a b < ↑(n + 1)

Proof state:
case mp.right.hm
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ emultiplicity a b < ↑(n + 1)

Tactic:
rw [h]

Result:
case mp.right.hm
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ↑n < ↑(n + 1)

Proof state:
case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ emultiplicity a b = ↑n → a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ emultiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ emultiplicity a b = ↑n → a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n

Proof state:
case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n

Tactic:
rw [and_imp]

Result:
case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b → ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n

Proof state:
case mp.right.hm
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ↑n < ↑(n + 1)

Tactic:
norm_cast

Result:
case mp.right.hm
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ n < n + 1

Proof state:
case mp.left
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ a ^ n ∣ b

Tactic:
apply pow_dvd_of_le_emultiplicity

Result:
case mp.left.hk
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ↑n ≤ emultiplicity a b
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem lift_comp_ι (i : 𝒰.J) :
    pullback.lift (pullback.snd _ _) (pullback.fst _ _ ≫ p2 𝒰 f g)
          (by rw [← pullback.condition_assoc, Category.assoc, p_comm]) ≫
        (gluing 𝒰 f g).ι i =
      (pullback.fst _ _ : pullback (p1 𝒰 f g) (𝒰.map i) ⟶ _)

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i ≫ (gluing 𝒰 f g).ι j =
    pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫
      pullback.fst (p1 𝒰 f g) (𝒰.map i)

Tactic:
rw [pullback.condition, ← Category.assoc]

Result:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
j : (Cover.pullbackCover (gluing 𝒰 f g).openCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J
⊢ (pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i) ≫ (gluing 𝒰 f g).ι j =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).openCover.map j) ≫ (gluing 𝒰 f g).openCover.map j
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_apply_succAbove (i : Fin (n + 1)) (x : α i) (p : ∀ j, α (i.succAbove j))
    (j : Fin n) : insertNth i x p (i.succAbove j) = p j

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
H₂ : i.succAbove ((i.succAbove j).pred H₁) = i.succAbove j
⊢ H₂ ▸ p ((i.succAbove j).pred H₁) = p j

Tactic:
revert H₂

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
⊢ ∀ (H₂ : i.succAbove ((i.succAbove j).pred H₁) = i.succAbove j), H₂ ▸ p ((i.succAbove j).pred H₁) = p j
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
lemma tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint
    {X : Type*} [MeasurableSpace X] {μ : Measure X} [IsFiniteMeasure μ]
    {Es : ℕ → Set X} (Es_mble : ∀ i, NullMeasurableSet (Es i) μ)
    (Es_disj : Pairwise fun n m ↦ Disjoint (Es n) (Es m)) :
    Tendsto (μ ∘ fun n ↦ ⋃ i ≥ n, Es i) atTop (𝓝 0)

Proof state:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
nothing : ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i = ∅
⊢ Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)

Tactic:
have key := tendsto_measure_iInter_atTop (μ := μ) (fun n ↦ by measurability)
  decr ⟨0, measure_ne_top _ _⟩

Result:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
nothing : ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i = ∅
key : Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 (μ (⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i)))
⊢ Tendsto (⇑μ ∘ fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)

Proof state:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : x ∈ ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i
⊢ x ∈ ∅

Tactic:
simp only [mem_iInter, mem_iUnion, exists_prop] at hx

Result:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
⊢ x ∈ ∅

Proof state:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
⊢ ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i = ∅

Tactic:
apply subset_antisymm _ (empty_subset _)

Result:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m => Disjoint (Es n) (Es m)
decr : Antitone fun n => ⋃ i, ⋃ (_ : i ≥ n), Es i
⊢ ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i ⊆ ∅
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem isComplete_aeStronglyMeasurable' [hp : Fact (1 ≤ p)] [CompleteSpace F] (hm : m ≤ m0) :
    IsComplete {f : Lp F p μ | AEStronglyMeasurable[m] f μ}

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace F
hm : m ≤ m0
⊢ CompleteSpace ↑{f | AEStronglyMeasurable (↑↑f) μ}

Tactic:
haveI : Fact (m ≤ m0) := ⟨hm⟩

Result:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace F
hm : m ≤ m0
this : Fact (m ≤ m0)
⊢ CompleteSpace ↑{f | AEStronglyMeasurable (↑↑f) μ}

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace F
hm : m ≤ m0
this : Fact (m ≤ m0)
⊢ CompleteSpace ↥(lpMeasSubgroup F m p μ)

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace F
hm : m ≤ m0
this : Fact (m ≤ m0)
⊢ CompleteSpace ↑{f | AEStronglyMeasurable (↑↑f) μ}

Tactic:
change CompleteSpace (lpMeasSubgroup F m p μ)

Result:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace F
hm : m ≤ m0
this : Fact (m ≤ m0)
⊢ CompleteSpace ↥(lpMeasSubgroup F m p μ)

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace F
hm : m ≤ m0
⊢ IsComplete {f | AEStronglyMeasurable (↑↑f) μ}

Tactic:
rw [← completeSpace_coe_iff_isComplete]

Result:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace F
hm : m ≤ m0
⊢ CompleteSpace ↑{f | AEStronglyMeasurable (↑↑f) μ}
-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
theorem asIdeal_matricesOver [DecidableEq n] (I : TwoSidedIdeal R) :
    asIdeal (I.matricesOver n) = (asIdeal I).matricesOver n

Proof state:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ asIdeal (matricesOver n I) = Ideal.matricesOver n (asIdeal I)

Tactic:
ext

Result:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
x✝ : Matrix n n R
⊢ x✝ ∈ asIdeal (matricesOver n I) ↔ x✝ ∈ Ideal.matricesOver n (asIdeal I)

Proof state:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
x✝ : Matrix n n R
⊢ x✝ ∈ asIdeal (matricesOver n I) ↔ x✝ ∈ Ideal.matricesOver n (asIdeal I)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem disjoint_ker' {p : Submodule R M} :
    Disjoint p (ker f) ↔ ∀ x ∈ p, ∀ y ∈ p, f x = f y → x = y :=
  disjoint_ker.trans
    ⟨fun H x hx y hy h => eq_of_sub_eq_zero <| H _ (sub_mem hx hy) (by simp [h]),
     fun H x h₁ h₂ => H x h₁ 0 (zero_mem _) (by simpa using h₂)⟩

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Ring R
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_11
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
H : ∀ x ∈ p, f x = 0 → x = 0
x : M
hx : x ∈ p
y : M
hy : y ∈ p
h : f x = f y
⊢ f (x - y) = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Ring R
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_11
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R M
H : ∀ x ∈ p, ∀ y ∈ p, f x = f y → x = y
x : M
h₁ : x ∈ p
h₂ : f x = 0
⊢ f x = f 0

Tactic:
simpa using h₂

Result:
no goals
-- Mathlib/Probability/Distributions/Poisson.lean
lemma poissonPMFRealSum (r : ℝ≥0) : HasSum (fun n ↦ poissonPMFReal r n) 1

Proof state:
r✝ : ℝ≥0
r : ℝ := ↑r✝
this : (fun i => rexp r * (rexp (-r) * r ^ i / ↑i !)) = fun i => r ^ i / ↑i !
⊢ HasSum (fun i => rexp r * (rexp (-↑r✝) * ↑r✝ ^ i / ↑i !)) (rexp r)

Tactic:
rw [this, exp_eq_exp_ℝ]

Result:
r✝ : ℝ≥0
r : ℝ := ↑r✝
this : (fun i => rexp r * (rexp (-r) * r ^ i / ↑i !)) = fun i => r ^ i / ↑i !
⊢ HasSum (fun i => r ^ i / ↑i !) (NormedSpace.exp ℝ r)

Proof state:
r✝ : ℝ≥0
r : ℝ := ↑r✝
⊢ HasSum (fun i => rexp r * (rexp (-↑r✝) * ↑r✝ ^ i / ↑i !)) (rexp r * 1)

Tactic:
simp only [mul_one]

Result:
r✝ : ℝ≥0
r : ℝ := ↑r✝
⊢ HasSum (fun i => rexp r * (rexp (-↑r✝) * ↑r✝ ^ i / ↑i !)) (rexp r)

Proof state:
r✝ : ℝ≥0
r : ℝ := ↑r✝
⊢ HasSum (fun i => rexp r * (rexp (-↑r✝) * ↑r✝ ^ i / ↑i !)) (rexp r)

Tactic:
have : (fun i ↦ rexp r * (rexp (-r) * r ^ i / ↑(Nat.factorial i))) =
    fun i ↦ r ^ i / ↑(Nat.factorial i) := by
  ext n
  rw [mul_div_assoc, exp_neg, ← mul_assoc, ← div_eq_mul_inv, div_self (exp_ne_zero r), one_mul]

Result:
r✝ : ℝ≥0
r : ℝ := ↑r✝
this : (fun i => rexp r * (rexp (-r) * r ^ i / ↑i !)) = fun i => r ^ i / ↑i !
⊢ HasSum (fun i => rexp r * (rexp (-↑r✝) * ↑r✝ ^ i / ↑i !)) (rexp r)

Proof state:
r✝ : ℝ≥0
r : ℝ := ↑r✝
⊢ HasSum (fun n => rexp (-↑r✝) * ↑r✝ ^ n / ↑n !) 1

Tactic:
apply (hasSum_mul_left_iff (exp_ne_zero r)).mp

Result:
r✝ : ℝ≥0
r : ℝ := ↑r✝
⊢ HasSum (fun i => rexp r * (rexp (-↑r✝) * ↑r✝ ^ i / ↑i !)) (rexp r * 1)

Proof state:
r✝ : ℝ≥0
r : ℝ := ↑r✝
this : (fun i => rexp r * (rexp (-r) * r ^ i / ↑i !)) = fun i => r ^ i / ↑i !
⊢ HasSum (fun i => r ^ i / ↑i !) (NormedSpace.exp ℝ r)

Tactic:
exact NormedSpace.expSeries_div_hasSum_exp ℝ r

Result:
no goals

Proof state:
r✝ : ℝ≥0
r : ℝ := ↑r✝
⊢ HasSum (fun n => poissonPMFReal r✝ n) 1

Tactic:
unfold poissonPMFReal

Result:
r✝ : ℝ≥0
r : ℝ := ↑r✝
⊢ HasSum (fun n => rexp (-↑r✝) * ↑r✝ ^ n / ↑n !) 1

Proof state:
r : ℝ≥0
⊢ HasSum (fun n => poissonPMFReal r n) 1

Tactic:
let r := r.toReal

Result:
r✝ : ℝ≥0
r : ℝ := ↑r✝
⊢ HasSum (fun n => poissonPMFReal r✝ n) 1

Proof state:
case h
r✝ : ℝ≥0
r : ℝ := ↑r✝
n : ℕ
⊢ rexp r * (rexp (-r) * r ^ n / ↑n !) = r ^ n / ↑n !

Tactic:
rw [mul_div_assoc, exp_neg, ← mul_assoc, ← div_eq_mul_inv, div_self (exp_ne_zero r), one_mul]

Result:
no goals

Proof state:
r✝ : ℝ≥0
r : ℝ := ↑r✝
⊢ (fun i => rexp r * (rexp (-r) * r ^ i / ↑i !)) = fun i => r ^ i / ↑i !

Tactic:
ext n

Result:
case h
r✝ : ℝ≥0
r : ℝ := ↑r✝
n : ℕ
⊢ rexp r * (rexp (-r) * r ^ n / ↑n !) = r ^ n / ↑n !
-- Mathlib/Data/List/DropRight.lean
theorem rtakeWhile_eq_self_iff : rtakeWhile p l = l ↔ ∀ x ∈ l, p x

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
simp [rtakeWhile, reverse_eq_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem AffineMap.vectorSpan_image_eq_submodule_map {s : Set P₁} :
    Submodule.map f.linear (vectorSpan k s) = vectorSpan k (f '' s)

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
⊢ Submodule.map f.linear (vectorSpan k s) = vectorSpan k (⇑f '' s)

Tactic:
rw [vectorSpan_def, vectorSpan_def, f.image_vsub_image, Submodule.span_image]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Ultra.lean
lemma isUltrametricDist_of_forall_norm_add_one_le_max_norm_one
    (h : ∀ x : R, ‖x + 1‖ ≤ max ‖x‖ 1) : IsUltrametricDist R

Proof state:
case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ ‖x‖ ⊔ 1
x y : R
hy : y ≠ 0
p : 0 < ‖y‖
⊢ ‖x + y‖ ≤ ‖x‖ ⊔ ‖y‖

Tactic:
simpa only [div_add_one hy, norm_div, div_le_iff₀ p, max_mul_of_nonneg _ _ p.le, one_mul,
  div_mul_cancel₀ _ p.ne'] using h (x / y)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ ‖x‖ ⊔ 1
⊢ IsUltrametricDist R

Tactic:
refine isUltrametricDist_of_forall_norm_add_le_max_norm (fun x y ↦ ?_)

Result:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ ‖x‖ ⊔ 1
x y : R
⊢ ‖x + y‖ ≤ ‖x‖ ⊔ ‖y‖

Proof state:
case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ ‖x‖ ⊔ 1
x : R
⊢ ‖x + 0‖ ≤ ‖x‖ ⊔ ‖0‖

Tactic:
simpa only [add_zero] using le_max_left _ _

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ ‖x‖ ⊔ 1
x y : R
hy : y ≠ 0
⊢ ‖x + y‖ ≤ ‖x‖ ⊔ ‖y‖

Tactic:
have p : 0 < ‖y‖ := norm_pos_iff.mpr hy

Result:
case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ ‖x‖ ⊔ 1
x y : R
hy : y ≠ 0
p : 0 < ‖y‖
⊢ ‖x + y‖ ≤ ‖x‖ ⊔ ‖y‖

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ ‖x‖ ⊔ 1
x y : R
⊢ ‖x + y‖ ≤ ‖x‖ ⊔ ‖y‖

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Result:
case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ ‖x‖ ⊔ 1
x : R
⊢ ‖x + 0‖ ≤ ‖x‖ ⊔ ‖0‖

case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ ‖x‖ ⊔ 1
x y : R
hy : y ≠ 0
⊢ ‖x + y‖ ≤ ‖x‖ ⊔ ‖y‖
-- Mathlib/Order/WellFoundedSet.lean
theorem IsWF.min_union (hs : s.IsWF) (hsn : s.Nonempty) (ht : t.IsWF) (htn : t.Nonempty) :
    (hs.union ht).min (union_nonempty.2 (Or.intro_left _ hsn)) =
      Min.min (hs.min hsn) (ht.min htn)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ hs.min hsn ≤ ⋯.min ⋯ ∨ ht.min htn ≤ ⋯.min ⋯

Tactic:
exact ((mem_union _ _ _).1 ((hs.union ht).min_mem (union_nonempty.2 (.inl hsn)))).imp
  (hs.min_le _) (ht.min_le _)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ ⋯.min ⋯ = hs.min hsn ⊓ ht.min htn

Tactic:
refine le_antisymm (le_min (IsWF.min_le_min_of_subset subset_union_left)
  (IsWF.min_le_min_of_subset subset_union_right)) ?_

Result:
α : Type u_2
inst✝ : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ hs.min hsn ⊓ ht.min htn ≤ ⋯.min ⋯

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ hs.min hsn ⊓ ht.min htn ≤ ⋯.min ⋯

Tactic:
rw [min_le_iff]

Result:
α : Type u_2
inst✝ : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ hs.min hsn ≤ ⋯.min ⋯ ∨ ht.min htn ≤ ⋯.min ⋯
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem preimage_of_IdealSetMap (a : idealSet K J) :
    (preimageOfMemIntegerSet (idealSetMap K J a) : 𝓞 K) ∈ (J : Set (𝓞 K))

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
left✝ : ↑a ∈ fundamentalCone K
x : 𝓞 K
hx₁ : x ∈ ↑↑J
hx₂ : (mixedEmbedding K) ↑x = ↑a
⊢ ↑(preimageOfMemIntegerSet (idealSetMap K J a)) ∈ ↑↑J

Tactic:
simp_rw [idealSetMap, ← hx₂, preimageOfMemIntegerSet_mixedEmbedding]

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
left✝ : ↑a ∈ fundamentalCone K
x : 𝓞 K
hx₁ : x ∈ ↑↑J
hx₂ : (mixedEmbedding K) ↑x = ↑a
⊢ x ∈ ↑↑J

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
left✝ : ↑a ∈ fundamentalCone K
x : 𝓞 K
hx₁ : x ∈ ↑↑J
hx₂ : (mixedEmbedding K) ↑x = ↑a
⊢ x ∈ ↑↑J

Tactic:
exact hx₁

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
⊢ ↑(preimageOfMemIntegerSet (idealSetMap K J a)) ∈ ↑↑J

Tactic:
obtain ⟨_, ⟨x, hx₁, hx₂⟩⟩ := mem_idealSet.mp a.prop

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
left✝ : ↑a ∈ fundamentalCone K
x : 𝓞 K
hx₁ : x ∈ ↑↑J
hx₂ : (mixedEmbedding K) ↑x = ↑a
⊢ ↑(preimageOfMemIntegerSet (idealSetMap K J a)) ∈ ↑↑J
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x

Proof state:
w : Nat
x y : BitVec w
⊢ x * (y + 1#w) = x * y + x

Tactic:
simp [mul_add]

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem id_apply_one' (x : E) {n : ℕ} (h : n = 1) (v : Fin n → E) :
    (id 𝕜 E x) n v = v ⟨0, h.symm ▸ zero_lt_one⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
n : ℕ
h : n = 1
v : Fin n → E
⊢ (id 𝕜 E x n) v = v ⟨0, ⋯⟩

Tactic:
subst n

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
v : Fin 1 → E
⊢ (id 𝕜 E x 1) v = v ⟨0, ⋯⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
v : Fin 1 → E
⊢ (id 𝕜 E x 1) v = v ⟨0, ⋯⟩

Tactic:
apply id_apply_one

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_comap_subtype : map p.subtype (comap p.subtype p') = p ⊓ p' :=
  ext fun x => ⟨by rintro ⟨⟨_, h₁⟩, h₂, rfl⟩; exact ⟨h₁, h₂⟩, fun ⟨h₁, h₂⟩ => ⟨⟨_, h₁⟩, h₂, rfl⟩⟩

Proof state:
case intro.mk.intro
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
val✝ : M
h₁ : val✝ ∈ p
h₂ : ⟨val✝, h₁⟩ ∈ ↑(comap p.subtype p')
⊢ p.subtype ⟨val✝, h₁⟩ ∈ p ⊓ p'

Tactic:
exact ⟨h₁, h₂⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ x ∈ map p.subtype (comap p.subtype p') → x ∈ p ⊓ p'

Tactic:
rintro ⟨⟨_, h₁⟩, h₂, rfl⟩

Result:
case intro.mk.intro
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
val✝ : M
h₁ : val✝ ∈ p
h₂ : ⟨val✝, h₁⟩ ∈ ↑(comap p.subtype p')
⊢ p.subtype ⟨val✝, h₁⟩ ∈ p ⊓ p'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
⊢ xs.toList.length = n

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem pow_succ : I ^ (n + 1) = I * I ^ n

Proof state:
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
⊢ I ^ (n + 1) = I * I ^ n

Tactic:
rw [add_comm, IsTwoSided.pow_add, Submodule.pow_one]

Result:
no goals