harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
/-- The composition of the derivative of the inverse of `extChartAt` with the derivative of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).target`. -/
lemma mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt
    {y : E} (hy : y ∈ (extChartAt I x).target) :
    (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y) ∘L
      (mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y))
      = ContinuousLinearMap.id _ _

Proof state:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)
this :
  mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y) =
    mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y)
z : M
hz : z ∈ (extChartAt I x).source
⊢ z ∈ ↑(extChartAt I x) ⁻¹' range ↑I

Tactic:
apply extChartAt_target_subset_range x

Result:
case h.a
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)
this :
  mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y) =
    mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y)
z : M
hz : z ∈ (extChartAt I x).source
⊢ ↑(extChartAt I x) z ∈ (extChartAt I x).target
-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
/-- The composition of the derivative of the inverse of `extChartAt` with the derivative of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).target`. -/
lemma mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt
    {y : E} (hy : y ∈ (extChartAt I x).target) :
    (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y) ∘L
      (mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y))
      = ContinuousLinearMap.id _ _

Proof state:
case hg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)
this :
  mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y) =
    mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y)
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) y

Tactic:
exact mdifferentiableWithinAt_extChartAt_symm hy

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)
this :
  mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y) =
    mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y)
⊢ (extChartAt I x).source ⊆ ↑(extChartAt I x) ⁻¹' range ↑I

Tactic:
intro z hz

Result:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)
this :
  mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y) =
    mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y)
z : M
hz : z ∈ (extChartAt I x).source
⊢ z ∈ ↑(extChartAt I x) ⁻¹' range ↑I
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem isFiniteMeasure_withDensity_ofReal {f : α → ℝ} (hfi : HasFiniteIntegral f μ) :
    IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal <| f x)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : HasFiniteIntegral f μ
⊢ IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))

Tactic:
refine isFiniteMeasure_withDensity ((lintegral_mono fun x => ?_).trans_lt hfi).ne

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : HasFiniteIntegral f μ
x : α
⊢ ENNReal.ofReal (f x) ≤ ‖f x‖ₑ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : HasFiniteIntegral f μ
x : α
⊢ ENNReal.ofReal (f x) ≤ ‖f x‖ₑ

Tactic:
exact Real.ofReal_le_enorm (f x)

Result:
no goals
-- Mathlib/ModelTheory/Complexity.lean
theorem realize_toPrenexImpRight {φ ψ : L.BoundedFormula α n} (hφ : IsQF φ) (hψ : IsPrenex ψ)
    {v : α → M} {xs : Fin n → M} :
    (φ.toPrenexImpRight ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs

Proof state:
case ex.refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
ψ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n✝ + 1)},
    φ.IsQF → ∀ {xs : Fin (n✝ + 1) → M}, (φ.toPrenexImpRight φ✝).Realize v xs ↔ (φ ⟹ φ✝).Realize v xs
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
xs : Fin n✝ → M
h' : φ.Realize v xs → ∃ a, φ✝.Realize v (snoc xs a)
⊢ ∃ a, φ.Realize v xs → φ✝.Realize v (snoc xs a)

Tactic:
by_cases h : φ.Realize v xs

Result:
case pos
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
ψ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n✝ + 1)},
    φ.IsQF → ∀ {xs : Fin (n✝ + 1) → M}, (φ.toPrenexImpRight φ✝).Realize v xs ↔ (φ ⟹ φ✝).Realize v xs
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
xs : Fin n✝ → M
h' : φ.Realize v xs → ∃ a, φ✝.Realize v (snoc xs a)
h : φ.Realize v xs
⊢ ∃ a, φ.Realize v xs → φ✝.Realize v (snoc xs a)

case neg
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
ψ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n✝ + 1)},
    φ.IsQF → ∀ {xs : Fin (n✝ + 1) → M}, (φ.toPrenexImpRight φ✝).Realize v xs ↔ (φ ⟹ φ✝).Realize v xs
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
xs : Fin n✝ → M
h' : φ.Realize v xs → ∃ a, φ✝.Realize v (snoc xs a)
h : ¬φ.Realize v xs
⊢ ∃ a, φ.Realize v xs → φ✝.Realize v (snoc xs a)
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
lemma fderivWithin_fderivWithin_eq_of_mem_nhds {f : E → F} {x : E} {s : Set E}
    (h : s ∈ 𝓝 x) :
    fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderiv 𝕜 (fderiv 𝕜 f) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderiv 𝕜 (fderiv 𝕜 f) x

Tactic:
simp only [← fderivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f univ) univ x

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ s =ᶠ[𝓝 x] univ

Tactic:
simp [h]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f univ) univ x

Tactic:
apply fderivWithin_fderivWithin_eq_of_eventuallyEq

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ s =ᶠ[𝓝 x] univ
-- Mathlib/Data/List/Basic.lean
theorem foldr_hom₂ (l : List ι) (f : α → β → γ) (op₁ : ι → α → α) (op₂ : ι → β → β)
    (op₃ : ι → γ → γ) (a : α) (b : β) (h : ∀ a b i, f (op₁ i a) (op₂ i b) = op₃ i (f a b)) :
    foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
