harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma HasFPowerSeriesAt.restrictScalars (hf : HasFPowerSeriesAt f p x) :
    HasFPowerSeriesAt f (p.restrictScalars 𝕜) x

Proof state:
case intro
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) x

Tactic:
exact ⟨r, hr.restrictScalars⟩

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
hf : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) x

Tactic:
rcases hf with ⟨r, hr⟩

Result:
case intro
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) x
-- Mathlib/Order/SuccPred/Limit.lean
theorem isPredLimit_iff [OrderTop α] : IsPredLimit a ↔ a ≠ ⊤ ∧ IsPredPrelimit a

Proof state:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ IsPredLimit a ↔ a ≠ ⊤ ∧ IsPredPrelimit a

Tactic:
rw [IsPredLimit, isMax_iff_eq_top]

Result:
no goals
-- Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
/-- A map from ℝⁿ to X is continuous iff it is continuous regarding the
  delta-generated topology on X. Outside of this file, use the more general
  `continuous_to_deltaGenerated` instead. -/
private lemma continuous_euclidean_to_deltaGenerated {n : ℕ} {f : (Fin n → ℝ) → X} :
    Continuous[_, deltaGenerated X] f ↔ Continuous f

Proof state:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
⊢ coinduced f Pi.topologicalSpace ≤ deltaGenerated X ↔ coinduced f Pi.topologicalSpace ≤ tX

Tactic:
refine ⟨fun h ↦ h.trans deltaGenerated_le, fun h ↦ ?_⟩

Result:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
h : coinduced f Pi.topologicalSpace ≤ tX
⊢ coinduced f Pi.topologicalSpace ≤ deltaGenerated X

Proof state:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
h : coinduced f Pi.topologicalSpace ≤ tX
⊢ coinduced f Pi.topologicalSpace ≤ ⨆ f, coinduced (⇑f.snd) inferInstance

Tactic:
exact le_iSup_of_le (i := ⟨n, f, continuous_iff_coinduced_le.mpr h⟩) le_rfl

Result:
no goals

Proof state:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
⊢ Continuous f ↔ Continuous f

Tactic:
simp_rw [continuous_iff_coinduced_le]

Result:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
⊢ coinduced f Pi.topologicalSpace ≤ deltaGenerated X ↔ coinduced f Pi.topologicalSpace ≤ tX

Proof state:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
h : coinduced f Pi.topologicalSpace ≤ tX
⊢ coinduced f Pi.topologicalSpace ≤ deltaGenerated X

Tactic:
simp_rw [deltaGenerated]

Result:
X : Type u_1
tX : TopologicalSpace X
n : ℕ
f : (Fin n → ℝ) → X
h : coinduced f Pi.topologicalSpace ≤ tX
⊢ coinduced f Pi.topologicalSpace ≤ ⨆ f, coinduced (⇑f.snd) inferInstance
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_submatrix_le [StrongRankCondition R] [Fintype m] (f : n → m) (e : n ≃ m)
    (A : Matrix m m R) : rank (A.submatrix f e) ≤ rank A

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype m
f : n → m
e : n ≃ m
A : Matrix m m R
⊢ finrank R ↥(Submodule.map (LinearMap.funLeft R R f) (LinearMap.range A.mulVecLin)) ≤
    finrank R ↥(LinearMap.range A.mulVecLin)

Tactic:
exact Submodule.finrank_map_le _ _

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype m
f : n → m
e : n ≃ m
A : Matrix m m R
⊢ (A.submatrix f ⇑e).rank ≤ A.rank

Tactic:
rw [rank, rank, mulVecLin_submatrix, LinearMap.range_comp, LinearMap.range_comp,
  show LinearMap.funLeft R R e.symm = LinearEquiv.funCongrLeft R R e.symm from rfl,
  LinearEquiv.range, Submodule.map_top]

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype m
f : n → m
e : n ≃ m
A : Matrix m m R
⊢ finrank R ↥(Submodule.map (LinearMap.funLeft R R f) (LinearMap.range A.mulVecLin)) ≤
    finrank R ↥(LinearMap.range A.mulVecLin)
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem noAtoms_hausdorff {d : ℝ} (hd : 0 < d) : NoAtoms (hausdorffMeasure d : Measure X)

Proof state:
case refine_3
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
x✝ : 0 < ε
⊢ ∑' (n : ℕ), ⨆ (_ : ((fun x_1 => {x}) n).Nonempty), diam ((fun x_2 => {x}) n) ^ d ≤ 0

