harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setLIntegral_condKernel_univ_left (hf : Measurable f) {t : Set Ω}
    (ht : MeasurableSet t) :
    ∫⁻ b, ∫⁻ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst
      = ∫⁻ x in Set.univ ×ˢ t, f x ∂ρ

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫⁻ (b : β) in Set.univ, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst

Tactic:
simp_rw [Measure.restrict_univ]

Result:
no goals

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ

Tactic:
rw [← setLIntegral_condKernel hf MeasurableSet.univ ht]

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫⁻ (b : β) in Set.univ, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst
-- Mathlib/Data/TypeVec.lean
theorem Arrow.ext {α β : TypeVec n} (f g : α ⟹ β) :
    (∀ i, f i = g i) → f = g

Proof state:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
⊢ f = g

Tactic:
funext i

Result:
case h
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
i : Fin2 n
⊢ f i = g i

Proof state:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
f g : α ⟹ β
⊢ (∀ (i : Fin2 n), f i = g i) → f = g

Tactic:
intro h

Result:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
⊢ f = g

Proof state:
case h
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
i : Fin2 n
⊢ f i = g i

Tactic:
apply h

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobject_arrow :
    (kernelSubobjectIso f).hom ≫ kernel.ι f = (kernelSubobject f).arrow

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ (kernelSubobjectIso f).hom ≫ kernel.ι f = (kernelSubobject f).arrow

Tactic:
simp [kernelSubobjectIso]

Result:
no goals
-- Mathlib/Data/Set/Subsingleton.lean
theorem nontrivial_coe_sort {s : Set α} : Nontrivial s ↔ s.Nontrivial

Proof state:
α : Type u
s : Set α
⊢ Nontrivial ↑s ↔ s.Nontrivial

Tactic:
simp [← nontrivial_univ_iff, Set.Nontrivial]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem getElem_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
    (k) (h' : k < (as.insertIdx i v).size) :
    (as.insertIdx i v)[k] =
      if h₁ : k < i then
        as[k]'(by omega)
      else
        if h₂ : k = i then
          v
        else
          as[k - 1]'(by simp at h'; omega)

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h).size
⊢ (let j := as.size;
      let as_1 := as.push v;
      insertIdx.loop i as_1 ⟨j, ⋯⟩)[k] =
    if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]

Tactic:
rw [getElem_insertIdx_loop]

Result:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h' : k < (as.insertIdx i v h).size
⊢ (if h₁ : k < i then (as.push v)[k]
    else
      if h₂ : k = i then if i ≤ as.size then (as.push v)[as.size] else (as.push v)[i]
      else if k ≤ as.size then (as.push v)[k - 1] else (as.push v)[k]) =
    if h₁ : k < i then as[k] else if h₂ : k = i then v else as[k - 1]

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
k : Nat
h'✝ : k < (as.insertIdx i v h).size
h' : k ≤ as.size
h₁ : k < i
⊢ k < as.size

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem mem_tangentConeAt_of_pow_smul {r : 𝕜} (hr₀ : r ≠ 0) (hr : ‖r‖ < 1)
    (hs : ∀ᶠ n : ℕ in atTop, x + r ^ n • y ∈ s) : y ∈ tangentConeAt 𝕜 s x

Proof state:
case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x y : E
s : Set E
r : 𝕜
hr₀ : r ≠ 0
hr : ‖r‖ < 1
hs : ∀ᶠ (n : ℕ) in atTop, x + r ^ n • y ∈ s
⊢ Tendsto (fun n => (fun n => (r ^ n)⁻¹) n • (fun n => r ^ n • y) n) atTop (𝓝 y)

Tactic:
simp only [inv_smul_smul₀ (pow_ne_zero _ hr₀), tendsto_const_nhds]

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x y : E
s : Set E
r : 𝕜
hr₀ : r ≠ 0
hr : ‖r‖ < 1
hs : ∀ᶠ (n : ℕ) in atTop, x + r ^ n • y ∈ s
⊢ Tendsto (fun n => ‖(fun n => (r ^ n)⁻¹) n‖) atTop atTop

Tactic:
simp only [norm_inv, norm_pow, ← inv_pow]

Result:
case refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x y : E
s : Set E
r : 𝕜
hr₀ : r ≠ 0
hr : ‖r‖ < 1
hs : ∀ᶠ (n : ℕ) in atTop, x + r ^ n • y ∈ s
⊢ Tendsto (fun n => ‖r‖⁻¹ ^ n) atTop atTop

