harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_one (a : Ordinal) : a ^ (1 : Ordinal) = a

Proof state:
a : Ordinal.{u_1}
⊢ a ^ 0 * a = a

Tactic:
simp only [opow_zero, one_mul]

Result:
no goals

Proof state:
a : Ordinal.{u_1}
⊢ a ^ 1 = a

Tactic:
rw [← succ_zero, opow_succ]

Result:
a : Ordinal.{u_1}
⊢ a ^ 0 * a = a
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem isUnit_nonsing_inv_iff {A : Matrix n n α} : IsUnit A⁻¹ ↔ IsUnit A

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ IsUnit A⁻¹ ↔ IsUnit A

Tactic:
simp_rw [isUnit_iff_isUnit_det, isUnit_nonsing_inv_det_iff]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem subOneIntegralPowerBasis_gen_prime [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) :
    Prime hζ.subOneIntegralPowerBasis.gen

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
⊢ Prime hζ.subOneIntegralPowerBasis.gen

Tactic:
simpa only [subOneIntegralPowerBasis_gen] using hζ.zeta_sub_one_prime

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem realize_boundedFormula_top {α : Type*} {n : ℕ} {φ : L.BoundedFormula α n}
    {v : α → (⊤ : L.Substructure M)} {xs : Fin n → (⊤ : L.Substructure M)} :
    φ.Realize v xs ↔ φ.Realize (((↑) : _ → M) ∘ v) ((↑) ∘ xs)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u_3
n : ℕ
φ : L.BoundedFormula α n
v : α → ↥⊤
xs : Fin n → ↥⊤
⊢ φ.Realize v xs ↔ φ.Realize (Subtype.val ∘ v) (Subtype.val ∘ xs)

Tactic:
rw [← StrongHomClass.realize_boundedFormula Substructure.topEquiv φ]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u_3
n : ℕ
φ : L.BoundedFormula α n
v : α → ↥⊤
xs : Fin n → ↥⊤
⊢ φ.Realize (⇑topEquiv ∘ v) (⇑topEquiv ∘ xs) ↔ φ.Realize (Subtype.val ∘ v) (Subtype.val ∘ xs)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u_3
n : ℕ
φ : L.BoundedFormula α n
v : α → ↥⊤
xs : Fin n → ↥⊤
⊢ φ.Realize (⇑topEquiv ∘ v) (⇑topEquiv ∘ xs) ↔ φ.Realize (Subtype.val ∘ v) (Subtype.val ∘ xs)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem flip (n ν : ℕ) (h : ν ≤ n) :
    (bernsteinPolynomial R n ν).comp (1 - X) = bernsteinPolynomial R n (n - ν)

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ (bernsteinPolynomial R n ν).comp (1 - X) = bernsteinPolynomial R n (n - ν)