Tactic:
simp [hd]

Result:
no goals

Proof state:
case refine_2
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
x✝¹ : 0 < ε
x✝ : ℕ
⊢ diam ((fun x_1 => {x}) x✝) ≤ ε

Tactic:
simp only [EMetric.diam_singleton, zero_le]

Result:
no goals

Proof state:
case refine_1
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
x✝ : 0 < ε
⊢ {x} ⊆ ⋃ n, (fun x_1 => {x}) n

Tactic:
exact subset_iUnion (fun _ => {x} : ℕ → Set X) 0

Result:
no goals

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : {x} ⊆ ⋃ n, t n),
            ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤
    0

Tactic:
refine iSup₂_le fun ε _ => iInf₂_le_of_le (fun _ => {x}) ?_ <| iInf_le_of_le (fun _ => ?_) ?_

Result:
case refine_1
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
x✝ : 0 < ε
⊢ {x} ⊆ ⋃ n, (fun x_1 => {x}) n

case refine_2
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
x✝¹ : 0 < ε
x✝ : ℕ
⊢ diam ((fun x_1 => {x}) x✝) ≤ ε

case refine_3
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
x✝ : 0 < ε
⊢ ∑' (n : ℕ), ⨆ (_ : ((fun x_1 => {x}) n).Nonempty), diam ((fun x_2 => {x}) n) ^ d ≤ 0

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
⊢ μH[d] {x} = 0

Tactic:
rw [← nonpos_iff_eq_zero, hausdorffMeasure_apply]

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : {x} ⊆ ⋃ n, t n),
            ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤
    0

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
⊢ NoAtoms μH[d]

Tactic:
refine ⟨fun x => ?_⟩

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
⊢ μH[d] {x} = 0
-- Mathlib/Data/FinEnum.lean
theorem mem_toList [FinEnum α] (x : α) : x ∈ toList α

Proof state:
α : Type u
inst✝ : FinEnum α
x : α
⊢ ∃ a, equiv.symm a = x

Tactic:
exists equiv x

Result:
α : Type u
inst✝ : FinEnum α
x : α
⊢ equiv.symm (equiv x) = x

Proof state:
α : Type u
inst✝ : FinEnum α
x : α
⊢ equiv.symm (equiv x) = x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : FinEnum α
x : α
⊢ x ∈ toList α

Tactic:
simp [toList]

Result:
α : Type u
inst✝ : FinEnum α
x : α
⊢ ∃ a, equiv.symm a = x
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eq_conj_eqToHom {X Y : C} (f : X ⟶ Y) : f = eqToHom rfl ≫ f ≫ eqToHom rfl

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ f = eqToHom ⋯ ≫ f ≫ eqToHom ⋯

Tactic:
simp only [Category.id_comp, eqToHom_refl, Category.comp_id]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem coeff_zero_eq_eval_zero (p : R[X]) : coeff p 0 = p.eval 0 :=
  calc
    coeff p 0 = coeff p 0 * 0 ^ 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ eval 0 p = p.coeff 0 * 0 ^ 0

Tactic:
rw [eval_eq_sum]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun e a => a * 0 ^ e) = p.coeff 0 * 0 ^ 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun e a => a * 0 ^ e) = p.coeff 0 * 0 ^ 0

Tactic:
exact Finset.sum_eq_single _ (fun b _ hb => by simp [zero_pow hb]) (by simp)

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeff 0 = p.coeff 0 * 0 ^ 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
b : ℕ
x✝ : b ∈ p.support
hb : b ≠ 0
⊢ (fun e a => a * 0 ^ e) b (p.coeff b) = 0

Tactic:
simp [zero_pow hb]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ 0 ∉ p.support → (fun e a => a * 0 ^ e) 0 (p.coeff 0) = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeff 0 * 0 ^ 0 = eval 0 p

