harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Cover.lean
theorem WCovBy.eq_or_eq (h : a ⩿ b) (h2 : a ≤ c) (h3 : c ≤ b) : c = a ∨ c = b

Proof state:
case inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b

Tactic:
exact Or.inl h2.symm

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a < c
⊢ c = a ∨ c = b

Tactic:
rcases h3.eq_or_lt with (h3 | h3)

Result:
case inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b

case inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b

Proof state:
case inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b

Tactic:
exact (h.2 h2 h3).elim

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2 : a ≤ c
h3 : c ≤ b
⊢ c = a ∨ c = b

Tactic:
rcases h2.eq_or_lt with (h2 | h2)

Result:
case inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b

case inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a < c
⊢ c = a ∨ c = b

Proof state:
case inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b

Tactic:
exact Or.inr h3

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCodetecting_unop_iff {𝒢 : Set Cᵒᵖ} : IsCodetecting 𝒢.unop ↔ IsDetecting 𝒢

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set Cᵒᵖ
⊢ IsCodetecting 𝒢.unop ↔ IsDetecting 𝒢

Tactic:
rw [← isDetecting_op_iff, Set.unop_op]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem sub_orthogonalProjection_mem_orthogonal (v : E) : v - orthogonalProjection K v ∈ Kᗮ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v w : E
hw : w ∈ K
⊢ ⟪w, v - ↑((orthogonalProjection K) v)⟫_𝕜 = 0

Tactic:
rw [inner_eq_zero_symm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v w : E
hw : w ∈ K
⊢ ⟪v - ↑((orthogonalProjection K) v), w⟫_𝕜 = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
⊢ v - ↑((orthogonalProjection K) v) ∈ Kᗮ

Tactic:
intro w hw

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v w : E
hw : w ∈ K
⊢ ⟪w, v - ↑((orthogonalProjection K) v)⟫_𝕜 = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v w : E
hw : w ∈ K
⊢ ⟪v - ↑((orthogonalProjection K) v), w⟫_𝕜 = 0

Tactic:
exact orthogonalProjection_inner_eq_zero _ _ hw

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) :
    s₁.sup f = s₂.sup g

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.sup f = s₁.sup g

Tactic:
exact Finset.fold_congr hfg

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
⊢ s₁.sup f = s₂.sup g

Tactic:
subst hs

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.sup f = s₁.sup g
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem Submodule.sup_orthogonal_of_completeSpace [HasOrthogonalProjection K] : K ⊔ Kᗮ = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
⊢ K ⊔ Kᗮ = ⊤

Tactic:
convert Submodule.sup_orthogonal_inf_of_completeSpace (le_top : K ≤ ⊤) using 2

Result:
case h.e'_2.h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
⊢ Kᗮ = Kᗮ ⊓ ⊤

Proof state:
case h.e'_2.h.e'_4
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
⊢ Kᗮ = Kᗮ ⊓ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Iic_eq_cons_Iio (b : α) : Iic b = (Iio b).cons b not_mem_Iio_self

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) ⋯

Tactic:
classical rw [cons_eq_insert, Iio_insert]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) ⋯

Tactic:
rw [cons_eq_insert, Iio_insert]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/EpiMono.lean
lemma mono_of_injective (hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Injective (f.app X)) : Mono f where
  right_cancellation {M} g₁ g₂ hg

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(ConcreteCategory.hom (f.app X))
M : PresheafOfModules R
g₁ g₂ : M ⟶ M₁
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂

Tactic:
ext X m

Result:
case h.hf.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(ConcreteCategory.hom (f.app X))
M : PresheafOfModules R
g₁ g₂ : M ⟶ M₁
hg : g₁ ≫ f = g₂ ≫ f
X : Cᵒᵖ
m : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom (g₁.app X)) m = (ModuleCat.Hom.hom (g₂.app X)) m

