harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Choose.lean
/-- `n.descFactorial k` is asymptotically equivalent to `n^k`. -/
lemma isEquivalent_descFactorial (k : ℕ) :
    (fun (n : ℕ) ↦ (n.descFactorial k : ℝ)) ~[atTop] (fun (n : ℕ) ↦ (n^k : ℝ))

Proof state:
case succ
k : ℕ
h : (fun n => ↑(n.descFactorial k)) ~[atTop] fun n => ↑n ^ k
⊢ (fun n => ↑(n - k)) ~[atTop] Nat.cast

Tactic:
have hz : ∀ᶠ (x : ℕ) in atTop, (x : ℝ) ≠ 0 :=
  eventually_atTop.mpr ⟨1, fun n hn ↦ ne_of_gt (mod_cast hn)⟩

Result:
case succ
k : ℕ
h : (fun n => ↑(n.descFactorial k)) ~[atTop] fun n => ↑n ^ k
hz : ∀ᶠ (x : ℕ) in atTop, ↑x ≠ 0
⊢ (fun n => ↑(n - k)) ~[atTop] Nat.cast

Proof state:
case zero

⊢ (fun n => ↑(n.descFactorial 0)) ~[atTop] fun n => ↑n ^ 0

Tactic:
simpa using IsEquivalent.refl

Result:
no goals

Proof state:
k : ℕ
⊢ (fun n => ↑(n.descFactorial k)) ~[atTop] fun n => ↑n ^ k

