harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_mul_two_pow_add_eq (a b i : Nat) :
    testBit (2^i*a + b) i = (a%2 = 1 ^^ testBit b i)

Proof state:
a b i : Nat
⊢ (2 ^ i * a + b).testBit i = (decide (a % 2 = 1) ^^ b.testBit i)

Tactic:
match a with
| 0 => simp
| a+1 =>
  simp [Nat.mul_succ, Nat.add_assoc,
        testBit_mul_two_pow_add_eq a,
        testBit_two_pow_add_eq,
        Nat.succ_mod_two]
  cases mod_two_eq_zero_or_one a with
  | _ p => simp [p]

Result:
no goals

Proof state:
case inr
a✝ b i a : Nat
p : a % 2 = 1
⊢ (decide (a % 2 = 1) != b.testBit i) = !(decide (1 - a % 2 = 1) ^^ b.testBit i)

Tactic:
simp [p]

Result:
no goals

Proof state:
a b i : Nat
⊢ (2 ^ i * 0 + b).testBit i = (decide (0 % 2 = 1) ^^ b.testBit i)

Tactic:
simp

Result:
no goals

Proof state:
a✝ b i a : Nat
⊢ (decide (a % 2 = 1) != b.testBit i) = !(decide (1 - a % 2 = 1) ^^ b.testBit i)

Tactic:
cases mod_two_eq_zero_or_one a with
| _ p => simp [p]

Result:
no goals

Proof state:
a✝ b i a : Nat
⊢ (2 ^ i * (a + 1) + b).testBit i = (decide ((a + 1) % 2 = 1) ^^ b.testBit i)

Tactic:
simp [Nat.mul_succ, Nat.add_assoc,
      testBit_mul_two_pow_add_eq a,
      testBit_two_pow_add_eq,
      Nat.succ_mod_two]

Result:
a✝ b i a : Nat
⊢ (decide (a % 2 = 1) != b.testBit i) = !(decide (1 - a % 2 = 1) ^^ b.testBit i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] {l : Vector α n} {a₁ a₂} :
    l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂

Proof state:
α : Type u_1
n : Nat
op : α → α → α
ha : Std.Associative op
l : Vector α n
a₁ a₂ : α
⊢ foldr op (op a₁ a₂) l = op (foldr op a₁ l) a₂

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
op : α → α → α
ha : Std.Associative op
a₁ a₂ : α
l : Array α
⊢ foldr op (op a₁ a₂) { toArray := l, size_toArray := ⋯ } = op (foldr op a₁ { toArray := l, size_toArray := ⋯ }) a₂

Proof state:
case mk
α : Type u_1
op : α → α → α
ha : Std.Associative op
a₁ a₂ : α
l : Array α
⊢ foldr op (op a₁ a₂) { toArray := l, size_toArray := ⋯ } = op (foldr op a₁ { toArray := l, size_toArray := ⋯ }) a₂

