harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
theorem le_of_lt_succFn (j i : ι) (hij : j < succFn i) : j ≤ i

Proof state:
case intro.intro
ι : Type u_1
inst✝ : LinearOrder ι
j i k : ι
hk_lb : ∀ x ∈ Set.Ioi i, k ≤ x
hk : j < k
⊢ j ≤ i

Tactic:
exact not_lt.mp fun hi_lt_j ↦ not_le.mpr hk (hk_lb j hi_lt_j)

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : j < succFn i
⊢ j ≤ i

Tactic:
rw [lt_isGLB_iff (succFn_spec i)] at hij

Result:
ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : ∃ c ∈ lowerBounds (Set.Ioi i), j < c
⊢ j ≤ i

Proof state:
ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : ∃ c ∈ lowerBounds (Set.Ioi i), j < c
⊢ j ≤ i

Tactic:
obtain ⟨k, hk_lb, hk⟩ := hij

Result:
case intro.intro
ι : Type u_1
inst✝ : LinearOrder ι
j i k : ι
hk_lb : k ∈ lowerBounds (Set.Ioi i)
hk : j < k
⊢ j ≤ i

Proof state:
case intro.intro
ι : Type u_1
inst✝ : LinearOrder ι
j i k : ι
hk_lb : k ∈ lowerBounds (Set.Ioi i)
hk : j < k
⊢ j ≤ i

Tactic:
rw [mem_lowerBounds] at hk_lb

Result:
case intro.intro
ι : Type u_1
inst✝ : LinearOrder ι
j i k : ι
hk_lb : ∀ x ∈ Set.Ioi i, k ≤ x
hk : j < k
⊢ j ≤ i
-- Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean
@[simp]
lemma desc_d (b : B) : D.desc (CommRingCat.KaehlerDifferential.d b) = D.d b

Proof state:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
D : M.Derivation f
b : ↑B
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
⊢ (ConcreteCategory.hom D.desc) (CommRingCat.KaehlerDifferential.d b) = D.d b

Tactic:
apply D.liftKaehlerDifferential_comp_D

Result:
no goals

Proof state:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
D : M.Derivation f
b : ↑B
this : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
⊢ (ConcreteCategory.hom D.desc) (CommRingCat.KaehlerDifferential.d b) = D.d b

Tactic:
letI := Module.compHom M f.hom

Result:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
D : M.Derivation f
b : ↑B
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
⊢ (ConcreteCategory.hom D.desc) (CommRingCat.KaehlerDifferential.d b) = D.d b

Proof state:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
D : M.Derivation f
b : ↑B
⊢ (ConcreteCategory.hom D.desc) (CommRingCat.KaehlerDifferential.d b) = D.d b

Tactic:
letI := f.hom.toAlgebra

Result:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
D : M.Derivation f
b : ↑B
this : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
⊢ (ConcreteCategory.hom D.desc) (CommRingCat.KaehlerDifferential.d b) = D.d b
-- Mathlib/Deprecated/Cardinal/PartENat.lean
theorem toPartENat_apply_of_lt_aleph0 {c : Cardinal} (h : c < ℵ₀) : toPartENat c = toNat c

Proof state:
case intro
c : ℕ
⊢ toPartENat ↑c = ↑(toNat ↑c)

Tactic:
simp

Result:
no goals

Proof state:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ toPartENat c = ↑(toNat c)

Tactic:
lift c to ℕ using h

Result:
case intro
c : ℕ
⊢ toPartENat ↑c = ↑(toNat ↑c)
-- Mathlib/AlgebraicGeometry/PointsPi.lean
lemma pointsPi_injective [QuasiSeparatedSpace X] : Function.Injective (pointsPi R X)

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f g : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X
e : pointsPi R X f = pointsPi R X g
this : IsIso (equalizer.ι f g)
⊢ f = g

Tactic:
rw [← cancel_epi (equalizer.ι f g), equalizer.condition]

Result:
no goals