Tactic:
induction k with
| zero => simpa using IsEquivalent.refl
| succ k h =>
  simp_rw [descFactorial_succ, cast_mul, _root_.pow_succ']
  refine IsEquivalent.mul ?_ h
  have hz : ∀ᶠ (x : ℕ) in atTop, (x : ℝ) ≠ 0 :=
    eventually_atTop.mpr ⟨1, fun n hn ↦ ne_of_gt (mod_cast hn)⟩
  rw [isEquivalent_iff_tendsto_one hz, ← tendsto_add_atTop_iff_nat k]
  simpa using tendsto_natCast_div_add_atTop (k : ℝ)

Result:
no goals

Proof state:
case succ
k : ℕ
h : (fun n => ↑(n.descFactorial k)) ~[atTop] fun n => ↑n ^ k
hz : ∀ᶠ (x : ℕ) in atTop, ↑x ≠ 0
⊢ Tendsto (fun n => ((fun n => ↑(n - k)) / Nat.cast) (n + k)) atTop (𝓝 1)

Tactic:
simpa using tendsto_natCast_div_add_atTop (k : ℝ)

Result:
no goals

Proof state:
case succ
k : ℕ
h : (fun n => ↑(n.descFactorial k)) ~[atTop] fun n => ↑n ^ k
⊢ (fun n => ↑(n.descFactorial (k + 1))) ~[atTop] fun n => ↑n ^ (k + 1)

Tactic:
simp_rw [descFactorial_succ, cast_mul, _root_.pow_succ']

Result:
case succ
k : ℕ
h : (fun n => ↑(n.descFactorial k)) ~[atTop] fun n => ↑n ^ k
⊢ (fun n => ↑(n - k) * ↑(n.descFactorial k)) ~[atTop] fun n => ↑n * ↑n ^ k

Proof state:
case succ
k : ℕ
h : (fun n => ↑(n.descFactorial k)) ~[atTop] fun n => ↑n ^ k
hz : ∀ᶠ (x : ℕ) in atTop, ↑x ≠ 0
⊢ (fun n => ↑(n - k)) ~[atTop] Nat.cast

Tactic:
rw [isEquivalent_iff_tendsto_one hz, ← tendsto_add_atTop_iff_nat k]

Result:
case succ
k : ℕ
h : (fun n => ↑(n.descFactorial k)) ~[atTop] fun n => ↑n ^ k
hz : ∀ᶠ (x : ℕ) in atTop, ↑x ≠ 0
⊢ Tendsto (fun n => ((fun n => ↑(n - k)) / Nat.cast) (n + k)) atTop (𝓝 1)

Proof state:
case succ
k : ℕ
h : (fun n => ↑(n.descFactorial k)) ~[atTop] fun n => ↑n ^ k
⊢ (fun n => ↑(n - k) * ↑(n.descFactorial k)) ~[atTop] fun n => ↑n * ↑n ^ k

Tactic:
refine IsEquivalent.mul ?_ h

Result:
case succ
k : ℕ
h : (fun n => ↑(n.descFactorial k)) ~[atTop] fun n => ↑n ^ k
⊢ (fun n => ↑(n - k)) ~[atTop] Nat.cast
-- Mathlib/Probability/Density.lean
theorem hasPDF_iff_of_aemeasurable (hX : AEMeasurable X ℙ) :
    HasPDF X ℙ μ ↔ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
⊢ HasPDF X ℙ μ ↔ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ

Tactic:
rw [hasPDF_iff]

Result:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
⊢ AEMeasurable X ℙ ∧ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ ↔
    (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
⊢ AEMeasurable X ℙ ∧ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ ↔
    (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ

Tactic:
simp only [hX, true_and]

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem Finset.eq_univ_of_card [Fintype α] (s : Finset α) (hs : #s = Fintype.card α) :
    s = univ :=
  eq_of_subset_of_card_le (subset_univ _) <| by rw [hs, Finset.card_univ]

Proof state:
α : Type u_1
inst✝ : Fintype α
s : Finset α
hs : #s = Fintype.card α
⊢ #univ ≤ #s

Tactic:
rw [hs, Finset.card_univ]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_zero : (∫ _ in a..b, (0 : E) ∂μ) = 0

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
⊢ ∫ (x : ℝ) in a..b, 0 ∂μ = 0

Tactic:
simp [intervalIntegral]

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma homotopyEquivalences_le_quasiIso [CategoryWithHomology C] :
    homotopyEquivalences C c ≤ quasiIso C c

Proof state:
case intro
ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
c : ComplexShape ι
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
e : HomotopyEquiv K L
⊢ quasiIso C c e.hom

Tactic:
simp only [HomologicalComplex.mem_quasiIso_iff]

Result:
case intro
ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
c : ComplexShape ι
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
e : HomotopyEquiv K L
⊢ QuasiIso e.hom

Proof state:
ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
c : ComplexShape ι
inst✝ : CategoryWithHomology C
⊢ homotopyEquivalences C c ≤ quasiIso C c

Tactic:
rintro K L _ ⟨e, rfl⟩

Result:
case intro
ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
c : ComplexShape ι
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
e : HomotopyEquiv K L
⊢ quasiIso C c e.hom

Proof state:
case intro
ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
c : ComplexShape ι
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
e : HomotopyEquiv K L
⊢ QuasiIso e.hom

Tactic:
infer_instance

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem Subtype.volume_univ (hu : NullMeasurableSet u) : volume (univ : Set u) = volume u

Proof state:
δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ volume (Subtype.val '' univ) = volume u

Tactic:
congr

Result:
case h.e_6.h
δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ Subtype.val '' univ = u

Proof state:
δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ Injective Subtype.val

Tactic:
exact Subtype.coe_injective

Result:
no goals

Proof state:
case h.e_6.h
δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ Subtype.val '' univ = u

Tactic:
simp only [image_univ, Subtype.range_coe_subtype, setOf_mem_eq]

Result:
no goals

Proof state:
δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ ∀ (s : Set { x // x ∈ u }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume

Tactic:
exact fun t => MeasurableSet.nullMeasurableSet_subtype_coe hu

Result:
no goals

Proof state:
δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ volume univ = volume u

Tactic:
rw [Subtype.volume_def, comap_apply₀ _ _ _ _ MeasurableSet.univ.nullMeasurableSet]

Result:
δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ volume (Subtype.val '' univ) = volume u

δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ Injective Subtype.val

δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ ∀ (s : Set { x // x ∈ u }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume
-- Mathlib/Order/Category/Preord.lean
lemma id_apply (X : Preord) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : Preord
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_add_bdiv (x : Int) (m : Nat) : bmod x m + m * bdiv x m = x

Proof state:
x : Int
m : Nat
⊢ x.bmod m + ↑m * x.bdiv m = x

Tactic:
rw [Int.add_comm]

Result:
x : Int
m : Nat
⊢ ↑m * x.bdiv m + x.bmod m = x

Proof state:
x : Int
m : Nat
⊢ ↑m * x.bdiv m + x.bmod m = x

Tactic:
exact bdiv_add_bmod x m

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem ofUnitHom_coe (f : Rˣ →* R'ˣ) (a : Rˣ) : ofUnitHom f ↑a = f a

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
a : Rˣ
⊢ (ofUnitHom f) ↑a = ↑(f a)

Tactic:
simp [ofUnitHom]

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem form_perm_zpow_apply_mem_imp_mem (l : List α) (x : α) (hx : x ∈ l) (n : ℤ) :
    (formPerm l ^ n) x ∈ l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
by_cases h : (l.formPerm ^ n) x = x

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : (l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l

case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬(l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬(l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
have h : x ∈ { x | (l.formPerm ^ n) x ≠ x } := h

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : x ∈ {x | (l.formPerm ^ n) x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : x ∈ {x | (l.formPerm ^ n) x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
rw [← set_support_apply_mem] at h

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : (l.formPerm ^ n) x ∈ {x | (l.formPerm ^ n) x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : (l.formPerm ^ n) x ∈ {x | l.formPerm x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
simpa using support_formPerm_le' _ h

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : (l.formPerm ^ n) x ∈ {x | (l.formPerm ^ n) x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
replace h := set_support_zpow_subset _ _ h

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : (l.formPerm ^ n) x ∈ {x | l.formPerm x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : (l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
simpa [h] using hx

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem toMatrix_reindexEquiv_prod (e : n ≃ p) (L : List (TransvectionStruct n R)) :
    (L.map (toMatrix ∘ reindexEquiv e)).prod = reindexAlgEquiv R _ e (L.map toMatrix).prod

Proof state:
case cons
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ reindexEquiv e) L).prod = (reindexAlgEquiv R R e) (List.map toMatrix L).prod
⊢ (List.map (toMatrix ∘ reindexEquiv e) (t :: L)).prod = (reindexAlgEquiv R R e) (List.map toMatrix (t :: L)).prod

Tactic:
simp only [toMatrix_reindexEquiv, IH, Function.comp_apply, List.prod_cons,
  reindexAlgEquiv_apply, List.map]

Result:
case cons
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ reindexEquiv e) L).prod = (reindexAlgEquiv R R e) (List.map toMatrix L).prod
⊢ (reindex e e) t.toMatrix * (reindex e e) (List.map toMatrix L).prod =
    (reindex e e) (t.toMatrix * (List.map toMatrix L).prod)

Proof state:
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
L : List (TransvectionStruct n R)
⊢ (List.map (toMatrix ∘ reindexEquiv e) L).prod = (reindexAlgEquiv R R e) (List.map toMatrix L).prod

Tactic:
induction L with
| nil => simp
| cons t L IH =>
  simp only [toMatrix_reindexEquiv, IH, Function.comp_apply, List.prod_cons,
    reindexAlgEquiv_apply, List.map]
  exact (reindexAlgEquiv_mul R _ _ _ _).symm

Result:
no goals

Proof state:
case nil
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
⊢ (List.map (toMatrix ∘ reindexEquiv e) []).prod = (reindexAlgEquiv R R e) (List.map toMatrix []).prod

Tactic:
simp

Result:
no goals

Proof state:
case cons
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ reindexEquiv e) L).prod = (reindexAlgEquiv R R e) (List.map toMatrix L).prod
⊢ (reindex e e) t.toMatrix * (reindex e e) (List.map toMatrix L).prod =
    (reindex e e) (t.toMatrix * (List.map toMatrix L).prod)

Tactic:
exact (reindexAlgEquiv_mul R _ _ _ _).symm

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem sSup_image2_eq_sSup_sSup (h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) : sSup (image2 l s t) = l (sSup s) (sSup t)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
⊢ sSup (image2 l s t) = l (sSup s) (sSup t)

Tactic:
simp_rw [sSup_image2, ← (h₂ _).l_sSup, ← (h₁ _).l_sSup]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
theorem natCast_eq_zero_or_one_of_two_eq_zero' (n : ℕ) (h : (2 : R) = 0) :
    (Even n → (n : R) = 0) ∧ (Odd n → (n : R) = 1)

Proof state:
case zero
R : Type u_4
inst✝ : AddMonoidWithOne R
h : 2 = 0
⊢ (Even 0 → ↑0 = 0) ∧ (Odd 0 → ↑0 = 1)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
⊢ (Even n → ↑n = 0) ∧ (Odd n → ↑n = 1)

Tactic:
induction n using Nat.twoStepInduction with
| zero => simp
| one => simp
| more n _ _ => simpa [add_assoc, Nat.even_add_one, Nat.odd_add_one, h]

Result:
no goals

Proof state:
case more
R : Type u_4
inst✝ : AddMonoidWithOne R
h : 2 = 0
n : ℕ
a✝¹ : (Even n → ↑n = 0) ∧ (Odd n → ↑n = 1)
a✝ : (Even (n + 1) → ↑(n + 1) = 0) ∧ (Odd (n + 1) → ↑(n + 1) = 1)
⊢ (Even (n + 2) → ↑(n + 2) = 0) ∧ (Odd (n + 2) → ↑(n + 2) = 1)

Tactic:
simpa [add_assoc, Nat.even_add_one, Nat.odd_add_one, h]

Result:
no goals

Proof state:
case one
R : Type u_4
inst✝ : AddMonoidWithOne R
h : 2 = 0
⊢ (Even 1 → ↑1 = 0) ∧ (Odd 1 → ↑1 = 1)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem mul_equiv_zero (g : CauSeq _ abv) {f : CauSeq _ abv} (hf : f ≈ 0) : g * f ≈ 0 :=
  have : LimZero (f - 0) := hf
  have : LimZero (g * f) := mul_limZero_right _ <| by simpa
  show LimZero (g * f - 0) by simpa

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
g f : CauSeq β abv
hf : f ≈ 0
this : (f - 0).LimZero
⊢ f.LimZero

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
g f : CauSeq β abv
hf : f ≈ 0
this✝ : (f - 0).LimZero
this : (g * f).LimZero
⊢ (g * f - 0).LimZero

Tactic:
simpa

Result:
no goals
-- Mathlib/Probability/Distributions/Exponential.lean
/-- The CDF of the exponential distribution equals ``1 - exp (-(r * x))`` -/
lemma exponentialCDFReal_eq {r : ℝ} (hr : 0 < r) (x : ℝ) :
    exponentialCDFReal r x = if 0 ≤ x then 1 - exp (-(r * x)) else 0

Proof state:
case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ r * x

Tactic:
exact mul_nonneg hr.le h

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
⊢ 0 ≤ if 0 ≤ x then 1 - rexp (-(r * x)) else 0

Tactic:
split_ifs with h

Result:
case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ 1 - rexp (-(r * x))

case neg
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ 0 ≤ 0

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
⊢ ↑(exponentialCDFReal r) x = if 0 ≤ x then 1 - rexp (-(r * x)) else 0

Tactic:
rw [exponentialCDFReal_eq_lintegral hr, lintegral_exponentialPDF_eq_antiDeriv hr x,
  ENNReal.toReal_ofReal_eq_iff]

Result:
r : ℝ
hr : 0 < r
x : ℝ
⊢ 0 ≤ if 0 ≤ x then 1 - rexp (-(r * x)) else 0

Proof state:
case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ 1 - rexp (-(r * x))

Tactic:
simp only [sub_nonneg, exp_le_one_iff, Left.neg_nonpos_iff]

Result:
case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ r * x

Proof state:
case neg
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ 0 ≤ 0

Tactic:
exact le_rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem back_eq_of_push_eq {a b : α} {xs ys : Vector α n} (h : xs.push a = ys.push b) : a = b

Proof state:
case mk.mk
α : Type u_1
n : Nat
a b : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h :
  ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.push a).toArray =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push b).toArray
⊢ a = b

Tactic:
simp only [push_mk] at h

Result:
case mk.mk
α : Type u_1
n : Nat
a b : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : toArray✝¹.push a = toArray✝.push b
⊢ a = b

Proof state:
α : Type u_1
n : Nat
a b : α
xs ys : Vector α n
h : xs.push a = ys.push b
⊢ a = b

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : Nat
a b : α
ys : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : { toArray := toArray✝, size_toArray := size_toArray✝ }.push a = ys.push b
⊢ a = b

Proof state:
case mk
α : Type u_1
n : Nat
a b : α
ys : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : { toArray := toArray✝, size_toArray := size_toArray✝ }.push a = ys.push b
⊢ a = b

Tactic:
cases ys

Result:
case mk.mk
α : Type u_1
n : Nat
a b : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h :
  { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.push a =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.push b
⊢ a = b

Proof state:
case mk.mk
α : Type u_1
n : Nat
a b : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : toArray✝¹.push a = toArray✝.push b
⊢ a = b

Tactic:
apply Array.back_eq_of_push_eq h

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
n : Nat
a b : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h :
  { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.push a =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.push b
⊢ a = b

Tactic:
replace h := congrArg Vector.toArray h

Result:
case mk.mk
α : Type u_1
n : Nat
a b : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h :
  ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.push a).toArray =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push b).toArray
⊢ a = b
-- Mathlib/Topology/Category/TopCat/Basic.lean
theorem isOpenEmbedding_iff_isIso_comp {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] :
    IsOpenEmbedding (f ≫ g) ↔ IsOpenEmbedding g

Proof state:
case mpr
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom g) → IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))

Tactic:
exact fun h => h.comp (TopCat.homeoOfIso (asIso f)).isOpenEmbedding

Result:
no goals

Proof state:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g)) ↔ IsOpenEmbedding ⇑(ConcreteCategory.hom g)

Tactic:
constructor

Result:
case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g)) → IsOpenEmbedding ⇑(ConcreteCategory.hom g)

case mpr
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom g) → IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))

Proof state:
case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g)) → IsOpenEmbedding ⇑(ConcreteCategory.hom g)

