harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem generate_le_iff (R : Presieve X) (S : Sieve X) : generate R ≤ S ↔ R ≤ S :=
  ⟨fun H _ _ hg => H _ ⟨_, 𝟙 _, _, hg, id_comp _⟩, fun ss Y f => by
    rintro ⟨Z, f, g, hg, rfl⟩
    exact S.downward_closed (ss Z hg) f⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Presieve X
S : Sieve X
ss : R ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ (generate R).arrows f → S.arrows f

Tactic:
rintro ⟨Z, f, g, hg, rfl⟩

Result:
case intro.intro.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Presieve X
S : Sieve X
ss : R ≤ S.arrows
Y Z : C
f : Y ⟶ Z
g : Z ⟶ X
hg : R g
⊢ S.arrows (f ≫ g)

Proof state:
case intro.intro.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Presieve X
S : Sieve X
ss : R ≤ S.arrows
Y Z : C
f : Y ⟶ Z
g : Z ⟶ X
hg : R g
⊢ S.arrows (f ≫ g)

Tactic:
exact S.downward_closed (ss Z hg) f

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem abs_exp_sub_one_sub_id_le {x : ℝ} (hx : |x| ≤ 1) : |exp x - 1 - x| ≤ x ^ 2

Proof state:
x : ℝ
hx : |x| ≤ 1
this : ‖↑x‖ ≤ 1
⊢ |rexp x - 1 - x| ≤ |x| ^ 2

Tactic:
exact_mod_cast Complex.norm_exp_sub_one_sub_id_le this

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1 - x| ≤ |x| ^ 2

Tactic:
have : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx

Result:
x : ℝ
hx : |x| ≤ 1
this : ‖↑x‖ ≤ 1
⊢ |rexp x - 1 - x| ≤ |x| ^ 2

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1 - x| ≤ x ^ 2

Tactic:
rw [← sq_abs]

Result:
x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1 - x| ≤ |x| ^ 2
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma PosSMulMono.lift [PosSMulMono α γ]
    (hf : ∀ {b₁ b₂}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂)
    (smul : ∀ (a : α) b, f (a • b) = a • f b) : PosSMulMono α β where
  elim a ha b₁ b₂ hb

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulMono α γ
a : α
ha : 0 ≤ a
b₁ b₂ : β
hf : ∀ {b₁ b₂ : β}, True
smul : α → β → True
hb : f b₁ ≤ f b₂
⊢ a • f b₁ ≤ a • f b₂

Tactic:
exact smul_le_smul_of_nonneg_left hb ha

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 ≤ a
b₁ b₂ : β
hb : b₁ ≤ b₂
⊢ a • b₁ ≤ a • b₂

Tactic:
simp only [← hf, smul] at *

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulMono α γ
a : α
ha : 0 ≤ a
b₁ b₂ : β
hf : ∀ {b₁ b₂ : β}, True
smul : α → β → True
hb : f b₁ ≤ f b₂
⊢ a • f b₁ ≤ a • f b₂
-- Mathlib/Data/Matroid/Map.lean
lemma eq_of_restrictSubtype_eq {N : Matroid α} (hM : M.E = E) (hN : N.E = E)
    (h : M.restrictSubtype E = N.restrictSubtype E) : M = N

Proof state:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
⊢ M = N

Tactic:
refine ext_indep (by rw [hN]) (fun I hI ↦ ?_)

Result:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ N.Indep I

Proof state:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ N.Indep I

Tactic:
rwa [← restrictSubtype_indep_iff_of_subset hI, h, restrictSubtype_indep_iff_of_subset]

Result:
no goals

Proof state:
α : Type u_1
E : Set α
M N : Matroid α
hM : M.E = E
hN : N.E = E
h : M.restrictSubtype E = N.restrictSubtype E
⊢ M = N

Tactic:
subst hM

Result:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
⊢ M = N

Proof state:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
⊢ M.E = N.E

