harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
theorem orderOf_xa [NeZero n] (i : ZMod (2 * n)) : orderOf (xa i) = 4

Proof state:
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : ↑n = 0
⊢ False

Tactic:
apply_fun ZMod.val at h'

Result:
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : (↑n).val = ZMod.val 0
⊢ False

Proof state:
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ ¬xa i ^ 2 ^ 1 = 1

Tactic:
intro h

Result:
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h : xa i ^ 2 ^ 1 = 1
⊢ False

Proof state:
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ orderOf (xa i) = 2 ^ 2

Tactic:
apply orderOf_eq_prime_pow

Result:
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ ¬xa i ^ 2 ^ 1 = 1

case hfin
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ xa i ^ 2 ^ (1 + 1) = 1

Proof state:
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h : a ↑n = 1
⊢ False

Tactic:
injection h with h'

Result:
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : ↑n = 0
⊢ False

Proof state:
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : (↑n).val / n = ZMod.val 0 / n
⊢ False

Tactic:
simp only [ZMod.val_natCast, ZMod.val_zero, Nat.zero_div, Nat.mod_mul_left_div_self,
  Nat.div_self (NeZero.pos n), reduceCtorEq] at h'

Result:
no goals

Proof state:
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h : xa i ^ 2 ^ 1 = 1
⊢ False

Tactic:
simp only [pow_one, xa_sq] at h

Result:
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h : a ↑n = 1
⊢ False

Proof state:
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (xa i) = 4

Tactic:
change _ = 2 ^ 2

Result:
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (xa i) = 2 ^ 2

Proof state:
case hfin
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ xa i ^ 2 ^ (1 + 1) = 1

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (xa i) = 2 ^ 2

Tactic:
haveI : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two

Result:
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ orderOf (xa i) = 2 ^ 2
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_eq_iff_rpow_eq (hy : 0 < y) : logb b y = x ↔ b ^ x = y

Proof state:
case mpr
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < b ^ x
⊢ logb b (b ^ x) = x

Tactic:
exact logb_rpow b_pos b_ne_one

Result:
no goals

Proof state:
case mp
b y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
⊢ b ^ logb b y = y

Tactic:
exact rpow_logb b_pos b_ne_one hy

Result:
no goals

Proof state:
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
⊢ logb b y = x ↔ b ^ x = y

Tactic:
constructor <;> rintro rfl

Result:
case mp
b y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
⊢ b ^ logb b y = y

case mpr
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < b ^ x
⊢ logb b (b ^ x) = x
-- Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
/-- If `γ` is an integral curve of a vector field `v`, then `γ t` is tangent to `v (γ t)` when
expressed in the local chart around the initial point `γ t₀`. -/
lemma IsIntegralCurveOn.hasDerivAt (hγ : IsIntegralCurveOn γ v s) {t : ℝ} (ht : t ∈ s)
    (hsrc : γ t ∈ (extChartAt I (γ t₀)).source) :
    HasDerivAt ((extChartAt I (γ t₀)) ∘ γ)
      (tangentCoordChange I (γ t) (γ t₀) (γ t) (v (γ t))) t

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc✝ : γ t ∈ (extChartAt I (γ t₀)).source
hsrc : γ t ∈ (chartAt H (γ t₀)).source
⊢ ∀ (x : TangentSpace 𝓘(ℝ, ℝ) t),
    ((mfderiv I I (↑(chartAt H (γ t₀))) (γ t)).comp (ContinuousLinearMap.smulRight 1 (v (γ t)))) x =
      (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) x

Tactic:
intro a

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc✝ : γ t ∈ (extChartAt I (γ t₀)).source
hsrc : γ t ∈ (chartAt H (γ t₀)).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ ((mfderiv I I (↑(chartAt H (γ t₀))) (γ t)).comp (ContinuousLinearMap.smulRight 1 (v (γ t)))) a =
    (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) a
-- Mathlib/Order/Cover.lean
theorem OrderEmbedding.covBy_of_apply {α β : Type*} [Preorder α] [Preorder β]
    (f : α ↪o β) {x y : α} (h : f x ⋖ f y) : x ⋖ y

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⋖ f y
⊢ x ⋖ y

Tactic:
use f.lt_iff_lt.1 h.1

