harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/NAry.lean
theorem biUnion_image_right : (t.biUnion fun b => s.image fun a => f a b) = image₂ f s t :=
  coe_injective <| by
    push_cast
    exact Set.iUnion_image_right _

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ ↑(t.biUnion fun b => image (fun a => f a b) s) = ↑(image₂ f s t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ ⋃ x ∈ ↑t, (fun a => f a x) '' ↑s = image2 f ↑s ↑t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ ⋃ x ∈ ↑t, (fun a => f a x) '' ↑s = image2 f ↑s ↑t

Tactic:
exact Set.iUnion_image_right _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ : Vector ι n) (l₂ : Vector ι m)
    (h : ∀ a ∈ l₁ ++ l₂, p a) :
    (l₁ ++ l₂).pmap f h =
      (l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++
        l₂.pmap f fun a ha => h a (mem_append_right l₁ ha)

Proof state:
case mk
ι : Type u_1
α : Type u_2
n m : Nat
p : ι → Prop
f : (a : ι) → p a → α
l₂ : Vector ι m
toArray✝ : Array ι
size_toArray✝ : toArray✝.size = n
h : ∀ (a : ι), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ++ l₂ → p a
⊢ pmap f ({ toArray := toArray✝, size_toArray := size_toArray✝ } ++ l₂) h =
    pmap f { toArray := toArray✝, size_toArray := size_toArray✝ } ⋯ ++ pmap f l₂ ⋯

Tactic:
cases l₂

Result:
case mk.mk
ι : Type u_1
α : Type u_2
n m : Nat
p : ι → Prop
f : (a : ι) → p a → α
toArray✝¹ : Array ι
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array ι
size_toArray✝ : toArray✝.size = m
h :
  ∀ (a : ι),
    a ∈
        { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
          { toArray := toArray✝, size_toArray := size_toArray✝ } →
      p a
⊢ pmap f
      ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ })
      h =
    pmap f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ⋯ ++
      pmap f { toArray := toArray✝, size_toArray := size_toArray✝ } ⋯

Proof state:
case mk.mk
ι : Type u_1
α : Type u_2
n m : Nat
p : ι → Prop
f : (a : ι) → p a → α
toArray✝¹ : Array ι
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array ι
size_toArray✝ : toArray✝.size = m
h :
  ∀ (a : ι),
    a ∈
        { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
          { toArray := toArray✝, size_toArray := size_toArray✝ } →
      p a
⊢ pmap f
      ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ })
      h =
    pmap f { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ⋯ ++
      pmap f { toArray := toArray✝, size_toArray := size_toArray✝ } ⋯

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
n m : Nat
p : ι → Prop
f : (a : ι) → p a → α
l₁ : Vector ι n
l₂ : Vector ι m
h : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a
⊢ pmap f (l₁ ++ l₂) h = pmap f l₁ ⋯ ++ pmap f l₂ ⋯

Tactic:
cases l₁

Result:
case mk
ι : Type u_1
α : Type u_2
n m : Nat
p : ι → Prop
f : (a : ι) → p a → α
l₂ : Vector ι m
toArray✝ : Array ι
size_toArray✝ : toArray✝.size = n
h : ∀ (a : ι), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ++ l₂ → p a
⊢ pmap f ({ toArray := toArray✝, size_toArray := size_toArray✝ } ++ l₂) h =
    pmap f { toArray := toArray✝, size_toArray := size_toArray✝ } ⋯ ++ pmap f l₂ ⋯
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
@[simp]
lemma comp_smul (a : ℝ≥0∞) : κ ∘ₘ (a • μ) = a • (κ ∘ₘ μ)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
a : ℝ≥0∞
⊢ ⇑κ ∘ₘ (a • μ) = a • ⇑κ ∘ₘ μ

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
a : ℝ≥0∞
s : Set β
hs : MeasurableSet s
⊢ (⇑κ ∘ₘ (a • μ)) s = (a • ⇑κ ∘ₘ μ) s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
a : ℝ≥0∞
s : Set β
hs : MeasurableSet s
⊢ (⇑κ ∘ₘ (a • μ)) s = (a • ⇑κ ∘ₘ μ) s

Tactic:
simp only [bind_apply hs κ.measurable, lintegral_smul_measure, smul_apply, smul_eq_mul]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive]
lemma eq_of_inv_mul_eq_one (h : a⁻¹ * b = 1) : a = b

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a⁻¹ * b = 1
⊢ a = b

