harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Complex/IntegerCompl.lean
lemma integerComplement.add_coe_int_mem {x : ℂ} (a : ℤ) : x + (a : ℂ) ∈ ℂ_ℤ ↔ x ∈ ℂ_ℤ

Proof state:
x : ℂ
a : ℤ
x✝ : ∃ n, ↑n = x
n : ℤ
hn : ↑n = x
⊢ ↑(n + a) = x + ↑a

Tactic:
simp [hn]

Result:
no goals

Proof state:
x : ℂ
a : ℤ
⊢ x + ↑a ∈ ℂ_ℤ ↔ x ∈ ℂ_ℤ

Tactic:
simp only [mem_iff, not_iff_not]

Result:
x : ℂ
a : ℤ
⊢ (∃ n, ↑n = x + ↑a) ↔ ∃ n, ↑n = x

Proof state:
x : ℂ
a : ℤ
x✝ : ∃ n, ↑n = x + ↑a
n : ℤ
hn : ↑n = x + ↑a
⊢ ↑(n - a) = x

Tactic:
simp [hn]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem map_punctured_nhds_eq (h : X ≃ₜ Y) (x : X) : map h (𝓝[≠] x) = 𝓝[≠] (h x)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ map (⇑h) (𝓝[≠] x) = 𝓝[≠] h x

Tactic:
convert h.isEmbedding.map_nhdsWithin_eq ({x}ᶜ) x

Result:
case h.e'_3.h.e'_4
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ {h x}ᶜ = ⇑h '' {x}ᶜ

Proof state:
case h.e'_3.h.e'_4
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ {h x}ᶜ = ⇑h '' {x}ᶜ

Tactic:
rw [h.image_compl, Set.image_singleton]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infinite_abs_iff {x : ℝ*} : Infinite |x| ↔ Infinite x

Proof state:
x : ℝ*
⊢ |x|.Infinite ↔ x.Infinite

Tactic:
cases le_total 0 x <;> simp [*, abs_of_nonneg, abs_of_nonpos, infinite_neg]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem continuous_symm_of_mem_pretrivializationAtlas (he : e ∈ a.pretrivializationAtlas) :
    @ContinuousOn _ _ _ a.totalSpaceTopology e.toPartialEquiv.symm e.target

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
z : B × F
H : z ∈ e.target
U : Set (TotalSpace F E)
h : U ∈ 𝓝 (↑e.symm z)
⊢ coinduced (fun x => ↑e.symm ↑x) inferInstance ≤ a.totalSpaceTopology

Tactic:
exact le_iSup₂ (α := TopologicalSpace (TotalSpace F E)) e he

Result:
no goals

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
⊢ ContinuousOn (↑e.symm) e.target

Tactic:
refine fun z H U h => preimage_nhdsWithin_coinduced' H (le_def.1 (nhds_mono ?_) U h)

Result:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
z : B × F
H : z ∈ e.target
U : Set (TotalSpace F E)
h : U ∈ 𝓝 (↑e.symm z)
⊢ coinduced (fun x => ↑e.symm ↑x) inferInstance ≤ a.totalSpaceTopology
-- Mathlib/Data/Int/Init.lean
protected lemma two_mul : ∀ n : ℤ, 2 * n = n + n
  | (n : ℕ) => by norm_cast; exact n.two_mul
  | -[n+1] => by
    change (2 : ℕ) * (_ : ℤ) = _
    rw [Int.ofNat_mul_negSucc, Nat.two_mul, ofNat_add, Int.neg_add]
    rfl

Proof state:
n : ℕ
⊢ 2 * n = n + n

Tactic:
exact n.two_mul

Result:
no goals

Proof state:
n : ℕ
⊢ -↑n.succ + -↑n.succ = -[n+1] + -[n+1]

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ ↑2 * -[n+1] = -[n+1] + -[n+1]

Tactic:
rw [Int.ofNat_mul_negSucc, Nat.two_mul, ofNat_add, Int.neg_add]

Result:
n : ℕ
⊢ -↑n.succ + -↑n.succ = -[n+1] + -[n+1]

