harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_pow_of_ne_zero {n : ℕ} (hn : n ≠ 0) :
    (f ^ n).natSepDegree = f.natSepDegree

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
hn : n ≠ 0
⊢ (f ^ n).natSepDegree = f.natSepDegree

Tactic:
simp_rw [natSepDegree_pow, hn, ite_false]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_of_ge (h : b ≤ a) : ∫ x in a..b, f x ∂μ = -∫ x in Ioc b a, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = -∫ (x : ℝ) in Ioc b a, f x ∂μ

Tactic:
simp only [integral_symm b, integral_of_le h]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
lemma floor_eq_self_iff_mem (a : α) : ⌊a⌋ = a ↔ a ∈ Set.range Int.cast

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ↑⌊a⌋ = a ↔ a ∈ range Int.cast

Tactic:
aesop

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem L1.integral_eq_integral (f : α →₁[μ] E) : L1.integral f = ∫ a, f a ∂μ

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp E 1 μ)
⊢ integralCLM f = setToFun μ (weightedSMul μ) ⋯ ↑↑f

Tactic:
exact (L1.setToFun_eq_setToL1 (dominatedFinMeasAdditive_weightedSMul μ) f).symm

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp E 1 μ)
⊢ integral f = ∫ (a : α), ↑↑f a ∂μ

Tactic:
simp only [integral, L1.integral, integral_eq_setToFun]

Result:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp E 1 μ)
⊢ integralCLM f = setToFun μ (weightedSMul μ) ⋯ ↑↑f
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousWithinAt.comp_of_mem_nhdsWithin_image_of_eq {g : β → γ} {t : Set β} {y : β}
    (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x)
    (hs : t ∈ 𝓝[f '' s] y) (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t (f x)
hs : t ∈ 𝓝[f '' s] f x
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
exact hg.comp_of_mem_nhdsWithin_image hf hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
hs : t ∈ 𝓝[f '' s] y
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
subst hy

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t (f x)
hs : t ∈ 𝓝[f '' s] f x
⊢ ContinuousWithinAt (g ∘ f) s x
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem mem_span_gramSchmidt (f : ι → E) {i j : ι} (hij : i ≤ j) :
    f i ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i + ∑ i_1 ∈ Finset.Iio i, ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

Tactic:
simp_rw [orthogonalProjection_singleton]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i +
      ∑ x ∈ Finset.Iio i, (inner (gramSchmidt 𝕜 f x) (f i) / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2)) • gramSchmidt 𝕜 f x ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ι
hij : i ≤ j
⊢ f i ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

Tactic:
rw [gramSchmidt_def' 𝕜 f i]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i + ∑ i_1 ∈ Finset.Iio i, ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
i j : ι
hij : i ≤ j
⊢ gramSchmidt 𝕜 f i +
      ∑ x ∈ Finset.Iio i, (inner (gramSchmidt 𝕜 f x) (f i) / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2)) • gramSchmidt 𝕜 f x ∈
    span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)

Tactic:
exact Submodule.add_mem _ (subset_span <| mem_image_of_mem _ hij)
  (Submodule.sum_mem _ fun k hk => smul_mem (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)) _ <|
    subset_span <| mem_image_of_mem (gramSchmidt 𝕜 f) <| (Finset.mem_Iio.1 hk).le.trans hij)

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
@[reassoc (attr := simp)]
lemma hom_inv_id_app_app {F G : C ⥤ D ⥤ E} (e : F ≅ G) (X₁ : C) (X₂ : D) :
    (e.hom.app X₁).app X₂ ≫ (e.inv.app X₁).app X₂ = 𝟙 _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D ⥤ E
e : F ≅ G
X₁ : C
X₂ : D
⊢ (e.hom.app X₁).app X₂ ≫ (e.inv.app X₁).app X₂ = 𝟙 ((F.obj X₁).obj X₂)

Tactic:
rw [← NatTrans.comp_app, Iso.hom_inv_id_app, NatTrans.id_app]

Result:
no goals
-- Mathlib/Order/PartialSups.lean
theorem partialSups_eq_ciSup_Iic [ConditionallyCompleteLattice α] (f : ι → α) (i : ι) :
    partialSups f i = ⨆ i : Set.Iic i, f i

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i j : ι
hj : j ∈ Iic i
⊢ j ∈ Set.Iic i