Proof state:
case refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x y : E
s : Set E
r : 𝕜
hr₀ : r ≠ 0
hr : ‖r‖ < 1
hs : ∀ᶠ (n : ℕ) in atTop, x + r ^ n • y ∈ s
⊢ Tendsto (fun n => ‖r‖⁻¹ ^ n) atTop atTop

Tactic:
exact tendsto_pow_atTop_atTop_of_one_lt <| (one_lt_inv₀ (norm_pos_iff.2 hr₀)).2 hr

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x y : E
s : Set E
r : 𝕜
hr₀ : r ≠ 0
hr : ‖r‖ < 1
hs : ∀ᶠ (n : ℕ) in atTop, x + r ^ n • y ∈ s
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
refine ⟨fun n ↦ (r ^ n)⁻¹, fun n ↦ r ^ n • y, hs, ?_, ?_⟩

Result:
case refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x y : E
s : Set E
r : 𝕜
hr₀ : r ≠ 0
hr : ‖r‖ < 1
hs : ∀ᶠ (n : ℕ) in atTop, x + r ^ n • y ∈ s
⊢ Tendsto (fun n => ‖(fun n => (r ^ n)⁻¹) n‖) atTop atTop

case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x y : E
s : Set E
r : 𝕜
hr₀ : r ≠ 0
hr : ‖r‖ < 1
hs : ∀ᶠ (n : ℕ) in atTop, x + r ^ n • y ∈ s
⊢ Tendsto (fun n => (fun n => (r ^ n)⁻¹) n • (fun n => r ^ n • y) n) atTop (𝓝 y)
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma ι₁_desc : ι₁ K ≫ desc φ₀ φ₁ h = φ₁

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
φ₀ φ₁ : K ⟶ F
h : Homotopy φ₀ φ₁
⊢ ι₁ K ≫ desc φ₀ φ₁ h = φ₁

Tactic:
simp [ι₁, desc]

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
theorem isCauSeq_iff_lift {f : ℕ → ℚ} : IsCauSeq abs f ↔ IsCauSeq abs fun i => (f i : ℝ) where
  mp H ε ε0 :=
    let ⟨δ, δ0, δε⟩ := exists_pos_rat_lt ε0
    (H _ δ0).imp fun i hi j ij => by dsimp; exact lt_trans (mod_cast hi _ ij) δε
  mpr H ε ε0 :=
    (H _ (Rat.cast_pos.2 ε0)).imp fun i hi j ij => by dsimp at hi; exact mod_cast hi _ ij

Proof state:
f : ℕ → ℚ
H : IsCauSeq abs f
ε : ℝ
ε0 : ε > 0
δ : ℚ
δ0 : 0 < δ
δε : ↑δ < ε
i : ℕ
hi : ∀ j ≥ i, |f j - f i| < δ
j : ℕ
ij : j ≥ i
⊢ |↑(f j) - ↑(f i)| < ε

Tactic:
exact lt_trans (mod_cast hi _ ij) δε

Result:
no goals

Proof state:
f : ℕ → ℚ
H : IsCauSeq abs fun i => ↑(f i)
ε : ℚ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |↑(f j) - ↑(f i)| < ↑ε
j : ℕ
ij : j ≥ i
⊢ |f j - f i| < ε

Tactic:
exact mod_cast hi _ ij

Result:
no goals

Proof state:
f : ℕ → ℚ
H : IsCauSeq abs f
ε : ℝ
ε0 : ε > 0
δ : ℚ
δ0 : 0 < δ
δε : ↑δ < ε
i : ℕ
hi : ∀ j ≥ i, |f j - f i| < δ
j : ℕ
ij : j ≥ i
⊢ |(fun i => ↑(f i)) j - (fun i => ↑(f i)) i| < ε

Tactic:
dsimp

Result:
f : ℕ → ℚ
H : IsCauSeq abs f
ε : ℝ
ε0 : ε > 0
δ : ℚ
δ0 : 0 < δ
δε : ↑δ < ε
i : ℕ
hi : ∀ j ≥ i, |f j - f i| < δ
j : ℕ
ij : j ≥ i
⊢ |↑(f j) - ↑(f i)| < ε

Proof state:
f : ℕ → ℚ
H : IsCauSeq abs fun i => ↑(f i)
ε : ℚ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun i => ↑(f i)) j - (fun i => ↑(f i)) i| < ↑ε
j : ℕ
ij : j ≥ i
⊢ |f j - f i| < ε

Tactic:
dsimp at hi

