harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/SupClosed.lean
lemma SupClosed.biSup_mem {ι : Type*} {t : Set ι} {f : ι → α} (hs : SupClosed s)
    (ht : t.Finite) (hbot : ⊥ ∈ s) (hf : ∀ i ∈ t, f i ∈ s) : ⨆ i ∈ t, f i ∈ s

Proof state:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ sSup (f '' t) ∈ s

Tactic:
exact hs.sSup_mem (ht.image _) hbot (by simpa)

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ f '' t ⊆ s

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ ⨆ i ∈ t, f i ∈ s

Tactic:
rw [← sSup_image]

Result:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ sSup (f '' t) ∈ s
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem norm_eq {x : ℝ} : ‖(x : AddCircle p)‖ = |x - round (p⁻¹ * x) * p|

Proof state:
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
h : b ∈ lowerBounds (abs '' {m | ↑m = ↑x})
⊢ |fract x - 1| = 1 - fract x

Tactic:
rw [abs_sub_comm, abs_one_sub_fract]

Result:
no goals

Proof state:
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ x = b - ↑z

Tactic:
rw [hz]

Result:
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
b : ℝ
z : ℤ
hz : ↑z = b - x
⊢ x = b - (b - x)

Proof state:
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
⊢ fract x ⊓ (1 - fract x) ≤ sInf (norm '' {m | ↑m = ↑x})