a : α
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

Tactic:
revert a

Result:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

Tactic:
induction l <;> intros <;> [rfl; simp only [*, foldr]]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/SubMulAction.lean
theorem neg_mem_iff : -x ∈ p ↔ x ∈ p :=
  ⟨fun h => by
    rw [← neg_neg x]
    exact neg_mem _ h, neg_mem _⟩

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : SubMulAction R M
x : M
h : -x ∈ p
⊢ x ∈ p

Tactic:
rw [← neg_neg x]

Result:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : SubMulAction R M
x : M
h : -x ∈ p
⊢ - -x ∈ p

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : SubMulAction R M
x : M
h : -x ∈ p
⊢ - -x ∈ p

Tactic:
exact neg_mem _ h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
theorem colimit_sound' {j j' : J} {x : F.obj j} {x' : F.obj j'} {j'' : J}
    (f : j ⟶ j'') (f' : j' ⟶ j'') (w : F.map f x = F.map f' x') :
    colimit.ι F j x = colimit.ι F j' x'

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
j'' : J
f : j ⟶ j''
f' : j' ⟶ j''
w : F.map f x = F.map f' x'
⊢ colimit.ι F j x = colimit.ι F j' x'

Tactic:
rw [← colimit.w _ f, ← colimit.w _ f']

Result:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
j'' : J
f : j ⟶ j''
f' : j' ⟶ j''
w : F.map f x = F.map f' x'
⊢ (F.map f ≫ colimit.ι F j'') x = (F.map f' ≫ colimit.ι F j'') x'

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
j'' : J
f : j ⟶ j''
f' : j' ⟶ j''
w : F.map f x = F.map f' x'
⊢ (F.map f ≫ colimit.ι F j'') x = (F.map f' ≫ colimit.ι F j'') x'

Tactic:
rw [types_comp_apply, types_comp_apply, w]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
@[simp] lemma shadow_compls : ∂ 𝒜ᶜˢ = (∂⁺ 𝒜)ᶜˢ

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ s_1, s_1ᶜ ∈ 𝒜 ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ

Tactic:
refine (compl_involutive.toPerm _).exists_congr_left.trans ?_

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ b,
      ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b)ᶜ ∈ 𝒜 ∧
        ∃ a ∈ (Equiv.symm (Function.Involutive.toPerm compl ⋯)) b,
          ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b).erase a = s) ↔
    ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
⊢ ∂ 𝒜ᶜˢ = (∂⁺ 𝒜)ᶜˢ

Tactic:
ext s

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂ 𝒜ᶜˢ ↔ s ∈ (∂⁺ 𝒜)ᶜˢ

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ b,
      ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b)ᶜ ∈ 𝒜 ∧
        ∃ a ∈ (Equiv.symm (Function.Involutive.toPerm compl ⋯)) b,
          ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b).erase a = s) ↔
    ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ

Tactic:
simp [← compl_involutive.eq_iff]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂ 𝒜ᶜˢ ↔ s ∈ (∂⁺ 𝒜)ᶜˢ

Tactic:
simp only [mem_image, exists_prop, mem_shadow_iff, mem_upShadow_iff, mem_compls]

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ s_1, s_1ᶜ ∈ 𝒜 ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem isOpen_singleton_iff {α : Type*} [PseudoMetricSpace α] {x : α} :
    IsOpen ({x} : Set α) ↔ ∃ ε > 0, ∀ y, dist y x < ε → y = x

Proof state:
α : Type u_3
inst✝ : PseudoMetricSpace α
x : α
⊢ IsOpen {x} ↔ ∃ ε > 0, ∀ (y : α), dist y x < ε → y = x

Tactic:
simp [isOpen_iff, subset_singleton_iff, mem_ball]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem karoubi_PInfty_f {Y : Karoubi (SimplicialObject C)} (n : ℕ) :
    ((PInfty : K[(karoubiFunctorCategoryEmbedding _ _).obj Y] ⟶ _).f n).f =
      Y.p.app (op ⦋n⦌) ≫ (PInfty : K[Y.X] ⟶ _).f n

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  PInfty.f n =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n

Tactic:
rw [← h₃₂, ← h₄₃, h₁₄]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  PInfty.f n =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
        PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)).f =
    Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
-- Mathlib/NumberTheory/SumFourSquares.lean
theorem exists_sq_add_sq_add_one_eq_mul (p : ℕ) [hp : Fact p.Prime] :
    ∃ (a b k : ℕ), 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p

Tactic:
rcases Nat.sq_add_sq_zmodEq p (-1) with ⟨a, b, ha, hb, hab⟩

Result:
case inr.intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p

Proof state:
case h
hp : Fact (Nat.Prime 2)
⊢ 0 < 1 ∧ 1 < 2 ∧ 1 ^ 2 + 0 ^ 2 + 1 = 1 * 2

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem sum_schlomilch_le {C : ℕ} (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ n, 0 < u n)
    (h_nonneg : ∀ n, 0 ≤ f n) (hu : Monotone u) (h_succ_diff : SuccDiffBounded C u) (n : ℕ) :
    ∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k) ≤
    (u 1 - u 0) • f (u 0) + C • ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k