Proof state:
n : ℕ
⊢ 2 * ↑n = ↑n + ↑n

Tactic:
norm_cast

Result:
n : ℕ
⊢ 2 * n = n + n

Proof state:
n : ℕ
⊢ 2 * -[n+1] = -[n+1] + -[n+1]

Tactic:
change (2 : ℕ) * (_ : ℤ) = _

Result:
n : ℕ
⊢ ↑2 * -[n+1] = -[n+1] + -[n+1]
-- Mathlib/Order/Cover.lean
lemma exists_covBy_of_wellFoundedGT [wf : WellFoundedGT α] ⦃a : α⦄ (h : ¬ IsMin a) :
    ∃ a', a' ⋖ a

Proof state:
α : Type u_1
inst✝ : Preorder α
wf : WellFoundedGT α
a : α
h : ¬IsMin a
⊢ ∃ a', a' ⋖ a

Tactic:
rw [not_isMin_iff] at h

Result:
α : Type u_1
inst✝ : Preorder α
wf : WellFoundedGT α
a : α
h : ∃ b, b < a
⊢ ∃ a', a' ⋖ a

Proof state:
α : Type u_1
inst✝ : Preorder α
wf : WellFoundedGT α
a : α
h : ∃ b, b < a
⊢ ∃ a', a' ⋖ a

Tactic:
exact ⟨_, wf.wf.min_mem _ h, fun a' h₁ h₂ ↦ wf.wf.not_lt_min _ h h₂ h₁⟩

Result:
no goals
-- Mathlib/FieldTheory/AxGrothendieck.lean
theorem ax_grothendieck_zeroLocus
    (I : Ideal (MvPolynomial ι K))
    (p : ι → MvPolynomial ι K) :
    let S := zeroLocus I
    S.MapsTo (fun v i => eval v (p i)) S →
    S.InjOn (fun v i => eval v (p i)) →
    S.SurjOn (fun v i => eval v (p i)) S

Proof state:
K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
I : Ideal (MvPolynomial ι K)
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
⊢ let S := zeroLocus I;
  Set.MapsTo (fun v i => (eval v) (p i)) S S →
    Set.InjOn (fun v i => (eval v) (p i)) S → Set.SurjOn (fun v i => (eval v) (p i)) S S

Tactic:
intro S

Result:
K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
I : Ideal (MvPolynomial ι K)
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
S : Set (ι → K) := zeroLocus I
⊢ Set.MapsTo (fun v i => (eval v) (p i)) S S →
    Set.InjOn (fun v i => (eval v) (p i)) S → Set.SurjOn (fun v i => (eval v) (p i)) S S

Proof state:
K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
I : Ideal (MvPolynomial ι K)
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
S : Set (ι → K) := zeroLocus I
⊢ Set.MapsTo (fun v i => (eval v) (p i)) S S →
    Set.InjOn (fun v i => (eval v) (p i)) S → Set.SurjOn (fun v i => (eval v) (p i)) S S

Tactic:
obtain ⟨s, rfl⟩ : I.FG := IsNoetherian.noetherian I

Result:
case intro
K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
s : Finset (MvPolynomial ι K)
S : Set (ι → K) := zeroLocus (Ideal.span ↑s)
⊢ Set.MapsTo (fun v i => (eval v) (p i)) S S →
    Set.InjOn (fun v i => (eval v) (p i)) S → Set.SurjOn (fun v i => (eval v) (p i)) S S

Proof state:
K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
I : Ideal (MvPolynomial ι K)
p : ι → MvPolynomial ι K
⊢ let S := zeroLocus I;
  Set.MapsTo (fun v i => (eval v) (p i)) S S →
    Set.InjOn (fun v i => (eval v) (p i)) S → Set.SurjOn (fun v i => (eval v) (p i)) S S

Tactic:
letI := compatibleRingOfRing K

