harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem image_of_isOpenImmersion (f : X ⟶ Y) [H : IsOpenImmersion f] :
    IsAffineOpen (f ''ᵁ U)

Proof state:
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen (f ''ᵁ U)

Tactic:
have : IsAffine _ := hU

Result:
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
this : IsAffine ↑U
⊢ IsAffineOpen (f ''ᵁ U)

Proof state:
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
this : IsAffine ↑U
⊢ IsAffineOpen (f ''ᵁ U)

Tactic:
convert isAffineOpen_opensRange (U.ι ≫ f)

Result:
case h.e'_2
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
this : IsAffine ↑U
⊢ f ''ᵁ U = Scheme.Hom.opensRange (U.ι ≫ f)

Proof state:
case h.e'_2.h
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
this : IsAffine ↑U
⊢ ↑(f ''ᵁ U) = ↑(Scheme.Hom.opensRange (U.ι ≫ f))

Tactic:
exact Set.image_eq_range _ _

Result:
no goals

Proof state:
case h.e'_2
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
this : IsAffine ↑U
⊢ f ''ᵁ U = Scheme.Hom.opensRange (U.ι ≫ f)

Tactic:
ext1

Result:
case h.e'_2.h
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
this : IsAffine ↑U
⊢ ↑(f ''ᵁ U) = ↑(Scheme.Hom.opensRange (U.ι ≫ f))
-- Mathlib/Data/Set/Function.lean
theorem surjOn_range (h : Semiconj f fa fb) (ha : Surjective fa) :
    SurjOn fb (range f) (range f)

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (f '' univ) (f '' univ)

Tactic:
exact h.surjOn_image (ha.surjOn univ)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (range f) (range f)

Tactic:
rw [← image_univ]

Result:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (f '' univ) (f '' univ)
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
/-- The difference of `log (1-z)⁻¹` and its `(n+1)`st Taylor polynomial can be bounded in
terms of `‖z‖`. -/
lemma norm_log_one_sub_inv_add_logTaylor_neg_le (n : ℕ) {z : ℂ} (hz : ‖z‖ < 1) :
    ‖log (1 - z)⁻¹ + logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (n + 1)

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 - z)⁻¹ + logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
rw [sub_eq_add_neg,
  log_inv _ <| slitPlane_arg_ne_pi <| mem_slitPlane_of_norm_lt_one <| (norm_neg z).symm ▸ hz,
  ← sub_neg_eq_add, ← neg_sub', norm_neg]

Result:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + -z) - logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Proof state:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + -z) - logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
convert norm_log_sub_logTaylor_le n <| (norm_neg z).symm ▸ hz using 4 <;> rw [norm_neg]

Result:
no goals
-- Mathlib/RingTheory/Flat/EquationalCriterion.lean
theorem _root_.Equiv.isTrivialRelation_comp {κ} [Fintype κ] (e : κ ≃ ι) :
    IsTrivialRelation (f ∘ e) (x ∘ e) ↔ IsTrivialRelation f x

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
f : ι → R
x : ι → M
κ : Type u_4
inst✝ : Fintype κ
e : κ ≃ ι
⊢ IsTrivialRelation (f ∘ ⇑e) (x ∘ ⇑e) ↔ IsTrivialRelation f x

Tactic:
simp_rw [isTrivialRelation_iff_vanishesTrivially, e.vanishesTrivially_comp]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem measure_toMeasurable_inter_of_cover {s : Set α} (hs : MeasurableSet s) {t : Set α}
    {v : ℕ → Set α} (hv : t ⊆ ⋃ n, v n) (h'v : ∀ n, μ (t ∩ v n) ≠ ∞) :
    μ (toMeasurable μ t ∩ s) = μ (t ∩ s)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ⊤
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
⊢ μ
      ((if h : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t then h.choose
        else
          if h' : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ ∀ (u : Set α), MeasurableSet u → μ (t_1 ∩ u) = μ (t ∩ u) then h'.choose
          else ⋯.choose) ∩
        s) =
    μ (t ∩ s)

Tactic:
split_ifs with ht

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ⊤
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
⊢ μ (ht.choose ∩ s) = μ (t ∩ s)

case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ⊤
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ¬∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
⊢ μ (A.choose ∩ s) = μ (t ∩ s)

Proof state:
case e_f.h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ⊤
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ μ (t ∩ disjointed w n) ≠ ⊤

Tactic:
apply ne_of_lt

Result:
case e_f.h.h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ⊤
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ μ (t ∩ disjointed w n) < ⊤

Proof state:
case hn
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ⊤
w : ℕ → Set α := fun n => toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ⊤
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Pairwise (Disjoint on disjointed w)

Tactic:
exact disjoint_disjointed _

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublists'_eq_sublists'Aux (l : List α) :
    sublists' l = l.foldr (fun a r => sublists'Aux a r r) [[]]