Tactic:
symm

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ eval 0 p = p.coeff 0 * 0 ^ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem set_append_right {s : Vector α n} {t : Vector α m} {i : Nat} {x : α}
    (h' : i < n + m) (h : n ≤ i) :
    (s ++ t).set i x = s ++ t.set (i - n) x

Proof state:
α : Type u_1
n m : Nat
s : Vector α n
t : Vector α m
i : Nat
x : α
h' : i < n + m
h : n ≤ i
⊢ (s ++ t).set i x h' = s ++ t.set (i - n) x ⋯

Tactic:
rw [set_append, dif_neg (by omega)]

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
s : Vector α n
t : Vector α m
i : Nat
x : α
h' : i < n + m
h : n ≤ i
⊢ ¬i < n

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem hasGradientWithinAt_univ : HasGradientWithinAt f f' univ x ↔ HasGradientAt f f' x

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
f' x : F
⊢ HasFDerivWithinAt f ((toDual 𝕜 F) f') univ x ↔ HasFDerivAt f ((toDual 𝕜 F) f') x

Tactic:
exact hasFDerivWithinAt_univ

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
f' x : F
⊢ HasGradientWithinAt f f' univ x ↔ HasGradientAt f f' x

Tactic:
rw [hasGradientWithinAt_iff_hasFDerivWithinAt, hasGradientAt_iff_hasFDerivAt]

Result:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
f' x : F
⊢ HasFDerivWithinAt f ((toDual 𝕜 F) f') univ x ↔ HasFDerivAt f ((toDual 𝕜 F) f') x
-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
lemma homEquiv_extendScalarsId (M : ModuleCat R) :
    (extendRestrictScalarsAdj (RingHom.id R)).homEquiv _ _ ((extendScalarsId R).hom.app M) =
      (restrictScalarsId R).inv.app M

Proof state:
case hf.h
R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom ((extendScalarsId R).inv.app M ≫ (extendScalarsId R).hom.app M)) m =
    (Hom.hom ((restrictScalarsId R).inv.app M)) m

Tactic:
simp

Result:
no goals

Proof state:
case hf.h
R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (Hom.hom
        (((extendRestrictScalarsAdj (RingHom.id R)).homEquiv M ((𝟭 (ModuleCat R)).obj M))
          ((extendScalarsId R).hom.app M)))
      m =
    (Hom.hom ((restrictScalarsId R).inv.app M)) m

Tactic:
rw [extendRestrictScalarsAdj_homEquiv_apply, ← extendScalarsId_inv_app_apply, ← comp_apply]

Result:
case hf.h
R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom ((extendScalarsId R).inv.app M ≫ (extendScalarsId R).hom.app M)) m =
    (Hom.hom ((restrictScalarsId R).inv.app M)) m

Proof state:
R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
⊢ ((extendRestrictScalarsAdj (RingHom.id R)).homEquiv M ((𝟭 (ModuleCat R)).obj M)) ((extendScalarsId R).hom.app M) =
    (restrictScalarsId R).inv.app M

Tactic:
ext m

Result:
case hf.h
R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (Hom.hom
        (((extendRestrictScalarsAdj (RingHom.id R)).homEquiv M ((𝟭 (ModuleCat R)).obj M))
          ((extendScalarsId R).hom.app M)))
      m =
    (Hom.hom ((restrictScalarsId R).inv.app M)) m
-- Mathlib/Computability/PartrecCode.lean
theorem evaln_map (k c n) :
    ((List.range k)[n]?.bind fun a ↦ evaln k c a) = evaln k c n

Proof state:
case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (Option.none.bind fun a => evaln k c a) = evaln k c n

Tactic:
cases e : evaln k c n

Result:
case neg.none
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
e : evaln k c n = Option.none
⊢ (Option.none.bind fun a => evaln k c a) = Option.none

case neg.some
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
val✝ : ℕ
e : evaln k c n = some val✝
⊢ (Option.none.bind fun a => evaln k c a) = some val✝

Proof state:
case neg.none
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
e : evaln k c n = Option.none
⊢ (Option.none.bind fun a => evaln k c a) = Option.none

Tactic:
rfl

Result:
no goals

Proof state:
case neg.some
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
val✝ : ℕ
e : evaln k c n = some val✝
⊢ (Option.none.bind fun a => evaln k c a) = some val✝

Tactic:
exact kn.elim (evaln_bound e)

Result:
no goals

Proof state:
case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (List.range k).length ≤ n

Tactic:
simpa using kn

Result:
no goals

Proof state:
k : ℕ
c : Code
n : ℕ
⊢ ((List.range k)[n]?.bind fun a => evaln k c a) = evaln k c n

Tactic:
by_cases kn : n < k

Result:
case pos
k : ℕ
c : Code
n : ℕ
kn : n < k
⊢ ((List.range k)[n]?.bind fun a => evaln k c a) = evaln k c n

