harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem get!_eq {β : Type v} [BEq α] [Inhabited β] {l : AssocList α (fun _ => β)} {a : α} :
    l.get! a = getValue! a l.toList

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Inhabited β
l : AssocList α fun x => β
a : α
⊢ get! a l = getValue! a l.toList

Tactic:
induction l

Result:
case nil
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Inhabited β
a : α
⊢ get! a nil = getValue! a nil.toList

case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Inhabited β
a key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
tail_ih✝ : get! a tail✝ = getValue! a tail✝.toList
⊢ get! a (cons key✝ value✝ tail✝) = getValue! a (cons key✝ value✝ tail✝).toList

Proof state:
case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Inhabited β
a key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
tail_ih✝ : get! a tail✝ = getValue! a tail✝.toList
⊢ get! a (cons key✝ value✝ tail✝) = getValue! a (cons key✝ value✝ tail✝).toList

Tactic:
simp_all [get!, List.getValue!, List.getValue!, List.getValue?_cons,
  Bool.apply_cond Option.get!]

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Inhabited β
a : α
⊢ get! a nil = getValue! a nil.toList

Tactic:
simp [get!, List.getValue!]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@[simp] lemma sum_comp_equiv {ι ι' : Type*} (e : ι' ≃ ι) (m : ι → Measure α) :
    sum (m ∘ e) = sum m

Proof state:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
e : ι' ≃ ι
m : ι → Measure α
⊢ sum (m ∘ ⇑e) = sum m

Tactic:
ext s hs

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
e : ι' ≃ ι
m : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum (m ∘ ⇑e)) s = (sum m) s

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
e : ι' ≃ ι
m : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum (m ∘ ⇑e)) s = (sum m) s

Tactic:
simpa [hs, sum_apply] using e.tsum_eq (fun n ↦ m n s)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem mul_get (xs ys : IntList) (i : Nat) : (xs * ys).get i = xs.get i * ys.get i

Proof state:
xs ys : IntList
i : Nat
⊢ (match xs[i]?, ys[i]? with
        | some a, some b => some (a * b)
        | x, x_1 => none).getD
      0 =
    xs[i]?.getD 0 * ys[i]?.getD 0

Tactic:
cases xs[i]? <;> cases ys[i]? <;> simp

Result:
no goals

Proof state:
xs ys : IntList
i : Nat
⊢ (xs * ys).get i = xs.get i * ys.get i

Tactic:
simp only [get, mul_def, List.get?_eq_getElem?, List.getElem?_zipWith]

Result:
xs ys : IntList
i : Nat
⊢ (match xs[i]?, ys[i]? with
        | some a, some b => some (a * b)
        | x, x_1 => none).getD
      0 =
    xs[i]?.getD 0 * ys[i]?.getD 0
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem coe_splitLower : (splitLower I i x : Set (ι → ℝ)) = ↑I ∩ { y | y i ≤ x }

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (univ.pi fun i_1 => Ioc (I.lower i_1) (update I.upper i (x ⊓ I.upper i) i_1)) = ↑I ∩ {y | y i ≤ x}

Tactic:
ext y

Result:
case h
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (y ∈ univ.pi fun i_1 => Ioc (I.lower i_1) (update I.upper i (x ⊓ I.upper i) i_1)) ↔ y ∈ ↑I ∩ {y | y i ≤ x}

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ↑(I.splitLower i x) = ↑I ∩ {y | y i ≤ x}

Tactic:
rw [splitLower, coe_mk']

Result:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (univ.pi fun i_1 => Ioc (I.lower i_1) (update I.upper i (x ⊓ I.upper i) i_1)) = ↑I ∩ {y | y i ≤ x}

Proof state:
case h
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (y ∈ univ.pi fun i_1 => Ioc (I.lower i_1) (update I.upper i (x ⊓ I.upper i) i_1)) ↔ y ∈ ↑I ∩ {y | y i ≤ x}

Tactic:
simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and, ← Pi.le_def,
  le_update_iff, le_min_iff, and_assoc, and_forall_ne (p := fun j => y j ≤ upper I j) i, mem_def]