Tactic:
intro h

Result:
case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom g)

Proof state:
case h.e'_5
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))
⊢ ⇑(ConcreteCategory.hom g) = ⇑(ConcreteCategory.hom (f ≫ g)) ∘ ⇑(homeoOfIso (asIso f).symm)

Tactic:
exact congr_arg (DFunLike.coe ∘ ConcreteCategory.hom) (IsIso.inv_hom_id_assoc f g).symm

Result:
no goals

Proof state:
case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom g)

Tactic:
convert h.comp (TopCat.homeoOfIso (asIso f).symm).isOpenEmbedding

Result:
case h.e'_5
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g))
⊢ ⇑(ConcreteCategory.hom g) = ⇑(ConcreteCategory.hom (f ≫ g)) ∘ ⇑(homeoOfIso (asIso f).symm)
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_zero_mul_X (φ : MvPowerSeries σ R) (s : σ) : coeff R (0 : σ →₀ ℕ) (φ * X s) = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
s : σ
⊢ (coeff R 0) (φ * X s) = 0

Tactic:
have : ¬single s 1 ≤ 0 := fun h => by simpa using h s

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
s : σ
this : ¬single s 1 ≤ 0
⊢ (coeff R 0) (φ * X s) = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
s : σ
this : ¬single s 1 ≤ 0
⊢ (coeff R 0) (φ * X s) = 0