Tactic:
simp [bernsteinPolynomial, h, tsub_tsub_assoc, mul_right_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_some_get [LawfulBEq α] (h : m.WF) {a : α} {h} : m.get? a = some (m.get a h)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h✝ : m.WF
a : α
h : a ∈ m
⊢ m.get? a = some (m.get a h)

Tactic:
simp_to_raw using Raw₀.get?_eq_some_get

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.contains a = (get? m a).isSome

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
⊢ m.contains a = (get? m a).isSome

Tactic:
simp_to_raw using Raw₀.Const.contains_eq_isSome_get?

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem normSq_natCast (n : ℕ) : normSq (n : ℍ[R]) = (n : R) ^ 2

Proof state:
R : Type u_3
inst✝ : CommRing R
n : ℕ
⊢ normSq ↑n = ↑n ^ 2

Tactic:
rw [← coe_natCast, normSq_coe]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degrees_def [DecidableEq σ] (p : MvPolynomial σ R) :
    p.degrees = p.support.sup fun s : σ →₀ ℕ => Finsupp.toMultiset s

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ (p.support.sup fun s => toMultiset s) = p.support.sup fun s => toMultiset s

Tactic:
convert rfl

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ p.degrees = p.support.sup fun s => toMultiset s

Tactic:
rw [degrees]

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ (p.support.sup fun s => toMultiset s) = p.support.sup fun s => toMultiset s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_flatMap_eq_none_iff {xs : Array α} {f : α → Array β} {p : β → Bool} :
    (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y

Proof state:
α : Type u_1
β : Type u_2
xs : Array α
f : α → Array β
p : β → Bool
⊢ find? p (flatMap f xs) = none ↔ ∀ (x : α), x ∈ xs → ∀ (y : β), y ∈ f x → (!p y) = true

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_sSup (s : Set ℝ≥0∞) (hf : ∀ r ∈ s, r ≠ ∞) :
    (sSup s).toReal = sSup (ENNReal.toReal '' s)

Proof state:
s : Set ℝ≥0∞
hf : ∀ r ∈ s, r ≠ ⊤
⊢ (sSup s).toReal = sSup (ENNReal.toReal '' s)

Tactic:
simp only [ENNReal.toReal, toNNReal_sSup s hf, NNReal.coe_sSup, Set.image_image]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Trim.lean
theorem restrict_trim (hm : m ≤ m0) (μ : Measure α) (hs : @MeasurableSet α m s) :
    @Measure.restrict α m (μ.trim hm) s = (μ.restrict s).trim hm

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
⊢ (μ.trim hm).restrict s = (μ.restrict s).trim hm

Tactic:
refine @Measure.ext _ m _ _ (fun t ht => ?_)

Result:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ((μ.trim hm).restrict s) t = ((μ.restrict s).trim hm) t

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ((μ.trim hm).restrict s) t = ((μ.restrict s).trim hm) t

Tactic:
rw [@Measure.restrict_apply α m _ _ _ ht, trim_measurableSet_eq hm ht,
  Measure.restrict_apply (hm t ht),
  trim_measurableSet_eq hm (@MeasurableSet.inter α m t s ht hs)]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem dense_pi {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] {s : ∀ i, Set (α i)}
    (I : Set ι) (hs : ∀ i ∈ I, Dense (s i)) : Dense (pi I s)

Proof state:
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
s : (i : ι) → Set (α i)
I : Set ι
hs : ∀ i ∈ I, Dense (s i)
⊢ Dense (I.pi s)

Tactic:
simp only [dense_iff_closure_eq, closure_pi_set, pi_congr rfl fun i hi => (hs i hi).closure_eq,
  pi_univ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem X_pow_eq_monomial (n) : X ^ n = monomial n (1 : R)

Proof state:
case succ
R : Type u
inst✝ : Semiring R
n : ℕ
hn : X ^ n = (monomial n) 1
⊢ X ^ (n + 1) = (monomial (n + 1)) 1

Tactic:
rw [pow_succ, hn, X, monomial_mul_monomial, one_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ X ^ n = (monomial n) 1

Tactic:
induction n with
| zero => rw [pow_zero, monomial_zero_one]
| succ n hn => rw [pow_succ, hn, X, monomial_mul_monomial, one_mul]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
⊢ X ^ 0 = (monomial 0) 1

Tactic:
rw [pow_zero, monomial_zero_one]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Module.lean
theorem IsInternal.collectedBasis_mem (h : IsInternal A) {α : ι → Type*}
    (v : ∀ i, Basis (α i) R (A i)) (a : Σi, α i) : h.collectedBasis v a ∈ A a.1

Proof state:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
a : (i : ι) × α i
⊢ (h.collectedBasis v) a ∈ A a.fst

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
@[simp]
lemma dual_zero :
    dual A K (0 : FractionalIdeal B⁰ L) = 0

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ dual A K 0 = 0

Tactic:
rw [dual, dif_pos rfl]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem piecewise_univ [∀ i : α, Decidable (i ∈ (Set.univ : Set α))] :
    piecewise Set.univ f g = f

Proof state:
case h
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ univ)
i : α
⊢ univ.piecewise f g i = f i

Tactic:
simp [piecewise]

Result:
no goals

Proof state:
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ univ)
⊢ univ.piecewise f g = f

Tactic:
ext i

Result:
case h
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ univ)
i : α
⊢ univ.piecewise f g i = f i
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem gcd_union [DecidableEq β] : (s₁ ∪ s₂).gcd f = GCDMonoid.gcd (s₁.gcd f) (s₂.gcd f) :=
  Finset.induction_on s₁ (by rw [empty_union, gcd_empty, gcd_zero_left, normalize_gcd])
    fun a s _ ih ↦ by rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ (∅ ∪ s₂).gcd f = GCDMonoid.gcd (∅.gcd f) (s₂.gcd f)

Tactic:
rw [empty_union, gcd_empty, gcd_zero_left, normalize_gcd]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : a ∉ s
ih : (s ∪ s₂).gcd f = GCDMonoid.gcd (s.gcd f) (s₂.gcd f)
⊢ (insert a s ∪ s₂).gcd f = GCDMonoid.gcd ((insert a s).gcd f) (s₂.gcd f)

Tactic:
rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_diff' (s : Set α) (hm : NullMeasurableSet t μ) (h_fin : μ t ≠ ∞) :
    μ (s \ t) = μ (s ∪ t) - μ t :=
  ENNReal.eq_sub_of_add_eq h_fin <| by rw [add_comm, measure_add_diff hm, union_comm]

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
hm : NullMeasurableSet t μ
h_fin : μ t ≠ ⊤
⊢ μ (s \ t) + μ t = μ (s ∪ t)

Tactic:
rw [add_comm, measure_add_diff hm, union_comm]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem IsHilbertSum.mk [∀ i, CompleteSpace <| G i] (hVortho : OrthogonalFamily 𝕜 G V)
    (hVtotal : ⊤ ≤ (⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure) :
    IsHilbertSum 𝕜 G V :=
  { OrthogonalFamily := hVortho
    surjective_isometry

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
inst✝ : ∀ (i : ι), CompleteSpace (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : ⊤ ≤ (⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure
⊢ Function.Surjective ⇑hVortho.linearIsometry.toLinearMap

Tactic:
exact LinearMap.range_eq_top.mp
  (eq_top_iff.mpr <| hVtotal.trans_eq hVortho.range_linearIsometry.symm)

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
inst✝ : ∀ (i : ι), CompleteSpace (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : ⊤ ≤ (⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure
⊢ Function.Surjective ⇑hVortho.linearIsometry

Tactic:
rw [← LinearIsometry.coe_toLinearMap]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
inst✝ : ∀ (i : ι), CompleteSpace (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : ⊤ ≤ (⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure
⊢ Function.Surjective ⇑hVortho.linearIsometry.toLinearMap
-- Mathlib/Data/Finset/Card.lean
lemma card_inter (s t : Finset α) : #(s ∩ t) = #s + #t - #(s ∪ t)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∩ t) = #s + #t - #(s ∪ t)

Tactic:
rw [← card_inter_add_card_union, Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one (B : E →L[𝕜] F →L[𝕜] G)
    {f : D → E} {g : D → F} {N : WithTop ℕ∞} (hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g)
    (x : D) {n : ℕ} (hn : n ≤ N) (hB : ‖B‖ ≤ 1) :
    ‖iteratedFDeriv 𝕜 n (fun y => B (f y) (g y)) x‖ ≤
      ∑ i ∈ Finset.range (n + 1),
        (n.choose i : ℝ) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : WithTop ℕ∞
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : D
n : ℕ
hn : ↑n ≤ N
hB : ‖B‖ ≤ 1
⊢ ‖iteratedFDeriv 𝕜 n (fun y => (B (f y)) (g y)) x‖ ≤
    ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Tactic:
simp_rw [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : WithTop ℕ∞
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : D
n : ℕ
hn : ↑n ≤ N
hB : ‖B‖ ≤ 1
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) univ x‖ ≤
    ∑ x_1 ∈ Finset.range (n + 1),
      ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f univ x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g univ x‖

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : WithTop ℕ∞
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : D
n : ℕ
hn : ↑n ≤ N
hB : ‖B‖ ≤ 1
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) univ x‖ ≤
    ∑ x_1 ∈ Finset.range (n + 1),
      ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f univ x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g univ x‖

Tactic:
exact B.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one hf.contDiffOn hg.contDiffOn
  uniqueDiffOn_univ (mem_univ x) hn hB

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem min'_eq_sorted_zero {s : Finset α} {h : s.Nonempty} :
    s.min' h = (s.sort (· ≤ ·))[0]'(by rw [length_sort]; exact card_pos.2 h) :=
  (sorted_zero_eq_min'_aux _ _ _).symm

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ 0 < (sort (fun x1 x2 => x1 ≤ x2) s).length

Tactic:
rw [length_sort]

Result:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ 0 < #s

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ 0 < #s

Tactic:
exact card_pos.2 h

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_smul (p : Seminorm 𝕜 E) {c : NNReal} (hc : 0 < c) (r : ℝ) (x : E) :
    (c • p).closedBall x r = p.closedBall x (r / c)

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x✝ : E
⊢ x✝ ∈ (c • p).closedBall x r ↔ x✝ ∈ p.closedBall x (r / ↑c)

Tactic:
rw [mem_closedBall, mem_closedBall, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
  le_div_iff₀ (NNReal.coe_pos.mpr hc)]

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x : E
⊢ (c • p).closedBall x r = p.closedBall x (r / ↑c)

Tactic:
ext

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x✝ : E
⊢ x✝ ∈ (c • p).closedBall x r ↔ x✝ ∈ p.closedBall x (r / ↑c)
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_lt_self_iff (a : α) {b : α} : a / b < a ↔ 1 < b

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b : α
⊢ a / b < a ↔ 1 < b

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem appendList_nil (arr : Array α) : arr ++ ([] : List α) = arr := Array.ext' (by simp)

Proof state:
α : Type u_1
arr : Array α
⊢ (arr ++ []).toList = arr.toList

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_of_ZFSet (A : Class.{u}) (x : ZFSet.{u}) : ToSet A x ↔ A x :=
  ⟨fun ⟨y, yx, py⟩ => by rwa [ofSet.inj yx] at py, fun px => ⟨x, rfl, px⟩⟩

Proof state:
A : Class.{u}
x : ZFSet.{u}
x✝ : A.ToSet ↑x
y : ZFSet.{u}
yx : ↑y = ↑x
py : A y
⊢ A x

Tactic:
rwa [ofSet.inj yx] at py

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Ordered.setBlack {t : RBNode α} : (setBlack t).Ordered cmp ↔ t.Ordered cmp

Proof state:
α : Type u_1
cmp : α → α → Ordering
t : RBNode α
⊢ Ordered cmp
      (match t with
      | nil => nil
      | node c l v r => node black l v r) ↔
    Ordered cmp t

Tactic:
split <;> simp [Ordered]

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
t : RBNode α
⊢ Ordered cmp t.setBlack ↔ Ordered cmp t

Tactic:
unfold setBlack

Result:
α : Type u_1
cmp : α → α → Ordering
t : RBNode α
⊢ Ordered cmp
      (match t with
      | nil => nil
      | node c l v r => node black l v r) ↔
    Ordered cmp t
-- Mathlib/Combinatorics/SimpleGraph/Girth.lean
@[simp]
lemma le_egirth {n : ℕ∞} : n ≤ G.egirth ↔ ∀ a (w : G.Walk a a), w.IsCycle → n ≤ w.length

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ∞
⊢ n ≤ G.egirth ↔ ∀ (a : α) (w : G.Walk a a), w.IsCycle → n ≤ ↑w.length

Tactic:
simp [egirth]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJ0_c₄ : (ofJ0 R).c₄ = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂) ^
        2 -
      24 *
        (2 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ +
          { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃) =
    0

Tactic:
norm_num1

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ (ofJ0 R).c₄ = 0

Tactic:
rw [ofJ0, c₄, b₂, b₄]

Result:
R : Type u_1
inst✝ : CommRing R
⊢ ({ a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₂) ^
        2 -
      24 *
        (2 * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₄ +
          { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₁ * { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }.a₃) =
    0
-- Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean
lemma opEquiv'_apply {a' : ℤ} (f : ShiftedHom X Y a') (n a : ℤ) (h : n + a = a') :
    opEquiv' n a a' h f =
      opEquiv n (f ≫ (shiftFunctorAdd' C a n a' (by omega)).hom.app Y)

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.55292, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a' : ℤ
f : ShiftedHom X Y a'
n a : ℤ
h : n + a = a'
⊢ a + n = a'

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a' : ℤ
f : ShiftedHom X Y a'
n a : ℤ
h : n + a = a'
⊢ (opEquiv' n a a' h) f = (opEquiv n) (f ≫ (shiftFunctorAdd' C a n a' ⋯).hom.app Y)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_zero (n : Nat) : n / 0 = 0

Proof state:
n : Nat
⊢ ite (0 < 0 ∧ 0 ≤ n) ((n - 0) / 0 + 1) 0 = 0

Tactic:
simp [Nat.lt_irrefl]

Result:
no goals

Proof state:
n : Nat
⊢ n / 0 = 0

Tactic:
rw [div_eq]

Result:
n : Nat
⊢ ite (0 < 0 ∧ 0 ≤ n) ((n - 0) / 0 + 1) 0 = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
theorem Liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [Entails α σ1] [Entails α σ2]
    (f1 : σ1) (f2 : σ2) :
    Liff α f1 f2 → Liff α f2 f1

Proof state:
α : Type u
σ1 : Type v
σ2 : Type 2
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
⊢ Liff α f1 f2 → Liff α f2 f1

Tactic:
intros h p

Result:
α : Type u
σ1 : Type v
σ2 : Type 2
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : Liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 ↔ p ⊨ f1

Proof state:
α : Type u
σ1 : Type v
σ2 : Type 2
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : Liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 ↔ p ⊨ f1

Tactic:
rw [h p]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get_range' {n m step} (i) (H : i < (range' n m step).length) :
    get (range' n m step) ⟨i, H⟩ = n + step * i

Proof state:
n m step i : Nat
H : i < (range' n m step).length
⊢ (range' n m step).get ⟨i, H⟩ = n + step * i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Finite.lean
theorem card_le_one_iff_eq_bot [Finite H] : Nat.card H ≤ 1 ↔ H = ⊥ :=
  ⟨H.eq_bot_of_card_le, fun h => by simp [h]⟩

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↥H
h : H = ⊥
⊢ Nat.card ↥H ≤ 1

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_singleton' {f : α → ℝ≥0∞} (hf : Measurable f) (a : α) :
    ∫⁻ x in {a}, f x ∂μ = f a * μ {a}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∫⁻ (x : α) in {a}, f x ∂μ = f a * μ {a}

Tactic:
simp only [restrict_singleton, lintegral_smul_measure, lintegral_dirac' _ hf, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) :
    Array.zipWith f as.toArray bs.toArray = (List.zipWith f as bs).toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
⊢ Array.zipWith f as.toArray bs.toArray = (zipWith f as bs).toArray

Tactic:
rw [Array.zipWith]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
⊢ as.toArray.zipWithAux bs.toArray f 0 #[] = (zipWith f as bs).toArray

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
⊢ as.toArray.zipWithAux bs.toArray f 0 #[] = (zipWith f as bs).toArray

Tactic:
simp [zipWithAux_toArray_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
theorem pullback_symmetry_hom_of_epi_eq : (pushoutSymmetry f f).hom = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ (pushoutSymmetry f f).hom = 𝟙 (pushout f f)

Tactic:
ext <;> simp [inl_eq_inr_of_epi_eq]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem compl_le_compl_iff_le : yᶜ ≤ xᶜ ↔ x ≤ y :=
  ⟨fun h => by have h := compl_le_compl h; simpa using h, compl_le_compl⟩

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h✝ : yᶜ ≤ xᶜ
h : xᶜᶜ ≤ yᶜᶜ
⊢ x ≤ y

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : yᶜ ≤ xᶜ
⊢ x ≤ y

Tactic:
have h := compl_le_compl h

Result:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h✝ : yᶜ ≤ xᶜ
h : xᶜᶜ ≤ yᶜᶜ
⊢ x ≤ y