Proof state:
case h.hf.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(ConcreteCategory.hom (f.app X))
M : PresheafOfModules R
g₁ g₂ : M ⟶ M₁
hg : g₁ ≫ f = g₂ ≫ f
X : Cᵒᵖ
m : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom (g₁.app X)) m = (ModuleCat.Hom.hom (g₂.app X)) m

Tactic:
exact hf (congr_fun ((evaluation R X ⋙ forget _).congr_map hg) m)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJ_1728_of_two_ne_zero (h2 : (2 : F) ≠ 0) : ofJ 1728 = ofJ1728 F

Proof state:
case neg
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : ¬3 = 0
⊢ ofJ 1728 = ofJ1728 F

Tactic:
rw [ofJ, show (1728 : F) = 2 ^ 6 * 3 ^ 3 by norm_num1,
  if_neg (mul_ne_zero (pow_ne_zero 6 h2) (pow_ne_zero 3 h3)), if_pos rfl]

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
⊢ ofJ 1728 = ofJ1728 F

Tactic:
by_cases h3 : (3 : F) = 0

Result:
case pos
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : 3 = 0
⊢ ofJ 1728 = ofJ1728 F

case neg
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : ¬3 = 0
⊢ ofJ 1728 = ofJ1728 F

Proof state:
case pos
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : 3 = 0
⊢ ofJ 1728 = ofJ1728 F

Tactic:
exact ofJ_1728_of_three_eq_zero h3

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : ¬3 = 0
⊢ 1728 = 2 ^ 6 * 3 ^ 3

