harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Equiv/Basic.lean
theorem piCongrLeft'_symm_update [DecidableEq α] [DecidableEq β] (P : α → Sort*) (e : α ≃ β)
    (f : ∀ b, P (e.symm b)) (b : β) (x : P (e.symm b)) :
    (e.piCongrLeft' P).symm (update f b x) = update ((e.piCongrLeft' P).symm f) (e.symm b) x

Proof state:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (b : β) → P (e.symm b)
b : β
x : P (e.symm b)
⊢ (Equiv.piCongrLeft' P e).symm (update f b x) = update ((Equiv.piCongrLeft' P e).symm f) (e.symm b) x

Tactic:
simp [(e.piCongrLeft' P).symm_apply_eq, piCongrLeft'_update]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem toMonoidWithZeroHom_eq_coe (f : α →*₀o β) : f.toMonoidWithZeroHom = f

Proof state:
α : Type u_2
β : Type u_3
hα : Preorder α
hα' : MulZeroOneClass α
hβ : Preorder β
hβ' : MulZeroOneClass β
f : α →*₀o β
⊢ f.toMonoidWithZeroHom = ↑f

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_lt_d6 : π < 3.141593

Proof state:
⊢ π < 3.141593

Tactic:
pi_upper_bound [
  35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
  2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem center_eq_bot_of_subsingleton [Subsingleton n] :
    center (SpecialLinearGroup n R) = ⊥ :=
  eq_bot_iff.mpr fun x _ ↦ by rw [mem_bot, Subsingleton.elim x 1]

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x : SpecialLinearGroup n R
x✝ : x ∈ center (SpecialLinearGroup n R)
⊢ x ∈ ⊥

Tactic:
rw [mem_bot, Subsingleton.elim x 1]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.comp_sub (hf : HasFPowerSeriesOnBall f p x r) (y : E) :
    HasFPowerSeriesOnBall (fun z => f (z - y)) p (x + y) r :=
  { r_le := hf.r_le
    r_pos := hf.r_pos
    hasSum := fun {z} hz => by
      convert hf.hasSum hz using 2
      abel }

Proof state:
case h.e'_6.h.e'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y z : E
hz : z ∈ EMetric.ball 0 r
⊢ x + y + z - y = x + z

Tactic:
abel

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y z : E
hz : z ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p n) fun x => z) (f (x + y + z - y))

Tactic:
convert hf.hasSum hz using 2

Result:
case h.e'_6.h.e'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y z : E
hz : z ∈ EMetric.ball 0 r
⊢ x + y + z - y = x + z
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem isOfFinOrder_iff_pow_eq_one : IsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n = 1

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
⊢ IsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
simp [IsOfFinOrder, mem_periodicPts, isPeriodicPt_mul_iff_pow_eq_one]

