harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Sum/Interval.lean
lemma Ioc_inr_inr :
    Ioc (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Ioc b₁ b₂).map (Embedding.inr.trans toLex.toEmbedding)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Ioc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioc b₁ b₂))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Ioc (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Ioc b₁ b₂)

Tactic:
rw [← Finset.map_map]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Ioc (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioc b₁ b₂))
-- Mathlib/Analysis/Analytic/Constructions.lean
/-- The Cartesian product of analytic functions is analytic. -/
lemma AnalyticWithinAt.prod {e : E} {f : E → F} {g : E → G} {s : Set E}
    (hf : AnalyticWithinAt 𝕜 f s e) (hg : AnalyticWithinAt 𝕜 g s e) :
    AnalyticWithinAt 𝕜 (fun x ↦ (f x, g x)) s e

Proof state:
case intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
hg : AnalyticWithinAt 𝕜 g s e
w✝ : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesWithinAt f w✝ s e
⊢ AnalyticWithinAt 𝕜 (fun x => (f x, g x)) s e

Tactic:
rcases hg with ⟨_, hg⟩

Result:
case intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
w✝¹ : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesWithinAt f w✝¹ s e
w✝ : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesWithinAt g w✝ s e
⊢ AnalyticWithinAt 𝕜 (fun x => (f x, g x)) s e

Proof state:
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
hf : AnalyticWithinAt 𝕜 f s e
hg : AnalyticWithinAt 𝕜 g s e
⊢ AnalyticWithinAt 𝕜 (fun x => (f x, g x)) s e

Tactic:
rcases hf with ⟨_, hf⟩

Result:
case intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
hg : AnalyticWithinAt 𝕜 g s e
w✝ : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesWithinAt f w✝ s e
⊢ AnalyticWithinAt 𝕜 (fun x => (f x, g x)) s e

Proof state:
case intro.intro
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
s : Set E
w✝¹ : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesWithinAt f w✝¹ s e
w✝ : FormalMultilinearSeries 𝕜 E G
hg : HasFPowerSeriesWithinAt g w✝ s e
⊢ AnalyticWithinAt 𝕜 (fun x => (f x, g x)) s e

Tactic:
exact ⟨_, hf.prod hg⟩

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
lemma prodMk_mem_divisorsAntidiag (hz : z ≠ 0) : (x, y) ∈ z.divisorsAntidiag ↔ x * y = z

Proof state:
x y z : ℤ
hz : z ≠ 0
⊢ (x, y) ∈ z.divisorsAntidiag ↔ x * y = z