Tactic:
simpa using eq_inv_of_mul_eq_one_left h

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Supported.lean
theorem supportedEquivMvPolynomial_symm_C (s : Set σ) (x : R) :
    (supportedEquivMvPolynomial s).symm (C x) = algebraMap R (supported R s) x

Proof state:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
x : R
⊢ (supportedEquivMvPolynomial s).symm (C x) = (algebraMap R ↥(supported R s)) x

Tactic:
ext1

Result:
case a
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
x : R
⊢ ↑((supportedEquivMvPolynomial s).symm (C x)) = ↑((algebraMap R ↥(supported R s)) x)

Proof state:
case a
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
x : R
⊢ ↑((supportedEquivMvPolynomial s).symm (C x)) = ↑((algebraMap R ↥(supported R s)) x)

Tactic:
simp [supportedEquivMvPolynomial, MvPolynomial.algebraMap_eq]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Spectrum.lean
theorem orthogonalComplement_iSup_eigenspaces_invariant (hT : T.IsSymmetric)
    ⦃v : E⦄ (hv : v ∈ (⨆ μ, eigenspace T μ)ᗮ) : T v ∈ (⨆ μ, eigenspace T μ)ᗮ

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
v : E
hv : v ∈ (⨆ μ, eigenspace T μ)ᗮ
⊢ T v ∈ (⨆ μ, eigenspace T μ)ᗮ

Tactic:
rw [← Submodule.iInf_orthogonal] at hv ⊢

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
v : E
hv : v ∈ ⨅ i, (eigenspace T i)ᗮ
⊢ T v ∈ ⨅ i, (eigenspace T i)ᗮ

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
v : E
hv : v ∈ ⨅ i, (eigenspace T i)ᗮ
⊢ T v ∈ ⨅ i, (eigenspace T i)ᗮ

Tactic:
exact T.iInf_invariant hT.invariant_orthogonalComplement_eigenspace v hv

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
lemma subsingleton_iff (S : Submonoid R) (g : M →ₗ[R] M')
    [IsLocalizedModule S g] :
    Subsingleton M' ↔ ∀ m : M, ∃ r ∈ S, r • m = 0

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
⊢ Subsingleton M' ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0

Tactic:
simp_rw [subsingleton_iff_ker_eq_top S g, ← top_le_iff, SetLike.le_def,
  mem_ker_iff S, Submodule.mem_top, true_implies]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Continuum.lean
theorem power_aleph0_of_le_continuum {x : Cardinal} (h₁ : 2 ≤ x) (h₂ : x ≤ 𝔠) : x ^ ℵ₀ = 𝔠

Proof state:
case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ ≤ 𝔠 ^ ℵ₀

Tactic:
exact power_le_power_right h₂

Result:
no goals

Proof state:
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ = 𝔠

Tactic:
apply le_antisymm

Result:
case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ ≤ 𝔠

case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ 𝔠 ≤ x ^ ℵ₀

Proof state:
case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ 𝔠 ≤ x ^ ℵ₀

Tactic:
rw [← two_power_aleph0]

Result:
case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ 2 ^ ℵ₀ ≤ x ^ ℵ₀

Proof state:
case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ 2 ^ ℵ₀ ≤ x ^ ℵ₀

Tactic:
exact power_le_power_right h₁

Result:
no goals

Proof state:
case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ ≤ 𝔠

Tactic:
rw [← continuum_power_aleph0]

Result:
case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ ≤ 𝔠 ^ ℵ₀
-- Mathlib/Probability/Independence/Kernel.lean
@[simp] lemma indepSets_zero_right : IndepSets s1 s2 κ 0

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
s1 s2 : Set (Set Ω)
⊢ IndepSets s1 s2 κ 0

Tactic:
simp [IndepSets]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_iff_eventually : f =O[l] g' ↔ ∀ᶠ c in atTop, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g' x‖ :=
  isBigO_iff_eventually_isBigOWith.trans <| by simp only [IsBigOWith_def]

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (c : ℝ) in atTop, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g' x‖

Tactic:
simp only [IsBigOWith_def]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
theorem isomorphisms.iff : (isomorphisms C) f ↔ IsIso f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ isomorphisms C f ↔ IsIso f

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem pow_inj_iff_of_orderOf_eq_zero (h : orderOf x = 0) {n m : ℕ} : x ^ n = x ^ m ↔ n = m

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : orderOf x = 0
n m : ℕ
⊢ x ^ n = x ^ m ↔ n = m

Tactic:
rw [pow_eq_pow_iff_modEq, h, modEq_zero_iff]

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem fib_golden_conj_exp (n : ℕ) : Nat.fib (n + 1) - φ * Nat.fib n = ψ ^ n

Proof state:
n : ℕ
nz : √5 ≠ 0
⊢ √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n

Tactic:
rw [← (mul_inv_cancel₀ nz).symm, one_mul]

Result:
no goals

Proof state:
n : ℕ
⊢ √5 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1) - (φ ^ (n + 1) - φ * ψ ^ n)) / √5 = ψ ^ n