Result:
case right
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⋖ f y
⊢ ∀ ⦃c : α⦄, x < c → ¬c < y

Proof state:
case right
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⋖ f y
⊢ ∀ ⦃c : α⦄, x < c → ¬c < y

Tactic:
intro a

Result:
case right
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⋖ f y
a : α
⊢ x < a → ¬a < y

Proof state:
case right
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⋖ f y
a : α
⊢ x < a → ¬a < y

Tactic:
rw [← f.lt_iff_lt, ← f.lt_iff_lt]

Result:
case right
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⋖ f y
a : α
⊢ f x < f a → ¬f a < f y

Proof state:
case right
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
x y : α
h : f x ⋖ f y
a : α
⊢ f x < f a → ¬f a < f y

Tactic:
apply h.2

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_mul_const' (r : ℝ≥0∞) (f : α → ℝ≥0∞) (hr : r ≠ ∞) :
    ∫⁻ a, f a * r ∂μ = (∫⁻ a, f a ∂μ) * r

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ⊤
⊢ ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r

Tactic:
simp_rw [mul_comm, lintegral_const_mul' r f hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem ofNat_sub (h : m ≤ n) : ((n - m : Nat) : Int) = n - m

Proof state:
m✝ n m : Nat
h : m.succ ≤ n
⊢ ofNat (n - m.succ) = subNatNat n m.succ

Tactic:
rw [subNatNat, Nat.sub_eq_zero_of_le h]

Result:
no goals

Proof state:
m✝ n m : Nat
h : m.succ ≤ n
⊢ ↑(n - m.succ) = ↑n - ↑m.succ

Tactic:
show ofNat (n - succ m) = subNatNat n (succ m)

Result:
m✝ n m : Nat
h : m.succ ≤ n
⊢ ofNat (n - m.succ) = subNatNat n m.succ

Proof state:
m n : Nat
h : m ≤ n
⊢ ↑(n - m) = ↑n - ↑m

Tactic:
match m with
| 0 => rfl
| succ m =>
  show ofNat (n - succ m) = subNatNat n (succ m)
  rw [subNatNat, Nat.sub_eq_zero_of_le h]

Result:
no goals

Proof state:
m n : Nat
h : 0 ≤ n
⊢ ↑(n - 0) = ↑n - ↑0

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem Equiv.pointReflection_midpoint_right (x y : P) :
    (Equiv.pointReflection (midpoint R x y)) y = x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (pointReflection (midpoint R x y)) y = x

Tactic:
rw [midpoint_comm, Equiv.pointReflection_midpoint_left]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem continuousAt_coe {Y : Type*} [TopologicalSpace Y] {f : OnePoint X → Y} {x : X} :
    ContinuousAt f x ↔ ContinuousAt (f ∘ (↑)) x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ Tendsto (f ∘ some) (𝓝 x) (𝓝 (f ↑x)) ↔ Tendsto (f ∘ some) (𝓝 x) (𝓝 ((f ∘ some) x))

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ ContinuousAt f ↑x ↔ ContinuousAt (f ∘ some) x

Tactic:
rw [ContinuousAt, nhds_coe_eq, tendsto_map'_iff, ContinuousAt]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ Tendsto (f ∘ some) (𝓝 x) (𝓝 (f ↑x)) ↔ Tendsto (f ∘ some) (𝓝 x) (𝓝 ((f ∘ some) x))
-- Mathlib/AlgebraicGeometry/Modules/Tilde.lean
theorem localizationToStalk_mk (x : PrimeSpectrum.Top R) (f : M) (s : x.asIdeal.primeCompl) :
    (localizationToStalk M x).hom (LocalizedModule.mk f s) =
      (tildeInModuleCat M).germ (PrimeSpectrum.basicOpen (s : R)) x s.2
        (const M f s (PrimeSpectrum.basicOpen s) fun _ => id) :=
  (Module.End_isUnit_iff _ |>.1 (isUnit_toStalk M x s)).injective <| by
  erw [← LinearMap.mul_apply]
  simp only [IsUnit.mul_val_inv, LinearMap.one_apply, Module.algebraMap_end_apply]
  show (M.tildeInModuleCat.germ ⊤ x ⟨⟩) ((toOpen M ⊤) f) = _
  rw [← map_smul]
  fapply TopCat.Presheaf.germ_ext (W := PrimeSpectrum.basicOpen s.1) (hxW := s.2)
    (F := M.tildeInModuleCat)
  · exact homOfLE le_top
  · exact 𝟙 _
  refine Subtype.eq <| funext fun y => show LocalizedModule.mk f 1 = _ from ?_
  #adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
    added this refine hack to be able to add type hint in `change` -/
  refine (?_ : @Eq ?ty _ _)
  change LocalizedModule.mk f 1 = (s.1 • LocalizedModule.mk f _ : ?ty)
  rw [LocalizedModule.smul'_mk, LocalizedModule.mk_eq]
  exact ⟨1, by simp⟩

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ (Hom.hom (toStalk M x)) f =
    ↑s •
      (ConcreteCategory.hom (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen ↑s) x ⋯))
        (const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)

Tactic:
show (M.tildeInModuleCat.germ ⊤ x ⟨⟩) ((toOpen M ⊤) f) = _

Result:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ (ConcreteCategory.hom (M.tildeInModuleCat.germ ⊤ x True.intro)) ((ConcreteCategory.hom (toOpen M ⊤)) f) =
    ↑s •
      (ConcreteCategory.hom (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen ↑s) x ⋯))
        (const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)

Proof state:
case iWU
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ PrimeSpectrum.basicOpen ↑s ⟶ ⊤

Tactic:
exact homOfLE le_top

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem pullbackP1Iso_inv_snd (i : 𝒰.J) :
    (pullbackP1Iso 𝒰 f g i).inv ≫ pullback.snd _ _ = pullback.fst _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
⊢ (pullbackP1Iso 𝒰 f g i).inv ≫ pullback.snd (p1 𝒰 f g) (𝒰.map i) = pullback.fst (𝒰.map i ≫ f) g

Tactic:
simp_rw [pullbackP1Iso, pullback.lift_snd]

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem span_singleton_sup_orthogonal_eq_top {B : V →ₗ[K] V →ₗ[K] K} {x : V} (hx : ¬B.IsOrtho x x) :
    (K ∙ x) ⊔ Submodule.orthogonalBilin (N := K ∙ x) (B := B) = ⊤

Proof state:
K : Type u_13
V : Type u_16
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬B.IsOrtho x x
⊢ Submodule.span K {x} ⊔ (Submodule.span K {x}).orthogonalBilin B = ⊤

Tactic:
rw [orthogonal_span_singleton_eq_to_lin_ker]

Result:
K : Type u_13
V : Type u_16
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬B.IsOrtho x x
⊢ Submodule.span K {x} ⊔ ker (B x) = ⊤

Proof state:
K : Type u_13
V : Type u_16
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬B.IsOrtho x x
⊢ Submodule.span K {x} ⊔ ker (B x) = ⊤

Tactic:
exact (B x).span_singleton_sup_ker_eq_top hx

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem neg_one_mul {R} [Ring R] {a b : R} (_ : (Int.negOfNat (nat_lit 1)).rawCast * a = b) :
    -a = b

Proof state:
R : Type u_2
inst✝ : Ring R
a b : R
x✝ : (Int.negOfNat 1).rawCast * a = b
⊢ -a = b

Tactic:
subst_vars

Result:
R : Type u_2
inst✝ : Ring R
a : R
⊢ -a = (Int.negOfNat 1).rawCast * a

Proof state:
R : Type u_2
inst✝ : Ring R
a : R
⊢ -a = (Int.negOfNat 1).rawCast * a

Tactic:
simp [Int.negOfNat]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem add_comm {X Y : C} (a b : X ⟶ Y) : a + b = b + a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (-b - a) = b + a

Tactic:
rw [sub_sub_sub, add_def, ← neg_def, neg_neg b, neg_def]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ - -a - -b = b + a

Tactic:
rw [neg_def, neg_def, neg_def, sub_sub_sub]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (0 - a - b) = b + a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a - -b = b + a

Tactic:
conv_lhs => rw [← neg_neg a]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ - -a - -b = b + a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a + b = b + a

Tactic:
rw [add_def]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a - -b = b + a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (0 - a - b) = b + a

Tactic:
conv_lhs =>
  congr
  next => skip
  rw [← neg_def, neg_sub]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (-b - a) = b + a
-- Mathlib/Logic/Relation.lean
theorem Reflexive.rel_of_ne_imp (h : Reflexive r) {x y : α} (hr : x ≠ y → r x y) : r x y

Proof state:
case pos
α : Type u_1
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
hxy : x = y
⊢ r x y

Tactic:
exact hxy ▸ h x

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
⊢ r x y

Tactic:
by_cases hxy : x = y

Result:
case pos
α : Type u_1
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
hxy : x = y
⊢ r x y

case neg
α : Type u_1
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
hxy : ¬x = y
⊢ r x y

Proof state:
case neg
α : Type u_1
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
hxy : ¬x = y
⊢ r x y

Tactic:
exact hr hxy

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Free.lean
theorem finite_of_finrank_eq_succ {n : ℕ} (hn : finrank R M = n.succ) : Module.Finite R M :=
  finite_of_finrank_pos <| by rw [hn]; exact n.succ_pos

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < finrank R M

Tactic:
rw [hn]

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < n.succ

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < n.succ

Tactic:
exact n.succ_pos

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma ker_of_isAffine {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] :
    f.ker = ofIdealTop (RingHom.ker f.appTop.hom)

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
U : ↑Y.affineOpens
⊢ (ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom (Hom.app f ↑U))

Tactic:
simp only [ofIdealTop_ideal, homOfLE_leOfHom, Ideal.map_le_iff_le_comap, RingHom.comap_ker,
  ← CommRingCat.hom_comp, f.naturality]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
U : ↑Y.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)) ≤
    RingHom.ker
      (CommRingCat.Hom.hom
        (Hom.app f ⊤ ≫ X.presheaf.map ((TopologicalSpace.Opens.map f.base).map (homOfLE ⋯).op.unop).op))

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
U : ↑Y.affineOpens
x : ↑Γ(Y, ⊤)
⊢ x ∈ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)) →
    x ∈
      RingHom.ker
        (CommRingCat.Hom.hom
          (Hom.app f ⊤ ≫ X.presheaf.map ((TopologicalSpace.Opens.map f.base).map (homOfLE ⋯).op.unop).op))

