harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem length_eraseP_of_mem (al : a ∈ l) (pa : p a) :
    length (l.eraseP p) = length l - 1

Proof state:
α✝ : Type u_1
l : List α✝
a : α✝
p : α✝ → Bool
al : a ∈ l
pa : p a = true
w✝ : α✝
l₁ l₂ : List α✝
left✝¹ : ∀ (b : α✝), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
e₁ : l = l₁ ++ w✝ :: l₂
e₂ : eraseP p l = l₁ ++ l₂
⊢ (l₁ ++ l₂).length = l.length - 1

Tactic:
simp [length_append, e₁]

Result:
α✝ : Type u_1
l : List α✝
a : α✝
p : α✝ → Bool
al : a ∈ l
pa : p a = true
w✝ : α✝
l₁ l₂ : List α✝
left✝¹ : ∀ (b : α✝), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
e₁ : l = l₁ ++ w✝ :: l₂
e₂ : eraseP p l = l₁ ++ l₂
⊢ l₁.length + l₂.length = l₁.length + (l₂.length + 1) - 1

Proof state:
α✝ : Type u_1
l : List α✝
a : α✝
p : α✝ → Bool
al : a ∈ l
pa : p a = true
w✝ : α✝
l₁ l₂ : List α✝
left✝¹ : ∀ (b : α✝), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
e₁ : l = l₁ ++ w✝ :: l₂
e₂ : eraseP p l = l₁ ++ l₂
⊢ l₁.length + l₂.length = l₁.length + (l₂.length + 1) - 1

Tactic:
rfl

Result:
no goals

Proof state:
α✝ : Type u_1
l : List α✝
a : α✝
p : α✝ → Bool
al : a ∈ l
pa : p a = true
⊢ (eraseP p l).length = l.length - 1

Tactic:
let ⟨_, l₁, l₂, _, _, e₁, e₂⟩ := exists_of_eraseP al pa

Result:
α✝ : Type u_1
l : List α✝
a : α✝
p : α✝ → Bool
al : a ∈ l
pa : p a = true
w✝ : α✝
l₁ l₂ : List α✝
left✝¹ : ∀ (b : α✝), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
e₁ : l = l₁ ++ w✝ :: l₂
e₂ : eraseP p l = l₁ ++ l₂
⊢ (eraseP p l).length = l.length - 1

Proof state:
α✝ : Type u_1
l : List α✝
a : α✝
p : α✝ → Bool
al : a ∈ l
pa : p a = true
w✝ : α✝
l₁ l₂ : List α✝
left✝¹ : ∀ (b : α✝), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
e₁ : l = l₁ ++ w✝ :: l₂
e₂ : eraseP p l = l₁ ++ l₂
⊢ (eraseP p l).length = l.length - 1

Tactic:
rw [e₂]

Result:
α✝ : Type u_1
l : List α✝
a : α✝
p : α✝ → Bool
al : a ∈ l
pa : p a = true
w✝ : α✝
l₁ l₂ : List α✝
left✝¹ : ∀ (b : α✝), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
e₁ : l = l₁ ++ w✝ :: l₂
e₂ : eraseP p l = l₁ ++ l₂
⊢ (l₁ ++ l₂).length = l.length - 1
-- Mathlib/Computability/EpsilonNFA.lean
theorem mem_evalFrom_iff_exists {s : σ} {S : Set σ} {x : List α} :
    s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

Proof state:
case nil
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
⊢ s ∈ M.evalFrom S [] ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} []

Tactic:
apply mem_εClosure_iff_exists

Result:
no goals

Proof state:
case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l✝ : List α
a✝ : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l✝ ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l✝
s : σ
⊢ (∃ t, (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l✝) ∧ s ∈ M.εClosure (M.step t (some a✝))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l✝, s ∈ M.εClosure (M.step t_1 (some a✝))

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
s : σ
S : Set σ
x : List α
⊢ s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

Tactic:
induction' x using List.reverseRecOn with _ _ ih generalizing s

Result:
case nil
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
⊢ s ∈ M.evalFrom S [] ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} []

case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l✝ : List α
a✝ : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l✝ ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l✝
s : σ
⊢ s ∈ M.evalFrom S (l✝ ++ [a✝]) ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} (l✝ ++ [a✝])