Result:
f : ℕ → ℚ
H : IsCauSeq abs fun i => ↑(f i)
ε : ℚ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |↑(f j) - ↑(f i)| < ↑ε
j : ℕ
ij : j ≥ i
⊢ |f j - f i| < ε
-- Mathlib/Analysis/Matrix.lean
theorem linfty_opNorm_def (A : Matrix m n α) :
    ‖A‖ = ((Finset.univ : Finset m).sup fun i : m => ∑ j : n, ‖A i j‖₊ : ℝ≥0)

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖fun i => (WithLp.equiv 1 (n → α)).symm (A i)‖ = ↑(Finset.univ.sup fun i => ∑ j : n, ‖A i j‖₊)

Tactic:
simp [Pi.norm_def, PiLp.nnnorm_eq_of_L1]

Result:
no goals

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖A‖ = ↑(Finset.univ.sup fun i => ∑ j : n, ‖A i j‖₊)

Tactic:
change ‖fun i => (WithLp.equiv 1 _).symm (A i)‖ = _

Result:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖fun i => (WithLp.equiv 1 (n → α)).symm (A i)‖ = ↑(Finset.univ.sup fun i => ∑ j : n, ‖A i j‖₊)
-- Mathlib/Topology/Inseparable.lean
/-- A set is stable under specialization iff it is a union of closed sets. -/
lemma stableUnderSpecialization_iff_exists_sUnion_eq {s : Set X} :
    StableUnderSpecialization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed s) ∧ ⋃₀ S = s

Proof state:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ⋃₀ ((fun x => closure {x}) '' s) = ⋃ x ∈ s, closure {x}

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ∀ s_1 ∈ (fun x => closure {x}) '' s, IsClosed s_1

Tactic:
rintro _ ⟨_, _, rfl⟩

Result:
case refine_1.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
w✝ : X
left✝ : w✝ ∈ s
⊢ IsClosed ((fun x => closure {x}) w✝)

Proof state:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ⋃₀ ((fun x => closure {x}) '' s) = s

Tactic:
conv_rhs => rw [← H.Union_eq]

Result:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ⋃₀ ((fun x => closure {x}) '' s) = ⋃ x ∈ s, closure {x}

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderSpecialization s ↔ ∃ S, (∀ s ∈ S, IsClosed s) ∧ ⋃₀ S = s

Tactic:
refine ⟨fun H ↦ ⟨(fun x : X ↦ closure {x}) '' s, ?_, ?_⟩, fun ⟨S, hS, e⟩ ↦ e ▸
  stableUnderSpecialization_sUnion S (fun x hx ↦ (hS x hx).stableUnderSpecialization)⟩

Result:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ∀ s_1 ∈ (fun x => closure {x}) '' s, IsClosed s_1

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ ⋃₀ ((fun x => closure {x}) '' s) = s

Proof state:
case refine_1.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
w✝ : X
left✝ : w✝ ∈ s
⊢ IsClosed ((fun x => closure {x}) w✝)

Tactic:
exact isClosed_closure

Result:
no goals
-- Mathlib/Data/Nat/Factorial/BigOperators.lean
theorem prod_factorial_dvd_factorial_sum : (∏ i ∈ s, (f i)!) ∣ (∑ i ∈ s, f i)!

Proof state:
case h₁
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i ∈ ∅, (f i)! ∣ (∑ i ∈ ∅, f i)!

Tactic:
simp

Result:
no goals

Proof state:
case h₂
α : Type u_1
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ (f a)! * ∏ x ∈ s, (f x)! ∣ (f a + ∑ x ∈ s, f x)!

Tactic:
exact (mul_dvd_mul_left _ ih).trans (Nat.factorial_mul_factorial_dvd_factorial_add _ _)

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!

Tactic:
induction' s using Finset.cons_induction_on with a s has ih

Result:
case h₁
α : Type u_1
s : Finset α
f : α → ℕ
⊢ ∏ i ∈ ∅, (f i)! ∣ (∑ i ∈ ∅, f i)!

case h₂
α : Type u_1
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ ∏ i ∈ cons a s has, (f i)! ∣ (∑ i ∈ cons a s has, f i)!

Proof state:
case h₂
α : Type u_1
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ ∏ i ∈ cons a s has, (f i)! ∣ (∑ i ∈ cons a s has, f i)!

Tactic:
rw [prod_cons, Finset.sum_cons]