Tactic:
simp +contextual

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
U : ↑Y.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)) ≤
    RingHom.ker
      (CommRingCat.Hom.hom
        (Hom.app f ⊤ ≫ X.presheaf.map ((TopologicalSpace.Opens.map f.base).map (homOfLE ⋯).op.unop).op))

Tactic:
intro x

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
U : ↑Y.affineOpens
x : ↑Γ(Y, ⊤)
⊢ x ∈ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)) →
    x ∈
      RingHom.ker
        (CommRingCat.Hom.hom
          (Hom.app f ⊤ ≫ X.presheaf.map ((TopologicalSpace.Opens.map f.base).map (homOfLE ⋯).op.unop).op))

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ Hom.ker f = ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))

Tactic:
refine (le_of_isAffine ((ideal_ofIdeals_le _ _).trans (by simp))).antisymm
  (le_ofIdeals_iff.mpr fun U ↦ ?_)

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
U : ↑Y.affineOpens
⊢ (ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom (Hom.app f ↑U))

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.app f ↑⟨⊤, ⋯⟩)) ≤
    (ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))).ideal ⟨⊤, ⋯⟩

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n

Proof state:
n k : Nat
h : n ≠ 0
⊢ 0 ≤ n.log2 ↔ 2 ^ 0 ≤ n