Tactic:
rw [hN]

Result:
no goals
-- Mathlib/GroupTheory/CommutingProbability.lean
lemma commProb_odd {n : ℕ} (hn : Odd n) :
    commProb (DihedralGroup n) = (n + 3) / (4 * n)

Proof state:
n : ℕ
hn : Odd n
⊢ ↑((n + 3) / 2) / ↑(2 * n) = (↑n + 3) / (4 * ↑n)

Tactic:
qify [show 2 ∣ n + 3 by rw [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.odd_iff.mp hn]]

Result:
n : ℕ
hn : Odd n
⊢ (↑n + 3) / 2 / (2 * ↑n) = (↑n + 3) / (4 * ↑n)

Proof state:
case e_a.e_a
n : ℕ
hn : Odd n
⊢ 2 * 2 = 4

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
hn : Odd n
⊢ 2 ∣ n + 3

Tactic:
rw [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.odd_iff.mp hn]

Result:
no goals

Proof state:
n : ℕ
hn : Odd n
⊢ (↑n + 3) / 2 / (2 * ↑n) = (↑n + 3) / (4 * ↑n)

Tactic:
rw [div_div, ← mul_assoc]

Result:
n : ℕ
hn : Odd n
⊢ (↑n + 3) / (2 * 2 * ↑n) = (↑n + 3) / (4 * ↑n)

Proof state:
n : ℕ
hn : Odd n
⊢ commProb (DihedralGroup n) = (↑n + 3) / (4 * ↑n)