Tactic:
ring_nf

Result:
n : ℕ
⊢ √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n

Proof state:
n : ℕ
⊢ √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n

Tactic:
have nz : sqrt 5 ≠ 0 := by norm_num

Result:
n : ℕ
nz : √5 ≠ 0
⊢ √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n

Proof state:
n : ℕ
⊢ ↑(Nat.fib (n + 1)) - φ * ↑(Nat.fib n) = ψ ^ n

Tactic:
repeat rw [coe_fib_eq]

Result:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n

Proof state:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n

Tactic:
rw [mul_div, div_sub_div_same, mul_sub, ← pow_succ']

Result:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1) - (φ ^ (n + 1) - φ * ψ ^ n)) / √5 = ψ ^ n

Proof state:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ↑(Nat.fib n) = ψ ^ n

Tactic:
rw [coe_fib_eq]

Result:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma setIntegral_toReal_rnDeriv_eq_withDensity [SigmaFinite μ] [SFinite ν] (s : Set α) :
    ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν) s).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

Tactic:
rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ⊤

Tactic:
exact ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ (ν.withDensity (μ.rnDeriv ν)) s = (ν.withDensity (μ.rnDeriv ν)) s ∨
    (ν.withDensity (μ.rnDeriv ν)) s = 0 ∧ (ν.withDensity (μ.rnDeriv ν)) s = ⊤ ∨
      (ν.withDensity (μ.rnDeriv ν)) s = ⊤ ∧ (ν.withDensity (μ.rnDeriv ν)) s = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

Tactic:
rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply' _ s]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ (ν.withDensity (μ.rnDeriv ν)) s = (ν.withDensity (μ.rnDeriv ν)) s ∨
    (ν.withDensity (μ.rnDeriv ν)) s = 0 ∧ (ν.withDensity (μ.rnDeriv ν)) s = ⊤ ∨
      (ν.withDensity (μ.rnDeriv ν)) s = ⊤ ∧ (ν.withDensity (μ.rnDeriv ν)) s = 0
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem hasSum_geometric_of_norm_lt_one (h : ‖ξ‖ < 1) : HasSum (fun n : ℕ ↦ ξ ^ n) (1 - ξ)⁻¹

Proof state:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹

Tactic:
rw [hasSum_iff_tendsto_nat_of_summable_norm]

Result:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)

K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Summable fun i => ‖ξ ^ i‖

Proof state:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Summable fun i => ‖ξ ^ i‖

Tactic:
simp [norm_pow, summable_geometric_of_lt_one (norm_nonneg _) h]

Result:
no goals

Proof state:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : ξ = 1
⊢ 1 ≤ ‖ξ‖