Proof state:
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n k : ℕ
a✝ : k ∈ range n
⊢ (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ (C * (u (k + 1) - u k)) • f (u (k + 1))

Tactic:
gcongr

Result:
case ha
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n k : ℕ
a✝ : k ∈ range n
⊢ 0 ≤ f (u (k + 1))

case h
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n k : ℕ
a✝ : k ∈ range n
⊢ u (k + 2) - u (k + 1) ≤ C * (u (k + 1) - u k)

Proof state:
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ (u (0 + 1) - u 0) • f (u 0) + ∑ k ∈ range n, (u (k + 1 + 1) - u (k + 1)) • f (u (k + 1)) ≤
    (u 1 - u 0) • f (u 0) + C • ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k

Tactic:
gcongr

Result:
case bc
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ ∑ k ∈ range n, (u (k + 1 + 1) - u (k + 1)) • f (u (k + 1)) ≤ C • ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_eq_nil_iff (l : List (Option α)) :
    l.reduceOption = [] ↔ ∃ n, l = replicate n none

Proof state:
α : Type u_1
l : List (Option α)
⊢ filterMap id l = [] ↔ ∃ n, l = replicate n none

Tactic:
rw [filterMap_eq_nil_iff]

Result:
α : Type u_1
l : List (Option α)
⊢ (∀ (a : Option α), a ∈ l → id a = none) ↔ ∃ n, l = replicate n none

Proof state:
case mp
α : Type u_1
l : List (Option α)
⊢ (∀ (a : Option α), a ∈ l → id a = none) → ∃ n, l = replicate n none

Tactic:
intro h

Result:
case mp
α : Type u_1
l : List (Option α)
h : ∀ (a : Option α), a ∈ l → id a = none
⊢ ∃ n, l = replicate n none

Proof state:
α : Type u_1
l : List (Option α)
⊢ (∀ (a : Option α), a ∈ l → id a = none) ↔ ∃ n, l = replicate n none

Tactic:
constructor

Result:
case mp
α : Type u_1
l : List (Option α)
⊢ (∀ (a : Option α), a ∈ l → id a = none) → ∃ n, l = replicate n none

case mpr
α : Type u_1
l : List (Option α)
⊢ (∃ n, l = replicate n none) → ∀ (a : Option α), a ∈ l → id a = none

Proof state:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption = [] ↔ ∃ n, l = replicate n none

Tactic:
dsimp [reduceOption]

Result:
α : Type u_1
l : List (Option α)
⊢ filterMap id l = [] ↔ ∃ n, l = replicate n none

Proof state:
case mpr
α : Type u_1
l : List (Option α)
w✝ : ℕ
h : l = replicate w✝ none
⊢ ∀ (a : Option α), a ∈ l → id a = none

Tactic:
simp_rw [h, mem_replicate]

Result:
case mpr
α : Type u_1
l : List (Option α)
w✝ : ℕ
h : l = replicate w✝ none
⊢ ∀ (a : Option α), w✝ ≠ 0 ∧ a = none → id a = none

Proof state:
case mpr
α : Type u_1
l : List (Option α)
w✝ : ℕ
h : l = replicate w✝ none
⊢ ∀ (a : Option α), w✝ ≠ 0 ∧ a = none → id a = none

Tactic:
tauto

Result:
no goals

Proof state:
case mp
α : Type u_1
l : List (Option α)
h : ∀ (a : Option α), a ∈ l → id a = none
⊢ ∃ n, l = replicate n none

Tactic:
exact ⟨l.length, eq_replicate_of_mem h⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
l : List (Option α)
⊢ (∃ n, l = replicate n none) → ∀ (a : Option α), a ∈ l → id a = none

Tactic:
intro ⟨_, h⟩

Result:
case mpr
α : Type u_1
l : List (Option α)
w✝ : ℕ
h : l = replicate w✝ none
⊢ ∀ (a : Option α), a ∈ l → id a = none
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem exists_eq_spanSingleton_mul (I : FractionalIdeal R₁⁰ K) :
    ∃ (a : R₁) (aI : Ideal R₁), a ≠ 0 ∧ I = spanSingleton R₁⁰ (algebraMap R₁ K a)⁻¹ * aI

Proof state:
case intro.intro
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
⊢ ∃ a aI, a ≠ 0 ∧ I = spanSingleton R₁⁰ ((algebraMap R₁ K) a)⁻¹ * ↑aI

Tactic:
have map_a_nonzero : algebraMap R₁ K a_inv ≠ 0 :=
  mt IsFractionRing.to_map_eq_zero_iff.mp nonzero

Result:
case intro.intro
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
⊢ ∃ a aI, a ≠ 0 ∧ I = spanSingleton R₁⁰ ((algebraMap R₁ K) a)⁻¹ * ↑aI