Proof state:
case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l✝ : List α
a✝ : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l✝ ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l✝
s : σ
⊢ s ∈ M.evalFrom S (l✝ ++ [a✝]) ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} (l✝ ++ [a✝])

Tactic:
simp_rw [evalFrom_append_singleton, mem_stepSet_iff, ih]

Result:
case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l✝ : List α
a✝ : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l✝ ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l✝
s : σ
⊢ (∃ t, (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l✝) ∧ s ∈ M.εClosure (M.step t (some a✝))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l✝, s ∈ M.εClosure (M.step t_1 (some a✝))
-- Mathlib/Data/PNat/Find.lean
theorem lt_find_iff (n : ℕ+) : n < PNat.find h ↔ ∀ m ≤ n, ¬p m

Proof state:
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ+
⊢ n < PNat.find h ↔ ∀ m ≤ n, ¬p m

Tactic:
simp only [← add_one_le_iff, le_find_iff, add_le_add_iff_right]

Result:
no goals
-- Mathlib/Algebra/BigOperators/NatAntidiagonal.lean
theorem prod_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → M} :
    (∏ p ∈ antidiagonal (n + 1), f p)
      = f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p ∈ antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)

Tactic:
rw [antidiagonal_succ, prod_cons, prod_map]

Result:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1) *
      ∏ x ∈ antidiagonal n,
        f (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) x) =
    f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1) *
      ∏ x ∈ antidiagonal n,
        f (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) x) =
    f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_self (x : M) : polar Q x x = 2 • Q x

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ 4 • Q x = (2 * 2) • Q x

Tactic:
norm_num

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ polar (⇑Q) x x = 2 • Q x

Tactic:
rw [polar, map_add_self, sub_sub, sub_eq_iff_eq_add, ← two_smul ℕ, ← two_smul ℕ, ← mul_smul]

Result:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ 4 • Q x = (2 * 2) • Q x
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem neLocus_self_add_right : neLocus f (f + g) = g.support

Proof state:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus (f + g) = g.support