case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ ((List.range k)[n]?.bind fun a => evaln k c a) = evaln k c n

Proof state:
case pos
k : ℕ
c : Code
n : ℕ
kn : n < k
⊢ ((List.range k)[n]?.bind fun a => evaln k c a) = evaln k c n

Tactic:
simp [List.getElem?_range kn]

Result:
no goals

Proof state:
case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ ((List.range k)[n]?.bind fun a => evaln k c a) = evaln k c n

Tactic:
rw [List.getElem?_eq_none]

Result:
case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (Option.none.bind fun a => evaln k c a) = evaln k c n

case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (List.range k).length ≤ n
-- Mathlib/Deprecated/Cardinal/Finite.lean
theorem card_eq_zero_iff_empty (α : Type*) : card α = 0 ↔ IsEmpty α

Proof state:
α : Type u_1
⊢ card α = 0 ↔ IsEmpty α

Tactic:
rw [← Cardinal.mk_eq_zero_iff]

Result:
α : Type u_1
⊢ card α = 0 ↔ #α = 0

Proof state:
α : Type u_1
⊢ card α = 0 ↔ toPartENat #α = ↑0

Tactic:
simp only [PartENat.card, Nat.cast_zero]

Result:
no goals

Proof state:
α : Type u_1
⊢ card α = 0 ↔ #α = 0

Tactic:
conv_rhs => rw [← Nat.cast_zero]

Result:
α : Type u_1
⊢ card α = 0 ↔ #α = ↑0

Proof state:
α : Type u_1
⊢ card α = 0 ↔ #α = ↑0

Tactic:
simp only [← Cardinal.toPartENat_eq_natCast_iff]

Result:
α : Type u_1
⊢ card α = 0 ↔ toPartENat #α = ↑0
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem pos_add_limZero {f g : CauSeq α abs} : Pos f → LimZero g → Pos (f + g)
  | ⟨F, F0, hF⟩, H =>
    let ⟨i, h⟩ := exists_forall_ge_and hF (H _ (half_pos F0))
    ⟨_, half_pos F0, i, fun j ij => by
      obtain ⟨h₁, h₂⟩ := h j ij
      have := add_le_add h₁ (le_of_lt (abs_lt.1 h₂).1)
      rwa [← sub_eq_add_neg, sub_self_div_two] at this⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ j ≥ i, F ≤ ↑f j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ ↑f j ∧ |↑g j| < F / 2
j : ℕ
ij : j ≥ i
⊢ F / 2 ≤ ↑(f + g) j

Tactic:
obtain ⟨h₁, h₂⟩ := h j ij

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ j ≥ i, F ≤ ↑f j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ ↑f j ∧ |↑g j| < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ ↑f j
h₂ : |↑g j| < F / 2
⊢ F / 2 ≤ ↑(f + g) j

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ j ≥ i, F ≤ ↑f j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ ↑f j ∧ |↑g j| < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ ↑f j
h₂ : |↑g j| < F / 2
⊢ F / 2 ≤ ↑(f + g) j

Tactic:
have := add_le_add h₁ (le_of_lt (abs_lt.1 h₂).1)

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ j ≥ i, F ≤ ↑f j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ ↑f j ∧ |↑g j| < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ ↑f j
h₂ : |↑g j| < F / 2
this : F + -(F / 2) ≤ ↑f j + ↑g j
⊢ F / 2 ≤ ↑(f + g) j

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ j ≥ i, F ≤ ↑f j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ ↑f j ∧ |↑g j| < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ ↑f j
h₂ : |↑g j| < F / 2
this : F + -(F / 2) ≤ ↑f j + ↑g j
⊢ F / 2 ≤ ↑(f + g) j

Tactic:
rwa [← sub_eq_add_neg, sub_self_div_two] at this

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
lemma prodMk_mem_divisorsAntidiag {x y : ℕ} (hn : n ≠ 0) :
    (x, y) ∈ n.divisorsAntidiagonal ↔ x * y = n

Proof state:
n x y : ℕ
hn : n ≠ 0
⊢ (x, y) ∈ n.divisorsAntidiagonal ↔ x * y = n

Tactic:
simp [hn]

Result:
no goals
-- Mathlib/RingTheory/NoetherNormalization.lean
private lemma lt_up (vlt : ∀ i, v i < up) : ∀ l ∈ ofFn v, l < up

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
l : ℕ
h : ∃ i, v i = l
⊢ l < up