Tactic:
simp [Array.foldr_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_tdiv_assoc' (b : Int) {a c : Int} (h : c ∣ a) :
    (a * b).tdiv c = a.tdiv c * b

Proof state:
b a c : Int
h : c ∣ a
⊢ (a * b).tdiv c = a.tdiv c * b

Tactic:
rw [Int.mul_comm, Int.mul_tdiv_assoc _ h, Int.mul_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem zero_compLinearMap (g : M₂ →ₗ[R] M) : (0 : M [⋀^ι]→ₗ[R] N).compLinearMap g = 0

Proof state:
case H
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₂ →ₗ[R] M
x✝ : ι → M₂
⊢ (compLinearMap 0 g) x✝ = 0 x✝

Tactic:
simp only [compLinearMap_apply, zero_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₂ →ₗ[R] M
⊢ compLinearMap 0 g = 0

Tactic:
ext

Result:
case H
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₂ →ₗ[R] M
x✝ : ι → M₂
⊢ (compLinearMap 0 g) x✝ = 0 x✝
-- Mathlib/Algebra/Central/Basic.lean
lemma of_algEquiv (e : D ≃ₐ[K] D') : IsCentral K D' where
  out x hx :=
    have ⟨k, hk⟩ := h.1 ((MulEquivClass.apply_mem_center_iff e.symm).mpr hx)
    ⟨k, by simpa [ofId] using congr(e $hk)⟩

Proof state:
K : Type u
inst✝⁴ : CommSemiring K
D D' : Type v
inst✝³ : Semiring D
inst✝² : Algebra K D
h : IsCentral K D
inst✝¹ : Semiring D'
inst✝ : Algebra K D'
e : D ≃ₐ[K] D'
x : D'
hx : x ∈ Subalgebra.center K D'
k : K
hk : (ofId K D).toRingHom k = e.symm x
⊢ (ofId K D').toRingHom k = x

Tactic:
simpa [ofId] using congr(e $hk)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.filter (p : α → Bool) {l₁ l₂ : List α} (s : l₁ ~ l₂) :
    filter p l₁ ~ filter p l₂

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ ~ l₂
⊢ List.filterMap (Option.guard fun x => p x = true) l₁ ~ List.filterMap (Option.guard fun x => p x = true) l₂

Tactic:
apply s.filterMap

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ ~ l₂
⊢ List.filter p l₁ ~ List.filter p l₂

Tactic:
rw [← filterMap_eq_filter]

Result:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ ~ l₂
⊢ List.filterMap (Option.guard fun x => p x = true) l₁ ~ List.filterMap (Option.guard fun x => p x = true) l₂
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem of_boolalg_symmDiff_aux (a b : α) : (a + b + a * b) * (1 + a * b) = a + b :=
  calc (a + b + a * b) * (1 + a * b)
    _ = a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b)

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b) = a + b

Tactic:
simp only [mul_self, add_self, add_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ (a + b + a * b) * (1 + a * b) = a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b)

Tactic:
ring

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
protected lemma add (h1 : μ₁ ≪ ν) (h2 : μ₂ ≪ ν') : μ₁ + μ₂ ≪ ν + ν'

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
⊢ μ₁ + μ₂ ≪ ν + ν'

Tactic:
intro s hs

Result:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
hs : (ν + ν') s = 0
⊢ (μ₁ + μ₂) s = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
hs : (ν + ν') s = 0
⊢ (μ₁ + μ₂) s = 0

Tactic:
simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢

Result:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
hs : ν s = 0 ∧ ν' s = 0
⊢ μ₁ s = 0 ∧ μ₂ s = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
hs : ν s = 0 ∧ ν' s = 0
⊢ μ₁ s = 0 ∧ μ₂ s = 0

Tactic:
exact ⟨h1 hs.1, h2 hs.2⟩

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
@[simp]
lemma biUnion_nonempty : (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (∃ x, ∃ a ∈ s, x ∈ t a) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x

Tactic:
rw [exists_swap]

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (∃ y x, y ∈ s ∧ x ∈ t y) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty

Tactic:
simp only [Finset.Nonempty, mem_biUnion]

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (∃ x, ∃ a ∈ s, x ∈ t a) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (∃ y x, y ∈ s ∧ x ∈ t y) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x

Tactic:
simp [exists_and_left]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.HasBasis.uniformEquicontinuousOn_iff_left {p : κ → Prop}
    {s : κ → Set (β × β)} {F : ι → β → α} {S : Set β} (hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s) :
    UniformEquicontinuousOn F S ↔
      ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x y, (x, y) ∈ s k → ∀ i, (F i x, F i y) ∈ U

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α,
      ∃ ia, p ia ∧ ∀ (a b : β), (a, b) ∈ s ia → ((⇑ofFun ∘ swap F) a, (⇑ofFun ∘ swap F) b) ∈ UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
⊢ UniformEquicontinuousOn F S ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
  hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]

Result:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ x ∈ s ia, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ x ∈ s ia, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
simp only [Prod.forall]

Result:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α,
      ∃ ia, p ia ∧ ∀ (a b : β), (a, b) ∈ s ia → ((⇑ofFun ∘ swap F) a, (⇑ofFun ∘ swap F) b) ∈ UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
-- Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
theorem innerRegularWRT_isCompact_isClosed [UniformSpace α] [CompleteSpace α]
    [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
    [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed

Proof state:
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
exact innerRegularWRT_isCompact_closure P

Result:
no goals

Proof state:
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) IsClosed

Tactic:
rw [innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure]

Result:
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (IsCompact ∘ closure) IsClosed
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_add_add_self (x y : E) : ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x + y, x + y⟫_𝕜 = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

Tactic:
simp only [inner_add_left, inner_add_right]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, x⟫_𝕜 + ⟪y, x⟫_𝕜 + (⟪x, y⟫_𝕜 + ⟪y, y⟫_𝕜) = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, x⟫_𝕜 + ⟪y, x⟫_𝕜 + (⟪x, y⟫_𝕜 + ⟪y, y⟫_𝕜) = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

Tactic:
ring

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem uIcc_subset_uIcc_union_uIcc : [[a, c]] ⊆ [[a, b]] ∪ [[b, c]] :=
  coe_subset.1 <| by
    push_cast
    exact Set.uIcc_subset_uIcc_union_uIcc

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑[[a, c]] ⊆ ↑([[a, b]] ∪ [[b, c]])

Tactic:
push_cast

Result:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c

Tactic:
exact Set.uIcc_subset_uIcc_union_uIcc

Result:
no goals
-- Mathlib/NumberTheory/Padics/ProperSpace.lean
theorem totallyBounded_univ : TotallyBounded (Set.univ : Set ℤ_[p])

Proof state:
case intro.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ dist z ↑(z.appr k) < ε

Tactic:
exact (((z - z.appr k).norm_le_pow_iff_mem_span_pow k).mpr (z.appr_spec k)).trans_lt hk

Result:
no goals

Proof state:
case intro.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ z.appr k ∈ ↑(Finset.range (p ^ k))

Tactic:
simpa only [Finset.mem_coe, Finset.mem_range] using z.appr_lt k

Result:
no goals

Proof state:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ ∃ x ∈ ↑(Finset.range (p ^ k)), dist z ↑x < ε

Tactic:
refine ⟨z.appr k, ?_, ?_⟩

Result:
case intro.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ z.appr k ∈ ↑(Finset.range (p ^ k))

case intro.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ dist z ↑(z.appr k) < ε

Proof state:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, ball y ε

Tactic:
refine ⟨Nat.cast '' Finset.range (p ^ k), Set.toFinite _, fun z _ ↦ ?_⟩

Result:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ z ∈ ⋃ y ∈ Nat.cast '' ↑(Finset.range (p ^ k)), ball y ε

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ TotallyBounded Set.univ

Tactic:
refine Metric.totallyBounded_iff.mpr (fun ε hε ↦ ?_)

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, ball y ε

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, ball y ε

Tactic:
obtain ⟨k, hk⟩ := exists_pow_neg_lt p hε

Result:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, ball y ε

Proof state:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ z ∈ ⋃ y ∈ Nat.cast '' ↑(Finset.range (p ^ k)), ball y ε

Tactic:
simp only [PadicInt, Set.mem_iUnion, Metric.mem_ball, exists_prop, Set.exists_mem_image]

Result:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ ∃ x ∈ ↑(Finset.range (p ^ k)), dist z ↑x < ε
-- Mathlib/Order/CompleteLattice.lean
theorem swap_iSup [SupSet α] [SupSet β] (f : ι → α × β) : (iSup f).swap = ⨆ i, (f i).swap

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : SupSet α
inst✝ : SupSet β
f : ι → α × β
⊢ (iSup f).swap = ⨆ i, (f i).swap

Tactic:
simp_rw [iSup, swap_sSup, ← range_comp, comp_def]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_map {k : β → α} {l : Filter β} :
    IsBigOWith c (map k l) f g ↔ IsBigOWith c l (f ∘ k) (g ∘ k)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ IsBigOWith c (map k l) f g ↔ IsBigOWith c l (f ∘ k) (g ∘ k)

Tactic:
simp only [IsBigOWith_def]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ (∀ᶠ (x : α) in map k l, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (x : β) in l, ‖(f ∘ k) x‖ ≤ c * ‖(g ∘ k) x‖

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ (∀ᶠ (x : α) in map k l, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (x : β) in l, ‖(f ∘ k) x‖ ≤ c * ‖(g ∘ k) x‖

Tactic:
exact eventually_map

Result:
no goals
-- Mathlib/RingTheory/Ideal/IsPrincipal.lean
theorem associatesNonZeroDivisorsEquivIsPrincipal_map_one :
    (associatesNonZeroDivisorsEquivIsPrincipal R 1 : Ideal R) = 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) 1) = 1

Tactic:
rw [associatesNonZeroDivisorsEquivIsPrincipal_coe, map_one, OneMemClass.coe_one,
  associatesEquivIsPrincipal_map_one]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem negAt_apply_isReal_and_not_mem (x : mixedSpace K) {w : {w // IsReal w}} (hw : w ∉ s) :
    (negAt s x).1 w = x.1 w

Proof state:
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∉ s
⊢ ((negAt s) x).1 w = x.1 w

Tactic:
simp_rw [negAt, ContinuousLinearEquiv.prod_apply, piCongrRight_apply, if_neg hw,
  ContinuousLinearEquiv.refl_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
@[simp]
lemma pushout.map_id {X Y Z : C}
    {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] :
    pushout.map f g f g (𝟙 _) (𝟙 _) (𝟙 _) (by simp) (by simp) = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ g ≫ 𝟙 Z = 𝟙 X ≫ g

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ map f g f g (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯ = 𝟙 (pushout f g)

Tactic:
ext <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/Residual.lean
theorem setOf_liouville_eq_irrational_inter_iInter_iUnion :
    { x | Liouville x } =
      { x | Irrational x } ∩ ⋂ n : ℕ, ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b),
      ball (a / b) (1 / (b : ℝ) ^ n)

Proof state:
case refine_1

⊢ {x | Liouville x} ⊆ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)

Tactic:
refine subset_inter (fun x hx => hx.irrational) ?_

Result:
case refine_1

⊢ {x | Liouville x} ⊆ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)

Proof state:
case refine_2

⊢ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ⊆ {x | Liouville x}

Tactic:
simp only [inter_iInter, inter_iUnion, setOf_liouville_eq_iInter_iUnion]

Result:
case refine_2

⊢ ⋂ i, ⋃ i_1, ⋃ i_2, ⋃ (_ : 1 < i_2), {x | Irrational x} ∩ ball (↑i_1 / ↑i_2) (1 / ↑i_2 ^ i) ⊆
    ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}

Proof state:
n : ℕ
a b : ℤ
hb : 1 < b
⊢ ↑(↑a / ↑b) = ↑a / ↑b

Tactic:
norm_cast

Result:
no goals

Proof state:
case refine_1

⊢ {x | Liouville x} ⊆ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)

Tactic:
rw [setOf_liouville_eq_iInter_iUnion]

Result:
case refine_1

⊢ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b} ⊆
    ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)

Proof state:
case refine_1

⊢ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b} ⊆
    ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)

Tactic:
exact iInter_mono fun n => iUnion₂_mono fun a b => iUnion_mono fun _hb => diff_subset

Result:
no goals

Proof state:
case refine_2
n : ℕ
a b : ℤ
hb : 1 < b
⊢ {x | Irrational x} ∩ ball (↑a / ↑b) (1 / ↑b ^ n) ⊆ ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}

Tactic:
rw [inter_comm]

Result:
case refine_2
n : ℕ
a b : ℤ
hb : 1 < b
⊢ ball (↑a / ↑b) (1 / ↑b ^ n) ∩ {x | Irrational x} ⊆ ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}