Tactic:
rw [← neLocus_zero_left, ← @neLocus_add_left α N _ _ _ f 0 g, add_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_flatten_eq_none_iff {xs : Array (Array α)} {p : α → Bool} :
    xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x

Proof state:
α : Type u_1
xs : Array (Array α)
p : α → Bool
⊢ find? p xs.flatten = none ↔ ∀ (ys : Array α), ys ∈ xs → ∀ (x : α), x ∈ ys → (!p x) = true

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem inv_one_add_tan_sq {x : ℝ} (hx : cos x ≠ 0) : (1 + tan x ^ 2)⁻¹ = cos x ^ 2 :=
  have : Complex.cos x ≠ 0 := mt (congr_arg re) hx
  ofReal_inj.1 <| by simpa using Complex.inv_one_add_tan_sq this

Proof state:
x : ℝ
hx : cos x ≠ 0
this : Complex.cos ↑x ≠ 0
⊢ ↑(1 + tan x ^ 2)⁻¹ = ↑(cos x ^ 2)

Tactic:
simpa using Complex.inv_one_add_tan_sq this

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean
@[ext]
lemma ext_inner {A B : E →WOT[𝕜] F} (h : ∀ x y, ⟪y, A x⟫_𝕜 = ⟪y, B x⟫_𝕜) : A = B

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
A B : E →WOT[𝕜] F
h : ∀ (x : E) (y : F), ⟪y, A x⟫_𝕜 = ⟪y, B x⟫_𝕜
⊢ A = B

Tactic:
rw [ext_iff]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
A B : E →WOT[𝕜] F
h : ∀ (x : E) (y : F), ⟪y, A x⟫_𝕜 = ⟪y, B x⟫_𝕜
⊢ ∀ (x : E), A x = B x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
A B : E →WOT[𝕜] F
h : ∀ (x : E) (y : F), ⟪y, A x⟫_𝕜 = ⟪y, B x⟫_𝕜
⊢ ∀ (x : E), A x = B x

Tactic:
exact fun x => ext_inner_left 𝕜 fun y => h x y

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem decode₂ : Primrec (decode₂ α) :=
  option_bind .decode <|
    option_guard (Primrec.beq.comp₂ (by exact encode_iff.mpr snd) (by exact fst.comp fst)) snd

Proof state:
α : Type u_1
inst✝ : Primcodable α
⊢ Primrec₂ fun p => encode

Tactic:
exact encode_iff.mpr snd

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Primcodable α
⊢ Primrec₂ fun p a => p.1

Tactic:
exact fst.comp fst

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
lemma isLocalHomeomorph_circleExp : IsLocalHomeomorph Circle.exp

Proof state:
this : Fact (0 < 2 * π)
⊢ IsLocalHomeomorph ⇑Circle.exp

Tactic:
exact homeomorphCircle'.isLocalHomeomorph.comp (isLocalHomeomorph_coe (2 * π))

Result:
no goals

Proof state:
⊢ 0 < 2 * π

Tactic:
positivity

Result:
no goals

Proof state:
⊢ IsLocalHomeomorph ⇑Circle.exp

Tactic:
have : Fact (0 < 2 * π) := ⟨by positivity⟩

Result:
this : Fact (0 < 2 * π)
⊢ IsLocalHomeomorph ⇑Circle.exp
-- Mathlib/LinearAlgebra/Dual.lean
theorem Module.Dual.eval_naturality (f : M₁ →ₗ[R] M₂) :
    f.dualMap.dualMap ∘ₗ eval R M₁ = eval R M₂ ∘ₗ f

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
⊢ f.dualMap.dualMap ∘ₗ eval R M₁ = eval R M₂ ∘ₗ f

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
@[to_additive]
lemma pow_mem_of_relindex_ne_zero_of_dvd (h : H.relindex K ≠ 0) {a : G} (ha : a ∈ K) {n : ℕ}
    (hn : ∀ m, 0 < m → m ≤ H.relindex K → m ∣ n) : a ^ n ∈ H ⊓ K

Proof state:
case a
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relindex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.relindex K → m ∣ n
⊢ a ^ n ∈ H ⊓ K ↔ ⟨a, ha⟩ ^ n ∈ H.subgroupOf K

Tactic:
simp [pow_mem ha, mem_subgroupOf]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relindex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.relindex K → m ∣ n
⊢ a ^ n ∈ H ⊓ K

Tactic:
convert pow_mem_of_index_ne_zero_of_dvd h ⟨a, ha⟩ hn

Result:
case a
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relindex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.relindex K → m ∣ n
⊢ a ^ n ∈ H ⊓ K ↔ ⟨a, ha⟩ ^ n ∈ H.subgroupOf K
-- Mathlib/Data/Finset/PImage.lean
theorem toFinset_none [Decidable (none : Part α).Dom] : none.toFinset = (∅ : Finset α)

Proof state:
α : Type u_1
inst✝ : Decidable none.Dom
⊢ none.toFinset = ∅

Tactic:
simp [toFinset]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_not_self : ∀ (x : Bool), (x && !x) = false

Proof state:
⊢ ∀ (x : Bool), (x && !x) = false

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem modular_S_smul (z : ℍ) : ModularGroup.S • z = mk (-z : ℂ)⁻¹ z.im_inv_neg_coe_pos

Proof state:
z : ℍ
⊢ ModularGroup.S • z = mk (-↑z)⁻¹ ⋯

Tactic:
rw [specialLinearGroup_apply]

Result:
z : ℍ
⊢ mk
      ((↑((algebraMap ℤ ℝ) (↑ModularGroup.S 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑ModularGroup.S 0 1))) /
        (↑((algebraMap ℤ ℝ) (↑ModularGroup.S 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑ModularGroup.S 1 1))))
      ⋯ =
    mk (-↑z)⁻¹ ⋯

Proof state:
z : ℍ
⊢ mk
      ((↑((algebraMap ℤ ℝ) (↑ModularGroup.S 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑ModularGroup.S 0 1))) /
        (↑((algebraMap ℤ ℝ) (↑ModularGroup.S 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑ModularGroup.S 1 1))))
      ⋯ =
    mk (-↑z)⁻¹ ⋯

Tactic:
simp [ModularGroup.S, neg_div, inv_neg, toGL]

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem isOpen_iff_ultrafilter' [CompactSpace X] (U : Set X) :
    IsOpen U ↔ ∀ F : Ultrafilter X, F.lim ∈ U → U ∈ F.1

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
x : X
hx : x ∈ U
f : Ultrafilter X
h : ↑f ≤ 𝓝 x
⊢ U ∈ f

Tactic:
rw [← Ultrafilter.lim_eq_iff_le_nhds.2 h] at hx

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
x : X
f : Ultrafilter X
hx : f.lim ∈ U
h : ↑f ≤ 𝓝 x
⊢ U ∈ f

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
⊢ IsOpen U ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F

Tactic:
rw [isOpen_iff_ultrafilter]

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
⊢ (∀ x ∈ U, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l) ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
⊢ (∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F) → ∀ x ∈ U, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l

Tactic:
intro cond x hx f h

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
x : X
hx : x ∈ U
f : Ultrafilter X
h : ↑f ≤ 𝓝 x
⊢ U ∈ f

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
x : X
f : Ultrafilter X
hx : f.lim ∈ U
h : ↑f ≤ 𝓝 x
⊢ U ∈ f

Tactic:
exact cond _ hx

Result:
no goals

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
⊢ (∀ x ∈ U, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l) ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F

Tactic:
refine ⟨fun h F hF => h F.lim hF F F.le_nhds_lim, ?_⟩

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
⊢ (∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F) → ∀ x ∈ U, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem integral_eq_tsum (h : IsFundamentalDomain G s μ) (f : α → E) (hf : Integrable f μ) :
    ∫ x, f x ∂μ = ∑' g : G, ∫ x in g • s, f x ∂μ :=
  integral_eq_tsum_of_ac h (by rfl) f hf

Proof state:
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
s : Set α
μ : Measure α
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
f : α → E
hf : Integrable f μ
⊢ μ ≪ μ

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsb?_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : x[i]? = none

Proof state:
w : Nat
x : BitVec w
i : Nat
ge : w ≤ i
⊢ x[i]? = none

Tactic:
simp [ge]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma div_eq_iff (hbot : b ≠ ⊥) (htop : b ≠ ⊤) (hzero : b ≠ 0) : c / b = a ↔ c = a * b

Proof state:
case refine_2
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
⊢ c / b = a

Tactic:
rw [h, mul_comm a b, ← mul_div b a b, @mul_div_cancel a b hbot htop hzero]

Result:
no goals

Proof state:
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
⊢ c / b = a ↔ c = a * b

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
⊢ c = a * b

case refine_2
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
⊢ c / b = a

Proof state:
case refine_1
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
⊢ c = a * b

Tactic:
rw [← @mul_div_cancel c b hbot htop hzero, h, mul_comm a b]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_tendsto_closure_iSup {ι : Type*} [Preorder ι]
    (U : ι → Submodule 𝕜 E) [∀ i, HasOrthogonalProjection (U i)]
    [HasOrthogonalProjection (⨆ i, U i).topologicalClosure] (hU : Monotone U) (x : E) :
    Filter.Tendsto (fun i => (orthogonalProjection (U i) x : E)) atTop
      (𝓝 (orthogonalProjection (⨆ i, U i).topologicalClosure x : E))

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)
proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ⨅ x, ‖y - ↑x‖ ≤ ‖y - a‖