Tactic:
simp [show 1 ≤ n from Nat.pos_of_ne_zero h]

Result:
no goals

Proof state:
case isTrue
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
n0 : 0 < n / 2
⊢ 2 ^ k ≤ n / 2 ↔ 2 ^ k * 2 ≤ n

Tactic:
exact Nat.le_div_iff_mul_le (by decide)

Result:
no goals

Proof state:
case isFalse
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : ¬n ≥ 2
⊢ ¬2 ^ (k + 1) ≤ n

Tactic:
refine mt (Nat.le_trans ?_) ‹_›

Result:
case isFalse
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : ¬n ≥ 2
⊢ 2 ≤ 2 ^ (k + 1)

Proof state:
case isTrue
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
n0 : 0 < n / 2
⊢ k + 1 ≤ (n / 2).log2 + 1 ↔ 2 ^ (k + 1) ≤ n

Tactic:
simp only [Nat.add_le_add_iff_right, le_log2 (Nat.ne_of_gt n0), le_div_iff_mul_le,
  Nat.pow_succ]

Result:
case isTrue
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
n0 : 0 < n / 2
⊢ 2 ^ k ≤ n / 2 ↔ 2 ^ k * 2 ≤ n

Proof state:
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
case isFalse
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : ¬n ≥ 2
⊢ k + 1 ≤ 0 ↔ 2 ^ (k + 1) ≤ n