Result:
case h
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (∀ (x : ι), I.lower x < y x) ∧ y i ≤ x ∧ y ≤ I.upper ↔ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x

Proof state:
case h
ι : Type u_1
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (∀ (x : ι), I.lower x < y x) ∧ y i ≤ x ∧ y ≤ I.upper ↔ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x

Tactic:
rw [and_comm (a := y i ≤ x)]

Result:
no goals
-- Mathlib/Dynamics/FixedPoints/Basic.lean
theorem apply {x : α} (hx : IsFixedPt f x) : IsFixedPt f (f x)

Proof state:
α : Type u
f : α → α
x : α
hx : IsFixedPt f x
⊢ IsFixedPt f (f x)

Tactic:
convert hx

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem Multipliable.countable_mulSupport [FirstCountableTopology G] [T1Space G]
    (hf : Multipliable f) : f.mulSupport.Countable

Proof state:
α : Type u_1
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
f : α → G
inst✝¹ : FirstCountableTopology G
inst✝ : T1Space G
hf : Multipliable f
⊢ (mulSupport f).Countable

Tactic:
simpa only [ker_nhds] using hf.tendsto_cofinite_one.countable_compl_preimage_ker

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem pow_eq_pow_iff_modEq : x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m n : ℕ
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
wlog hmn : m ≤ n generalizing m n

Result:
case inr
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n✝ m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Proof state:
case intro
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]

Tactic:
rw [← mul_one (x ^ m), pow_add, mul_left_cancel_iff, pow_eq_one_iff_modEq]

Result:
case intro
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]

Proof state:
case intro
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]

Tactic:
exact ⟨fun h => Nat.ModEq.add_left _ h, fun h => Nat.ModEq.add_left_cancel' _ h⟩

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
rw [eq_comm, ModEq.comm, this (le_of_not_le hmn)]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n✝ m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Result:
case intro
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
-- Mathlib/Topology/Connected/PathConnected.lean
theorem JoinedIn.trans (hxy : JoinedIn F x y) (hyz : JoinedIn F y z) : JoinedIn F x z

Proof state:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hx✝¹ : x ∈ F
hy✝¹ : y ∈ F
hy✝ : z ∈ F
hxy : Joined ⟨x, hx✝¹⟩ ⟨y, hy✝¹⟩
hyz : Joined ⟨y, hy✝¹⟩ ⟨z, hy✝⟩
hx✝ : x ∈ F
hx : y ∈ F
hy : z ∈ F
⊢ Joined ⟨x, hx✝¹⟩ ⟨z, hy✝⟩

Tactic:
exact hxy.trans hyz

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
⊢ JoinedIn F x z

Tactic:
obtain ⟨hx, hy⟩ := hxy.mem

Result:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F x z

Proof state:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F x z

Tactic:
obtain ⟨hx, hy⟩ := hyz.mem

Result:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx✝ : x ∈ F
hy✝ hx : y ∈ F
hy : z ∈ F
⊢ JoinedIn F x z

Proof state:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx✝ : x ∈ F
hy✝ hx : y ∈ F
hy : z ∈ F
⊢ JoinedIn F x z

Tactic:
simp_all only [joinedIn_iff_joined]

Result:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hx✝¹ : x ∈ F
hy✝¹ : y ∈ F
hy✝ : z ∈ F
hxy : Joined ⟨x, hx✝¹⟩ ⟨y, hy✝¹⟩
hyz : Joined ⟨y, hy✝¹⟩ ⟨z, hy✝⟩
hx✝ : x ∈ F
hx : y ∈ F
hy : z ∈ F
⊢ Joined ⟨x, hx✝¹⟩ ⟨z, hy✝⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx_of_getElem?_eq_some {xs : Array α} (w : xs[xs.findIdx p]? = some y) : p y

Proof state:
α : Type u_1
p : α → Bool
y : α
xs : List α
w : { toList := xs }[findIdx p { toList := xs }]? = some y
⊢ ?m.61114[List.findIdx p ?m.61114]? = some y

Tactic:
simpa using w

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
y : α
xs : Array α
w : xs[findIdx p xs]? = some y
⊢ p y = true

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
y : α
xs : List α
w : { toList := xs }[findIdx p { toList := xs }]? = some y
⊢ p y = true