Proof state:
α : Type u
l : List α
⊢ l.sublists' = foldr (fun a r => sublists'Aux a r r) [[]] l

Tactic:
simp only [sublists', sublists'Aux_eq_array_foldl]

Result:
α : Type u
l : List α
⊢ (foldr (fun a arr => Array.foldl (fun r l => r.push (a :: l)) arr arr) #[[]] l).toList =
    foldr (fun a r => (Array.foldl (fun r l => r.push (a :: l)) r.toArray r.toArray).toList) [[]] l

Proof state:
α : Type u
l : List α
⊢ (foldr (fun a arr => Array.foldl (fun r l => r.push (a :: l)) arr arr) #[[]] l).toList =
    foldr (fun a r => (Array.foldl (fun r l => r.push (a :: l)) r.toArray r.toArray).toList) [[]] l

Tactic:
rw [← List.foldr_hom Array.toList]

Result:
case H
α : Type u
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    (Array.foldl (fun r l => r.push (x :: l)) y.toList.toArray y.toList.toArray).toList =
      (Array.foldl (fun r l => r.push (x :: l)) y y).toList

Proof state:
case H
α : Type u
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    (Array.foldl (fun r l => r.push (x :: l)) y.toList.toArray y.toList.toArray).toList =
      (Array.foldl (fun r l => r.push (x :: l)) y y).toList

Tactic:
intros _ _

Result:
case H
α : Type u
l : List α
x✝ : α
y✝ : Array (List α)
⊢ (Array.foldl (fun r l => r.push (x✝ :: l)) y✝.toList.toArray y✝.toList.toArray).toList =
    (Array.foldl (fun r l => r.push (x✝ :: l)) y✝ y✝).toList

Proof state:
case H
α : Type u
l : List α
x✝ : α
y✝ : Array (List α)
⊢ (Array.foldl (fun r l => r.push (x✝ :: l)) y✝.toList.toArray y✝.toList.toArray).toList =
    (Array.foldl (fun r l => r.push (x✝ :: l)) y✝ y✝).toList

Tactic:
congr

Result:
no goals
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
@[simp]
lemma bind_const {m : Measure α} {ν : Measure β} : m.bind (fun _ ↦ ν) = m Set.univ • ν

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
⊢ (m.bind fun x => ν) s = (m univ • ν) s

Tactic:
rw [bind_apply hs measurable_const, lintegral_const, smul_apply, smul_eq_mul, mul_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
ν : Measure β
⊢ (m.bind fun x => ν) = m univ • ν

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
⊢ (m.bind fun x => ν) s = (m univ • ν) s
-- Mathlib/CategoryTheory/Subpresheaf/OfSection.lean
lemma range_eq_ofSection {X : C} (f : yoneda.obj X ⟶ F) :
    range f = ofSection (yonedaEquiv f)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : C
f : yoneda.obj X ⟶ F
⊢ range f = ofSection (yonedaEquiv f)

Tactic:
rw [ofSection_eq_range, Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_eq_cons_Ioo (h : a < b) : Ico a b = (Ioo a b).cons a left_not_mem_Ioo

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ico a b = cons a (Ioo a b) ⋯

Tactic:
classical rw [cons_eq_insert, Ioo_insert_left h]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ico a b = cons a (Ioo a b) ⋯

Tactic:
rw [cons_eq_insert, Ioo_insert_left h]

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean
lemma strictConcaveOn_sqrt : StrictConcaveOn ℝ (Set.Ici 0) (√· : ℝ → ℝ)

Proof state:
⊢ StrictConcaveOn ℝ (Ici 0) fun x => (fun x => x ^ (1 / 2)) x

Tactic:
exact strictConcaveOn_rpow (by positivity) (by linarith)

Result:
no goals

Proof state:
⊢ StrictConcaveOn ℝ (Ici 0) fun x => √x

Tactic:
rw [funext Real.sqrt_eq_rpow]

Result:
⊢ StrictConcaveOn ℝ (Ici 0) fun x => (fun x => x ^ (1 / 2)) x

Proof state:
⊢ 0 < 1 / 2

Tactic:
positivity

Result:
no goals

Proof state:
⊢ 1 / 2 < 1

Tactic:
linarith

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem iInf_toSubmodule {ι : Sort*} (S : ι → Subalgebra R A) :
    toSubmodule (⨅ i, S i) = ⨅ i, toSubmodule (S i) :=
  SetLike.coe_injective <| by simp

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
⊢ ↑(toSubmodule (⨅ i, S i)) = ↑(⨅ i, toSubmodule (S i))

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/Lemmas.lean
/-- If `μ` is a primitive `n`th root of unity in `R`, then `∏(1≤k<n) (1-μ^k) = n`.
(Stated with `n+1` in place of `n` to avoid the condition `n ≠ 0`.) -/
lemma prod_one_sub_pow_eq_order {n : ℕ} {μ : R} (hμ : IsPrimitiveRoot μ (n + 1)) :
    ∏ k ∈ range n, (1 - μ ^ (k + 1)) = n + 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : eval 1 (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) = eval 1 (∑ i ∈ range (n + 1), X ^ i)
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Tactic:
simpa only [mul_one, map_pow, eval_prod, eval_sub, eval_X, eval_pow, eval_C, eval_geom_sum,
  one_pow, sum_const, card_range, nsmul_eq_mul, Nat.cast_add, Nat.cast_one] using this

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : ∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1)) = ∑ i ∈ range (n + 1), X ^ i
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Tactic:
apply_fun Polynomial.eval 1 at this

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : eval 1 (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) = eval 1 (∑ i ∈ range (n + 1), X ^ i)
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : X ^ (n + 1) - C 1 = ∏ i ∈ range (n + 1), (X - C (μ ^ i * 1))
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Tactic:
rw [C_1, ← mul_geom_sum, prod_range_succ', pow_zero, mul_one, mul_comm, eq_comm] at this

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) * (X - C 1) = (∑ i ∈ range (n + 1), X ^ i) * (X - 1)
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Tactic:
have := X_pow_sub_C_eq_prod hμ n.zero_lt_succ (one_pow (n + 1))

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : X ^ (n + 1) - C 1 = ∏ i ∈ range (n + 1), (X - C (μ ^ i * 1))
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) * (X - C 1) = (∑ i ∈ range (n + 1), X ^ i) * (X - 1)
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Tactic:
replace this := mul_right_cancel₀ (Polynomial.X_sub_C_ne_zero 1) this

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : ∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1)) = ∑ i ∈ range (n + 1), X ^ i
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1
-- Mathlib/Topology/Algebra/SeparationQuotient/Section.lean
theorem exists_out_continuousLinearMap :
    ∃ f : SeparationQuotient E →L[K] E, mkCLM K E ∘L f = .id K (SeparationQuotient E)