Tactic:
simp [h]

Result:
no goals

Proof state:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹

Tactic:
have A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹)) :=
  ((tendsto_pow_atTop_nhds_zero_of_norm_lt_one h).sub tendsto_const_nhds).mul tendsto_const_nhds

Result:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹

Proof state:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
⊢ ξ ≠ 1

Tactic:
contrapose! h

Result:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : ξ = 1
⊢ 1 ≤ ‖ξ‖

Proof state:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹

Tactic:
have xi_ne_one : ξ ≠ 1 := by
  contrapose! h
  simp [h]

Result:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹

Proof state:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)

Tactic:
simpa [geom_sum_eq, xi_ne_one, neg_inv, div_eq_mul_inv] using A

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem collinear_insert_iff_of_mem_affineSpan {s : Set P} {p : P} (h : p ∈ affineSpan k s) :
    Collinear k (insert p s) ↔ Collinear k s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Collinear k (insert p s) ↔ Collinear k s

Tactic:
rw [Collinear, Collinear, vectorSpan_insert_eq_vectorSpan h]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_pow {p : MvPolynomial σ R} : ∀ {n : ℕ}, (p ^ n).eval₂ f g = p.eval₂ f g ^ n
  | 0 => by
    rw [pow_zero, pow_zero]
    exact eval₂_one _ _
  | n + 1 => by rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g (p ^ (n + 1)) = eval₂ f g p ^ (n + 1)

Tactic:
rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g (p ^ 0) = eval₂ f g p ^ 0

Tactic:
rw [pow_zero, pow_zero]

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g 1 = 1

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g 1 = 1

Tactic:
exact eval₂_one _ _

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive zsmul_zero_sub]
lemma one_div_zpow (a : α) (n : ℤ) : (1 / a) ^ n = 1 / a ^ n

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ (1 / a) ^ n = 1 / a ^ n

Tactic:
simp only [one_div, inv_zpow]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem Scheme.isoSpec_inv_naturality {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) :
    Spec.map (f.appTop) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f

Proof state:
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f