Result:
K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
I : Ideal (MvPolynomial ι K)
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
⊢ let S := zeroLocus I;
  Set.MapsTo (fun v i => (eval v) (p i)) S S →
    Set.InjOn (fun v i => (eval v) (p i)) S → Set.SurjOn (fun v i => (eval v) (p i)) S S

Proof state:
case intro
K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
s : Finset (MvPolynomial ι K)
S : Set (ι → K) := zeroLocus (Ideal.span ↑s)
⊢ Set.MapsTo (fun v i => (eval v) (p i)) S S →
    Set.InjOn (fun v i => (eval v) (p i)) S → Set.SurjOn (fun v i => (eval v) (p i)) S S

Tactic:
exact ax_grothendieck_of_definable S (mvPolynomial_zeroLocus_definable s) p

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem length_le_length_insertIdx (l : List α) (x : α) (n : Nat) :
    l.length ≤ (insertIdx n x l).length

Proof state:
α : Type u
l : List α
x : α
n : Nat
⊢ l.length ≤ if n ≤ l.length then l.length + 1 else l.length

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n : Nat
⊢ l.length ≤ (insertIdx n x l).length

Tactic:
simp only [length_insertIdx]

Result:
α : Type u
l : List α
x : α
n : Nat
⊢ l.length ≤ if n ≤ l.length then l.length + 1 else l.length
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderiv_sub_const (c : F) : fderiv 𝕜 (fun y => f y - c) x = fderiv 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
c : F
⊢ fderiv 𝕜 (fun y => f y - c) x = fderiv 𝕜 f x

Tactic:
simp only [sub_eq_add_neg, fderiv_add_const]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Prime.lean
theorem not_isPrime_iff {I : Ideal α} :
    ¬I.IsPrime ↔ I = ⊤ ∨ ∃ (x : α) (_hx : x ∉ I) (y : α) (_hy : y ∉ I), x * y ∈ I

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ (I = ⊤ ∨ ∃ x x_1, ∃ (_ : x * x_1 ∈ I), x ∉ I ∧ x_1 ∉ I) ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I

Tactic:
exact
  or_congr Iff.rfl
    ⟨fun ⟨x, y, hxy, hx, hy⟩ => ⟨x, hx, y, hy, hxy⟩, fun ⟨x, hx, y, hy, hxy⟩ =>
      ⟨x, y, hxy, hx, hy⟩⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ ¬I.IsPrime ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I

Tactic:
simp_rw [Ideal.isPrime_iff, not_and_or, Ne, Classical.not_not, not_forall, not_or]

Result:
α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ (I = ⊤ ∨ ∃ x x_1, ∃ (_ : x * x_1 ∈ I), x ∉ I ∧ x_1 ∉ I) ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I
-- Mathlib/Data/Rel.lean
theorem inv_comp (r : Rel α β) (s : Rel β γ) : inv (r • s) = inv s • inv r

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
⊢ (r • s).inv = s.inv • r.inv

Tactic:
ext x z

Result:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
x : γ
z : α
⊢ (r • s).inv x z ↔ (s.inv • r.inv) x z

Proof state:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
x : γ
z : α
⊢ (r • s).inv x z ↔ (s.inv • r.inv) x z