Tactic:
norm_num1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem unattach_append {p : α → Prop} {l₁ l₂ : Array { x // p x }} :
    (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach

Proof state:
case mk
α : Type u_1
p : α → Prop
l₂ : Array { x // p x }
toList✝ : List { x // p x }
⊢ ({ toList := toList✝ } ++ l₂).unattach = { toList := toList✝ }.unattach ++ l₂.unattach

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
p : α → Prop
toList✝¹ toList✝ : List { x // p x }
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ }).unattach =
    { toList := toList✝¹ }.unattach ++ { toList := toList✝ }.unattach

Proof state:
α : Type u_1
p : α → Prop
l₁ l₂ : Array { x // p x }
⊢ (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach

Tactic:
cases l₁

Result:
case mk
α : Type u_1
p : α → Prop
l₂ : Array { x // p x }
toList✝ : List { x // p x }
⊢ ({ toList := toList✝ } ++ l₂).unattach = { toList := toList✝ }.unattach ++ l₂.unattach

Proof state:
case mk.mk
α : Type u_1
p : α → Prop
toList✝¹ toList✝ : List { x // p x }
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ }).unattach =
    { toList := toList✝¹ }.unattach ++ { toList := toList✝ }.unattach

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem not_mem_iff_subset (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ∉ y ↔ y ⊆ x

Proof state:
x y : ZFSet.{u}
⊢ x.IsOrdinal → y.IsOrdinal → x ∉ y → y ⊆ x

Tactic:
apply Sym2.GameAdd.induction mem_wf _ x y

Result:
x y : ZFSet.{u}
⊢ ∀ (a₁ b₁ : ZFSet.{u}),
    (∀ (a₂ b₂ : ZFSet.{u}),
        Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(a₁, b₁) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ∉ b₂ → b₂ ⊆ a₂) →
      a₁.IsOrdinal → b₁.IsOrdinal → a₁ ∉ b₁ → b₁ ⊆ a₁

Proof state:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ∉ b₂ → b₂ ⊆ a₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hyx : x ∉ y
z : ZFSet.{u}
hzy : z ∈ y
⊢ z ∈ x

Tactic:
by_contra hzx

Result:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ∉ b₂ → b₂ ⊆ a₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hyx : x ∉ y
z : ZFSet.{u}
hzy : z ∈ y
hzx : z ∉ x
⊢ False

Proof state:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∉ y ↔ y ⊆ x

Tactic:
refine ⟨?_, fun hxy hyx ↦ mem_irrefl _ (hxy hyx)⟩

Result:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∉ y → y ⊆ x

Proof state:
x y : ZFSet.{u}
⊢ ∀ (a₁ b₁ : ZFSet.{u}),
    (∀ (a₂ b₂ : ZFSet.{u}),
        Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(a₁, b₁) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ∉ b₂ → b₂ ⊆ a₂) →
      a₁.IsOrdinal → b₁.IsOrdinal → a₁ ∉ b₁ → b₁ ⊆ a₁

Tactic:
intros x y IH hx hy hyx z hzy

Result:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ∉ b₂ → b₂ ⊆ a₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hyx : x ∉ y
z : ZFSet.{u}
hzy : z ∈ y
⊢ z ∈ x

Proof state:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∉ y → y ⊆ x

Tactic:
revert hx hy

Result:
x y : ZFSet.{u}
⊢ x.IsOrdinal → y.IsOrdinal → x ∉ y → y ⊆ x

Proof state:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ∉ b₂ → b₂ ⊆ a₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hyx : x ∉ y
z : ZFSet.{u}
hzy : z ∈ y
hzx : z ∉ x
⊢ False

Tactic:
exact hyx (mem_of_subset_of_mem hx hy (IH z x (Sym2.GameAdd.fst_snd hzy) (hy.mem hzy) hx hzx) hzy)

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_two_mul (n : ℕ) : fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)

Proof state:
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) = fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + fib n✝)

Tactic:
ring

Result:
no goals

Proof state:
case zero

⊢ fib (2 * 0) = fib 0 * (2 * fib (0 + 1) - fib 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) =
    fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + (fib n✝ + fib (n✝ + 1)) - fib (n✝ + 1))

Tactic:
simp only [← add_assoc, add_tsub_cancel_right]

Result:
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) = fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + fib n✝)

Proof state:
n : ℕ
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)

Tactic:
cases n

Result:
case zero

⊢ fib (2 * 0) = fib 0 * (2 * fib (0 + 1) - fib 0)

case succ
n✝ : ℕ
⊢ fib (2 * (n✝ + 1)) = fib (n✝ + 1) * (2 * fib (n✝ + 1 + 1) - fib (n✝ + 1))

Proof state:
case succ
n✝ : ℕ
⊢ fib (2 * (n✝ + 1)) = fib (n✝ + 1) * (2 * fib (n✝ + 1 + 1) - fib (n✝ + 1))

Tactic:
rw [two_mul, ← add_assoc, fib_add, fib_add_two, two_mul]

Result:
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) =
    fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + (fib n✝ + fib (n✝ + 1)) - fib (n✝ + 1))
-- Mathlib/Analysis/Convex/Gauge.lean
theorem tendsto_gauge_nhds_zero' (hs : s ∈ 𝓝 0) : Tendsto (gauge s) (𝓝 0) (𝓝[≥] 0)

Proof state:
case h
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
ε : ℝ
hs : ε • s ∈ 𝓝 0
hε : 0 < ε
x : E
hx : x ∈ ε • s
⊢ gauge s x ∈ Icc 0 ε

Tactic:
exact ⟨gauge_nonneg _, gauge_le_of_mem hε.le hx⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : s ∈ 𝓝 0
⊢ Tendsto (gauge s) (𝓝 0) (𝓝[≥] 0)

Tactic:
refine nhdsGE_basis_Icc.tendsto_right_iff.2 fun ε hε ↦ ?_

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : s ∈ 𝓝 0
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : s ∈ 𝓝 0
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε

Tactic:
rw [← set_smul_mem_nhds_zero_iff hε.ne'] at hs

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
ε : ℝ
hs : ε • s ∈ 𝓝 0
hε : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
ε : ℝ
hs : ε • s ∈ 𝓝 0
hε : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε

Tactic:
filter_upwards [hs] with x hx

Result:
case h
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
ε : ℝ
hs : ε • s ∈ 𝓝 0
hε : 0 < ε
x : E
hx : x ∈ ε • s
⊢ gauge s x ∈ Icc 0 ε
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
theorem hasSum_int_sinZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℤ ↦ -I * n.sign * cexp (2 * π * I * a * n) / ↑|n| ^ s / 2) (sinZeta a s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s / (s + 1).Gammaℝ)

Tactic:
refine ((hasSum_int_completedSinZeta a hs).div_const (Gammaℝ (s + 1))).congr_fun fun n ↦ ?_

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 =
    (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 / (s + 1).Gammaℝ

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 =
    (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 / (s + 1).Gammaℝ

Tactic:
have : 0 < re (s + 1) := by rw [add_re, one_re]; positivity

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
this : 0 < (s + 1).re
⊢ -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 =
    (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 / (s + 1).Gammaℝ

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
this : 0 < (s + 1).re
⊢ -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 =
    (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 / (s + 1).Gammaℝ

Tactic:
simp only [mul_assoc, div_right_comm _ _ (Gammaℝ _),
  mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos this)]

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ 0 < s.re + 1

Tactic:
positivity

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (sinZeta (↑a) s)

Tactic:
rw [sinZeta]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s / (s + 1).Gammaℝ)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ 0 < (s + 1).re

Tactic:
rw [add_re, one_re]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ 0 < s.re + 1
-- Mathlib/Algebra/Order/SuccPred.lean
lemma antitoneOn_of_le_sub_one (hs : s.OrdConnected) :
    (∀ a, ¬ IsMin a → a ∈ s → a - 1 ∈ s → f a ≤ f (a - 1)) → AntitoneOn f s

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f a ≤ f (a - 1)) → AntitoneOn f s

Tactic:
simpa [Order.pred_eq_sub_one] using antitoneOn_of_le_pred hs (f := f)

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem isUnit_iff_singleton_aux {α} [Group α] {s : Finset α} :
    (∃ a, s = {a} ∧ IsUnit a) ↔ ∃ a, s = {a}

Proof state:
α : Type u_5
inst✝ : Group α
s : Finset α
⊢ (∃ a, s = {a} ∧ IsUnit a) ↔ ∃ a, s = {a}

Tactic:
simp only [Group.isUnit, and_true]

Result:
no goals
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem unit_mul_pow_congr_unit {ϖ : R} (hirr : Irreducible ϖ) (u v : Rˣ) (m n : ℕ)
    (h : ↑u * ϖ ^ m = v * ϖ ^ n) : u = v

Proof state:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ϖ ^ m = 0
⊢ u = v

Tactic:
apply (hirr.ne_zero (pow_eq_zero h)).elim

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u * ϖ ^ m - ↑v * ϖ ^ m = 0
⊢ u = v

Tactic:
rw [← sub_mul, mul_eq_zero] at h

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u - ↑v = 0 ∨ ϖ ^ m = 0
⊢ u = v

Proof state:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u - ↑v = 0
⊢ u = v

Tactic:
rw [sub_eq_zero] at h

Result:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u = ↑v
⊢ u = v

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u - ↑v = 0 ∨ ϖ ^ m = 0
⊢ u = v

Tactic:
rcases h with h | h

Result:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u - ↑v = 0
⊢ u = v

case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ϖ ^ m = 0
⊢ u = v

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u * ϖ ^ m = ↑v * ϖ ^ m
⊢ u = v

Tactic:
rw [← sub_eq_zero] at h

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u * ϖ ^ m - ↑v * ϖ ^ m = 0
⊢ u = v

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m n : ℕ
h : ↑u * ϖ ^ m = ↑v * ϖ ^ n
⊢ u = v

Tactic:
obtain rfl : m = n := unit_mul_pow_congr_pow hirr hirr u v m n h

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u * ϖ ^ m = ↑v * ϖ ^ m
⊢ u = v

Proof state:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hirr : Irreducible ϖ
u v : Rˣ
m : ℕ
h : ↑u = ↑v
⊢ u = v

Tactic:
exact mod_cast h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem max_le {a b c : Int} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c :=
  ⟨fun h => ⟨Int.le_trans (Int.le_max_left ..) h, Int.le_trans (Int.le_max_right ..) h⟩,
   fun ⟨h₁, h₂⟩ => by rw [Int.max_def]; split <;> assumption⟩

Proof state:
a b c : Int
x✝ : a ≤ c ∧ b ≤ c
h₁ : a ≤ c
h₂ : b ≤ c
⊢ max a b ≤ c

Tactic:
rw [Int.max_def]

Result:
a b c : Int
x✝ : a ≤ c ∧ b ≤ c
h₁ : a ≤ c
h₂ : b ≤ c
⊢ (if a ≤ b then b else a) ≤ c

Proof state:
a b c : Int
x✝ : a ≤ c ∧ b ≤ c
h₁ : a ≤ c
h₂ : b ≤ c
⊢ (if a ≤ b then b else a) ≤ c

Tactic:
split <;> assumption

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_ne_zero (f0 : 2 ≤ #f.support) : eraseLead f ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ ¬#(f.support.erase f.natDegree) = 0

Tactic:
exact
  (zero_lt_one.trans_le <| (tsub_le_tsub_right f0 1).trans Finset.pred_card_le_card_erase).ne.symm

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ f.eraseLead ≠ 0

Tactic:
rw [Ne, ← card_support_eq_zero, eraseLead_support]

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ ¬#(f.support.erase f.natDegree) = 0
-- Mathlib/Algebra/EuclideanDomain/Defs.lean
theorem gcdA_zero_left {s : R} : gcdA 0 s = 0

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ gcdA 0 s = 0

Tactic:
unfold gcdA

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).fst = 0

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).fst = 0