Tactic:
obtain ⟨y, rfl⟩ := h

Result:
case intro
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
y : Fin (n + 1)
⊢ v y < up

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
l : ℕ
h : l ∈ ofFn ⇑v
⊢ l < up

Tactic:
rw [mem_ofFn] at h

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
l : ℕ
h : ∃ i, v i = l
⊢ l < up

Proof state:
case intro
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
y : Fin (n + 1)
⊢ v y < up

Tactic:
exact vlt y

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
⊢ ∀ l ∈ ofFn ⇑v, l < up

Tactic:
intro l h

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), v i < up
l : ℕ
h : l ∈ ofFn ⇑v
⊢ l < up
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_toList (l : Array α) (f : α → List β) :
    l.toList.flatMap f = (l.flatMap (fun a => (f a).toArray)).toList

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → List β
l : List α
⊢ List.flatMap f { toList := l }.toList = (flatMap (fun a => (f a).toArray) { toList := l }).toList

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → List β
⊢ List.flatMap f l.toList = (flatMap (fun a => (f a).toArray) l).toList

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → List β
l : List α
⊢ List.flatMap f { toList := l }.toList = (flatMap (fun a => (f a).toArray) { toList := l }).toList
-- Mathlib/Probability/Martingale/Basic.lean
theorem setIntegral_le [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} (hf : Submartingale f ℱ μ)
    {i j : ι} (hij : i ≤ j) {s : Set Ω} (hs : MeasurableSet[ℱ i] s) :
    ∫ ω in s, f i ω ∂μ ≤ ∫ ω in s, f j ω ∂μ

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ

Tactic:
rw [← neg_le_neg_iff, ← integral_neg, ← integral_neg]

Result:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (a : Ω) in s, -f j a ∂μ ≤ ∫ (a : Ω) in s, -f i a ∂μ

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (a : Ω) in s, -f j a ∂μ ≤ ∫ (a : Ω) in s, -f i a ∂μ

Tactic:
exact Supermartingale.setIntegral_le hf.neg hij hs

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean
theorem contsAux_stable_of_terminated (n_lt_m : n < m) (terminatedAt_n : g.TerminatedAt n) :
    g.contsAux m = g.contsAux (n + 1)

Proof state:
case intro
K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ n + k + 1
hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)
⊢ g.contsAux (n + k + 1 + 1) = g.contsAux (n + 1)

Tactic:
refine (contsAux_stable_step_of_terminated ?_).trans hk

Result:
case intro
K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ n + k + 1
hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)
⊢ g.TerminatedAt (n + k)

Proof state:
K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ k
hk : g.contsAux k = g.contsAux (n + 1)
⊢ g.contsAux (k + 1) = g.contsAux (n + 1)

Tactic:
rcases Nat.exists_eq_add_of_lt hnk with ⟨k, rfl⟩

Result:
case intro
K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ n + k + 1
hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)
⊢ g.contsAux (n + k + 1 + 1) = g.contsAux (n + 1)

Proof state:
case intro
K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ n + k + 1
hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)
⊢ g.TerminatedAt (n + k)

Tactic:
exact terminated_stable (Nat.le_add_right _ _) terminatedAt_n

Result:
no goals

Proof state:
K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
⊢ g.contsAux m = g.contsAux (n + 1)

Tactic:
refine Nat.le_induction rfl (fun k hnk hk => ?_) _ n_lt_m

Result:
K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ k
hk : g.contsAux k = g.contsAux (n + 1)
⊢ g.contsAux (k + 1) = g.contsAux (n + 1)
-- Mathlib/Data/Rat/Lemmas.lean
theorem inv_neg (q : ℚ) : (-q)⁻¹ = -q⁻¹

Proof state:
q : ℚ
⊢ (-(q.num /. ↑q.den))⁻¹ = -(q.num /. ↑q.den)⁻¹

Tactic:
simp only [Rat.neg_divInt, Rat.inv_divInt', eq_self_iff_true, Rat.divInt_neg]

Result:
no goals

Proof state:
q : ℚ
⊢ (-q)⁻¹ = -q⁻¹

Tactic:
rw [← num_divInt_den q]

Result:
q : ℚ
⊢ (-(q.num /. ↑q.den))⁻¹ = -(q.num /. ↑q.den)⁻¹