Proof state:
case h
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f g : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X
e : pointsPi R X f = pointsPi R X g
i : ι
⊢ Sigma.ι (fun i => Spec (R i)) i ≫ sigmaSpec R ≫ f = Sigma.ι (fun i => Spec (R i)) i ≫ sigmaSpec R ≫ g

Tactic:
simpa using congr_fun e i

Result:
no goals

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f g : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X
e : pointsPi R X f = pointsPi R X g
⊢ f = g

Tactic:
have := isIso_of_comp_eq_sigmaSpec R (V := equalizer f g)
  (equalizer.lift (sigmaSpec R) (by ext1 i; simpa using congr_fun e i))
  (equalizer.ι f g) (by simp)

Result:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f g : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X
e : pointsPi R X f = pointsPi R X g
this : IsIso (equalizer.ι f g)
⊢ f = g

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f g : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X
e : pointsPi R X f = pointsPi R X g
⊢ equalizer.lift (sigmaSpec R) ⋯ ≫ equalizer.ι f g = sigmaSpec R

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
⊢ Function.Injective (pointsPi R X)

Tactic:
rintro f g e

Result:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f g : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X
e : pointsPi R X f = pointsPi R X g
⊢ f = g

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f g : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X
e : pointsPi R X f = pointsPi R X g
⊢ sigmaSpec R ≫ f = sigmaSpec R ≫ g

Tactic:
ext1 i

Result:
case h
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f g : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X
e : pointsPi R X f = pointsPi R X g
i : ι
⊢ Sigma.ι (fun i => Spec (R i)) i ≫ sigmaSpec R ≫ f = Sigma.ι (fun i => Spec (R i)) i ≫ sigmaSpec R ≫ g
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem zero_eq_last_iff {n : Nat} : (0 : Fin (n + 1)) = last n ↔ n = 0

Proof state:
n : Nat
⊢ 0 = last n ↔ n = 0

Tactic:
constructor

Result:
case mp
n : Nat
⊢ 0 = last n → n = 0

case mpr
n : Nat
⊢ n = 0 → 0 = last n

Proof state:
case mp
n : Nat
⊢ 0 = last n → n = 0

Tactic:
intro h

Result:
case mp
n : Nat
h : 0 = last n
⊢ n = 0

Proof state:
case mpr
n : Nat
⊢ n = 0 → 0 = last n

Tactic:
rintro rfl

Result:
case mpr

⊢ 0 = last 0

Proof state:
case mp
n : Nat
h : 0 = last n
⊢ n = 0

Tactic:
simp_all [Fin.ext_iff]

Result:
no goals

Proof state:
case mpr