Proof state:
case mk
α : Type u_1
p : α → Bool
y : α
xs : List α
w : { toList := xs }[findIdx p { toList := xs }]? = some y
⊢ p y = true

Tactic:
exact List.findIdx_of_getElem?_eq_some (by simpa using w)

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem reverse_get_zero {v : Vector α (n + 1)} : v.reverse.head = v.last

Proof state:
case e_a
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.toList.length - 1 - ↑⟨↑0, ⋯⟩ = ↑⟨↑(Fin.last n), ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.toList.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))

Tactic:
simp_rw [toList_reverse]

Result:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.toList.reverse.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))

Proof state:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.toList[v.toList.length - 1 - ↑⟨↑0, ⋯⟩]? = v.toList[↑⟨↑(Fin.last n), ⋯⟩]?

Tactic:
congr

Result:
case e_a
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.toList.length - 1 - ↑⟨↑0, ⋯⟩ = ↑⟨↑(Fin.last n), ⋯⟩

Proof state:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ ↑⟨↑0, ⋯⟩ < v.toList.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.toList.reverse.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))

Tactic:
rw [List.get_eq_getElem, List.get_eq_getElem, ← Option.some_inj, Fin.cast, Fin.cast,
  ← List.getElem?_eq_getElem, ← List.getElem?_eq_getElem, List.getElem?_reverse]

Result:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.toList[v.toList.length - 1 - ↑⟨↑0, ⋯⟩]? = v.toList[↑⟨↑(Fin.last n), ⋯⟩]?

α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ ↑⟨↑0, ⋯⟩ < v.toList.length

Proof state:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.head = v.last

Tactic:
rw [← get_zero, last_def, get_eq_get_toList, get_eq_get_toList]

Result:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.toList.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))
-- Mathlib/RingTheory/Trace/Basic.lean
theorem det_traceForm_ne_zero [Algebra.IsSeparable K L] [DecidableEq ι] (b : Basis ι K L) :
    det (BilinForm.toMatrix b (traceForm K L)) ≠ 0

Proof state:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (b.toMatrix ⇑pb.basis * pb.basis.toMatrix ⇑b)ᵀ * b.toMatrix ⇑pb.basis).det = 1

Tactic:
simp only [Basis.toMatrix_mul_toMatrix_flip, Matrix.transpose_one, Matrix.mul_one,
  Matrix.det_one]

Result:
no goals
-- Mathlib/Data/Finsupp/Order.lean
theorem support_inf [DecidableEq ι] (f g : ι →₀ α) : (f ⊓ g).support = f.support ∩ g.support

Proof state:
case h
ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ ¬f a✝ ⊓ g a✝ = 0 ↔ ¬f a✝ = 0 ∧ ¬g a✝ = 0

Tactic:
simp only [← nonpos_iff_eq_zero, min_le_iff, not_or]

Result:
no goals

Proof state:
case h
ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊓ g).support ↔ a✝ ∈ f.support ∩ g.support

Tactic:
simp only [inf_apply, mem_support_iff, Ne, Finset.mem_union, Finset.mem_filter,
  Finset.mem_inter]

Result:
case h
ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ ¬f a✝ ⊓ g a✝ = 0 ↔ ¬f a✝ = 0 ∧ ¬g a✝ = 0

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊓ g).support = f.support ∩ g.support

Tactic:
ext

Result:
case h
ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊓ g).support ↔ a✝ ∈ f.support ∩ g.support
-- Mathlib/LinearAlgebra/Projection.lean
theorem prodEquivOfIsCompl_symm_apply_fst_eq_zero (h : IsCompl p q) {x : E} :
    ((prodEquivOfIsCompl p q h).symm x).1 = 0 ↔ x ∈ q

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ x ∈ q

Tactic:
conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]

Result:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ q

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ q

Tactic:
rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_left _ (Submodule.coe_mem _),
  mem_right_iff_eq_zero_of_disjoint h.disjoint]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem mem_integers_of_valuation_le_one (x : K)
    (h : ∀ v : HeightOneSpectrum R, v.valuation K x ≤ 1) : x ∈ (algebraMap R K).range

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
this : Ideal.span {d} ∣ Ideal.span {n}
⊢ IsLocalization.mk' K n ⟨d, hd⟩ ∈ (algebraMap R K).range