Proof state:
K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul K E
f : SeparationQuotient E →ₗ[K] E
hf : mk ∘ ⇑f = id
⊢ Continuous (mk ∘ f.toFun)

Tactic:
continuity

Result:
no goals

Proof state:
K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul K E
⊢ ∃ f, (mkCLM K E).comp f = ContinuousLinearMap.id K (SeparationQuotient E)

Tactic:
rcases (mkCLM K E).toLinearMap.exists_rightInverse_of_surjective
  (LinearMap.range_eq_top.mpr surjective_mk) with ⟨f, hf⟩

Result:
case intro
K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul K E
f : SeparationQuotient E →ₗ[K] E
hf : ↑(mkCLM K E) ∘ₗ f = LinearMap.id
⊢ ∃ f, (mkCLM K E).comp f = ContinuousLinearMap.id K (SeparationQuotient E)

Proof state:
case intro
K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul K E
f : SeparationQuotient E →ₗ[K] E
hf : mk ∘ ⇑f = id
⊢ ∃ f, (mkCLM K E).comp f = ContinuousLinearMap.id K (SeparationQuotient E)

Tactic:
exact ⟨⟨f, isInducing_mk.continuous_iff.2 (by continuity)⟩, DFunLike.ext' hf⟩

Result:
no goals

Proof state:
case intro
K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul K E
f : SeparationQuotient E →ₗ[K] E
hf : ↑(mkCLM K E) ∘ₗ f = LinearMap.id
⊢ ∃ f, (mkCLM K E).comp f = ContinuousLinearMap.id K (SeparationQuotient E)

Tactic:
replace hf : mk ∘ f = id := congr_arg DFunLike.coe hf