Tactic:
rw [xgcd, xgcd_zero_left]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem lookup_singleton_eq {a : α} {b : β a} : (singleton a b).lookup a = some b

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ lookup a (singleton a b) = some b

Tactic:
rw [singleton, lookup_toFinmap, AList.singleton, AList.lookup, dlookup_cons_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
/-- If `s ×ˢ t` is a null measurable set and `ν t ≠ 0`, then `s` is a null measurable set. -/
lemma _root_.MeasureTheory.NullMeasurableSet.left_of_prod {s : Set α} {t : Set β}
    (h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)) (ht : ν t ≠ 0) : NullMeasurableSet s μ

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : ν t ≠ 0
⊢ NullMeasurableSet s μ

Tactic:
refine .right_of_prod ?_ ht

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : ν t ≠ 0
⊢ NullMeasurableSet (t ×ˢ s) (ν.prod μ)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : ν t ≠ 0
⊢ NullMeasurableSet (Prod.swap ⁻¹' s ×ˢ t) (ν.prod μ)

Tactic:
exact h.preimage measurePreserving_swap.quasiMeasurePreserving

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : ν t ≠ 0
⊢ NullMeasurableSet (t ×ˢ s) (ν.prod μ)

Tactic:
rw [← preimage_swap_prod]

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : ν t ≠ 0
⊢ NullMeasurableSet (Prod.swap ⁻¹' s ×ˢ t) (ν.prod μ)
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_restrictVar' [DecidableEq α] {t : L.Term α} {s : Set α} (h : ↑t.varFinset ⊆ s)
    {v : α → M} : (t.restrictVar (Set.inclusion h)).realize (v ∘ (↑)) = t.realize v :=
  realize_restrictVar _ (by simp)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
t : L.Term α
s : Set α
h : ↑t.varFinset ⊆ s
v : α → M
⊢ ∀ (a : { x // x ∈ t.varFinset }), (v ∘ Subtype.val) (Set.inclusion h a) = v ↑a

Tactic:
simp

Result:
no goals