Tactic:
rw [commProb_def', DihedralGroup.card_conjClasses_odd hn, nat_card]

Result:
n : ℕ
hn : Odd n
⊢ ↑((n + 3) / 2) / ↑(2 * n) = (↑n + 3) / (4 * ↑n)

Proof state:
n : ℕ
hn : Odd n
⊢ (↑n + 3) / (2 * 2 * ↑n) = (↑n + 3) / (4 * ↑n)

Tactic:
congr

Result:
case e_a.e_a
n : ℕ
hn : Odd n
⊢ 2 * 2 = 4
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
lemma deriv_LFunctionTrivChar₁_apply_of_ne_one {s : ℂ} (hs : s ≠ 1) :
    deriv (LFunctionTrivChar₁ n) s =
      (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s

Proof state:
n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
H : deriv (LFunctionTrivChar₁ n) s = deriv (fun w => (w - 1) * LFunctionTrivChar n w) s
⊢ DifferentiableAt ℂ (fun w => w - 1) s

Tactic:
fun_prop

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
H : deriv (LFunctionTrivChar₁ n) s = deriv (fun w => (w - 1) * LFunctionTrivChar n w) s
⊢ deriv (LFunctionTrivChar₁ n) s = (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s

Tactic:
rw [H, deriv_mul (by fun_prop) (differentiableAt_LFunction _ s (.inl hs)), deriv_sub_const,
  deriv_id'', one_mul, add_comm]

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
⊢ deriv (LFunctionTrivChar₁ n) s = deriv (fun w => (w - 1) * LFunctionTrivChar n w) s

Tactic:
refine eventuallyEq_iff_exists_mem.mpr ?_ |>.deriv_eq

Result:
n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
⊢ ∃ s_1 ∈ 𝓝 s, Set.EqOn (LFunctionTrivChar₁ n) (fun w => (w - 1) * LFunctionTrivChar n w) s_1

Proof state:
n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
⊢ ∃ s_1 ∈ 𝓝 s, Set.EqOn (LFunctionTrivChar₁ n) (fun w => (w - 1) * LFunctionTrivChar n w) s_1

Tactic:
exact ⟨_, isOpen_ne.mem_nhds hs, fun _ hw ↦ Function.update_of_ne (Set.mem_setOf.mp hw) ..⟩

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
⊢ deriv (LFunctionTrivChar₁ n) s = (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s

Tactic:
have H : deriv (LFunctionTrivChar₁ n) s =
    deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s := by
  refine eventuallyEq_iff_exists_mem.mpr ?_ |>.deriv_eq
  exact ⟨_, isOpen_ne.mem_nhds hs, fun _ hw ↦ Function.update_of_ne (Set.mem_setOf.mp hw) ..⟩

Result:
n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
H : deriv (LFunctionTrivChar₁ n) s = deriv (fun w => (w - 1) * LFunctionTrivChar n w) s
⊢ deriv (LFunctionTrivChar₁ n) s = (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s
-- Mathlib/Algebra/QuaternionBasis.lean
theorem lift_smul (r : R) (x : ℍ[R,c₁,c₂,c₃]) : q.lift (r • x) = r • q.lift x

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ q.lift (r • x) = r • q.lift x

Tactic:
simp [lift, mul_smul, ← Algebra.smul_def]

Result:
no goals
-- Mathlib/Algebra/Module/SpanRank.lean
lemma spanFinrank_span_le_ncard_of_finite {s : Set M} (hs : s.Finite) :
    (span R s).spanFinrank ≤ s.ncard

Proof state:
case h.e'_3
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ ↑(toNat (span R s).spanRank) = (span R s).spanRank

Tactic:
refine Cardinal.cast_toNat_of_lt_aleph0 (lt_of_le_of_lt (spanRank_span_le_card s) ?_)

Result:
case h.e'_3
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ #↑s < ℵ₀

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ (span R s).spanFinrank ≤ s.ncard

Tactic:
rw [← Nat.cast_le (α := Cardinal)]

Result:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ ↑(span R s).spanFinrank ≤ ↑s.ncard

Proof state:
case h.e'_3
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ #↑s < ℵ₀

Tactic:
simpa

Result:
no goals

Proof state:
case h.e'_4
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ ↑s.ncard = #↑s

Tactic:
exact Set.cast_ncard hs

Result:
no goals

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ ↑(span R s).spanFinrank ≤ ↑s.ncard

Tactic:
convert spanRank_span_le_card (R := R) s

Result:
case h.e'_3
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ ↑(span R s).spanFinrank = (span R s).spanRank

case h.e'_4
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ ↑s.ncard = #↑s

Proof state:
case h.e'_3
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ ↑(span R s).spanFinrank = (span R s).spanRank

Tactic:
rw [spanFinrank]

Result:
case h.e'_3
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ ↑(toNat (span R s).spanRank) = (span R s).spanRank
-- Mathlib/CategoryTheory/Simple.lean
theorem epi_from_simple_zero_of_not_iso {X Y : C} [Simple X] {f : X ⟶ Y} [Epi f]
    (w : IsIso f → False) : f = 0

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : Epi f
w : IsIso f → False
⊢ f = 0

Tactic:
classical
  by_contra h
  exact w (isIso_of_epi_of_nonzero h)

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : Epi f
w : IsIso f → False
⊢ f = 0

Tactic:
by_contra h

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : Epi f
w : IsIso f → False
h : ¬f = 0
⊢ False

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : Epi f
w : IsIso f → False
h : ¬f = 0
⊢ False

Tactic:
exact w (isIso_of_epi_of_nonzero h)

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem lt_length_iff {s : Seq α} {n : ℕ} {h : s.Terminates} :
    n < s.length h ↔ ∃ a, a ∈ s.get? n

Proof state:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ n < s.length h ↔ ∃ a, a ∈ s.get? n

Tactic:
rw [← lt_length_iff']

Result:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ n < s.length h ↔ ∀ (h : s.Terminates), n < s.length h

Proof state:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ n < s.length h ↔ ∀ (h : s.Terminates), n < s.length h

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem supDegree_withBot_some_comp {s : AddMonoidAlgebra R A} (hs : s.support.Nonempty) :
    supDegree (WithBot.some ∘ D) s = supDegree D s

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
s : R[A]
hs : s.support.Nonempty
⊢ s.support.sup (WithBot.some ∘ D) = ↑(s.support.sup D)

Tactic:
rw [← Finset.coe_sup' hs, Finset.sup'_eq_sup]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
s : R[A]
hs : s.support.Nonempty
⊢ supDegree (WithBot.some ∘ D) s = ↑(supDegree D s)

Tactic:
unfold AddMonoidAlgebra.supDegree

Result:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
s : R[A]
hs : s.support.Nonempty
⊢ s.support.sup (WithBot.some ∘ D) = ↑(s.support.sup D)
-- Mathlib/CategoryTheory/Shift/SingleFunctors.lean
@[simp]
lemma shiftIso_zero_hom_app (a : A) (X : C) :
    (F.shiftIso 0 a a (zero_add a)).hom.app X = (shiftFunctorZero D A).hom.app _

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
a : A
X : C
⊢ (F.shiftIso 0 a a ⋯).hom.app X = (shiftFunctorZero D A).hom.app ((F.functor a).obj X)

Tactic:
rw [shiftIso_zero]

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
a : A
X : C
⊢ (isoWhiskerLeft (F.functor a) (shiftFunctorZero D A)).hom.app X = (shiftFunctorZero D A).hom.app ((F.functor a).obj X)

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
a : A
X : C
⊢ (isoWhiskerLeft (F.functor a) (shiftFunctorZero D A)).hom.app X = (shiftFunctorZero D A).hom.app ((F.functor a).obj X)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem IsClosed.intrinsicClosure (hs : IsClosed ((↑) ⁻¹' s : Set <| affineSpan 𝕜 s)) :
    intrinsicClosure 𝕜 s = s

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
hs : IsClosed (Subtype.val ⁻¹' s)
⊢ s ⊆ range Subtype.val

Tactic:
exact (subset_affineSpan _ _).trans Subtype.range_coe.superset

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
hs : IsClosed (Subtype.val ⁻¹' s)
⊢ intrinsicClosure 𝕜 s = s

Tactic:
rw [intrinsicClosure, hs.closure_eq, image_preimage_eq_of_subset]

Result:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
hs : IsClosed (Subtype.val ⁻¹' s)
⊢ s ⊆ range Subtype.val
-- Mathlib/LinearAlgebra/Projectivization/Cardinality.lean
lemma card_of_finrank_two [Finite k] (h : Module.finrank k V = 2) :
    Nat.card (ℙ k V) = Nat.card k + 1

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Module.finrank k V = 2
⊢ Nat.card (ℙ k V) = Nat.card k + 1

Tactic:
simp [card_of_finrank k V h]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_le_pow_iff_norm_lt_pow_add_one (x : ℚ_[p]) (n : ℤ) :
    ‖x‖ ≤ (p : ℝ) ^ n ↔ ‖x‖ < (p : ℝ) ^ (n + 1)

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Tactic:
simp [hx0, norm_zero, aux, le_of_lt (aux _)]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Tactic:
by_cases hx0 : x = 0

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ↑p ^ (-x.valuation) ≤ ↑p ^ n ↔ ↑p ^ (-x.valuation) < ↑p ^ (n + 1)

Tactic:
have h1p : 1 < (p : ℝ) := mod_cast hp.1.one_lt

Result:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
h1p : 1 < ↑p
⊢ ↑p ^ (-x.valuation) ≤ ↑p ^ n ↔ ↑p ^ (-x.valuation) < ↑p ^ (n + 1)

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
h1p : 1 < ↑p
H : StrictMono fun n => ↑p ^ n
⊢ ↑p ^ (-x.valuation) ≤ ↑p ^ n ↔ ↑p ^ (-x.valuation) < ↑p ^ (n + 1)

Tactic:
rw [H.le_iff_le, H.lt_iff_lt, Int.lt_add_one_iff]

Result:
no goals

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Tactic:
rw [norm_eq_zpow_neg_valuation hx0]

Result:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ↑p ^ (-x.valuation) ≤ ↑p ^ n ↔ ↑p ^ (-x.valuation) < ↑p ^ (n + 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Tactic:
have aux (n : ℤ) : 0 < ((p : ℝ) ^ n) := zpow_pos (mod_cast hp.1.pos) _

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
h1p : 1 < ↑p
⊢ ↑p ^ (-x.valuation) ≤ ↑p ^ n ↔ ↑p ^ (-x.valuation) < ↑p ^ (n + 1)

Tactic:
have H := zpow_right_strictMono₀ h1p

Result:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
h1p : 1 < ↑p
H : StrictMono fun n => ↑p ^ n
⊢ ↑p ^ (-x.valuation) ≤ ↑p ^ n ↔ ↑p ^ (-x.valuation) < ↑p ^ (n + 1)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma twoTorsionPolynomial_disc_isUnit (hu : IsUnit (2 : R)) :
    IsUnit W.twoTorsionPolynomial.disc ↔ IsUnit W.Δ

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
hu : IsUnit 2
⊢ IsUnit W.twoTorsionPolynomial.disc ↔ IsUnit W.Δ

Tactic:
rw [twoTorsionPolynomial_disc, IsUnit.mul_iff, show (16 : R) = 2 ^ 4 by norm_num1]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
hu : IsUnit 2
⊢ IsUnit (2 ^ 4) ∧ IsUnit W.Δ ↔ IsUnit W.Δ

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
hu : IsUnit 2
⊢ 16 = 2 ^ 4

Tactic:
norm_num1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
hu : IsUnit 2
⊢ IsUnit (2 ^ 4) ∧ IsUnit W.Δ ↔ IsUnit W.Δ

Tactic:
exact and_iff_right <| hu.pow 4

Result:
no goals
-- Mathlib/CategoryTheory/Sites/SheafHom.lean
@[simp]
lemma presheafHom_map_app_op_mk_id {X Y : C} (g : Y ⟶ X)
    (α : (presheafHom F G).obj (op X)) :
    ((presheafHom F G).map g.op α).app (op (Over.mk (𝟙 Y))) =
      α.app (op (Over.mk g)) :=
  presheafHom_map_app (𝟙 Y) g g (by simp) α

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X Y : C
g : Y ⟶ X
α : (presheafHom F G).obj (op X)
⊢ 𝟙 Y ≫ g = g

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.exists_maximal_wrt' [PartialOrder β] (f : α → β) (s : Set α) (h : (f '' s).Finite)
    (hs : s.Nonempty) : (∃ a ∈ s, ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a')

Proof state:
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s : Set α
h : (f '' s).Finite
hs : s.Nonempty
⊢ ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'

Tactic:
obtain ⟨_, ⟨a, ha, rfl⟩, hmax⟩ := Finite.exists_maximal_wrt id (f '' s) h (hs.image f)

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s : Set α
h : (f '' s).Finite
hs : s.Nonempty
a : α
ha : a ∈ s
hmax : ∀ a' ∈ f '' s, id (f a) ≤ id a' → id (f a) = id a'
⊢ ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s : Set α
h : (f '' s).Finite
hs : s.Nonempty
a : α
ha : a ∈ s
hmax : ∀ a' ∈ f '' s, id (f a) ≤ id a' → id (f a) = id a'
⊢ ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'

Tactic:
exact ⟨a, ha, fun a' ha' hf ↦ hmax _ (mem_image_of_mem f ha') hf⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.right_of_add_measure {f : α → β} (h : Integrable f (μ + ν)) :
    Integrable f ν

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : MemLp f 1 (μ + ν)
⊢ MemLp f 1 ν

Tactic:
exact h.right_of_add_measure

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f (μ + ν)
⊢ Integrable f ν

Tactic:
rw [← memLp_one_iff_integrable] at h ⊢

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : MemLp f 1 (μ + ν)
⊢ MemLp f 1 ν
-- Mathlib/Topology/Basic.lean
theorem isClosed_imp {p q : X → Prop} (hp : IsOpen { x | p x }) (hq : IsClosed { x | q x }) :
    IsClosed { x | p x → q x }

Proof state:
X : Type u
inst✝ : TopologicalSpace X
p q : X → Prop
hp : IsOpen {x | p x}
hq : IsClosed {x | q x}
⊢ IsClosed {x | p x → q x}

Tactic:
simpa only [imp_iff_not_or] using hp.isClosed_compl.union hq

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem iSupIndep.subtype_ne_bot_le_finrank
    {p : ι → Submodule R M} (hp : iSupIndep p) [Fintype { i // p i ≠ ⊥ }] :
    Fintype.card { i // p i ≠ ⊥ } ≤ finrank R M

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
inst✝² : Module.Finite R M
inst✝¹ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
inst✝ : Fintype { i // p i ≠ ⊥ }
⊢ Fintype.card { i // p i ≠ ⊥ } ≤ finrank R M

Tactic:
simpa using hp.subtype_ne_bot_le_finrank_aux

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem agree'_refl {n : ℕ} (x : M F) : Agree' n x x

Proof state:
case succ.f.a
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
i✝ : F.B a✝
⊢ Agree' n✝ (f✝ i✝) (f✝ i✝)

Tactic:
apply n_ih

Result:
no goals

Proof state:
case succ.f.a
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨a✝, ?succ.f.y⟩

Tactic:
rfl

Result:
no goals

Proof state:
F : PFunctor.{u}
n : ℕ
x : F.M
⊢ Agree' n x x

Tactic:
induction' n with _ n_ih generalizing x <;>
induction x using PFunctor.M.casesOn' <;> constructor <;> try rfl

Result:
case succ.f.a
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ ∀ (i : F.B a✝), Agree' n✝ (f✝ i) (f✝ i)

Proof state:
case succ.f.a
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ ∀ (i : F.B a✝), Agree' n✝ (f✝ i) (f✝ i)

Tactic:
intros

Result:
case succ.f.a
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
i✝ : F.B a✝
⊢ Agree' n✝ (f✝ i✝) (f✝ i✝)
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma div_mul_left (h : IsUnit b) : b / (a * b) = 1 / a

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a b : α
h : IsUnit b
⊢ b / (a * b) = 1 / a

Tactic:
rw [h.div_mul_cancel_right, one_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b

Proof state:
case nil
α : Type u_1
b : List α
h : #[] = b.toArray
⊢ [] = b

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
a b : List α
h : a.toArray = b.toArray
⊢ a = b

Tactic:
cases a with
| nil => simpa using h
| cons a as =>
  cases b with
  | nil => simp at h
  | cons b bs => simpa using h

Result:
no goals

Proof state:
case cons
α : Type u_1
b : List α
a : α
as : List α
h : (a :: as).toArray = b.toArray
⊢ a :: as = b

Tactic:
cases b with
| nil => simp at h
| cons b bs => simpa using h

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
a : α
as : List α
h : (a :: as).toArray = #[]
⊢ a :: as = []

Tactic:
simp at h

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
a : α
as : List α
b : α
bs : List α
h : (a :: as).toArray = (b :: bs).toArray
⊢ a :: as = b :: bs

Tactic:
simpa using h

Result:
no goals
-- Mathlib/CategoryTheory/Category/Cat.lean
lemma rightUnitor_inv_app {B C : Cat} (F : B ⟶ C) (X : B) : (ρ_ F).inv.app X = eqToHom (by simp) :=
  rfl

Proof state:
B C : Cat
F : B ⟶ C
X : ↑B
⊢ F.obj X = (F ≫ 𝟙 C).obj X

Tactic:
simp

Result:
no goals