Tactic:
obtain ⟨z, rfl⟩ := Ideal.span_singleton_le_span_singleton.1 (Ideal.le_of_dvd this)

Result:
case intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
d : R
hd : d ∈ nonZeroDivisors R
hd0 : d ≠ 0
z : R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K (d * z) ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K (d * z) ⟨d, hd⟩ * (algebraMap R K) ↑(d * z, ⟨d, hd⟩).2 = (algebraMap R K) (d * z, ⟨d, hd⟩).1
hn0 : d * z ≠ 0
this : Ideal.span {d} ∣ Ideal.span {d * z}
⊢ IsLocalization.mk' K (d * z) ⟨d, hd⟩ ∈ (algebraMap R K).range
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem _root_.Dense.exists_dist_lt {s : Set α} (hs : Dense s) (x : α) {ε : ℝ} (hε : 0 < ε) :
    ∃ y ∈ s, dist x y < ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
⊢ (ball x ε).Nonempty

Tactic:
simp [hε]

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
this : (ball x ε).Nonempty
⊢ ∃ y ∈ s, dist x y < ε

Tactic:
simpa only [mem_ball'] using hs.exists_mem_open isOpen_ball this

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
⊢ ∃ y ∈ s, dist x y < ε

Tactic:
have : (ball x ε).Nonempty := by simp [hε]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
this : (ball x ε).Nonempty
⊢ ∃ y ∈ s, dist x y < ε
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
theorem go_decl_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (acc : AIG.RefVec aig w)
    (lhs rhs : AIG.RefVec aig w) :
    ∀ (idx : Nat) (h1) (h2),
       (go aig lhs rhs curr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
case isTrue.isTrue
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
res : AIG.RefVecEntry BVBit w
h✝¹ : curr < w
h✝ : aig.isConstant (rhs.get curr h✝¹) false = true
hgo : go aig lhs rhs (curr + 1) acc = res
idx : Nat
h1 : idx < aig.decls.size
h2 : idx < (go aig lhs rhs (curr + 1) acc).aig.decls.size
⊢ (go aig lhs rhs (curr + 1) acc).aig.decls[idx] = aig.decls[idx]

Tactic:
rw [go_decl_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
theorem go_decl_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (acc : AIG.RefVec aig w)
    (lhs rhs : AIG.RefVec aig w) :
    ∀ (idx : Nat) (h1) (h2),
       (go aig lhs rhs curr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs rhs curr acc).aig.decls.size),
    (go aig lhs rhs curr acc).aig.decls[idx] = aig.decls[idx]

Tactic:
generalize hgo : go aig lhs rhs curr acc = res

Result:
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
res : AIG.RefVecEntry BVBit w
hgo : go aig lhs rhs curr acc = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Proof state:
case isFalse
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
res : AIG.RefVecEntry BVBit w
h✝ : ¬curr < w
hgo : { aig := aig, vec := acc } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
simp [← hgo]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem eq_top_iff_forall_lt (x : EReal) : x = ⊤ ↔ ∀ y : ℝ, (y : EReal) < x

Proof state:
case mpr
x : EReal
⊢ x ≠ ⊤ → ∃ y, x ≤ ↑y

Tactic:
intro h

Result:
case mpr
x : EReal
h : x ≠ ⊤
⊢ ∃ y, x ≤ ↑y

Proof state:
case mp
x : EReal
⊢ x = ⊤ → ∀ (y : ℝ), ↑y < x

Tactic:
rintro rfl

Result:
case mp

⊢ ∀ (y : ℝ), ↑y < ⊤

Proof state:
x : EReal
⊢ x = ⊤ ↔ ∀ (y : ℝ), ↑y < x

Tactic:
constructor

Result:
case mp
x : EReal
⊢ x = ⊤ → ∀ (y : ℝ), ↑y < x

case mpr
x : EReal
⊢ (∀ (y : ℝ), ↑y < x) → x = ⊤

Proof state:
case mp

⊢ ∀ (y : ℝ), ↑y < ⊤

Tactic:
exact EReal.coe_lt_top

Result:
no goals

Proof state:
case mpr
x : EReal
h : x ≠ ⊤
⊢ ∃ y, x ≤ ↑y

Tactic:
exact ⟨x.toReal, le_coe_toReal h⟩

Result:
no goals

Proof state:
case mpr
x : EReal
⊢ (∀ (y : ℝ), ↑y < x) → x = ⊤

Tactic:
contrapose!

Result:
case mpr
x : EReal
⊢ x ≠ ⊤ → ∃ y, x ≤ ↑y
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem degree_eq_degree_of_associated (h : Associated p q) : degree p = degree q

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : Associated p q
⊢ p.degree = q.degree

Tactic:
let ⟨u, hu⟩ := h

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : Associated p q
u : R[X]ˣ
hu : p * ↑u = q
⊢ p.degree = q.degree

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : Associated p q
u : R[X]ˣ
hu : p * ↑u = q
⊢ p.degree = q.degree

Tactic:
simp [hu.symm]

Result:
no goals
-- Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean
@[to_additive one_le]
lemma one_le (hA : IsApproximateSubgroup K A) : 1 ≤ K

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
⊢ 1 ≤ K

Tactic:
obtain ⟨F, hF, hSF⟩ := hA.sq_covBySMul

Result:
case intro.intro
G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hSF : A ^ 2 ⊆ ↑F • A
⊢ 1 ≤ K

Proof state:
case intro.intro
G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hSF : A ^ 2 ⊆ ↑F • A
hF₀ : F ≠ ∅
⊢ 1 ≤ K

Tactic:
exact hF.trans' <| by simpa [Finset.nonempty_iff_ne_empty]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hSF : A ^ 2 ⊆ ↑F • A
⊢ F ≠ ∅

Tactic:
rintro rfl

Result:
G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
hF : ↑(#∅) ≤ K
hSF : A ^ 2 ⊆ ↑∅ • A
⊢ False

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hSF : A ^ 2 ⊆ ↑F • A
hF₀ : F ≠ ∅
⊢ 1 ≤ ↑(#F)

Tactic:
simpa [Finset.nonempty_iff_ne_empty]

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hSF : A ^ 2 ⊆ ↑F • A
⊢ 1 ≤ K

Tactic:
have hF₀ : F ≠ ∅ := by rintro rfl; simp [hA.nonempty.pow.ne_empty] at hSF

Result:
case intro.intro
G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hSF : A ^ 2 ⊆ ↑F • A
hF₀ : F ≠ ∅
⊢ 1 ≤ K

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
hF : ↑(#∅) ≤ K
hSF : A ^ 2 ⊆ ↑∅ • A
⊢ False

Tactic:
simp [hA.nonempty.pow.ne_empty] at hSF

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_inv_lt_iff {x y : ℝ≥0∞} {z : ℝ} (hz : 0 < z) : x ^ z⁻¹ < y ↔ x < y ^ z

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ < y ↔ x < y ^ z

Tactic:
simp only [← not_le, le_rpow_inv_iff hz]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_le_iff {o : Ordinal} : ∀ {x : PSet}, rank x ≤ o ↔ ∀ ⦃y⦄, y ∈ x → rank y < o
  | ⟨_, A⟩ => by
    refine ⟨fun h _ h' => (rank_lt_of_mem h').trans_le h, fun h ↦ Ordinal.iSup_le fun a ↦ ?_⟩
    rw [succ_le_iff]
    exact h (Mem.mk A a)

Proof state:
o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o
a : α✝
⊢ (A a).rank < o

Tactic:
exact h (Mem.mk A a)

Result:
no goals

Proof state:
o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
⊢ (mk α✝ A).rank ≤ o ↔ ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o

Tactic:
refine ⟨fun h _ h' => (rank_lt_of_mem h').trans_le h, fun h ↦ Ordinal.iSup_le fun a ↦ ?_⟩

Result:
o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o
a : α✝
⊢ succ (A a).rank ≤ o

Proof state:
o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o
a : α✝
⊢ succ (A a).rank ≤ o

Tactic:
rw [succ_le_iff]

Result:
o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o
a : α✝
⊢ (A a).rank < o