⊢ 0 = last 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean
@[simp]
lemma coneπApp_eq_id : h.coneπApp i₀ = 𝟙 _

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_4, u_1} J
inst✝¹ : Category.{u_3, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
⊢ h.coneπApp i₀ = 𝟙 (F.obj i₀)

Tactic:
rw [h.coneπApp_eq i₀ i₀ (𝟙 _) (𝟙 _), h.isoMap_inv_hom_id]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/BaseChange.lean
lemma mem_subfield_of_mul_eq_one_of_mem_subfield_left
    (h_mem : ∀ i j, B i j ∈ K) (i : m) (j : n) :
    A i j ∈ K

Proof state:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
⊢ Bᵀ * Aᵀ = 1

Tactic:
simpa using congr_arg transpose hAB

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
hAB : A * B = 1
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
⊢ A i j ∈ K

Tactic:
replace hAB : Bᵀ * Aᵀ = 1 := by simpa using congr_arg transpose hAB

Result:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
hAB : Bᵀ * Aᵀ = 1
⊢ A i j ∈ K

Proof state:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
h_mem : ∀ (i : n) (j : m), Bᵀ j i ∈ K
i : m
j : n
hAB : Bᵀ * Aᵀ = 1
⊢ Aᵀ j i ∈ K

Tactic:
exact mem_subfield_of_mul_eq_one_of_mem_subfield_right e K hAB (fun i j ↦ h_mem j i) j i

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
hAB : Bᵀ * Aᵀ = 1
⊢ Aᵀ j i ∈ K

Tactic:
simp_rw [← B.transpose_apply] at h_mem

Result:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
h_mem : ∀ (i : n) (j : m), Bᵀ j i ∈ K
i : m
j : n
hAB : Bᵀ * Aᵀ = 1
⊢ Aᵀ j i ∈ K

Proof state:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
hAB : Bᵀ * Aᵀ = 1
⊢ A i j ∈ K

Tactic:
rw [← A.transpose_apply]

Result:
m : Type u_1
n : Type u_2
L : Type u_3
inst✝³ : Finite m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Field L
e : m ≃ n
K : Subfield L
A : Matrix m n L
B : Matrix n m L
h_mem : ∀ (i : n) (j : m), B i j ∈ K
i : m
j : n
hAB : Bᵀ * Aᵀ = 1
⊢ Aᵀ j i ∈ K
-- Mathlib/Algebra/GCDMonoid/Nat.lean
theorem Int.associated_iff {a b : ℤ} : Associated a b ↔ a = b ∨ a = -b

Proof state:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a = b ∨ a = -b

Tactic:
exact Int.natAbs_eq_natAbs_iff

Result:
no goals

Proof state:
a b : ℤ
⊢ Associated a b ↔ a = b ∨ a = -b

Tactic:
rw [Int.associated_iff_natAbs]

Result:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a = b ∨ a = -b
-- Mathlib/Analysis/Analytic/Basic.lean
theorem AnalyticWithinAt.mono_of_mem_nhdsWithin
    (h : AnalyticWithinAt 𝕜 f s x) (hst : s ∈ 𝓝[t] x) : AnalyticWithinAt 𝕜 f t x

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
s t : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
hst : s ∈ 𝓝[t] x
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
rcases h with ⟨p, hp⟩

Result:
case intro
𝕜 : 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
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f t x

Proof state:
case intro
𝕜 : 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
s t : Set E
x : E
hst : s ∈ 𝓝[t] x
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
exact ⟨p, hp.mono_of_mem_nhdsWithin hst⟩

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem abs_mul_sign (x : α) : (|x| * sign x : α) = x

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
x : α
⊢ |x| * ↑(sign x) = x

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_nonpos_of_ae {f : α → ℝ} (hf : f ≤ᵐ[μ] 0) : ∫ a, f a ∂μ ≤ 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf✝ : f ≤ᶠ[ae μ] 0
hf : 0 ≤ᶠ[ae μ] -f
⊢ ∫ (a : α), f a ∂μ ≤ 0

Tactic:
have : 0 ≤ ∫ a, -f a ∂μ := integral_nonneg_of_ae hf

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf✝ : f ≤ᶠ[ae μ] 0
hf : 0 ≤ᶠ[ae μ] -f
this : 0 ≤ ∫ (a : α), -f a ∂μ
⊢ ∫ (a : α), f a ∂μ ≤ 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : f ≤ᶠ[ae μ] 0
a : α
h : f a ≤ 0 a
⊢ 0 a ≤ (-f) a

Tactic:
rwa [Pi.neg_apply, Pi.zero_apply, neg_nonneg]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : f ≤ᶠ[ae μ] 0
⊢ ∫ (a : α), f a ∂μ ≤ 0

Tactic:
have hf : 0 ≤ᵐ[μ] -f := hf.mono fun a h => by rwa [Pi.neg_apply, Pi.zero_apply, neg_nonneg]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf✝ : f ≤ᶠ[ae μ] 0
hf : 0 ≤ᶠ[ae μ] -f
⊢ ∫ (a : α), f a ∂μ ≤ 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf✝ : f ≤ᶠ[ae μ] 0
hf : 0 ≤ᶠ[ae μ] -f
this : 0 ≤ ∫ (a : α), -f a ∂μ
⊢ ∫ (a : α), f a ∂μ ≤ 0

Tactic:
rwa [integral_neg, neg_nonneg] at this

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
theorem comapEq_symm {β γ : Type w} {f g : β → γ} (h : f = g) :
    comapEq C h.symm = (comapEq C h).symm

Proof state:
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
⊢ comapEq C ⋯ = (comapEq C h).symm

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toNNReal_iInf (hf : ∀ i, f i ≠ ∞) : (iInf f).toNNReal = ⨅ i, (f i).toNNReal

Proof state:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
h✝ : Nonempty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

Tactic:
lift f to ι → ℝ≥0 using hf

Result:
case inr.intro
ι : Sort u_1
h✝ : Nonempty ι
f : ι → ℝ≥0
⊢ (⨅ i, ↑(f i)).toNNReal = ⨅ i, ((fun i => ↑(f i)) i).toNNReal

Proof state:
case inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
h✝ : IsEmpty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

Tactic:
rw [iInf_of_empty, top_toNNReal, NNReal.iInf_empty]

Result:
no goals

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
h✝ : IsEmpty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

case inr
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
h✝ : Nonempty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

Proof state:
case inr.intro
ι : Sort u_1
h✝ : Nonempty ι
f : ι → ℝ≥0
⊢ (⨅ i, ↑(f i)).toNNReal = ⨅ i, ((fun i => ↑(f i)) i).toNNReal

Tactic:
simp_rw [← coe_iInf, toNNReal_coe]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma le_half_of_half_lt_sub (h : a / 2 < a - b) : b ≤ a / 2

Proof state:
a b : ℕ
h : a / 2 < a - b
⊢ b ≤ a / 2

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem dfoldr_succ_last {n : Nat} {α : Fin (n+2) → Sort _}
    (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x : α (last (n+1))) :
      dfoldr (n+1) α f x = dfoldr n (α ∘ castSucc) (f ·.castSucc) (f (last n) x)

Proof state:
case succ
n : Nat
ih :
  ∀ {α : Fin (n + 2) → Type u_1} (f : (i : Fin (n + 1)) → α i.succ → α i.castSucc) (x : α (last (n + 1))),
    dfoldr (n + 1) α f x = dfoldr n (α ∘ castSucc) (fun x => f x.castSucc) (f (last n) x)
α : Fin (n + 1 + 2) → Type u_1
f : (i : Fin (n + 1 + 1)) → α i.succ → α i.castSucc
x : α (last (n + 1 + 1))
⊢ f 0 (dfoldr n ((α ∘ succ) ∘ castSucc) (fun x => f x.castSucc.succ) (f (last n).succ x)) =
    f (castSucc 0) (dfoldr n ((α ∘ castSucc) ∘ succ) (fun x => f x.succ.castSucc) (f (last (n + 1)) x))

Tactic:
congr

Result:
no goals

Proof state:
case zero
α : Fin (0 + 2) → Type u_1
f : (i : Fin (0 + 1)) → α i.succ → α i.castSucc
x : α (last (0 + 1))
⊢ dfoldr (0 + 1) α f x = dfoldr 0 (α ∘ castSucc) (fun x => f x.castSucc) (f (last 0) x)

Tactic:
simp only [dfoldr_succ, dfoldr_zero, last, zero_eta]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma toNat_lt' {n : ℕ} (hn : n ≠ 0) : m.toNat < n ↔ m < n

Proof state:
m : ℤ
n : ℕ
hn : n ≠ 0
⊢ m.toNat < n ↔ m < ↑n

Tactic:
rw [← toNat_lt_toNat, toNat_natCast]

Result:
m : ℤ
n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n

Proof state:
m : ℤ
n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@[simp] lemma eLpNorm_conj (f : α → 𝕜) (p : ℝ≥0∞) (μ : Measure α) :
    eLpNorm (conj f) p μ = eLpNorm f p μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm ((starRingEnd (α → 𝕜)) f) p μ = eLpNorm f p μ

Tactic:
simp [← eLpNorm_norm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getThenInsertIfNew?_snd [LawfulBEq α] {k : α} {v : β k} :
    (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
k : α
v : β k
⊢ (m.getThenInsertIfNew? k v).snd = m.insertIfNew k v

Tactic:
rw [getThenInsertIfNew?_eq_insertIfNewₘ, insertIfNew_eq_insertIfNewₘ]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_const_smul_left {c : 𝕜} (hc : c ≠ 0) : (fun x => c • f' x) =O[l] g ↔ f' =O[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x => c • f' x) =O[l] g ↔ f' =O[l] g

Tactic:
rw [← isBigO_norm_left]

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x => ‖c • f' x‖) =O[l] g ↔ f' =O[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x => ‖c • f' x‖) =O[l] g ↔ f' =O[l] g

Tactic:
simp only [norm_smul]

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x => ‖c‖ * ‖f' x‖) =O[l] g ↔ f' =O[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x => ‖c‖ * ‖f' x‖) =O[l] g ↔ f' =O[l] g

Tactic:
rw [isBigO_const_mul_left_iff cne0, isBigO_norm_left]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
⊢ (fun x => c • f' x) =O[l] g ↔ f' =O[l] g

Tactic:
have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x => c • f' x) =O[l] g ↔ f' =O[l] g
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem cauchySeq_of_edist_le_geometric : CauchySeq f

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ 1 - r ≠ 0

Tactic:
exact (tsub_pos_iff_lt.2 hr).ne'

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ C * (1 - r)⁻¹ ≠ ⊤

Tactic:
refine ENNReal.mul_ne_top hC (ENNReal.inv_ne_top.2 ?_)

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ 1 - r ≠ 0

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ CauchySeq f

Tactic:
refine cauchySeq_of_edist_le_of_tsum_ne_top _ hu ?_

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ ∑' (n : ℕ), C * r ^ n ≠ ⊤

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ ∑' (n : ℕ), C * r ^ n ≠ ⊤

Tactic:
rw [ENNReal.tsum_mul_left, ENNReal.tsum_geometric]

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ C * (1 - r)⁻¹ ≠ ⊤
-- Mathlib/Data/Vector/Basic.lean
theorem toList_ofFn : ∀ {n} (f : Fin n → α), toList (ofFn f) = List.ofFn f
  | 0, f => by rw [ofFn, List.ofFn_zero, toList, nil]
  | n + 1, f => by rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]

Proof state:
α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ (ofFn f).toList = List.ofFn f

Tactic:
rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]

Result:
no goals

Proof state:
α : Type u_1
f : Fin 0 → α
⊢ (ofFn f).toList = List.ofFn f

Tactic:
rw [ofFn, List.ofFn_zero, toList, nil]

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem ofRelIsoLT_toRelIsoLT {α β} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
    ofRelIsoLT (toRelIsoLT e) = e

Proof state:
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : α ≃o β
⊢ ofRelIsoLT e.toRelIsoLT = e

Tactic:
ext

Result:
case h.h
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : α ≃o β
x✝ : α
⊢ (ofRelIsoLT e.toRelIsoLT) x✝ = e x✝

Proof state:
case h.h
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : α ≃o β
x✝ : α
⊢ (ofRelIsoLT e.toRelIsoLT) x✝ = e x✝

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
theorem centerAndRescale_center : a.centerAndRescale.c (last N) = 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
⊢ a.centerAndRescale.c (last N) = 0

Tactic:
simp [SatelliteConfig.centerAndRescale]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Finite.lean
theorem pi_mem_of_mulSingle_mem [Finite η] [DecidableEq η] {H : Subgroup (∀ i, f i)} (x : ∀ i, f i)
    (h : ∀ i, Pi.mulSingle i (x i) ∈ H) : x ∈ H

Proof state:
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H : Subgroup ((i : η) → f i)
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H

Tactic:
cases nonempty_fintype η

Result:
case intro
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H : Subgroup ((i : η) → f i)
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
val✝ : Fintype η
⊢ x ∈ H

Proof state:
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H : Subgroup ((i : η) → f i)
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
val✝ : Fintype η
⊢ ∀ i ∉ Finset.univ, x i = 1

Tactic:
simp

Result:
no goals

Proof state:
case intro
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H : Subgroup ((i : η) → f i)
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
val✝ : Fintype η
⊢ x ∈ H

Tactic:
exact pi_mem_of_mulSingle_mem_aux Finset.univ x (by simp) fun i _ => h i

Result:
no goals