Tactic:
simpa only [Set.mem_Iic, mem_Iic] using hj

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
x✝ : ↑(Set.Iic i)
j : ι
hj : j ∈ Set.Iic i
⊢ ↑⟨j, hj⟩ ∈ Iic i

Tactic:
simpa only [mem_Iic, Set.mem_Iic] using hj

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ (Iic i).sup' ⋯ f = ⨆ i_1, f ↑i_1

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ (Iic i).sup' ⋯ f ≤ ⨆ i_1, f ↑i_1

case a
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ ⨆ i_1, f ↑i_1 ≤ (Iic i).sup' ⋯ f

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ (partialSups f) i = ⨆ i_1, f ↑i_1

Tactic:
simp only [partialSups_apply]

Result:
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ (Iic i).sup' ⋯ f = ⨆ i_1, f ↑i_1

Proof state:
case a
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ ⨆ i_1, f ↑i_1 ≤ (Iic i).sup' ⋯ f

Tactic:
exact ciSup_le fun ⟨j, hj⟩ ↦ le_sup' f (by simpa only [mem_Iic, Set.mem_Iic] using hj)

Result:
no goals

Proof state:
case a
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ (Iic i).sup' ⋯ f ≤ ⨆ i_1, f ↑i_1

Tactic:
exact sup'_le _ _ fun j hj ↦ le_ciSup_of_le (Set.finite_range _).bddAbove
  ⟨j, by simpa only [Set.mem_Iic, mem_Iic] using hj⟩ le_rfl

Result:
no goals
-- Mathlib/Order/Filter/Pointwise.lean
theorem pow_mem_pow (hs : s ∈ f) : ∀ n : ℕ, s ^ n ∈ f ^ n
  | 0 => by
    rw [pow_zero]
    exact one_mem_one
  | n + 1 => by
    rw [pow_succ]
    exact mul_mem_mul (pow_mem_pow hs n) hs

Proof state:
α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ (n + 1)

Tactic:
rw [pow_succ]

Result:
α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ n * f

Proof state:
α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ n * f

Tactic:
exact mul_mem_mul (pow_mem_pow hs n) hs

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s ^ 0 ∈ f ^ 0

Tactic:
rw [pow_zero]

Result:
α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s ^ 0 ∈ 1

Proof state:
α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s ^ 0 ∈ 1

Tactic:
exact one_mem_one