Tactic:
simp [comp, inv, flip, and_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem length_modify [BEq α] {a : α} : (modify a f l).length = l.length

Proof state:
case cons
α : Type u_1
β✝ : Type u_2
f : α → β✝ → β✝
inst✝ : BEq α
a key✝ : α
value✝ : β✝
tail✝ : AssocList α β✝
tail_ih✝ : (modify a f tail✝).length = tail✝.length
⊢ (match key✝ == a with
      | true => cons a (f key✝ value✝) tail✝
      | false => cons key✝ value✝ (modify a f tail✝)).length =
    tail✝.length + 1

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
β✝ : Type u_2
f : α → β✝ → β✝
inst✝ : BEq α
a key✝ : α
value✝ : β✝
tail✝ : AssocList α β✝
tail_ih✝ : (modify a f tail✝).length = tail✝.length
⊢ (modify a f (cons key✝ value✝ tail✝)).length = (cons key✝ value✝ tail✝).length

Tactic:
simp only [modify, length_cons]

Result:
case cons
α : Type u_1
β✝ : Type u_2
f : α → β✝ → β✝
inst✝ : BEq α
a key✝ : α
value✝ : β✝
tail✝ : AssocList α β✝
tail_ih✝ : (modify a f tail✝).length = tail✝.length
⊢ (match key✝ == a with
      | true => cons a (f key✝ value✝) tail✝
      | false => cons key✝ value✝ (modify a f tail✝)).length =
    tail✝.length + 1

Proof state:
α : Type u_1
β✝ : Type u_2
f : α → β✝ → β✝
l : AssocList α β✝
inst✝ : BEq α
a : α
⊢ (modify a f l).length = l.length

Tactic:
induction l

Result:
case nil
α : Type u_1
β✝ : Type u_2
f : α → β✝ → β✝
inst✝ : BEq α
a : α
⊢ (modify a f nil).length = nil.length

case cons
α : Type u_1
β✝ : Type u_2
f : α → β✝ → β✝
inst✝ : BEq α
a key✝ : α
value✝ : β✝
tail✝ : AssocList α β✝
tail_ih✝ : (modify a f tail✝).length = tail✝.length
⊢ (modify a f (cons key✝ value✝ tail✝)).length = (cons key✝ value✝ tail✝).length

Proof state:
case nil
α : Type u_1
β✝ : Type u_2
f : α → β✝ → β✝
inst✝ : BEq α
a : α
⊢ (modify a f nil).length = nil.length

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_add_one {A : M} (h : IsUnit A.det) : ∀ n : ℤ, A ^ (n + 1) = A ^ n * A
  | (n : ℕ) => by simp only [← Nat.cast_succ, pow_succ, zpow_natCast]
  | -[n+1] =>
    calc
      A ^ (-(n + 1) + 1 : ℤ) = (A ^ n)⁻¹

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ A ^ (↑n + 1) = A ^ ↑n * A

Tactic:
simp only [← Nat.cast_succ, pow_succ, zpow_natCast]

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ (A ^ n)⁻¹ = (A * A ^ n)⁻¹ * A

Tactic:
rw [mul_inv_rev, Matrix.mul_assoc, nonsing_inv_mul _ h, Matrix.mul_one]

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ A ^ (-(↑n + 1) + 1) = (A ^ n)⁻¹

Tactic:
rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_natCast]

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ (A * A ^ n)⁻¹ * A = A ^ (-(↑n + 1)) * A

Tactic:
rw [zpow_neg h, ← Int.ofNat_succ, zpow_natCast, pow_succ']

Result:
no goals
-- Mathlib/Data/Nat/Basic.lean
lemma leRecOn_injective {C : ℕ → Sort*} {n m} (hnm : n ≤ m) (next : ∀ {k}, C k → C (k + 1))
    (Hnext : ∀ n, Injective (@next n)) : Injective (@leRecOn C n m hnm next)

Proof state:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} => next)
x y : C n
H : leRecOn ⋯ (fun {k} => next) x = leRecOn ⋯ (fun {k} => next) y
⊢ x = y

Tactic:
rw [leRecOn_succ hnm, leRecOn_succ hnm] at H

Result:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} => next)
x y : C n
H : next (leRecOn hnm (fun {k} => next) x) = next (leRecOn hnm (fun {k} => next) y)
⊢ x = y

Proof state:
C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
⊢ Injective (leRecOn hnm fun {k} => next)

Tactic:
induction hnm with
| refl =>
  intro x y H
  rwa [leRecOn_self, leRecOn_self] at H
| step hnm ih =>
  intro x y H
  rw [leRecOn_succ hnm, leRecOn_succ hnm] at H
  exact ih (Hnext _ H)

Result:
no goals

Proof state:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
x y : C n
H : leRecOn ⋯ (fun {k} => next) x = leRecOn ⋯ (fun {k} => next) y
⊢ x = y

Tactic:
rwa [leRecOn_self, leRecOn_self] at H