Result:
case h₂
α : Type u_1
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
has : a ∉ s
ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
⊢ (f a)! * ∏ x ∈ s, (f x)! ∣ (f a + ∑ x ∈ s, f x)!
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_modify [LawfulBEq α] {k k': α} {f : β k → β k} (h : m.WF) :
    k' ∈ m.modify k f ↔ k' ∈ m

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
h : m.WF
⊢ k' ∈ m.modify k f ↔ k' ∈ m

Tactic:
simp only [mem_iff_contains, contains_modify h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma toAffine_neg {P : Fin 3 → F} (hP : W.Nonsingular P) :
    toAffine W (W.neg P) = -toAffine W P

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
rw [neg_of_Z_eq_zero hP.left hPz, toAffine_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg,
  toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_zero]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
by_cases hPz : P z = 0

Result:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
rw [neg_of_Z_ne_zero hPz, toAffine_smul _ <| Ne.isUnit hPz, toAffine_some <|
    (nonsingular_smul _ <| Ne.isUnit hPz).mp <| neg_of_Z_ne_zero hPz ▸ nonsingular_neg hP,
  toAffine_of_Z_ne_zero hP hPz, Affine.Point.neg_some]

Result:
no goals
-- Mathlib/Probability/Distributions/Geometric.lean
lemma geometricPMFRealSum (hp_pos : 0 < p) (hp_le_one : p ≤ 1) :
    HasSum (fun n ↦ geometricPMFReal p n) 1

Proof state:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun i => (1 - p) ^ i * p) 1
⊢ HasSum (fun n => (1 - p) ^ n * p) 1

Tactic:
exact this

Result:
no goals

Proof state:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ HasSum (fun n => (1 - p) ^ n * p) 1

Tactic:
have := hasSum_geometric_of_lt_one (sub_nonneg.mpr hp_le_one) (sub_lt_self 1 hp_pos)

Result:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun n => (1 - p) ^ n) (1 - (1 - p))⁻¹
⊢ HasSum (fun n => (1 - p) ^ n * p) 1

Proof state:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun n => (1 - p) ^ n) (1 - (1 - p))⁻¹
⊢ HasSum (fun n => (1 - p) ^ n * p) 1

Tactic:
apply (hasSum_mul_right_iff (hp_pos.ne')).mpr at this

Result:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun i => (1 - p) ^ i * p) ((1 - (1 - p))⁻¹ * p)
⊢ HasSum (fun n => (1 - p) ^ n * p) 1

Proof state:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ HasSum (fun n => geometricPMFReal p n) 1

Tactic:
unfold geometricPMFReal

Result:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ HasSum (fun n => (1 - p) ^ n * p) 1

Proof state:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun i => (1 - p) ^ i * p) (p⁻¹ * p)
⊢ HasSum (fun n => (1 - p) ^ n * p) 1

Tactic:
rw [inv_mul_eq_div, div_self hp_pos.ne'] at this

Result:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun i => (1 - p) ^ i * p) 1
⊢ HasSum (fun n => (1 - p) ^ n * p) 1

Proof state:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun i => (1 - p) ^ i * p) ((1 - (1 - p))⁻¹ * p)
⊢ HasSum (fun n => (1 - p) ^ n * p) 1

Tactic:
simp only [sub_sub_cancel] at this

Result:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun i => (1 - p) ^ i * p) (p⁻¹ * p)
⊢ HasSum (fun n => (1 - p) ^ n * p) 1
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem le_restrict_empty : v ≤[∅] w

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
j : Set α
a✝ : MeasurableSet j
⊢ ↑(v.restrict ∅) j ≤ ↑(w.restrict ∅) j

Tactic:
rw [restrict_empty, restrict_empty]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤[∅] w