Tactic:
simp only [QuotientAddGroup.mk'_apply, Real.norm_eq_abs, le_csInf_iff h₁ h₂]

Result:
case a
x : ℝ
h₁ : BddBelow (abs '' {m | ↑m = ↑x})
h₂ : (abs '' {m | ↑m = ↑x}).Nonempty
⊢ ∀ b ∈ abs '' {m | ↑m = ↑x}, fract x ⊓ (1 - fract x) ≤ b
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem X_prime : Prime (X : R⟦X⟧)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (Ideal.span {X}).IsPrime

Tactic:
exact span_X_isPrime

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : X = 0
⊢ False

Tactic:
simpa [map_zero (coeff R 1)] using congr_arg (coeff R 1) h

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X ≠ 0

Tactic:
intro h

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : X = 0
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Prime X

Tactic:
rw [← Ideal.span_singleton_prime]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (Ideal.span {X}).IsPrime

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X ≠ 0
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_generateFrom_singleton_iff {s t : Set α} :
    MeasurableSet[MeasurableSpace.generateFrom {s}] t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Proof state:
case h
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
p : Prop
hp : p ∈ x
⊢ p = False

Tactic:
by_contra hpneg

Result:
case h
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
p : Prop
hp : p ∈ x
hpneg : ¬p = False
⊢ False

Proof state:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
p : Prop
hp : p ∈ x
hpneg : False ↔ p
⊢ False ∈ x

Tactic:
convert hp

Result:
no goals

Proof state:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
⊢ (fun x => x ∈ s) ⁻¹' x = ∅ ∨ (fun x => x ∈ s) ⁻¹' x = s ∨ (fun x => x ∈ s) ⁻¹' x = sᶜ ∨ (fun x => x ∈ s) ⁻¹' x = univ

Tactic:
have hx : x = {True} := by
  ext p
  refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩
  by_contra hpneg
  rw [eq_iff_iff, iff_true, ← false_iff] at hpneg
  exact hF (by convert hp)

Result:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
hx : x = {True}
⊢ (fun x => x ∈ s) ⁻¹' x = ∅ ∨ (fun x => x ∈ s) ⁻¹' x = s ∨ (fun x => x ∈ s) ⁻¹' x = sᶜ ∨ (fun x => x ∈ s) ⁻¹' x = univ

Proof state:
case h
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
p : Prop
hp : p ∈ x
hpneg : ¬p = True
⊢ False

Tactic:
rw [eq_iff_iff, iff_true, ← false_iff] at hpneg

Result:
case h
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
p : Prop
hp : p ∈ x
hpneg : False ↔ p
⊢ False

Proof state:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
⊢ (fun x => x ∈ s) ⁻¹' x = ∅ ∨ (fun x => x ∈ s) ⁻¹' x = s ∨ (fun x => x ∈ s) ⁻¹' x = sᶜ ∨ (fun x => x ∈ s) ⁻¹' x = univ

Tactic:
by_cases hF : False ∈ x

Result:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
⊢ (fun x => x ∈ s) ⁻¹' x = ∅ ∨ (fun x => x ∈ s) ⁻¹' x = s ∨ (fun x => x ∈ s) ⁻¹' x = sᶜ ∨ (fun x => x ∈ s) ⁻¹' x = univ

case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
⊢ (fun x => x ∈ s) ⁻¹' x = ∅ ∨ (fun x => x ∈ s) ⁻¹' x = s ∨ (fun x => x ∈ s) ⁻¹' x = sᶜ ∨ (fun x => x ∈ s) ⁻¹' x = univ
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis.iUnion_isBasis_iUnion {ι : Type _} (X I : ι → Set α)
    (hI : ∀ i, M.IsBasis (I i) (X i)) (h_ind : M.Indep (⋃ i, I i)) :
    M.IsBasis (⋃ i, I i) (⋃ i, X i)

Proof state:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
⊢ ∀ e ∈ (⋃ i, X i) \ ⋃ i, I i, M.Dep (insert e (⋃ i, I i))

Tactic:
rintro e ⟨⟨_, ⟨⟨i, hi, rfl⟩, (hes : e ∈ X i)⟩⟩, he'⟩

Result:
case intro.intro.intro.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : e ∉ ⋃ i, I i
i : ι
hes : e ∈ X i
⊢ M.Dep (insert e (⋃ i, I i))

Proof state:
case intro.intro.intro.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ insert e (⋃ i, I i) ⊆ M.E

Tactic:
rw [insert_subset_iff, iUnion_subset_iff, and_iff_left (fun i ↦ (hI i).indep.subset_ground)]

Result:
case intro.intro.intro.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ e ∈ M.E

Proof state:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
⊢ M.IsBasis (⋃ i, I i) (⋃ i, X i)

Tactic:
refine h_ind.isBasis_of_forall_insert
  (iUnion_subset (fun i ↦ (hI i).subset.trans (subset_iUnion _ _))) ?_

Result:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
⊢ ∀ e ∈ (⋃ i, X i) \ ⋃ i, I i, M.Dep (insert e (⋃ i, I i))

Proof state:
case intro.intro.intro.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : e ∉ ⋃ i, I i
i : ι
hes : e ∈ X i
⊢ M.Dep (insert e (⋃ i, I i))

Tactic:
rw [mem_iUnion, not_exists] at he'

Result:
case intro.intro.intro.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ M.Dep (insert e (⋃ i, I i))

Proof state:
case intro.intro.intro.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ M.Dep (insert e (⋃ i, I i))

Tactic:
refine ((hI i).insert_dep ⟨hes, he' _⟩).superset (insert_subset_insert (subset_iUnion _ _)) ?_

Result:
case intro.intro.intro.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ insert e (⋃ i, I i) ⊆ M.E

Proof state:
case intro.intro.intro.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ e ∈ M.E

Tactic:
exact (hI i).subset_ground hes

Result:
no goals
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_isSubordinate_chartAt_source_of_isClosed {s : Set M} (hs : IsClosed s) :
    ∃ f : SmoothPartitionOfUnity s I M s,
      f.IsSubordinate (fun x ↦ (chartAt H (x : M)).source)

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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
⊢ ∃ f, f.IsSubordinate fun x => (chartAt H ↑x).source

Tactic:
apply exists_isSubordinate _ hs _ (fun i ↦ (chartAt H _).open_source) (fun x hx ↦ ?_)

Result:
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
x : M
hx : x ∈ s
⊢ x ∈ ⋃ i, (chartAt H ↑i).source

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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
x : M
hx : x ∈ s
⊢ x ∈ ⋃ i, (chartAt H ↑i).source

Tactic:
exact mem_iUnion_of_mem ⟨x, hx⟩ (mem_chart_source H x)

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem le_to_nat {m n : Num} : (m : ℕ) ≤ n ↔ m ≤ n

Proof state:
m n : Num
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]

Result:
m n : Num
⊢ ¬↑n < ↑m ↔ m ≤ n

Proof state:
m n : Num
⊢ ¬↑n < ↑m ↔ m ≤ n

Tactic:
exact not_congr lt_to_nat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem admissible_or (P Q : α → Prop)
  (hadm₁ : admissible P) (hadm₂ : admissible Q) : admissible (fun x => P x ∨ Q x)

Proof state:
case inl.h
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
hP : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ P (csup fun x => c x ∧ P x)

Tactic:
apply hadm₁ _ (chain_conj _ _ hchain)

Result:
case inl.h
α : Sort u
inst✝ : CCPO α
P Q : α → Prop
hadm₁ : admissible P
hadm₂ : admissible Q
c : α → Prop
hchain : chain c
h : ∀ (x : α), c x → (fun x => P x ∨ Q x) x
hP : ∀ (x : α), c x → ∃ y, c y ∧ x ⊑ y ∧ P y
⊢ ∀ (x : α), c x ∧ P x → P x
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsCycle.snd_ne_penultimate {p : G.Walk u u} (hp : p.IsCycle) : p.snd ≠ p.penultimate

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 ≤ p.length - 1

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
this : 3 ≤ p.length
h : 1 = p.length - 1
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
simp

Result:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ p.length - 1 ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
simp

Result:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 ≤ p.length - 1

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
⊢ p.snd ≠ p.penultimate

Tactic:
intro h

Result:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ False

Tactic:
apply hp.getVert_injOn (by simp; omega) (by simp; omega) at h

Result:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
this : 3 ≤ p.length
h : 1 = p.length - 1
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
⊢ False

Tactic:
have := hp.three_le_length

Result:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 ≤ p.length

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteArray.lean
theorem data_append (a b : ByteArray) : (a ++ b).data = a.data ++ b.data

Proof state:
a b : ByteArray
⊢ (a ++ b).data = a.data ++ b.data

Tactic:
rw [←append_eq]

Result:
a b : ByteArray
⊢ (a.append b).data = a.data ++ b.data

Proof state:
a b : ByteArray
⊢ (a.append b).data = a.data ++ b.data

Tactic:
simp [ByteArray.append, size]

Result:
a b : ByteArray
⊢ a.data ++ (b.data ++ a.data.extract (a.data.size + b.data.size)) = a.data ++ b.data

Proof state:
a b : ByteArray
⊢ a.data ++ (b.data ++ a.data.extract (a.data.size + b.data.size)) = a.data ++ b.data

Tactic:
rw [Array.extract_empty_of_stop_le_start (h:=Nat.le_add_right ..), Array.append_empty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem insertMany_val [BEq α][Hashable α] {m : Raw₀ α β} {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {l : ρ} :
    m.val.insertMany l = m.insertMany l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw₀ α β
ρ : Type w
inst✝ : ForIn Id ρ ((a : α) × β a)
l : ρ
⊢ m.val.insertMany l = (m.insertMany l).val.val

Tactic:
simp [Raw.insertMany, m.2]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/FiniteDimension.lean
theorem LinearMap.isClosedEmbedding_of_injective [T2Space E] [FiniteDimensional 𝕜 E] {f : E →ₗ[𝕜] F}
    (hf : LinearMap.ker f = ⊥) : IsClosedEmbedding f :=
  let g := LinearEquiv.ofInjective f (LinearMap.ker_eq_bot.mp hf)
  { IsEmbedding.subtypeVal.comp g.toContinuousLinearEquiv.toHomeomorph.isEmbedding with
    isClosed_range

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : CompleteSpace 𝕜
inst✝¹² : AddCommGroup E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : IsTopologicalAddGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : ContinuousSMul 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : T2Space F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
hf : ker f = ⊥
g : E ≃ₗ[𝕜] ↥(range f) := LinearEquiv.ofInjective f ⋯
this : FiniteDimensional 𝕜 ↥(range f)
⊢ IsClosed (Set.range ⇑f)

Tactic:
simpa [LinearMap.range_coe f] using f.range.closed_of_finiteDimensional

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : CompleteSpace 𝕜
inst✝¹² : AddCommGroup E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : IsTopologicalAddGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : ContinuousSMul 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : T2Space F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
hf : ker f = ⊥
g : E ≃ₗ[𝕜] ↥(range f) := LinearEquiv.ofInjective f ⋯
⊢ IsClosed (Set.range ⇑f)

Tactic:
haveI := f.finiteDimensional_range

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : CompleteSpace 𝕜
inst✝¹² : AddCommGroup E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : IsTopologicalAddGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : ContinuousSMul 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : T2Space F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
hf : ker f = ⊥
g : E ≃ₗ[𝕜] ↥(range f) := LinearEquiv.ofInjective f ⋯
this : FiniteDimensional 𝕜 ↥(range f)
⊢ IsClosed (Set.range ⇑f)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
/-- The negated addition of two affine points in `W` on a sloped line lies in `W`. -/
lemma equation_negAdd {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
    (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : W.Equation
      (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) (W.negAddY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂)

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ W.Equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
rw [equation_add_iff, addPolynomial_slope h₁ h₂ hxy]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ eval (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
      (-((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))) =
    0

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ eval (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
      (-((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))) =
    0

Tactic:
eval_simp

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ -((W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) *
        (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) =
    0

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ -((W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) *
        (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) =
    0

Tactic:
rw [neg_eq_zero, sub_self, mul_zero]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Module.lean
theorem sum_Ioc_by_parts (hmn : m < n) :
    ∑ i ∈ Ioc m n, f i • g i =
      f n • G (n + 1) - f (m + 1) • G (m + 1)
        - ∑ i ∈ Ioc m (n - 1), (f (i + 1) - f i) • G (i + 1)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
⊢ ∑ i ∈ Ioc m n, f i • g i =
    f n • ∑ i ∈ range (n + 1), g i - f (m + 1) • ∑ i ∈ range (m + 1), g i -
      ∑ i ∈ Ioc m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
simpa only [← Nat.Ico_succ_succ, Nat.succ_eq_add_one, Nat.sub_add_cancel (Nat.one_le_of_lt hmn),
  add_tsub_cancel_right] using sum_Ico_by_parts f g (Nat.succ_lt_succ hmn)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Map.lean
theorem denote_map {aig : AIG α} (target : MapTarget aig len) :
    ∀ (idx : Nat) (hidx : idx < len),
      ⟦(map aig target).aig, (map aig target).vec.get idx hidx, assign⟧
        =
      ⟦target.func aig (target.vec.get idx hidx), assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
idx : Nat
hidx : idx < len
⊢ ⟦assign, { aig := (map aig target).aig, ref := (map aig target).vec.get idx hidx }⟧ =
    ⟦assign, target.func aig (target.vec.get idx hidx)⟧

Tactic:
unfold map

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
idx : Nat
hidx : idx < len
⊢ ⟦assign,
      { aig := (map.go aig 0 ⋯ empty target.vec target.func).aig,
        ref := (map.go aig 0 ⋯ empty target.vec target.func).vec.get idx hidx }⟧ =
    ⟦assign, target.func aig (target.vec.get idx hidx)⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
⊢ ∀ (idx : Nat) (hidx : idx < len),
    ⟦assign, { aig := (map aig target).aig, ref := (map aig target).vec.get idx hidx }⟧ =
      ⟦assign, target.func aig (target.vec.get idx hidx)⟧

Tactic:
intro idx hidx

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
idx : Nat
hidx : idx < len
⊢ ⟦assign, { aig := (map aig target).aig, ref := (map aig target).vec.get idx hidx }⟧ =
    ⟦assign, target.func aig (target.vec.get idx hidx)⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
idx : Nat
hidx : idx < len
⊢ ⟦assign,
      { aig := (map.go aig 0 ⋯ empty target.vec target.func).aig,
        ref := (map.go aig 0 ⋯ empty target.vec target.func).vec.get idx hidx }⟧ =
    ⟦assign, target.func aig (target.vec.get idx hidx)⟧

Tactic:
apply map.denote_go

Result:
case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
idx : Nat
hidx : idx < len
⊢ 0 ≤ idx

Proof state:
case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
target : MapTarget aig len
idx : Nat
hidx : idx < len
⊢ 0 ≤ idx

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_eq_pi_iff {z : ℂ} : arg z = π ↔ z.re < 0 ∧ z.im = 0

Proof state:
case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

Tactic:
constructor

Result:
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π → z.re < 0 ∧ z.im = 0

case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π

Proof state:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π
⊢ z.re < 0 ∧ z.im = 0

Tactic:
rw [← norm_mul_cos_add_sin_mul_I z, h]

Result:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π
⊢ (↑‖z‖ * (cos ↑π + sin ↑π * I)).re < 0 ∧ (↑‖z‖ * (cos ↑π + sin ↑π * I)).im = 0

Proof state:
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π

Tactic:
obtain ⟨x, y⟩ := z

Result:
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re < 0 ∧ { re := x, im := y }.im = 0 → { re := x, im := y }.arg = π

Proof state:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

Tactic:
simp [h₀, lt_irrefl, Real.pi_ne_zero.symm]

Result:
no goals

Proof state:
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π → z.re < 0 ∧ z.im = 0

Tactic:
intro h

Result:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π
⊢ z.re < 0 ∧ z.im = 0

Proof state:
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re < 0 ∧ { re := x, im := y }.im = 0 → { re := x, im := y }.arg = π

Tactic:
rintro ⟨h : x < 0, rfl : y = 0⟩

Result:
case neg.mpr.mk.intro
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ { re := x, im := 0 }.arg = π

Proof state:
case neg.mpr.mk.intro
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ { re := x, im := 0 }.arg = π

Tactic:
rw [← arg_neg_one, ← arg_real_mul (-1) (neg_pos.2 h)]

Result:
case neg.mpr.mk.intro
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ { re := x, im := 0 }.arg = (↑(-x) * -1).arg

Proof state:
case neg.mpr.mk.intro
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ { re := x, im := 0 }.arg = (↑(-x) * -1).arg

Tactic:
simp [← ofReal_def]

Result:
no goals

Proof state:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π
⊢ (↑‖z‖ * (cos ↑π + sin ↑π * I)).re < 0 ∧ (↑‖z‖ * (cos ↑π + sin ↑π * I)).im = 0

Tactic:
simp [h₀]

Result:
no goals

Proof state:
z : ℂ
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

Tactic:
by_cases h₀ : z = 0

Result:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[simp]
lemma ideal_iSup {ι : Type*} {I : ι → IdealSheafData X} : (iSup I).ideal = ⨆ i, (I i).ideal

Proof state:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
⊢ (iSup I).ideal = ⨆ i, (I i).ideal

Tactic:
rw [← sSup_range, ← sSup_range, ideal_sSup, ← Set.range_comp, Function.comp_def]

Result:
no goals