Result:
no goals
-- Mathlib/Analysis/Calculus/SmoothSeries.lean
theorem fderiv_tsum (hu : Summable u) (hf : ∀ n, Differentiable 𝕜 (f n))
    (hf' : ∀ n x, ‖fderiv 𝕜 (f n) x‖ ≤ u n) (hf0 : Summable fun n => f n x₀) :
    (fderiv 𝕜 fun y => ∑' n, f n y) = fun x => ∑' n, fderiv 𝕜 (f n) x

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
x₀ : E
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n
hf0 : Summable fun n => f n x₀
⊢ (fderiv 𝕜 fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), fderiv 𝕜 (f n) x

Tactic:
ext1 x

Result:
case h
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
x₀ : E
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n
hf0 : Summable fun n => f n x₀
x : E
⊢ fderiv 𝕜 (fun y => ∑' (n : α), f n y) x = ∑' (n : α), fderiv 𝕜 (f n) x

Proof state:
case h
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
x₀ : E
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n
hf0 : Summable fun n => f n x₀
x : E
⊢ fderiv 𝕜 (fun y => ∑' (n : α), f n y) x = ∑' (n : α), fderiv 𝕜 (f n) x

Tactic:
exact fderiv_tsum_apply hu hf hf' hf0 x

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem norm_expSeries_summable_of_mem_ball' (x : 𝔸)
    (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    Summable fun n => ‖(n !⁻¹ : 𝕂) • x ^ n‖

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n => (expSeries 𝕂 𝔸 n) fun x_1 => x)

Tactic:
exact norm_expSeries_summable_of_mem_ball x hx

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n => (↑n !)⁻¹ • x ^ n)

Tactic:
rw [← expSeries_apply_eq']

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n => (expSeries 𝕂 𝔸 n) fun x_1 => x)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable fun n => ‖(↑n !)⁻¹ • x ^ n‖

Tactic:
change Summable (norm ∘ _)

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n => (↑n !)⁻¹ • x ^ n)
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem bot_degree (v : V) : (⊥ : SimpleGraph V).degree v = 0

Proof state:
V : Type u_1
inst✝ : Fintype V
v : V
⊢ #∅ = 0

Tactic:
exact Finset.card_empty

Result:
no goals

Proof state:
V : Type u_1
inst✝ : Fintype V
v : V
⊢ ⊥.degree v = 0

Tactic:
erw [degree, neighborFinset_eq_filter, filter_False]

Result:
V : Type u_1
inst✝ : Fintype V
v : V
⊢ #∅ = 0
-- Mathlib/RingTheory/Generators.lean
lemma σ_injective : P.σ.Injective

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
x y : S
e : P.σ x = P.σ y
⊢ x = y

Tactic:
rw [← P.aeval_val_σ x, ← P.aeval_val_σ y, e]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
⊢ Function.Injective P.σ

Tactic:
intro x y e

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
x y : S
e : P.σ x = P.σ y
⊢ x = y
-- Mathlib/Algebra/Homology/Single.lean
@[ext]
lemma to_single_hom_ext {K : HomologicalComplex V c} {j : ι} {A : V}
    {f g : K ⟶ (single V c j).obj A} (hfg : f.f j = g.f j) : f = g

Proof state:
case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
i : ι
h : ¬i = j
⊢ f.f i = g.f i

Tactic:
apply (isZero_single_obj_X c j A i h).eq_of_tgt

Result:
no goals

Proof state:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
i : ι
h : i = j
⊢ f.f i = g.f i

Tactic:
subst h

Result:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
A : V
i : ι
f g : K ⟶ (single V c i).obj A
hfg : f.f i = g.f i
⊢ f.f i = g.f i

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
⊢ f = g

Tactic:
ext i

Result:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
i : ι
⊢ f.f i = g.f i

Proof state:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
A : V
i : ι
f g : K ⟶ (single V c i).obj A
hfg : f.f i = g.f i
⊢ f.f i = g.f i

Tactic:
exact hfg

Result:
no goals

Proof state:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
i : ι
⊢ f.f i = g.f i

Tactic:
by_cases h : i = j

Result:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
i : ι
h : i = j
⊢ f.f i = g.f i

case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
i : ι
h : ¬i = j
⊢ f.f i = g.f i
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem eventuallyEq_one_of_dist_lt (hs : x ∈ (chartAt H c).source)
    (hd : dist (extChartAt I c x) (extChartAt I c c) < f.rIn) : f =ᶠ[𝓝 x] 1

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : FiniteDimensional ℝ E
hs : x ∈ (chartAt H c).source
hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn
⊢ ↑f =ᶠ[𝓝 x] 1

Tactic:
filter_upwards [IsOpen.mem_nhds (isOpen_extChartAt_preimage c isOpen_ball) ⟨hs, hd⟩]

Result:
case h
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : FiniteDimensional ℝ E
hs : x ∈ (chartAt H c).source
hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn
⊢ ∀ a ∈ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rIn, ↑f a = 1 a

Proof state:
case h
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : FiniteDimensional ℝ E
hs : x ∈ (chartAt H c).source
hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn
⊢ ∀ a ∈ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rIn, ↑f a = 1 a

Tactic:
rintro z ⟨hzs, hzd⟩

Result:
case h.intro
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : FiniteDimensional ℝ E
hs : x ∈ (chartAt H c).source
hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn
z : M
hzs : z ∈ (chartAt H c).source
hzd : z ∈ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rIn
⊢ ↑f z = 1 z

Proof state:
case h.intro
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : FiniteDimensional ℝ E
hs : x ∈ (chartAt H c).source
hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn
z : M
hzs : z ∈ (chartAt H c).source
hzd : z ∈ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rIn
⊢ ↑f z = 1 z

Tactic:
exact f.one_of_dist_le hzs <| le_of_lt hzd

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_apply_eq (x : E) (n : ℕ) :
    ofScalars E c n (fun _ ↦ x) = c n • x ^ n

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
x : E
n : ℕ
⊢ ((ofScalars E c n) fun x_1 => x) = c n • x ^ n

Tactic:
simp [ofScalars]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem map_le_map {g : α →o β} (h : f ≤ g) : c.map f ≤ c.map g :=
  fun i => by simp only [map_coe, Function.comp_apply]; exists i; apply h

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f g : α →o β
h : f ≤ g
i : ℕ
⊢ f (c i) ≤ g (c i)

Tactic:
apply h

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f g : α →o β
h : f ≤ g
i : ℕ
⊢ ∃ j, f (c i) ≤ g (c j)

Tactic:
exists i

Result:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f g : α →o β
h : f ≤ g
i : ℕ
⊢ f (c i) ≤ g (c i)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f g : α →o β
h : f ≤ g
i : ℕ
⊢ ∃ j, (c.map f) i ≤ (c.map g) j

Tactic:
simp only [map_coe, Function.comp_apply]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f g : α →o β
h : f ≤ g
i : ℕ
⊢ ∃ j, f (c i) ≤ g (c j)
-- Mathlib/Algebra/Lie/Solvable.lean
theorem abelian_iff_derived_succ_eq_bot (I : LieIdeal R L) (k : ℕ) :
    IsLieAbelian (derivedSeriesOfIdeal R L k I) ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ IsLieAbelian ↥(D k I) ↔ D (k + 1) I = ⊥

Tactic:
rw [add_comm, derivedSeriesOfIdeal_add I 1 k, abelian_iff_derived_one_eq_bot]

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem AnalyticAt.comp_of_eq {g : F → G} {f : E → F} {y : F} {x : E} (hg : AnalyticAt 𝕜 g y)
    (hf : AnalyticAt 𝕜 f x) (hy : f x = y) : AnalyticAt 𝕜 (g ∘ f) x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticAt 𝕜 f x
hy : f x = y
⊢ AnalyticAt 𝕜 (g ∘ f) x

Tactic:
exact hg.comp hf

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
hg : AnalyticAt 𝕜 g y
hf : AnalyticAt 𝕜 f x
hy : f x = y
⊢ AnalyticAt 𝕜 (g ∘ f) x

Tactic:
rw [← hy] at hg

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticAt 𝕜 f x
hy : f x = y
⊢ AnalyticAt 𝕜 (g ∘ f) x
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma F_nat_zero_zero_sub_le {t : ℝ} (ht : 0 < t) :
    ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))