Tactic:
change _ ≤ ‖y - (⟨a, hU hi hI⟩ : U i)‖

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)
proj_x : ∀ (i : ι), (orthogonalProjection (U i)) x = (orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ i, U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ⨅ x, ‖y - ↑x‖ ≤ ‖y - ↑⟨a, ⋯⟩‖

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))

Tactic:
let y := (orthogonalProjection (⨆ i, U i).topologicalClosure x : E)

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), HasOrthogonalProjection (U i)
inst✝ : HasOrthogonalProjection (⨆ i, U i).topologicalClosure
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
y : E := ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)
⊢ Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x))
-- Mathlib/Order/Filter/CountablyGenerated.lean
theorem isCountablyGenerated_of_seq {f : Filter α} (h : ∃ x : ℕ → Set α, f = ⨅ i, 𝓟 (x i)) :
    f.IsCountablyGenerated

Proof state:
case intro
α : Type u_1
x : ℕ → Set α
⊢ (⨅ i, 𝓟 (x i)).IsCountablyGenerated

Tactic:
apply isCountablyGenerated_seq

Result:
no goals

Proof state:
α : Type u_1
f : Filter α
h : ∃ x, f = ⨅ i, 𝓟 (x i)
⊢ f.IsCountablyGenerated

Tactic:
rcases h with ⟨x, rfl⟩