Tactic:
simp [hz]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_modify (h : m.1.WF) {k k' fallback : α} {f : β k → β k} :
    (m.modify k f).getKeyD k' fallback =
      if k == k' then
        if m.contains k then k else fallback
      else
        m.getKeyD k' fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' fallback : α
f : β k → β k
⊢ (m.modify k f).getKeyD k' fallback =
    if (k == k') = true then if m.contains k = true then k else fallback else m.getKeyD k' fallback

Tactic:
simp_to_model [modify] using List.getKeyD_modifyKey

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.add_smul_mem (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s) {t : 𝕜}
    (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • y ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ x + t • y ∈ s

Tactic:
have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> noncomm_ring

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ s

Tactic:
rw [h]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ s

Tactic:
exact hs hx hy (sub_nonneg_of_le ht.2) ht.1 (sub_add_cancel _ _)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ x + t • y = (1 - t) • x + t • (x + y)

Tactic:
match_scalars <;> noncomm_ring

Result:
no goals
-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
@[simp, norm_cast]
lemma coe_finsetSup' {ι : Type*} {s : Finset ι} (H : s.Nonempty) (f : ι → C_c(α, β)) :
    ⇑(s.sup' H f) = s.sup' H fun i ↦ ⇑(f i)

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : SemilatticeSup β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousSup β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
x✝ : α
⊢ (s.sup' H f) x✝ = s.sup' H (fun i => ⇑(f i)) x✝

Tactic:
simp [finsetSup'_apply]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : SemilatticeSup β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousSup β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
⊢ ⇑(s.sup' H f) = s.sup' H fun i => ⇑(f i)

Tactic:
ext

Result:
case h
α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : SemilatticeSup β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousSup β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
x✝ : α
⊢ (s.sup' H f) x✝ = s.sup' H (fun i => ⇑(f i)) x✝
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem toSpanNonzeroSingleton_one :
    LinearEquiv.toSpanNonzeroSingleton R M x h 1 =
      (⟨x, Submodule.mem_span_singleton_self x⟩ : R ∙ x)

Proof state:
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
h : x ≠ 0
⊢ (toSpanNonzeroSingleton R M x h) 1 = ⟨x, ⋯⟩

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1]
    [Entails α σ2] (f1 : σ1) (f2 : σ2) :
    Liff α f1 f2 ↔ Limplies α f1 f2 ∧ Limplies α f2 f1

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
⊢ Liff α f1 f2 ↔ Limplies α f1 f2 ∧ Limplies α f2 f1

Tactic:
simp [Liff, Limplies, iff_iff_implies_and_implies, forall_and]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem uniformity_lift_le_swap {g : Set (α × α) → Filter β} {f : Filter β} (hg : Monotone g)
    (h : ((𝓤 α).lift fun s => g (preimage Prod.swap s)) ≤ f) : (𝓤 α).lift g ≤ f :=
  calc
    (𝓤 α).lift g ≤ (Filter.map (@Prod.swap α α) <| 𝓤 α).lift g :=
      lift_mono uniformity_le_symm le_rfl
    _ ≤ _

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : Set (α × α) → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s => g (Prod.swap ⁻¹' s)) ≤ f
⊢ (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f

Tactic:
exact h

Result:
no goals

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : Set (α × α) → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s => g (Prod.swap ⁻¹' s)) ≤ f
⊢ (map Prod.swap (𝓤 α)).lift g ≤ f

Tactic:
rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]

Result:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : Set (α × α) → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s => g (Prod.swap ⁻¹' s)) ≤ f
⊢ (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.subset {s : Set α} (hs : s.Finite) {t : Set α} (ht : t ⊆ s) : t.Finite

Proof state:
α : Type u
s : Set α
hs : s.Finite
t : Set α
ht : t ⊆ s
this : Finite ↑s
⊢ t.Finite

Tactic:
exact Finite.Set.subset _ ht

Result:
no goals

Proof state:
α : Type u
s : Set α
hs : s.Finite
t : Set α
ht : t ⊆ s
⊢ t.Finite

Tactic:
have := hs.to_subtype

Result:
α : Type u
s : Set α
hs : s.Finite
t : Set α
ht : t ⊆ s
this : Finite ↑s
⊢ t.Finite
-- Mathlib/Analysis/Complex/Basic.lean
theorem summable_ofReal {f : α → ℝ} : (Summable fun x => (f x : 𝕜)) ↔ Summable f :=
  ⟨fun h => by simpa only [RCLike.reCLM_apply, RCLike.ofReal_re] using reCLM.summable h,
    ofRealCLM.summable⟩

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
f : α → ℝ
h : Summable fun x => ↑(f x)
⊢ Summable f

Tactic:
simpa only [RCLike.reCLM_apply, RCLike.ofReal_re] using reCLM.summable h

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffOn_iff_target :
    ContMDiffOn I I' n f s ↔
      ContinuousOn f s ∧
        ∀ y : M',
          ContMDiffOn I 𝓘(𝕜, E') n (extChartAt I' y ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source)

Proof state:
case mp
𝕜 : 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
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContinuousOn f s
⊢ (∀ (x : M) (y : M'),
      ContDiffOn 𝕜 n
        (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘
          f ∘ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
        (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
          ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
            (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))) →
    ∀ (y : M'),
      ContinuousOn (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f)
          (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source) ∧
        ∀ (x : M),
          E' →
            ContDiffOn 𝕜 n
              (↑𝓘(𝕜, E').toPartialEquiv ∘
                (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f) ∘
                  ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
              (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
                ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
                  (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))

Tactic:
refine fun h' y => ⟨?_, fun x _ => h' x y⟩

Result:
case mp
𝕜 : 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
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n
      (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘
        f ∘ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
      (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
        ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
          (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))
y : M'
⊢ ContinuousOn (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f)
    (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source)
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_sum_nat_add (f : ℕ → ℝ≥0) : Tendsto (fun i => ∑' k, f (k + i)) atTop (𝓝 0)

Proof state:
f : ℕ → ℝ≥0
⊢ Tendsto (fun a => ↑(∑' (k : ℕ), f (k + a))) atTop (𝓝 ↑0)

Tactic:
convert _root_.tendsto_sum_nat_add fun i => (f i : ℝ)

Result:
case h.e'_3.h
f : ℕ → ℝ≥0
x✝ : ℕ
⊢ ↑(∑' (k : ℕ), f (k + x✝)) = ∑' (k : ℕ), ↑(f (k + x✝))

Proof state:
f : ℕ → ℝ≥0
⊢ Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)

Tactic:
rw [← tendsto_coe]

Result:
f : ℕ → ℝ≥0
⊢ Tendsto (fun a => ↑(∑' (k : ℕ), f (k + a))) atTop (𝓝 ↑0)

Proof state:
case h.e'_3.h
f : ℕ → ℝ≥0
x✝ : ℕ
⊢ ↑(∑' (k : ℕ), f (k + x✝)) = ∑' (k : ℕ), ↑(f (k + x✝))

Tactic:
norm_cast

Result:
no goals
-- Mathlib/CategoryTheory/LiftingProperties/Basic.lean
theorem of_arrow_iso_right {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'}
    (e : Arrow.mk p ≅ Arrow.mk p') [hip : HasLiftingProperty i p] : HasLiftingProperty i p'

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i p'

Tactic:
rw [Arrow.iso_w' e]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i (e.inv.left ≫ p ≫ e.hom.right)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i (e.inv.left ≫ p ≫ e.hom.right)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α}
    {b : β a} : (m.insert a b).getKey! a = a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
a : α
b : β a
⊢ (m.insert a b).getKey! a = a

Tactic:
simp_to_model [insert] using List.getKey!_insertEntry_self

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_pos_iff_of_base_lt_one (hx : 0 < x) : 0 < logb b x ↔ x < 1

Proof state:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ 0 < logb b x ↔ x < 1

Tactic:
rw [← @logb_one b, logb_lt_logb_iff_of_base_lt_one b_pos b_lt_one zero_lt_one hx]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
/-- An inequality of Daykin. Interestingly, any lattice in which this inequality holds is
distributive. -/
lemma Finset.le_card_infs_mul_card_sups [DecidableEq α] (s t : Finset α) :
    #s * #t ≤ #(s ⊼ t) * #(s ⊻ t)

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : DecidableEq α
s t : Finset α
⊢ #s * #t ≤ #(s ⊼ t) * #(s ⊻ t)

Tactic:
simpa using four_functions_theorem (1 : α → ℕ) 1 1 1 zero_le_one zero_le_one zero_le_one
  zero_le_one (fun _ _ ↦ le_rfl) s t

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConcaveOn.congr (hf : ConcaveOn 𝕜 s f) (hfg : EqOn f g s) : ConcaveOn 𝕜 s g :=
  ⟨hf.1, fun x hx y hy a b ha hb hab => by
    simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha hb hab)] using hf.2 hx hy ha hb hab⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f g : E → β
hf : ConcaveOn 𝕜 s f
hfg : EqOn f g s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • g x + b • g y ≤ g (a • x + b • y)

Tactic:
simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha hb hab)] using hf.2 hx hy ha hb hab

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
/-- The restriction of `f - μ • 1` to the generalized `μ`-eigenspace is nilpotent. -/
lemma isNilpotent_restrict_maxGenEigenspace_sub_algebraMap [IsNoetherian R M] (f : End R M) (μ : R)
    (h : MapsTo (f - algebraMap R (End R M) μ)
      ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ) :=
      mapsTo_maxGenEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ) :
    IsNilpotent ((f - algebraMap R (End R M) μ).restrict h)

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)) ⋯
⊢ f.maxGenEigenspace μ ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Tactic:
rw [maxGenEigenspace_eq]

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)) ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ) h)

Tactic:
apply isNilpotent_restrict_of_le (q := f.genEigenspace μ (maxUnifEigenspaceIndex f μ))
  _ (isNilpotent_restrict_genEigenspace_nat f μ (maxUnifEigenspaceIndex f μ))

Result:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)) ⋯
⊢ f.maxGenEigenspace μ ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)
-- Mathlib/Order/Chain.lean
theorem IsChain.exists3 (hchain : IsChain r s) [IsTrans α r] {a b c} (mem1 : a ∈ s) (mem2 : b ∈ s)
    (mem3 : c ∈ s) : ∃ (z : _) (_ : z ∈ s), r a z ∧ r b z ∧ r c z

Proof state:
case intro.intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
⊢ ∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z

Tactic:
rcases directedOn_iff_directed.mpr (IsChain.directed hchain) z mem4 c mem3 with
  ⟨z', mem5, H3, H4⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
z' : α
mem5 : z' ∈ s
H3 : r z z'
H4 : r c z'
⊢ ∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
z' : α
mem5 : z' ∈ s
H3 : r z z'
H4 : r c z'
⊢ ∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z

Tactic:
exact ⟨z', mem5, _root_.trans H1 H3, _root_.trans H2 H3, H4⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
⊢ ∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z

Tactic:
rcases directedOn_iff_directed.mpr (IsChain.directed hchain) a mem1 b mem2 with ⟨z, mem4, H1, H2⟩

Result:
case intro.intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
⊢ ∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.WF.tail (hwf : (s : Heap α).WF le) : (s.tail le).WF le

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
hwf : WF le s
⊢ WF le (Heap.tail le s)

Tactic:
simp only [Heap.tail]

Result:
α : Type u_1
s : Heap α
le : α → α → Bool
hwf : WF le s
⊢ WF le ((Heap.tail? le s).getD Heap.nil)

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
hwf : WF le s
⊢ WF le ((Heap.tail? le s).getD Heap.nil)

Tactic:
match eq : s.tail? le with
| none => exact Heap.WF.nil
| some tl => exact hwf.tail? eq

Result:
no goals

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
hwf : WF le s
eq : Heap.tail? le s = none
⊢ WF le (none.getD Heap.nil)

Tactic:
exact Heap.WF.nil

Result:
no goals

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
hwf : WF le s
tl : Heap α
eq : Heap.tail? le s = some tl
⊢ WF le ((some tl).getD Heap.nil)

Tactic:
exact hwf.tail? eq

Result:
no goals
-- Mathlib/Data/Finset/Update.lean
lemma restrict_updateFinset {s : Finset ι} (x : Π i, π i) (y : Π i : s, π i) :
    s.restrict (updateFinset x s y) = y

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
y : (i : { x // x ∈ s }) → π ↑i
⊢ restrict₂ ⋯ y = y

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
y : (i : { x // x ∈ s }) → π ↑i
⊢ s.restrict (updateFinset x s y) = y

Tactic:
rw [restrict_updateFinset_of_subset subset_rfl]

Result:
ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
y : (i : { x // x ∈ s }) → π ↑i
⊢ restrict₂ ⋯ y = y
-- Mathlib/Algebra/Order/Monovary.lean
lemma monovary_iff_forall_mul_nonneg : Monovary f g ↔ ∀ i j, 0 ≤ (f j - f i) * (g j - g i)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedRing α
f g : ι → α
⊢ Monovary f g ↔ ∀ (i j : ι), 0 ≤ (f j - f i) * (g j - g i)

Tactic:
simp only [smul_eq_mul, monovary_iff_forall_smul_nonneg]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem nfp_lt_ord {f : Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c) (hf : ∀ i < c, f i < c) {a} :
    a < c → nfp f a < c :=
  nfpFamily_lt_ord_lift hc (by simpa using Cardinal.one_lt_aleph0.trans hc) fun _ => hf

Proof state:
f : Ordinal.{u_1} → Ordinal.{u_1}
c : Ordinal.{u_1}
hc : ℵ₀ < c.cof
hf : ∀ i < c, f i < c
a : Ordinal.{u_1}
⊢ Cardinal.lift.{u_1, 0} #Unit < c.cof

Tactic:
simpa using Cardinal.one_lt_aleph0.trans hc

Result:
no goals
-- Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
theorem one_CNF {o : Ordinal} (ho : o ≠ 0) : CNF 1 o = [(0, o)]

Proof state:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ CNF 1 o = [(0, o)]

Tactic:
simp [CNF_ne_zero ho]

Result:
no goals