Proof state:
case refine_2
n : ℕ
a b : ℤ
hb : 1 < b
⊢ ball (↑a / ↑b) (1 / ↑b ^ n) ∩ {x | Irrational x} ⊆ ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}

Tactic:
exact diff_subset_diff Subset.rfl (singleton_subset_iff.2 ⟨a / b, by norm_cast⟩)

Result:
no goals

Proof state:
⊢ {x | Liouville x} = {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)

Tactic:
refine Subset.antisymm ?_ ?_

Result:
case refine_1

⊢ {x | Liouville x} ⊆ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)

case refine_2

⊢ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ⊆ {x | Liouville x}

Proof state:
case refine_2

⊢ ⋂ i, ⋃ i_1, ⋃ i_2, ⋃ (_ : 1 < i_2), {x | Irrational x} ∩ ball (↑i_1 / ↑i_2) (1 / ↑i_2 ^ i) ⊆
    ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}

Tactic:
refine iInter_mono fun n => iUnion₂_mono fun a b => iUnion_mono fun hb => ?_

Result:
case refine_2
n : ℕ
a b : ℤ
hb : 1 < b
⊢ {x | Irrational x} ∩ ball (↑a / ↑b) (1 / ↑b ^ n) ⊆ ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
-- Mathlib/Data/List/Basic.lean
theorem getLast_congr {l₁ l₂ : List α} (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []) (h₃ : l₁ = l₂) :
    getLast l₁ h₁ = getLast l₂ h₂

Proof state:
α : Type u
l₂ : List α
h₂ h₁ : l₂ ≠ []
⊢ l₂.getLast h₁ = l₂.getLast h₂

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
l₁ l₂ : List α
h₁ : l₁ ≠ []
h₂ : l₂ ≠ []
h₃ : l₁ = l₂
⊢ l₁.getLast h₁ = l₂.getLast h₂

Tactic:
subst l₁

Result:
α : Type u
l₂ : List α
h₂ h₁ : l₂ ≠ []
⊢ l₂.getLast h₁ = l₂.getLast h₂
-- Mathlib/Data/Finset/Option.lean
theorem card_toFinset (o : Option α) : o.toFinset.card = o.elim 0 1

Proof state:
α : Type u_1
o : Option α
⊢ o.toFinset.card = o.elim 0 1

Tactic:
cases o <;> rfl

Result:
no goals