Result:
case intro
K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul K E
f : SeparationQuotient E →ₗ[K] E
hf : mk ∘ ⇑f = id
⊢ ∃ f, (mkCLM K E).comp f = ContinuousLinearMap.id K (SeparationQuotient E)
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem union_succ : GoodProducts C = GoodProducts (π C (ord I · < o)) ∪ MaxProducts C ho

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ GoodProducts C = GoodProducts (π C fun x => ord I x < o) ∪ MaxProducts C ho

Tactic:
ext l

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
⊢ l ∈ GoodProducts C ↔ l ∈ GoodProducts (π C fun x => ord I x < o) ∪ MaxProducts C ho
-- Mathlib/Data/Rat/Defs.lean
lemma zero_of_num_zero {q : ℚ} (hq : q.num = 0) : q = 0

Proof state:
q : ℚ
hq : q.num = 0
⊢ q = 0

Tactic:
simpa [hq] using q.num_divInt_den.symm

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem sq_add_sq_of_nat_prime_of_not_irreducible (p : ℕ) [hp : Fact p.Prime]
    (hpi : ¬Irreducible (p : ℤ[i])) : ∃ a b, a ^ 2 + b ^ 2 = p :=
  have hpu : ¬IsUnit (p : ℤ[i]) :=
    mt norm_eq_one_iff.2 <| by
      rw [norm_natCast, Int.natAbs_mul, mul_eq_one]
      exact fun h => (ne_of_lt hp.1.one_lt).symm h.1
  have hab : ∃ a b, (p : ℤ[i]) = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
⊢ ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b

Tactic:
simpa only [true_and, not_false_iff, exists_prop, irreducible_iff, hpu, not_forall, not_or]
  using hpi

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
hnap : (norm a).natAbs = p
⊢ a.re.natAbs ^ 2 + a.im.natAbs ^ 2 = p

Tactic:
simpa [natAbs_norm_eq, sq] using hnap

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
⊢ ¬((↑p).natAbs = 1 ∧ (↑p).natAbs = 1)

Tactic:
exact fun h => (ne_of_lt hp.1.one_lt).symm h.1

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ (norm a).natAbs * (norm b).natAbs = p ^ 2

Tactic:
rw [← Int.natCast_inj, Int.natCast_pow, sq, ← @norm_natCast (-1), hpab]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ ↑((norm a).natAbs * (norm b).natAbs) = norm (a * b)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
⊢ ¬(norm ↑p).natAbs = 1

Tactic:
rw [norm_natCast, Int.natAbs_mul, mul_eq_one]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
⊢ ¬((↑p).natAbs = 1 ∧ (↑p).natAbs = 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ ↑((norm a).natAbs * (norm b).natAbs) = norm (a * b)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.noSibling_merge (le) (s₁ s₂ : Heap α) :
    (s₁.merge le s₂).NoSibling

Proof state:
case h_4
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₁✝ : α
c₁✝ sibling✝¹ : Heap α
a₂✝ : α
c₂✝ sibling✝ : Heap α
⊢ (if le a₁✝ a₂✝ = true then node a₁✝ (node a₂✝ c₂✝ c₁✝) nil else node a₂✝ (node a₁✝ c₁✝ c₂✝) nil).NoSibling

Tactic:
split

Result:
case h_4.isTrue
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₁✝ : α
c₁✝ sibling✝¹ : Heap α
a₂✝ : α
c₂✝ sibling✝ : Heap α
h✝ : le a₁✝ a₂✝ = true
⊢ (node a₁✝ (node a₂✝ c₂✝ c₁✝) nil).NoSibling

case h_4.isFalse
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₁✝ : α
c₁✝ sibling✝¹ : Heap α
a₂✝ : α
c₂✝ sibling✝ : Heap α
h✝ : ¬le a₁✝ a₂✝ = true
⊢ (node a₂✝ (node a₁✝ c₁✝ c₂✝) nil).NoSibling

Proof state:
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
⊢ (match s₁, s₂ with
    | nil, nil => nil
    | nil, node a₂ c₂ sibling => node a₂ c₂ nil
    | node a₁ c₁ sibling, nil => node a₁ c₁ nil
    | node a₁ c₁ sibling, node a₂ c₂ sibling_1 =>
      if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil).NoSibling

Tactic:
(split <;> try split) <;> constructor

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
⊢ (match s₁, s₂ with
    | nil, nil => nil
    | nil, node a₂ c₂ sibling => node a₂ c₂ nil
    | node a₁ c₁ sibling, nil => node a₁ c₁ nil
    | node a₁ c₁ sibling, node a₂ c₂ sibling_1 =>
      if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil).NoSibling

Tactic:
split <;> try split

Result:
case h_1
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
⊢ nil.NoSibling

case h_2
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₂✝ : α
c₂✝ sibling✝ : Heap α
⊢ (node a₂✝ c₂✝ nil).NoSibling

case h_3
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₁✝ : α
c₁✝ sibling✝ : Heap α
⊢ (node a₁✝ c₁✝ nil).NoSibling

case h_4.isTrue
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₁✝ : α
c₁✝ sibling✝¹ : Heap α
a₂✝ : α
c₂✝ sibling✝ : Heap α
h✝ : le a₁✝ a₂✝ = true
⊢ (node a₁✝ (node a₂✝ c₂✝ c₁✝) nil).NoSibling

case h_4.isFalse
α : Type u_1
le : α → α → Bool
x✝¹ x✝ : Heap α
a₁✝ : α
c₁✝ sibling✝¹ : Heap α
a₂✝ : α
c₂✝ sibling✝ : Heap α
h✝ : ¬le a₁✝ a₂✝ = true
⊢ (node a₂✝ (node a₁✝ c₁✝ c₂✝) nil).NoSibling

Proof state:
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
⊢ (merge le s₁ s₂).NoSibling

Tactic:
unfold merge

Result:
α : Type u_1
le : α → α → Bool
s₁ s₂ : Heap α
⊢ (match s₁, s₂ with
    | nil, nil => nil
    | nil, node a₂ c₂ sibling => node a₂ c₂ nil
    | node a₁ c₁ sibling, nil => node a₁ c₁ nil
    | node a₁ c₁ sibling, node a₂ c₂ sibling_1 =>
      if le a₁ a₂ = true then node a₁ (node a₂ c₂ c₁) nil else node a₂ (node a₁ c₁ c₂) nil).NoSibling
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α}
    {b : β a} :
    (m.insert a b).getKeyD a fallback = a

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