Tactic:
simp only [le_zero_eq, succ_ne_zero, false_iff]

Result:
case isFalse
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : ¬n ≥ 2
⊢ ¬2 ^ (k + 1) ≤ n

Proof state:
n k✝ : Nat
h : n ≠ 0
k : Nat
⊢ k + 1 ≤ n.log2 ↔ 2 ^ (k + 1) ≤ n

Tactic:
rw [log2]

Result:
n k✝ : Nat
h : n ≠ 0
k : Nat
⊢ (k + 1 ≤ if n ≥ 2 then (n / 2).log2 + 1 else 0) ↔ 2 ^ (k + 1) ≤ n

Proof state:
n k✝ : Nat
h : n ≠ 0
k : Nat
⊢ (k + 1 ≤ if n ≥ 2 then (n / 2).log2 + 1 else 0) ↔ 2 ^ (k + 1) ≤ n

Tactic:
split

Result:
case isTrue
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
⊢ k + 1 ≤ (n / 2).log2 + 1 ↔ 2 ^ (k + 1) ≤ n

case isFalse
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : ¬n ≥ 2
⊢ k + 1 ≤ 0 ↔ 2 ^ (k + 1) ≤ n

Proof state:
case isFalse
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : ¬n ≥ 2
⊢ 2 ≤ 2 ^ (k + 1)

Tactic:
exact Nat.pow_le_pow_of_le_right Nat.zero_lt_two (Nat.le_add_left 1 k)

Result:
no goals

Proof state:
case isTrue
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
⊢ k + 1 ≤ (n / 2).log2 + 1 ↔ 2 ^ (k + 1) ≤ n

Tactic:
have n0 : 0 < n / 2 := (Nat.le_div_iff_mul_le (by decide)).2 ‹_›

Result:
case isTrue
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
n0 : 0 < n / 2
⊢ k + 1 ≤ (n / 2).log2 + 1 ↔ 2 ^ (k + 1) ≤ n

Proof state:
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
n0 : 0 < n / 2
⊢ 0 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem count_finset_sup [DecidableEq β] (s : Finset α) (f : α → Multiset β) (b : β) :
    count b (s.sup f) = s.sup fun a => count b (f a)

Proof state:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
⊢ count b (s.sup f) = s.sup fun a => count b (f a)

Tactic:
letI := Classical.decEq α

Result:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (s.sup f) = s.sup fun a => count b (f a)

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (∅.sup f) = ∅.sup fun a => count b (f a)

Tactic:
exact count_zero _

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (s.sup f) = s.sup fun a => count b (f a)

Tactic:
refine s.induction ?_ ?_

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (∅.sup f) = ∅.sup fun a => count b (f a)

case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    a ∉ s →
      (count b (s.sup f) = s.sup fun a => count b (f a)) →
        count b ((insert a s).sup f) = (insert a s).sup fun a => count b (f a)

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    a ∉ s →
      (count b (s.sup f) = s.sup fun a => count b (f a)) →
        count b ((insert a s).sup f) = (insert a s).sup fun a => count b (f a)

Tactic:
intro i s _ ih

Result:
case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : i ∉ s
ih : count b (s.sup f) = s.sup fun a => count b (f a)
⊢ count b ((insert i s).sup f) = (insert i s).sup fun a => count b (f a)

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : i ∉ s
ih : count b (s.sup f) = s.sup fun a => count b (f a)
⊢ count b ((insert i s).sup f) = (insert i s).sup fun a => count b (f a)

Tactic:
rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih]

Result:
no goals