Result:
no goals

Proof state:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
⊢ Injective (leRecOn ⋯ fun {k} => next)

Tactic:
intro x y H

Result:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
x y : C n
H : leRecOn ⋯ (fun {k} => next) x = leRecOn ⋯ (fun {k} => next) y
⊢ x = y

Proof state:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} => next)
⊢ Injective (leRecOn ⋯ fun {k} => next)

Tactic:
intro x y H

Result:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} => next)
x y : C n
H : leRecOn ⋯ (fun {k} => next) x = leRecOn ⋯ (fun {k} => next) y
⊢ x = y

Proof state:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} => next)
x y : C n
H : next (leRecOn hnm (fun {k} => next) x) = next (leRecOn hnm (fun {k} => next) y)
⊢ x = y

Tactic:
exact ih (Hnext _ H)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem prehaar_le_index (K₀ : PositiveCompacts G) {U : Set G} (K : Compacts G)
    (hU : (interior U).Nonempty) : prehaar (K₀ : Set G) U K ≤ index (K : Set G) K₀

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ 0 < index (↑K₀) U

Tactic:
exact index_pos K₀ hU

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ prehaar (↑K₀) U K ≤ ↑(index ↑K ↑K₀)

Tactic:
unfold prehaar

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ ↑(index (↑K) U) / ↑(index (↑K₀) U) ≤ ↑(index ↑K ↑K₀)

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ ↑(index (↑K) U) / ↑(index (↑K₀) U) ≤ ↑(index ↑K ↑K₀)

Tactic:
rw [div_le_iff₀] <;> norm_cast

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ index (↑K) U ≤ index ↑K ↑K₀ * index (↑K₀) U

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ 0 < index (↑K₀) U

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
hU : (interior U).Nonempty
⊢ index (↑K) U ≤ index ↑K ↑K₀ * index (↑K₀) U

Tactic:
apply le_index_mul K₀ K hU

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem ne_zero_of_mem_nthRootsFinset {η : R} (hη : η ∈ nthRootsFinset n R) : η ≠ 0

Proof state:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Nontrivial R
n : ℕ
hη : 0 ∈ nthRootsFinset (n + 1) R
⊢ False

Tactic:
rw [mem_nthRootsFinset n.succ_pos, zero_pow n.succ_ne_zero] at hη

Result:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Nontrivial R
n : ℕ
hη : 0 = 1
⊢ False

Proof state:
R : Type u
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Nontrivial R
hη : 0 ∈ nthRootsFinset n R
⊢ False

Tactic:
cases n with
| zero =>
  simp only [nthRootsFinset_zero, not_mem_empty] at hη
| succ n =>
  rw [mem_nthRootsFinset n.succ_pos, zero_pow n.succ_ne_zero] at hη
  exact zero_ne_one hη

Result:
no goals

Proof state:
R : Type u
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
η : R
hη : η ∈ nthRootsFinset n R
⊢ η ≠ 0

Tactic:
nontriviality R

Result:
R : Type u
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
η : R
hη : η ∈ nthRootsFinset n R
inst✝ : Nontrivial R
⊢ η ≠ 0

Proof state:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Nontrivial R
n : ℕ
hη : 0 = 1
⊢ False

Tactic:
exact zero_ne_one hη

Result:
no goals

Proof state:
case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Nontrivial R
hη : 0 ∈ nthRootsFinset 0 R
⊢ False

Tactic:
simp only [nthRootsFinset_zero, not_mem_empty] at hη

Result:
no goals

Proof state:
R : Type u
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
η : R
hη : η ∈ nthRootsFinset n R
inst✝ : Nontrivial R
⊢ η ≠ 0

Tactic:
rintro rfl

Result:
R : Type u
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Nontrivial R
hη : 0 ∈ nthRootsFinset n R
⊢ False
-- Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean
theorem atImInfty_mem (S : Set ℍ) : S ∈ atImInfty ↔ ∃ A : ℝ, ∀ z : ℍ, A ≤ im z → z ∈ S