Tactic:
simp_to_model [insert] using List.getKeyD_insertEntry_self

Result:
no goals
-- Mathlib/Data/Nat/Choose/Bounds.lean
theorem choose_succ_le_two_pow (n k : ℕ) : (n + 1).choose k ≤ 2 ^ n

Proof state:
case neg.succ.zero
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ 1 ≤ 2 ^ (n + 1)

Tactic:
exact Nat.one_le_two_pow

Result:
no goals

Proof state:
case neg.succ.succ
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1 + 1).choose (k + 1) ≤ 2 ^ (n + 1)

Tactic:
rw [choose_succ_succ', two_pow_succ]

Result:
case neg.succ.succ
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1).choose k + (n + 1).choose (k + 1) ≤ 2 ^ n + 2 ^ n

Proof state:
case neg.succ.succ
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1).choose k + (n + 1).choose (k + 1) ≤ 2 ^ n + 2 ^ n

Tactic:
exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))

Result:
no goals

Proof state:
case neg.zero
k : ℕ
lt : ¬0 + 1 < k
⊢ (0 + 1).choose k ≤ 2 ^ 0

Tactic:
cases k <;> simp_all

Result:
no goals

Proof state:
case neg.succ
k n : ℕ
lt : ¬n + 1 + 1 < k
⊢ (n + 1 + 1).choose k ≤ 2 ^ (n + 1)

Tactic:
rcases k with - | k

Result:
case neg.succ.zero
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ (n + 1 + 1).choose 0 ≤ 2 ^ (n + 1)

case neg.succ.succ
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1 + 1).choose (k + 1) ≤ 2 ^ (n + 1)

Proof state:
case neg.succ.zero
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ (n + 1 + 1).choose 0 ≤ 2 ^ (n + 1)

Tactic:
rw [choose_zero_right]

Result:
case neg.succ.zero
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ 1 ≤ 2 ^ (n + 1)

Proof state:
n k : ℕ
⊢ (n + 1).choose k ≤ 2 ^ n

Tactic:
by_cases lt : n + 1 < k

Result:
case pos
n k : ℕ
lt : n + 1 < k
⊢ (n + 1).choose k ≤ 2 ^ n

case neg
n k : ℕ
lt : ¬n + 1 < k
⊢ (n + 1).choose k ≤ 2 ^ n

Proof state:
case pos
n k : ℕ
lt : n + 1 < k
⊢ (n + 1).choose k ≤ 2 ^ n

Tactic:
simp [choose_eq_zero_of_lt lt]

Result:
no goals