Proof state:
case h.e'_4.h.e'_5
t : ℝ
ht : 0 < t
⊢ rexp (-π * t) = rexp (-π * 1 ^ 2 * t)

Tactic:
rw [one_pow, mul_one]

Result:
no goals

Proof state:
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))

Tactic:
convert F_nat_zero_le zero_le_one ht using 2

Result:
case h.e'_3.h.e'_3
t : ℝ
ht : 0 < t
⊢ F_nat 0 0 t - 1 = F_nat 0 1 t

case h.e'_4.h.e'_5
t : ℝ
ht : 0 < t
⊢ rexp (-π * t) = rexp (-π * 1 ^ 2 * t)

Proof state:
case h.e'_3.h.e'_3
t : ℝ
ht : 0 < t
⊢ ∑' (b : ℕ), f_nat 0 0 t (b + 1) = F_nat 0 1 t

Tactic:
simp_rw [F_nat, f_nat, Nat.cast_add, Nat.cast_one, add_zero]

Result:
no goals

Proof state:
case h.e'_3.h.e'_3
t : ℝ
ht : 0 < t
⊢ F_nat 0 0 t - 1 = F_nat 0 1 t

Tactic:
rw [F_nat, tsum_eq_zero_add (summable_f_nat 0 0 ht), f_nat, Nat.cast_zero, add_zero, pow_zero,
  one_mul, pow_two, mul_zero, mul_zero, zero_mul, exp_zero, add_comm, add_sub_cancel_right]

Result:
case h.e'_3.h.e'_3
t : ℝ
ht : 0 < t
⊢ ∑' (b : ℕ), f_nat 0 0 t (b + 1) = F_nat 0 1 t