Tactic:
simp only [X, coeff_mul_monomial, if_neg this]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
s : σ
h : single s 1 ≤ 0
⊢ False

Tactic:
simpa using h s

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
protected lemma one [StarOrderedRing R] [DecidableEq n] : PosSemidef (1 : Matrix n n R) :=
  ⟨isHermitian_one, fun x => by
    rw [one_mulVec]; exact Fintype.sum_nonneg fun i => star_mul_self_nonneg _⟩

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
x : n → R
⊢ 0 ≤ star x ⬝ᵥ 1 *ᵥ x

Tactic:
rw [one_mulVec]

Result:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
x : n → R
⊢ 0 ≤ star x ⬝ᵥ x

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
x : n → R
⊢ 0 ≤ star x ⬝ᵥ x

Tactic:
exact Fintype.sum_nonneg fun i => star_mul_self_nonneg _

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The non-zero non-`N`-smooth numbers are `≥ N`. -/
lemma smoothNumbers_compl (N : ℕ) : (N.smoothNumbers)ᶜ \ {0} ⊆ {n | N ≤ n}

Proof state:
N : ℕ
⊢ N.smoothNumbersᶜ \ {0} ⊆ {n | N ≤ n}

Tactic:
simpa only [smoothNumbers_eq_factoredNumbers]
  using factoredNumbers_compl <| Finset.filter_subset _ (Finset.range N)

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_zero {ι : Type*} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι]
    [WellFoundedLT ι] (f : ι → E) : gramSchmidt 𝕜 f ⊥ = f ⊥

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : OrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
⊢ gramSchmidt 𝕜 f ⊥ = f ⊥

Tactic:
rw [gramSchmidt_def, Iio_eq_Ico, Finset.Ico_self, Finset.sum_empty, sub_zero]

Result:
no goals