Proof state:
S : Set ℍ
⊢ S ∈ atImInfty ↔ ∃ A, ∀ (z : ℍ), A ≤ z.im → z ∈ S

Tactic:
simp only [atImInfty_basis.mem_iff, true_and]

Result:
S : Set ℍ
⊢ (∃ i, im ⁻¹' Set.Ici i ⊆ S) ↔ ∃ A, ∀ (z : ℍ), A ≤ z.im → z ∈ S

Proof state:
S : Set ℍ
⊢ (∃ i, im ⁻¹' Set.Ici i ⊆ S) ↔ ∃ A, ∀ (z : ℍ), A ≤ z.im → z ∈ S

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean
lemma pretopology_le_inf [IsJointlySurjectivePreserving ⊤] :
    pretopology P ≤ surjectiveFamiliesPretopology ⊓ P.pretopology

Proof state:
case intro.intro
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
𝒰 : Cover P X
x : ↑↑X.toPresheafedSpace
a : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace
ha : (ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) a = x
⊢ ∃ Y y f, ∃ (_ : Presieve.ofArrows 𝒰.obj 𝒰.map f), (ConcreteCategory.hom f.base) y = x

Tactic:
refine ⟨𝒰.obj (𝒰.f x), a, 𝒰.map (𝒰.f x), ⟨_⟩, ha⟩

Result:
no goals

Proof state:
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
⊢ pretopology P ≤ surjectiveFamiliesPretopology ⊓ P.pretopology

Tactic:
rintro X S ⟨𝒰, rfl⟩

Result:
case intro
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
𝒰 : Cover P X
⊢ Presieve.ofArrows 𝒰.obj 𝒰.map ∈ (surjectiveFamiliesPretopology ⊓ P.pretopology).coverings X

Proof state:
case intro
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
𝒰 : Cover P X
⊢ Presieve.ofArrows 𝒰.obj 𝒰.map ∈ (surjectiveFamiliesPretopology ⊓ P.pretopology).coverings X

Tactic:
refine ⟨fun x ↦ ?_, fun ⟨i⟩ ↦ 𝒰.map_prop i⟩

Result:
case intro
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
𝒰 : Cover P X
x : ↑↑X.toPresheafedSpace
⊢ ∃ Y y f, ∃ (_ : Presieve.ofArrows 𝒰.obj 𝒰.map f), (ConcreteCategory.hom f.base) y = x

Proof state:
case intro
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
𝒰 : Cover P X
x : ↑↑X.toPresheafedSpace
⊢ ∃ Y y f, ∃ (_ : Presieve.ofArrows 𝒰.obj 𝒰.map f), (ConcreteCategory.hom f.base) y = x

Tactic:
obtain ⟨a, ha⟩ := 𝒰.covers x

Result:
case intro.intro
P : MorphismProperty Scheme
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : IsJointlySurjectivePreserving ⊤
X : Scheme
𝒰 : Cover P X
x : ↑↑X.toPresheafedSpace
a : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace
ha : (ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) a = x
⊢ ∃ Y y f, ∃ (_ : Presieve.ofArrows 𝒰.obj 𝒰.map f), (ConcreteCategory.hom f.base) y = x
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem fundamentalDomain_idealLattice :
    MeasureTheory.IsAddFundamentalDomain (mixedEmbedding.idealLattice K I)
      (ZSpan.fundamentalDomain (fractionalIdealLatticeBasis K I))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ MeasureTheory.IsAddFundamentalDomain (↥(idealLattice K I)) (ZSpan.fundamentalDomain (fractionalIdealLatticeBasis K I))
    MeasureTheory.volume

Tactic:
rw [← span_idealLatticeBasis]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))))
    (ZSpan.fundamentalDomain (fractionalIdealLatticeBasis K I)) MeasureTheory.volume

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))))
    (ZSpan.fundamentalDomain (fractionalIdealLatticeBasis K I)) MeasureTheory.volume

Tactic:
exact ZSpan.isAddFundamentalDomain (fractionalIdealLatticeBasis K I) _

Result:
no goals