harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_cancel' (m : M) (s : S) : s • mk' f m s = f m

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ s • mk' f m s = f m

Tactic:
rw [Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, mk'_cancel]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
theorem _root_.Filter.EventuallyEq.mlieBracket_vectorField
    (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) : mlieBracket I V₁ W₁ =ᶠ[𝓝 x] mlieBracket I V W

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
⊢ mlieBracket I V₁ W₁ =ᶠ[𝓝 x] mlieBracket I V W

Tactic:
filter_upwards [hV.eventuallyEq_nhds, hW.eventuallyEq_nhds] with y hVy hWy

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : M
hVy : V₁ =ᶠ[𝓝 y] V
hWy : W₁ =ᶠ[𝓝 y] W
⊢ mlieBracket I V₁ W₁ y = mlieBracket I V W y

Proof state:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : M
hVy : V₁ =ᶠ[𝓝 y] V
hWy : W₁ =ᶠ[𝓝 y] W
⊢ mlieBracket I V₁ W₁ y = mlieBracket I V W y

Tactic:
exact hVy.mlieBracket_vectorField_eq hWy

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
/-- The left options of `x * y` agree with that of `y * x` up to equivalence. -/
lemma mulOption_symm (x y) {i j} : ⟦mulOption x y i j⟧ = (⟦mulOption y x j i⟧ : Game)

Proof state:
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x * y.moveLeft j⟧ + ⟦x.moveLeft i * y⟧ - ⟦x.moveLeft i * y.moveLeft j⟧ =
    ⟦y.moveLeft j * x⟧ + ⟦y * x.moveLeft i⟧ - ⟦y.moveLeft j * x.moveLeft i⟧

Tactic:
congr 1

Result:
case e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x * y.moveLeft j⟧ + ⟦x.moveLeft i * y⟧ = ⟦y.moveLeft j * x⟧ + ⟦y * x.moveLeft i⟧

case e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.moveLeft i * y.moveLeft j⟧ = ⟦y.moveLeft j * x.moveLeft i⟧

Proof state:
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.mulOption y i j⟧ = ⟦y.mulOption x j i⟧

Tactic:
dsimp only [mulOption, quot_sub, quot_add]

Result:
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.moveLeft i * y⟧ + ⟦x * y.moveLeft j⟧ - ⟦x.moveLeft i * y.moveLeft j⟧ =
    ⟦y.moveLeft j * x⟧ + ⟦y * x.moveLeft i⟧ - ⟦y.moveLeft j * x.moveLeft i⟧

Proof state:
case e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.moveLeft i * y.moveLeft j⟧ = ⟦y.moveLeft j * x.moveLeft i⟧

Tactic:
rw [quot_mul_comm]

Result:
no goals

Proof state:
case e_a.e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x * y.moveLeft j⟧ = ⟦y.moveLeft j * x⟧

case e_a.e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.moveLeft i * y⟧ = ⟦y * x.moveLeft i⟧

case e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.moveLeft i * y.moveLeft j⟧ = ⟦y.moveLeft j * x.moveLeft i⟧

Tactic:
all_goals rw [quot_mul_comm]

Result:
no goals

Proof state:
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.moveLeft i * y⟧ + ⟦x * y.moveLeft j⟧ - ⟦x.moveLeft i * y.moveLeft j⟧ =
    ⟦y.moveLeft j * x⟧ + ⟦y * x.moveLeft i⟧ - ⟦y.moveLeft j * x.moveLeft i⟧

Tactic:
rw [add_comm]

Result:
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x * y.moveLeft j⟧ + ⟦x.moveLeft i * y⟧ - ⟦x.moveLeft i * y.moveLeft j⟧ =
    ⟦y.moveLeft j * x⟧ + ⟦y * x.moveLeft i⟧ - ⟦y.moveLeft j * x.moveLeft i⟧

Proof state:
case e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x * y.moveLeft j⟧ + ⟦x.moveLeft i * y⟧ = ⟦y.moveLeft j * x⟧ + ⟦y * x.moveLeft i⟧

case e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.moveLeft i * y.moveLeft j⟧ = ⟦y.moveLeft j * x.moveLeft i⟧

Tactic:
on_goal 1 => congr 1

Result:
case e_a.e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x * y.moveLeft j⟧ = ⟦y.moveLeft j * x⟧

case e_a.e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.moveLeft i * y⟧ = ⟦y * x.moveLeft i⟧

case e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.moveLeft i * y.moveLeft j⟧ = ⟦y.moveLeft j * x.moveLeft i⟧

Proof state:
case e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x * y.moveLeft j⟧ + ⟦x.moveLeft i * y⟧ = ⟦y.moveLeft j * x⟧ + ⟦y * x.moveLeft i⟧

Tactic:
congr 1

Result:
case e_a.e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x * y.moveLeft j⟧ = ⟦y.moveLeft j * x⟧

case e_a.e_a
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ ⟦x.moveLeft i * y⟧ = ⟦y * x.moveLeft i⟧
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfpFamily_le_fp (H : ∀ i, Monotone (f i)) {a b} (ab : a ≤ b) (h : ∀ i, f i b ≤ b) :
    nfpFamily f a ≤ b

Proof state:
case a.nil
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ b
a : Ordinal.{u}
ab : a ≤ b
⊢ List.foldr f a [] ≤ b

Tactic:
exact ab

Result:
no goals

Proof state:
case a.cons
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ b
i : ι
l : List ι
IH : ∀ {a : Ordinal.{u}}, a ≤ b → List.foldr f a l ≤ b
a : Ordinal.{u}
ab : a ≤ b
⊢ List.foldr f a (i :: l) ≤ b

Tactic:
exact (H i (IH ab)).trans (h i)

Result:
no goals

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal.{u}
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
⊢ nfpFamily f a ≤ b

Tactic:
apply Ordinal.iSup_le

Result:
case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal.{u}
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
⊢ ∀ (i : List ι), List.foldr f a i ≤ b

Proof state:
case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal.{u}
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
⊢ ∀ (i : List ι), List.foldr f a i ≤ b

Tactic:
intro l

Result:
case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal.{u}
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
l : List ι
⊢ List.foldr f a l ≤ b

Proof state:
case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal.{u}
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
l : List ι
⊢ List.foldr f a l ≤ b

Tactic:
induction' l with i l IH generalizing a

Result:
case a.nil
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ b
a : Ordinal.{u}
ab : a ≤ b
⊢ List.foldr f a [] ≤ b

case a.cons
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ b
i : ι
l : List ι
IH : ∀ {a : Ordinal.{u}}, a ≤ b → List.foldr f a l ≤ b
a : Ordinal.{u}
ab : a ≤ b
⊢ List.foldr f a (i :: l) ≤ b
-- Mathlib/RingTheory/RingHom/Flat.lean
/-- Bijective ring maps are flat. -/
lemma of_bijective {f : R →+* S} (hf : Function.Bijective f) : Flat f

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.Flat

Tactic:
exact Module.Flat.of_linearEquiv (LinearEquiv.ofBijective (Algebra.linearMap R S) hf).symm

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ f.Flat

Tactic:
algebraize [f]

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.Flat
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_length_sub_one_eq_getLast (l : List α) (h : l.length - 1 < l.length) :
    l[l.length - 1] = getLast l (by cases l; simp at h; simp)

Proof state:
α : Type u_1
l : List α
h : l.length - 1 < l.length
⊢ l[l.length - 1] = l.getLast ⋯

Tactic:
rw [← getLast_eq_getElem]

Result:
no goals

Proof state:
case cons
α : Type ?u.94998
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length - 1 < (head✝ :: tail✝).length
⊢ head✝ :: tail✝ ≠ []

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.94998
l : List α
h : l.length - 1 < l.length
⊢ l ≠ []

Tactic:
cases l

Result:
case nil
α : Type ?u.94998
h : [].length - 1 < [].length
⊢ [] ≠ []

case cons
α : Type ?u.94998
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length - 1 < (head✝ :: tail✝).length
⊢ head✝ :: tail✝ ≠ []

Proof state:
case nil
α : Type ?u.94998
h : [].length - 1 < [].length
⊢ [] ≠ []

case cons
α : Type ?u.94998
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length - 1 < (head✝ :: tail✝).length
⊢ head✝ :: tail✝ ≠ []

Tactic:
simp at h

Result:
case cons
α : Type ?u.94998
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length - 1 < (head✝ :: tail✝).length
⊢ head✝ :: tail✝ ≠ []
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
@[simp]
lemma centralizer_centralizer_centralizer {s : Set A} :
    centralizer R s.centralizer.centralizer = centralizer R s

Proof state:
case a
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ ↑(centralizer R s.centralizer.centralizer) = ↑(centralizer R s)

Tactic:
simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ centralizer R s.centralizer.centralizer = centralizer R s

Tactic:
apply SetLike.coe_injective

Result:
case a
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ ↑(centralizer R s.centralizer.centralizer) = ↑(centralizer R s)
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem lift_aux (x : L) : ∃ y : ℕ × K, i y.2 = x ^ p ^ y.1

Proof state:
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : L
⊢ ∃ y, i y.2 = x ^ p ^ y.1

Tactic:
obtain ⟨n, y, h⟩ := IsPRadical.pow_mem i p x

Result:
case intro.intro
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
h : i y = x ^ p ^ n
⊢ ∃ y, i y.2 = x ^ p ^ y.1

Proof state:
case intro.intro
K : Type u_1
L : Type u_2
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
i : K →+* L
p : ℕ
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
h : i y = x ^ p ^ n
⊢ ∃ y, i y.2 = x ^ p ^ y.1

Tactic:
exact ⟨(n, y), h⟩

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.Collinear.two_zsmul_oangle_eq_right {p₁ p₂ p₃ p₃' : P}
    (h : Collinear ℝ ({p₃, p₂, p₃'} : Set P)) (hp₃p₂ : p₃ ≠ p₂) (hp₃'p₂ : p₃' ≠ p₂) :
    (2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ p₁ p₂ p₃'

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₃' : P
h : Collinear ℝ {p₃, p₂, p₃'}
hp₃p₂ : p₃ ≠ p₂
hp₃'p₂ : p₃' ≠ p₂
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁ p₂ p₃'

Tactic:
rw [oangle_rev, smul_neg, h.two_zsmul_oangle_eq_left hp₃p₂ hp₃'p₂, ← smul_neg, ← oangle_rev]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
lemma le_largerSubobject (A : Subobject X) :
    A ≤ largerSubobject hG A

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A = ⊤
⊢ A ≤ largerSubobject hG A

Tactic:
subst hA

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
⊢ ⊤ ≤ largerSubobject hG ⊤

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
⊢ A ≤ largerSubobject hG A

Tactic:
by_cases hA : A = ⊤

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A = ⊤
⊢ A ≤ largerSubobject hG A

case neg
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : ¬A = ⊤
⊢ A ≤ largerSubobject hG A

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
⊢ ⊤ ≤ largerSubobject hG ⊤

Tactic:
simp only [largerSubobject_top, le_refl]

Result:
no goals

Proof state:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : ¬A = ⊤
⊢ A ≤ largerSubobject hG A

Tactic:
exact (lt_largerSubobject hG A hA).le

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem dense_induction {p : M → Prop} (x : M) {s : Set M} (hs : closure L s = ⊤)
    (Hs : ∀ x ∈ s, p x) (Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)) : p x

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
p : M → Prop
x : M
s : Set M
hs : (closure L).toFun s = ⊤
Hs : ∀ x ∈ s, p x
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)
⊢ p x

Tactic:
have : ∀ x ∈ closure L s, p x := fun x hx => closure_induction hx Hs fun {n} => Hfun

Result:
L : Language
M : Type w
inst✝ : L.Structure M
p : M → Prop
x : M
s : Set M
hs : (closure L).toFun s = ⊤
Hs : ∀ x ∈ s, p x
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)
this : ∀ x ∈ (closure L).toFun s, p x
⊢ p x

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
p : M → Prop
x : M
s : Set M
hs : (closure L).toFun s = ⊤
Hs : ∀ x ∈ s, p x
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)
this : ∀ x ∈ (closure L).toFun s, p x
⊢ p x

Tactic:
simpa [hs] using this x

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
/-- See also `map_yonedaEquiv'` for a more general version. -/
lemma map_yonedaULiftEquiv {X Y : C} {F : Sheaf J (Type (max v v'))}
    (f : J.yonedaULift.obj X ⟶ F) (g : Y ⟶ X) :
      F.val.map g.op (J.yonedaULiftEquiv f) = f.val.app (op Y) ⟨g⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (yonedaULift.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ F.val.map g.op (J.yonedaULiftEquiv f) = f.val.app (op Y) { down := g }

Tactic:
rw [yonedaULiftEquiv_naturality, yonedaULiftEquiv_comp, yonedaULiftEquiv_yonedaULift_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem neg_intMin {w : Nat} : -intMin w = intMin w

Proof state:
case pos
w : Nat
h : 0 < w
⊢ -intMin w = intMin w

Tactic:
simp [bv_toNat, h]

Result:
no goals

Proof state:
w : Nat
⊢ -intMin w = intMin w

Tactic:
by_cases h : 0 < w

Result:
case pos
w : Nat
h : 0 < w
⊢ -intMin w = intMin w

case neg
w : Nat
h : ¬0 < w
⊢ -intMin w = intMin w

Proof state:
case neg
w : Nat
h : ¬0 < w
⊢ -intMin w = intMin w

Tactic:
simp only [Nat.not_lt, Nat.le_zero_eq] at h

Result:
case neg
w : Nat
h : w = 0
⊢ -intMin w = intMin w

Proof state:
case neg
w : Nat
h : w = 0
⊢ -intMin w = intMin w

Tactic:
simp [bv_toNat, h]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem hasSum_geom_series_inverse (x : R) (h : ‖x‖ < 1) :
    HasSum (fun i ↦ x ^ i) (Ring.inverse (1 - x))

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ HasSum (fun i => x ^ i) (Ring.inverse (1 - x))

Tactic:
convert (summable_geometric_of_norm_lt_one h).hasSum

Result:
case h.e'_6
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ Ring.inverse (1 - x) = ∑' (b : ℕ), x ^ b

Proof state:
case h.e'_6
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ Ring.inverse (1 - x) = ∑' (b : ℕ), x ^ b

Tactic:
exact (geom_series_eq_inverse x h).symm

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean
@[reassoc, to_app]
lemma mapComp_id_left_hom (f : a ⟶ b) : (F.mapComp (𝟙 a) f).hom =
    F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId a).inv ▷ F.map f

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : Pseudofunctor B C
a b : B
f : a ⟶ b
⊢ (F.mapComp (𝟙 a) f).hom = F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId a).inv ▷ F.map f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem sshiftRight_eq_sshiftRightRec (x : BitVec w₁) (y : BitVec w₂) :
    (x.sshiftRight' y).getLsbD i = (sshiftRightRec x y (w₂ - 1)).getLsbD i

Proof state:
case succ
w₁ i : Nat
x : BitVec w₁
w₂ : Nat
y : BitVec (w₂ + 1)
⊢ (x.sshiftRight' y).getLsbD i = (x.sshiftRightRec y (w₂ + 1 - 1)).getLsbD i

Tactic:
simp [sshiftRightRec_eq]

Result:
no goals

Proof state:
w₁ w₂ i : Nat
x : BitVec w₁
y : BitVec w₂
⊢ (x.sshiftRight' y).getLsbD i = (x.sshiftRightRec y (w₂ - 1)).getLsbD i

Tactic:
rcases w₂ with rfl | w₂

Result:
case zero
w₁ i : Nat
x : BitVec w₁
y : BitVec 0
⊢ (x.sshiftRight' y).getLsbD i = (x.sshiftRightRec y (0 - 1)).getLsbD i

case succ
w₁ i : Nat
x : BitVec w₁
w₂ : Nat
y : BitVec (w₂ + 1)
⊢ (x.sshiftRight' y).getLsbD i = (x.sshiftRightRec y (w₂ + 1 - 1)).getLsbD i

Proof state:
case zero
w₁ i : Nat
x : BitVec w₁
y : BitVec 0
⊢ (x.sshiftRight' y).getLsbD i = (x.sshiftRightRec y (0 - 1)).getLsbD i

Tactic:
simp [of_length_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd) (BitVec.ofNat w 1) false).snd

Proof state:
w : Nat
x : BitVec w
⊢ -x = -x + -1 + 1#w

Tactic:
simp [← sub_toAdd, BitVec.sub_add_cancel]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ -x = (iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd + 1#w

Tactic:
rw [BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), sub_toAdd, BitVec.add_comm _ (-x)]

Result:
w : Nat
x : BitVec w
⊢ -x = -x + -1 + 1#w

Proof state:
w : Nat
x : BitVec w
⊢ -x = (iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd + 1#w

Tactic:
rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd) _ rfl]

Result:
w : Nat
x : BitVec w
⊢ -x = (iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd + 1#w

w : Nat
x : BitVec w
⊢ ∀ (i : Fin w), ((), !x.getLsbD ↑i) = ((), (iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.getLsbD ↑i)

Proof state:
w : Nat
x : BitVec w
⊢ -x = ((iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.adc (1#w) false).snd

Tactic:
simp only [← add_eq_adc]

Result:
w : Nat
x : BitVec w
⊢ -x = (iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd + 1#w

Proof state:
w : Nat
x : BitVec w
⊢ ∀ (i : Fin w), ((), !x.getLsbD ↑i) = ((), (iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.getLsbD ↑i)

Tactic:
simp [bit_not_testBit x _]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
lemma kernImage_preimage_eq_iff {s : Set β} : kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s

Tactic:
rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff,
    compl_subset_comm]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
lemma isInducing (h : X ≃ₜ Y) : IsInducing h :=
  .of_comp h.continuous h.symm.continuous <| by simp only [symm_comp_self, IsInducing.id]

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IsInducing (⇑h.symm ∘ ⇑h)

Tactic:
simp only [symm_comp_self, IsInducing.id]

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem max_of_mem {s : Finset α} {a : α} (h : a ∈ s) : ∃ b : α, s.max = b

Proof state:
case intro.intro
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
a : α
h✝ : a ∈ s
b : α
h : s.sup WithBot.some = ↑b
right✝ : a ≤ b
⊢ ∃ b, s.max = ↑b

Tactic:
exact ⟨b, h⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
a : α
h : a ∈ s
⊢ ∃ b, s.max = ↑b

Tactic:
obtain ⟨b, h, _⟩ := le_sup (α := WithBot α) h _ rfl

Result:
case intro.intro
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
a : α
h✝ : a ∈ s
b : α
h : s.sup WithBot.some = ↑b
right✝ : a ≤ b
⊢ ∃ b, s.max = ↑b
-- Mathlib/NumberTheory/NumberField/House.lean
theorem exists_ne_zero_int_vec_house_le :
    ∃ (ξ : β → 𝓞 K), ξ ≠ 0 ∧ a *ᵥ ξ = 0 ∧
    ∀ l, house (ξ l).1 ≤ c₁ K * ((c₁ K * q * A) ^ ((p : ℝ) / (q - p)))

Proof state:
case h
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
⊢ 0 < p ∧ 0 < h

Tactic:
exact ⟨h0p, finrank_pos⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
⊢ ∃ ξ,
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house ↑(ξ l) ≤ NumberField.house.c₁ K * (NumberField.house.c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))

Tactic:
have hfinq : Fintype.card (β × (K →+* ℂ)) = q * h := by
  rw [Fintype.card_prod, cardβ, Embeddings.card]

Result:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
hfinq : Fintype.card (β × (K →+* ℂ)) = q * h
⊢ ∃ ξ,
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house ↑(ξ l) ≤ NumberField.house.c₁ K * (NumberField.house.c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem map_injective (f : S →+* T) (hf : Function.Injective ⇑f) :
    Function.Injective (PowerSeries.map f)

Proof state:
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑(map f)

Tactic:
intro u v huv

Result:
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
u v : S⟦X⟧
huv : (map f) u = (map f) v
⊢ u = v

Proof state:
case h.a
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
u v : S⟦X⟧
huv : (map f) u = (map f) v
k : ℕ
⊢ f ((coeff S k) u) = f ((coeff S k) v)

Tactic:
rw [← PowerSeries.coeff_map, ← PowerSeries.coeff_map, huv]

Result:
no goals

Proof state:
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
u v : S⟦X⟧
huv : (map f) u = (map f) v
⊢ u = v

Tactic:
ext k

Result:
case h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
u v : S⟦X⟧
huv : (map f) u = (map f) v
k : ℕ
⊢ (coeff S k) u = (coeff S k) v

Proof state:
case h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
u v : S⟦X⟧
huv : (map f) u = (map f) v
k : ℕ
⊢ (coeff S k) u = (coeff S k) v

Tactic:
apply hf

Result:
case h.a
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
u v : S⟦X⟧
huv : (map f) u = (map f) v
k : ℕ
⊢ f ((coeff S k) u) = f ((coeff S k) v)