Tactic:
intro j _

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
j : Set α
a✝ : MeasurableSet j
⊢ ↑(v.restrict ∅) j ≤ ↑(w.restrict ∅) j
-- Mathlib/Algebra/Order/Antidiag/Finsupp.lean
theorem finsuppAntidiag_insert {a : ι} {s : Finset ι}
    (h : a ∉ s) (n : μ) :
    finsuppAntidiag (insert a s) n = (antidiagonal n).biUnion
      (fun p : μ × μ =>
        (finsuppAntidiag s p.snd).attach.map
        ⟨fun f => Finsupp.update f.val a p.fst,
        (fun ⟨f, hf⟩ ⟨g, hg⟩ hfg => Subtype.ext <| by
          simp only [mem_val, mem_finsuppAntidiag] at hf hg
          simp only [DFunLike.ext_iff] at hfg ⊢
          intro x
          obtain rfl | hx := eq_or_ne x a
          · replace hf := mt (hf.2 ·) h
            replace hg := mt (hg.2 ·) h
            rw [not_mem_support_iff.mp hf, not_mem_support_iff.mp hg]
          · simpa only [coe_update, Function.update, dif_neg hx] using hfg x)⟩)

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
⊢ (insert a s).finsuppAntidiag n =
    (antidiagonal n).biUnion fun p =>
      map { toFun := fun f => (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach

Tactic:
ext f

Result:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ f ∈ (insert a s).finsuppAntidiag n ↔
    f ∈
      (antidiagonal n).biUnion fun p =>
        map { toFun := fun f => (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach

Proof state:
case inl
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
s : Finset ι
n : μ
p : μ × μ
x✝¹ x✝ : { x // x ∈ s.finsuppAntidiag p.2 }
f : ι →₀ μ
hf✝ : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg✝ : g ∈ s.finsuppAntidiag p.2
x : ι
h : x ∉ s
hfg : ∀ (x_1 : ι), (f.update x p.1) x_1 = (g.update x p.1) x_1
hf : x ∉ f.support
hg : x ∉ g.support
⊢ f x = g x

Tactic:
rw [not_mem_support_iff.mp hf, not_mem_support_iff.mp hg]

Result:
no goals
-- Mathlib/Order/Cover.lean
lemma reflTransGen_wcovBy_eq_reflTransGen_covBy [PartialOrder α] :
    ReflTransGen ((· : α) ⩿ ·) = ReflTransGen (· ⋖ ·)

Proof state:
α : Type u_1
inst✝ : PartialOrder α
⊢ (ReflTransGen fun x1 x2 => x1 ⩿ x2) = ReflTransGen fun x1 x2 => x1 ⋖ x2

Tactic:
rw [wcovBy_eq_reflGen_covBy, reflTransGen_reflGen]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem rotateRight_mod_eq_rotateRight {x : BitVec w} {r : Nat} :
    x.rotateRight (r % w) = x.rotateRight r

Proof state:
w : Nat
x : BitVec w
r : Nat
⊢ x.rotateRight (r % w) = x.rotateRight r

Tactic:
simp only [rotateRight, Nat.mod_mod]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem hasSum_toReal {f : α → ℝ≥0∞} (hsum : ∑' x, f x ≠ ∞) :
    HasSum (fun x => (f x).toReal) (∑' x, (f x).toReal)

Proof state:
case intro
α : Type u_1
f : α → ℝ≥0
hsum : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤
⊢ HasSum (fun x => ((fun i => ↑(f i)) x).toReal) (∑' (x : α), ((fun i => ↑(f i)) x).toReal)

Tactic:
simp only [coe_toReal, ← NNReal.coe_tsum, NNReal.hasSum_coe]

Result:
case intro
α : Type u_1
f : α → ℝ≥0
hsum : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤
⊢ HasSum f (∑' (a : α), f a)

Proof state:
case intro
α : Type u_1
f : α → ℝ≥0
hsum : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤
⊢ HasSum f (∑' (a : α), f a)

Tactic:
exact (tsum_coe_ne_top_iff_summable.1 hsum).hasSum

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ≥0∞
hsum : ∑' (x : α), f x ≠ ⊤
⊢ HasSum (fun x => (f x).toReal) (∑' (x : α), (f x).toReal)

Tactic:
lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hsum

Result:
case intro
α : Type u_1
f : α → ℝ≥0
hsum : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤
⊢ HasSum (fun x => ((fun i => ↑(f i)) x).toReal) (∑' (x : α), ((fun i => ↑(f i)) x).toReal)
-- Mathlib/Algebra/Lie/UniversalEnveloping.lean
theorem lift_unique (g : UniversalEnvelopingAlgebra R L →ₐ[R] A) : g ∘ ι R = f ↔ g = lift R f

Proof state:
case mpr.h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : (lift R).symm g = f
x✝ : L
⊢ (⇑g ∘ ⇑(ι R)) x✝ = f x✝

Tactic:
simp [← h]

Result:
no goals

Proof state:
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ⇑g ∘ ⇑(ι R) = ⇑f ↔ g = (lift R) f

Tactic:
refine Iff.trans ?_ (lift R).symm_apply_eq

Result:
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ⇑g ∘ ⇑(ι R) = ⇑f ↔ (lift R).symm g = f

Proof state:
case mpr
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ (lift R).symm g = f → ⇑g ∘ ⇑(ι R) = ⇑f

Tactic:
intro h

Result:
case mpr
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : (lift R).symm g = f
⊢ ⇑g ∘ ⇑(ι R) = ⇑f

Proof state:
case mpr
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : (lift R).symm g = f
⊢ ⇑g ∘ ⇑(ι R) = ⇑f

Tactic:
ext

Result:
case mpr.h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : (lift R).symm g = f
x✝ : L
⊢ (⇑g ∘ ⇑(ι R)) x✝ = f x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Bool.lean
theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b)

Proof state:
⊢ ∀ (a b : Bool), (!decide ((a ^^ b) = (a == b))) = true

Tactic:
decide

Result:
no goals