Result:
case intro
α : Type u_1
x : ℕ → Set α
⊢ (⨅ i, 𝓟 (x i)).IsCountablyGenerated
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem blsub_lt_ord_lift_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c)
    (ho : Cardinal.lift.{v, u} o.card < c) :
    (∀ i hi, f i hi < c.ord) → Ordinal.blsub.{u, v} o f < c.ord :=
  blsub_lt_ord_lift (by rwa [hc.cof_eq])

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
ho : lift.{v, u} o.card < c
⊢ lift.{v, u} o.card < c.ord.cof

Tactic:
rwa [hc.cof_eq]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem isLocalization_stalk' (y : PrimeSpectrum Γ(X, U)) (hy : hU.fromSpec.base y ∈ U) :
    @IsLocalization.AtPrime
      (R := Γ(X, U))
      (S := X.presheaf.stalk <| hU.fromSpec.base y) _ _
      ((TopCat.Presheaf.algebra_section_stalk X.presheaf _)) y.asIdeal _

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : (ConcreteCategory.hom hU.fromSpec.base) y ∈ U
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) y))) y.asIdeal

Tactic:
apply
  (@IsLocalization.isLocalization_iff_of_ringEquiv (R := Γ(X, U))
    (S := X.presheaf.stalk (hU.fromSpec.base y)) _ y.asIdeal.primeCompl _
    (TopCat.Presheaf.algebra_section_stalk X.presheaf ⟨hU.fromSpec.base y, hy⟩) _ _
    (asIso <| hU.fromSpec.stalkMap y).commRingCatIsoToRingEquiv).mpr

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : (ConcreteCategory.hom hU.fromSpec.base) y ∈ U
⊢ IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y)

Proof state:
case a
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : (ConcreteCategory.hom hU.fromSpec.base) y ∈ U
⊢ IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y) ↔
    IsLocalization y.asIdeal.primeCompl ↑((structureSheaf ↑Γ(X, U)).presheaf.stalk y)

Tactic:
rfl

Result:
no goals

Proof state:
case a
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : (ConcreteCategory.hom hU.fromSpec.base) y ∈ U
⊢ IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y) ↔
    IsLocalization.AtPrime (↑((structureSheaf ↑Γ(X, U)).presheaf.stalk y)) y.asIdeal

Tactic:
delta IsLocalization.AtPrime StructureSheaf.stalkAlgebra

Result:
case a
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : (ConcreteCategory.hom hU.fromSpec.base) y ∈ U
⊢ IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y) ↔
    IsLocalization y.asIdeal.primeCompl ↑((structureSheaf ↑Γ(X, U)).presheaf.stalk y)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : (ConcreteCategory.hom hU.fromSpec.base) y ∈ U
⊢ IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y)

Tactic:
convert StructureSheaf.IsLocalization.to_stalk Γ(X, U) y using 1

Result:
case a
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hy : (ConcreteCategory.hom hU.fromSpec.base) y ∈ U
⊢ IsLocalization y.asIdeal.primeCompl ↑((Spec Γ(X, U)).presheaf.stalk y) ↔
    IsLocalization.AtPrime (↑((structureSheaf ↑Γ(X, U)).presheaf.stalk y)) y.asIdeal
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma ediam_ne_zero [Nontrivial α] : G.ediam ≠ 0

Proof state:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
huv : ∀ (i i_1 : α), i = i_1
⊢ u = v

Tactic:
exact huv u v

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
huv : G.ediam = 0
⊢ u = v

Tactic:
simp only [ediam, nonpos_iff_eq_zero, ENat.iSup_eq_zero, edist_eq_zero_iff] at huv

Result:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
huv : ∀ (i i_1 : α), i = i_1
⊢ u = v

Proof state:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
huv : u ≠ v
⊢ G.ediam ≠ 0

Tactic:
contrapose! huv

Result:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
huv : G.ediam = 0
⊢ u = v

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.ediam ≠ 0

Tactic:
obtain ⟨u, v, huv⟩ := exists_pair_ne ‹_›

Result:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u v : α
huv : u ≠ v
⊢ G.ediam ≠ 0