Result:
no goals
-- Mathlib/Order/Category/NonemptyFinLinOrd.lean
lemma comp_apply {X Y Z : NonemptyFinLinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : NonemptyFinLinOrd
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X.toLinOrd
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
theorem le_iff_exists_mul' : a ≤ b ↔ ∃ c, b = c * a

Proof state:
α : Type u
inst✝² : CommMagma α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedMul α
a b : α
⊢ a ≤ b ↔ ∃ c, b = c * a

Tactic:
simp only [mul_comm _ a, le_iff_exists_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem Dense.borel_eq_generateFrom_Ico_mem {α : Type*} [TopologicalSpace α] [LinearOrder α]
    [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMinOrder α] {s : Set α}
    (hd : Dense s) :
    borel α = .generateFrom { S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S } :=
  hd.borel_eq_generateFrom_Ico_mem_aux (by simp) fun _ _ hxy H =>
    ((nonempty_Ioo.2 hxy).ne_empty H).elim

Proof state:
α : Type u_5
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : SecondCountableTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
s : Set α
hd : Dense s
⊢ ∀ (x : α), IsBot x → x ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/CompleteField.lean
theorem cutMap_coe (q : ℚ) : cutMap β (q : α) = Rat.cast '' {r : ℚ | (r : β) < q}

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrderedField α
inst✝ : LinearOrderedField β
q : ℚ
⊢ cutMap β ↑q = Rat.cast '' {r | ↑r < ↑q}

Tactic:
simp_rw [cutMap, Rat.cast_lt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_pop (a : Array α) : a.pop.toList = a.toList.dropLast

Proof state:
α : Type u_1
a : Array α
⊢ a.pop.toList = a.toList.dropLast

Tactic:
simp [pop]

Result:
no goals
-- Mathlib/Data/Finset/Disjoint.lean
theorem disjoint_insert_left : Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t

Tactic:
simp only [disjoint_left, mem_insert, or_imp, forall_and, forall_eq]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
lemma le_minSmoothness {n : WithTop ℕ∞} : n ≤ minSmoothness 𝕜 n

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
⊢ n ≤ minSmoothness 𝕜 n

Tactic:
simp only [minSmoothness]

Result:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
⊢ n ≤ if IsRCLikeNormedField 𝕜 then n else ω

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
⊢ n ≤ if IsRCLikeNormedField 𝕜 then n else ω

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem isSubperm_iff {l₁ l₂ : List α} : l₁.isSubperm l₂ ↔ l₁ <+~ l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₁.isSubperm l₂ = true ↔ l₁ <+~ l₂

Tactic:
simp [isSubperm, subperm_ext_iff]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma lt_one_add_iff : m < 1 + n ↔ m ≤ n

Proof state:
m n : ℕ
⊢ m < 1 + n ↔ m ≤ n

Tactic:
simp only [Nat.add_comm, Nat.lt_succ_iff]

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
@[simp] lemma dens_eq_one : dens s = 1 ↔ s = univ

Proof state:
α : Type u_2
inst✝¹ : Fintype α
s : Finset α
inst✝ : Nonempty α
⊢ s.dens = 1 ↔ s = univ

Tactic:
simp [dens, div_eq_one_iff_eq, card_eq_iff_eq_univ]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem toPoly_eq_zero_iff (P : Cubic R) : P.toPoly = 0 ↔ P = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
P : Cubic R
⊢ P.toPoly = 0 ↔ P = 0

Tactic:
rw [← zero, toPoly_injective]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true

Proof state:
α : Type u_1
as : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ elem a (a :: as) = true

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/Verschiebung.lean
theorem verschiebungFun_coeff_zero (x : 𝕎 R) : (verschiebungFun x).coeff 0 = 0

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ x.verschiebungFun.coeff 0 = 0

Tactic:
rw [verschiebungFun_coeff, if_pos rfl]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem wOppSide_vadd_right_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
    s.WOppSide x (v +ᵥ y) ↔ s.WOppSide x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.WOppSide x (v +ᵥ y) ↔ s.WOppSide x y

Tactic:
rw [wOppSide_comm, wOppSide_vadd_left_iff hv, wOppSide_comm]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem add_pf_add_zero (a : R) : a + 0 = a

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a + 0 = a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_mul (a b c : Int) : (a + b) * c = a * c + b * c

Proof state:
a b c : Int
⊢ (a + b) * c = a * c + b * c

Tactic:
simp [Int.mul_comm, Int.mul_add]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isStrictlyGE_of_ge (p q : ℤ) (hpq : p ≤ q) [K.IsStrictlyGE q] :
    K.IsStrictlyGE p

Proof state:
case hi
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyGE q
i : ℤ
hi : i < p
⊢ i < q

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyGE q
i : ℤ
hi : i < p
⊢ IsZero (K.X i)

Tactic:
apply K.isZero_of_isStrictlyGE q

Result:
case hi
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyGE q
i : ℤ
hi : i < p
⊢ i < q

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyGE q
⊢ K.IsStrictlyGE p

Tactic:
rw [isStrictlyGE_iff]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyGE q
⊢ ∀ i < p, IsZero (K.X i)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyGE q
⊢ ∀ i < p, IsZero (K.X i)

Tactic:
intro i hi

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyGE q
i : ℤ
hi : i < p
⊢ IsZero (K.X i)
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_eq_of_trailingDegree_eq_some {p : R[X]} {n : ℕ}
    (h : trailingDegree p = n) : natTrailingDegree p = n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.trailingDegree = ↑n
⊢ p.natTrailingDegree = n

Tactic:
simp [natTrailingDegree, h]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
@[simp] lemma injOn_pair {b : α} : InjOn f {a, b} ↔ f a = f b → a = b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ (∀ ⦃x₁ : α⦄, x₁ ∈ {a, b} → ∀ ⦃x₂ : α⦄, x₂ ∈ {a, b} → f x₁ = f x₂ → x₁ = x₂) ↔ f a = f b → a = b

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ InjOn f {a, b} ↔ f a = f b → a = b

Tactic:
unfold InjOn

Result:
α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ (∀ ⦃x₁ : α⦄, x₁ ∈ {a, b} → ∀ ⦃x₂ : α⦄, x₂ ∈ {a, b} → f x₁ = f x₂ → x₁ = x₂) ↔ f a = f b → a = b
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem Filter.Tendsto.mul_atTop {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C))
    (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * g x) l atTop

Tactic:
simpa only [mul_comm] using hg.atTop_mul hC hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eq_true_of_not_eq_false {a : Prop} (h : (Not a) = False) : a = True

Proof state:
a : Prop
h : (¬a) = False
⊢ a = True

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean
@[to_additive]
lemma sSup_div : sSup (s / t) = sSup s / sInf t

Proof state:
M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
⊢ sSup (s / t) = sSup s / sInf t

Tactic:
simp_rw [div_eq_mul_inv, sSup_mul, sSup_inv]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem pow_card_eq_one : x ^ Fintype.card G = 1

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ x ^ card G = 1

Tactic:
rw [← Nat.card_eq_fintype_card, pow_card_eq_one']

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
lemma finsuppScalarLeft_apply (pn : (ι →₀ R) ⊗[R] N) (i : ι) :
    finsuppScalarLeft R N ι pn i = TensorProduct.lid R N ((Finsupp.lapply i).rTensor N pn)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
pn : (ι →₀ R) ⊗[R] N
i : ι
⊢ ((finsuppScalarLeft R N ι) pn) i = (TensorProduct.lid R N) ((rTensor N (Finsupp.lapply i)) pn)

Tactic:
simp [finsuppScalarLeft, finsuppLeft_apply]

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem FG.map {N : Type*} [L.Structure N] (f : M →[L] N) {s : L.Substructure M} (hs : s.FG) :
    (s.map f).FG :=
  let ⟨t, ht⟩ := fg_def.1 hs
  fg_def.2 ⟨f '' t, ht.1.image _, by rw [closure_image, ht.2]⟩

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M →[L] N
s : L.Substructure M
hs : s.FG
t : Set M
ht : t.Finite ∧ (closure L).toFun t = s
⊢ (closure L).toFun (⇑f '' t) = Substructure.map f s

Tactic:
rw [closure_image, ht.2]

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
lemma imaginaryPart_comp_subtype_selfAdjoint :
    imaginaryPart.comp (selfAdjoint.submodule ℝ A).subtype = 0

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
⊢ ℑ ∘ₗ (selfAdjoint.submodule ℝ A).subtype = 0

Tactic:
rw [imaginaryPart, LinearMap.comp_assoc, skewAdjointPart_comp_subtype_selfAdjoint,
  LinearMap.comp_zero]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma smul_sSup {R} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (s : Set ℝ≥0∞) (c : R) :
    c • sSup s = ⨆ a ∈ s, c • a

Proof state:
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
⊢ c • sSup s = ⨆ a ∈ s, c • a

Tactic:
simp_rw [← smul_one_mul c (sSup s), ENNReal.mul_sSup, smul_one_mul]

Result:
no goals
-- Mathlib/NumberTheory/GaussSum.lean
theorem MulChar.IsQuadratic.gaussSum_frob (hp : IsUnit (p : R)) {χ : MulChar R R'}
    (hχ : IsQuadratic χ) (ψ : AddChar R R') :
    gaussSum χ ψ ^ p = χ p * gaussSum χ ψ

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p = χ ↑p * gaussSum χ ψ

Tactic:
rw [_root_.gaussSum_frob, pow_mulShift, hχ.pow_char p, ← gaussSum_mulShift χ ψ hp.unit,
  ← mul_assoc, hp.unit_spec, ← pow_two, ← pow_apply' _ two_ne_zero, hχ.sq_eq_one, ← hp.unit_spec,
  one_apply_coe, one_mul]

Result:
no goals
-- Mathlib/Data/List/Map2.lean
theorem zipRight'_nil_left : zipRight' ([] : List α) bs = (bs.map fun b => (none, b), [])

Proof state:
α : Type u
β : Type v
bs : List β
⊢ [].zipRight' bs = (map (fun b => (none, b)) bs, [])

Tactic:
cases bs <;> rfl

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma formalMultilinearSeries_geometric_radius (𝕜 : Type*) [NontriviallyNormedField 𝕜]
    (A : Type*) [NormedRing A] [NormOneClass A] [NormedAlgebra 𝕜 A] :
    (formalMultilinearSeries_geometric 𝕜 A).radius = 1 :=
  formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
    FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto A _ one_ne_zero (by simp)

Proof state:
𝕜 : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormOneClass A
inst✝ : NormedAlgebra 𝕜 A
⊢ Tendsto (fun n => ‖1‖ / ‖1‖) atTop (𝓝 ↑1)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem RegularSpace.inf {X} {t₁ t₂ : TopologicalSpace X} (h₁ : @RegularSpace X t₁)
    (h₂ : @RegularSpace X t₂) : @RegularSpace X (t₁ ⊓ t₂)

Proof state:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : RegularSpace X
h₂ : RegularSpace X
⊢ RegularSpace X

Tactic:
exact regularSpace_iInf (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma sub_lt_iff_lt_add' (hba : b ≤ a) : a - b < c ↔ a < c + b

Proof state:
a b c : ℕ
hba : b ≤ a
⊢ a - b < c ↔ a < c + b

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Nat/Lattice.lean
theorem iInf_of_empty {ι : Sort*} [IsEmpty ι] (f : ι → ℕ) : iInf f = 0

Proof state:
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℕ
⊢ iInf f = 0

Tactic:
rw [iInf_of_isEmpty, sInf_empty]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem singleton_div_ball : {x} / ball y δ = ball (x / y) δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} / ball y δ = ball (x / y) δ

Tactic:
simp_rw [div_eq_mul_inv, inv_ball, singleton_mul_ball]

Result:
no goals
-- Mathlib/Data/Prod/TProd.lean
theorem elim_self (v : TProd α (i :: l)) : v.elim (l.mem_cons_self i) = v.1

Proof state:
ι : Type u
α : ι → Type v
i : ι
l : List ι
inst✝ : DecidableEq ι
v : TProd α (i :: l)
⊢ v.elim ⋯ = v.1

Tactic:
simp [TProd.elim]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem mem_span_singleton_mul {x y : R} {I : Ideal R} : x ∈ span {y} * I ↔ ∃ z ∈ I, y * z = x

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
I : Ideal R
⊢ x ∈ span {y} * I ↔ ∃ z ∈ I, y * z = x

Tactic:
simp only [mul_comm, mem_mul_span_singleton]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean
@[reassoc]
lemma map₂_hom_inv_isIso {f g : a ⟶ b} (η : f ⟶ g) [IsIso η] :
    F.map₂ η ≫ F.map₂ (inv η) = 𝟙 (F.map f)

Proof state:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst✝ : IsIso η
⊢ F.map₂ η ≫ F.map₂ (inv η) = 𝟙 (F.map f)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem union_mem_iff : s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f

Proof state:
α : Type u
f : Ultrafilter α
s t : Set α
⊢ s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f

Tactic:
simp only [← mem_coe, ← le_principal_iff, ← sup_principal, le_sup_iff]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem invOneSubPow_inv_zero_eq_one : (invOneSubPow S 0).inv = 1

Proof state:
S : Type u_1
inst✝ : CommRing S
⊢ (invOneSubPow S 0).inv = 1

Tactic:
delta invOneSubPow

Result:
S : Type u_1
inst✝ : CommRing S
⊢ (match 0 with
      | 0 => 1
      | d.succ =>
        { val := mk fun n => ↑((d + n).choose d), inv := (1 - X) ^ (d + 1), val_inv := ⋯, inv_val := ⋯ }).inv =
    1

Proof state:
S : Type u_1
inst✝ : CommRing S
⊢ (match 0 with
      | 0 => 1
      | d.succ =>
        { val := mk fun n => ↑((d + n).choose d), inv := (1 - X) ^ (d + 1), val_inv := ⋯, inv_val := ⋯ }).inv =
    1

Tactic:
simp only [Units.inv_eq_val_inv, inv_one, Units.val_one]

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem orderEmbOfFin_zero {s : Finset α} {k : ℕ} (h : s.card = k) (hz : 0 < k) :
    orderEmbOfFin s h ⟨0, hz⟩ = s.min' (card_pos.mp (h.symm ▸ hz))

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
hz : 0 < k
⊢ (s.orderEmbOfFin h) ⟨0, hz⟩ = s.min' ⋯

Tactic:
simp only [orderEmbOfFin_apply, Fin.getElem_fin, sorted_zero_eq_min']

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem nnreal_smul_coe_apply {_m : MeasurableSpace α} (c : ℝ≥0) (μ : Measure α) (s : Set α) :
    c • μ s = c * μ s

Proof state:
α : Type u_1
_m : MeasurableSpace α
c : ℝ≥0
μ : Measure α
s : Set α
⊢ c • μ s = ↑c * μ s

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_iff' {s : Set E} :
    Bornology.IsVonNBounded 𝕜 s ↔ ∃ r : ℝ, ∀ x ∈ s, ‖x‖ ≤ r

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ r, ∀ x ∈ s, ‖x‖ ≤ r

Tactic:
rw [NormedSpace.isVonNBounded_iff, isBounded_iff_forall_norm_le]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem toZNum_inj {m n : Num} : m.toZNum = n.toZNum ↔ m = n :=
  ⟨fun h => by cases m <;> cases n <;> cases h <;> rfl, congr_arg _⟩

Proof state:
m n : Num
h : m.toZNum = n.toZNum
⊢ m = n

Tactic:
cases m <;> cases n <;> cases h <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Closed.lean
theorem isClosed_pullback {X Y : C} (f : Y ⟶ X) (S : Sieve X) :
    J₁.IsClosed S → J₁.IsClosed (S.pullback f) :=
  fun hS Z g hg => hS (g ≫ f) (by rwa [J₁.covers_iff, Sieve.pullback_comp])

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
hS : J₁.IsClosed S
Z : C
g : Z ⟶ Y
hg : J₁.Covers (Sieve.pullback f S) g
⊢ J₁.Covers S (g ≫ f)

Tactic:
rwa [J₁.covers_iff, Sieve.pullback_comp]

Result:
no goals
-- Mathlib/GroupTheory/Submonoid/Inverses.lean
theorem fromLeftInv_eq_iff (a : S.leftInv) (b : M) :
    (S.fromLeftInv a : M) = b ↔ (a : M) * b = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S.leftInv
b : M
⊢ ↑(S.fromLeftInv a) = b ↔ ↑a * b = 1

Tactic:
rw [← IsUnit.mul_right_inj (leftInv_le_isUnit _ a.prop), S.mul_fromLeftInv, eq_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/CompareExp.lean
theorem isLittleO_exp_cpow (hl : IsExpCmpFilter l) (a : ℂ) {b : ℝ} (hb : b < 0) :
    (fun z => exp (b * z)) =o[l] fun z => z ^ a

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : b < 0
⊢ (fun z => cexp (↑b * z)) =o[l] fun z => z ^ a

Tactic:
simpa using hl.isLittleO_cpow_mul_exp hb 0 a

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem inv {f : Perm α} (h : IsThreeCycle f) : IsThreeCycle f⁻¹

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
h : f.IsThreeCycle
⊢ f⁻¹.IsThreeCycle

Tactic:
rwa [IsThreeCycle, cycleType_inv]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem coe_iSup_eq {ι : Sort*} {p : ι → Seminorm 𝕜 E} (hp : BddAbove (range p)) :
    ↑(⨆ i, p i) = ⨆ i, ((p i : Seminorm 𝕜 E) : E → ℝ)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
⊢ ⨆ p_1, ⇑↑p_1 = ⨆ i, ⇑(p i)

Tactic:
exact iSup_range' (fun p : Seminorm 𝕜 E => (p : E → ℝ)) p

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
⊢ ⇑(⨆ i, p i) = ⨆ i, ⇑(p i)

Tactic:
rw [← sSup_range, Seminorm.coe_sSup_eq hp]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
⊢ ⨆ p_1, ⇑↑p_1 = ⨆ i, ⇑(p i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem toNat_eq_one  {b : Bool} : b.toNat = 1 ↔ b = true

Proof state:
b : Bool
⊢ b.toNat = 1 ↔ b = true

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/UInt/Lemmas.lean
theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n → m < n.toNat

Proof state:
n : UInt32
m : Nat
h : m < size
⊢ ofNat m < n → m < n.toNat

Tactic:
simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem mem_lpMeas_iff_aeStronglyMeasurable {m m0 : MeasurableSpace α} {μ : Measure α}
    {f : Lp F p μ} : f ∈ lpMeas F 𝕜 m p μ ↔ AEStronglyMeasurable[m] f μ

Proof state:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
⊢ f ∈ lpMeas F 𝕜 m p μ ↔ AEStronglyMeasurable (↑↑f) μ

Tactic:
rw [← SetLike.mem_coe, ← Submodule.mem_carrier, lpMeas, Set.mem_setOf_eq]

Result:
no goals