Tactic:
rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
  asIso_inv, IsIso.hom_inv_id, Category.comp_id]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem IsTheta.of_norm_eventuallyEq {g : α → ℝ} (h : (fun x ↦ ‖f' x‖) =ᶠ[l] g) : f' =Θ[l] g :=
  of_norm_eventuallyEq_norm <| h.mono fun x hx ↦ by simp only [← hx, norm_norm]

Proof state:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
g : α → ℝ
h : (fun x => ‖f' x‖) =ᶠ[l] g
x : α
hx : (fun x => ‖f' x‖) x = g x
⊢ (fun x => ‖f' x‖) x = (fun x => ‖g x‖) x

Tactic:
simp only [← hx, norm_norm]

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem snd_toProd (x : M ∗ N) : (toProd x).2 = snd x

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).2 = snd x

Tactic:
rw [← snd_comp_toProd]

Result:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).2 = ((MonoidHom.snd M N).comp toProd) x

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).2 = ((MonoidHom.snd M N).comp toProd) x

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean
theorem right_induction {P : CliffordAlgebra Q → Prop} (algebraMap : ∀ r : R, P (algebraMap _ _ r))
    (add : ∀ x y, P x → P y → P (x + y)) (mul_ι : ∀ m x, P x → P (x * ι Q m)) : ∀ x, P x

Proof state:
case mem.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((_root_.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
r : R
⊢ P ((_root_.algebraMap R (CliffordAlgebra Q)) r)

Tactic:
exact algebraMap r

Result:
no goals
-- Mathlib/Data/Set/Sigma.lean
theorem sigma_univ_range_eq {f : ∀ i, α i → β i} :
    (univ : Set ι).sigma (fun i ↦ range (f i)) = range fun x : Σ i, α i ↦ ⟨x.1, f _ x.2⟩ :=
  ext <| by simp [range, Sigma.forall]

Proof state:
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_6
f : (i : ι) → α i → β i
⊢ ∀ (x : (i : ι) × β i), (x ∈ univ.sigma fun i => range (f i)) ↔ x ∈ range fun x => ⟨x.fst, f x.fst x.snd⟩

Tactic:
simp [range, Sigma.forall]

Result:
no goals
-- Mathlib/Data/NNReal/Basic.lean
theorem le_iInf_mul {a : ℝ≥0} {g : ι → ℝ≥0} {h : ℝ≥0} (H : ∀ i, a ≤ g i * h) : a ≤ iInf g * h

Proof state:
ι : Sort u_2
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ ⨅ i, g i * h

Tactic:
exact le_ciInf H

Result:
no goals

Proof state:
ι : Sort u_2
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ iInf g * h

Tactic:
rw [iInf_mul]

Result:
ι : Sort u_2
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ ⨅ i, g i * h
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem C_mul' (a : R) (f : R[X]) : C a * f = a • f

Proof state:
R : Type u
inst✝ : Semiring R
a : R
f : R[X]
⊢ C a * f = a • f

Tactic:
ext

Result:
case a
R : Type u
inst✝ : Semiring R
a : R
f : R[X]
n✝ : ℕ
⊢ (C a * f).coeff n✝ = (a • f).coeff n✝

Proof state:
case a
R : Type u
inst✝ : Semiring R
a : R
f : R[X]
n✝ : ℕ
⊢ (C a * f).coeff n✝ = (a • f).coeff n✝

Tactic:
rw [coeff_C_mul, coeff_smul, smul_eq_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ushiftRight_zero (x : BitVec w) : x >>> 0 = x

Proof state:
w : Nat
x : BitVec w
⊢ x >>> 0 = x

Tactic:
simp [bv_toNat]

Result:
no goals
-- Mathlib/NumberTheory/SumFourSquares.lean
theorem sq_add_sq_of_two_mul_sq_add_sq {m x y : ℤ} (h : 2 * m = x ^ 2 + y ^ 2) :
    m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2 :=
  have : Even (x ^ 2 + y ^ 2)

Proof state:
m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 * 2 ≠ 0

Tactic:
decide

Result:
no goals

Proof state:
m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 * 2 * m = (x - y) ^ 2 + (x + y) ^ 2

Tactic:
rw [mul_assoc, h]

Result:
m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 * (x ^ 2 + y ^ 2) = (x - y) ^ 2 + (x + y) ^ 2

Proof state:
m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 * (x ^ 2 + y ^ 2) = (x - y) ^ 2 + (x + y) ^ 2

Tactic:
ring

Result:
no goals

Proof state:
m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ (x - y) ^ 2 + (x + y) ^ 2 = (2 * ((x - y) / 2)) ^ 2 + (2 * ((x + y) / 2)) ^ 2

Tactic:
rw [Int.mul_ediv_cancel' _, Int.mul_ediv_cancel' _] <;>
  simpa [sq, parity_simps, ← even_iff_two_dvd]

Result:
no goals

Proof state:
m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ (2 * ((x - y) / 2)) ^ 2 + (2 * ((x + y) / 2)) ^ 2 = 2 * 2 * (((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2)

Tactic:
nlinarith

Result:
no goals

Proof state:
m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
⊢ Even (x ^ 2 + y ^ 2)

Tactic:
simp [← h, even_mul]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem Tendsto.eventually_forall_ge_atTop [Preorder β] {l : Filter α}
    {p : β → Prop} {f : α → β} (hf : Tendsto f l atTop) (h_evtl : ∀ᶠ x in atTop, p x) :
    ∀ᶠ x in l, ∀ y, f x ≤ y → p y

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atTop
h_evtl : ∀ᶠ (x : β) in atTop, ∀ (y : β), x ≤ y → p y
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y

Tactic:
exact (h_evtl.comap f).filter_mono hf.le_comap

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atTop
h_evtl : ∀ᶠ (x : β) in atTop, p x
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y

Tactic:
rw [← Filter.eventually_forall_ge_atTop] at h_evtl

Result:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atTop
h_evtl : ∀ᶠ (x : β) in atTop, ∀ (y : β), x ≤ y → p y
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y