harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean
theorem counit_tensorObj_tensorObj_left :
    Coalgebra.counit (R := R)
      (A := ((CoalgebraCat.of R M ⊗ CoalgebraCat.of R N) ⊗ CoalgebraCat.of R P : CoalgebraCat R))
      = Coalgebra.counit (A := (M ⊗[R] N) ⊗[R] P)

Proof state:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ CoalgebraStruct.counit = CoalgebraStruct.counit

Tactic:
ext

Result:
case h
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
x✝ : ↑((of R M ⊗ of R N) ⊗ of R P).toModuleCat
⊢ CoalgebraStruct.counit x✝ = CoalgebraStruct.counit x✝

Proof state:
case h
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
x✝ : ↑((of R M ⊗ of R N) ⊗ of R P).toModuleCat
⊢ CoalgebraStruct.counit x✝ = CoalgebraStruct.counit x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivWithinAt.mul_const (hc : HasDerivWithinAt c c' s x) (d : 𝔸) :
    HasDerivWithinAt (fun y => c y * d) (c' * d) s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' s x
d : 𝔸
⊢ HasDerivWithinAt (fun y => c y * d) (c' * d) s x

Tactic:
convert hc.mul (hasDerivWithinAt_const x s d) using 1

Result:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' s x
d : 𝔸
⊢ c' * d = c' * d + c x * 0

Proof state:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' s x
d : 𝔸
⊢ c' * d = c' * d + c x * 0

Tactic:
rw [mul_zero, add_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean
theorem intervalIntegrable_sub_inv_iff {a b c : ℝ} :
    IntervalIntegrable (fun x => (x - c)⁻¹) volume a b ↔ a = b ∨ c ∉ [[a, b]]

Proof state:
case mpr.inr
a b c : ℝ
h₀ : c ∉ [[a, b]]
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a b

Tactic:
refine ((continuous_sub_right c).continuousOn.inv₀ ?_).intervalIntegrable

Result:
case mpr.inr
a b c : ℝ
h₀ : c ∉ [[a, b]]
⊢ ∀ x ∈ [[a, b]], x - c ≠ 0

Proof state:
case mpr.inr
a b c : ℝ
h₀ : c ∉ [[a, b]]
⊢ ∀ x ∈ [[a, b]], x - c ≠ 0

Tactic:
exact fun x hx => sub_ne_zero.2 <| ne_of_mem_of_not_mem hx h₀

Result:
no goals

Proof state:
case mpr.inl
a c : ℝ
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a a

Tactic:
exact IntervalIntegrable.refl

Result:
no goals

Proof state:
a b c : ℝ
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a b ↔ a = b ∨ c ∉ [[a, b]]

Tactic:
constructor

Result:
case mp
a b c : ℝ
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a b → a = b ∨ c ∉ [[a, b]]

case mpr
a b c : ℝ
⊢ a = b ∨ c ∉ [[a, b]] → IntervalIntegrable (fun x => (x - c)⁻¹) volume a b

Proof state:
case mp
a b c : ℝ
h : IntervalIntegrable (fun x => (x - c)⁻¹) volume a b
hne : ¬a = b
hc : c ∈ [[a, b]]
⊢ False

Tactic:
exact not_intervalIntegrable_of_sub_inv_isBigO_punctured (isBigO_refl _ _) hne hc h

Result:
no goals

Proof state:
case mpr
a b c : ℝ
⊢ a = b ∨ c ∉ [[a, b]] → IntervalIntegrable (fun x => (x - c)⁻¹) volume a b

Tactic:
rintro (rfl | h₀)

Result:
case mpr.inl
a c : ℝ
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a a

case mpr.inr
a b c : ℝ
h₀ : c ∉ [[a, b]]
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a b

Proof state:
case mp
a b c : ℝ
⊢ IntervalIntegrable (fun x => (x - c)⁻¹) volume a b → a = b ∨ c ∉ [[a, b]]

Tactic:
refine fun h => or_iff_not_imp_left.2 fun hne hc => ?_

Result:
case mp
a b c : ℝ
h : IntervalIntegrable (fun x => (x - c)⁻¹) volume a b
hne : ¬a = b
hc : c ∈ [[a, b]]
⊢ False
-- Mathlib/Algebra/MvPolynomial/Comap.lean
theorem comap_eq_id_of_eq_id (f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (hf : ∀ φ, f φ = φ)
    (x : σ → R) : comap f x = x

Proof state:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), f φ = φ
x : σ → R
⊢ comap f x = x

Tactic:
convert comap_id_apply x

Result:
case h.e'_2.h.e'_5
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), f φ = φ
x : σ → R
⊢ f = AlgHom.id R (MvPolynomial σ R)

Proof state:
case h.e'_2.h.e'_5.hf
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), f φ = φ
x : σ → R
φ : σ
⊢ f (X φ) = (AlgHom.id R (MvPolynomial σ R)) (X φ)

Tactic:
simp [hf, AlgHom.id_apply]

Result:
no goals

Proof state:
case h.e'_2.h.e'_5
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), f φ = φ
x : σ → R
⊢ f = AlgHom.id R (MvPolynomial σ R)

Tactic:
ext1 φ

Result:
case h.e'_2.h.e'_5.hf
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), f φ = φ
x : σ → R
φ : σ
⊢ f (X φ) = (AlgHom.id R (MvPolynomial σ R)) (X φ)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma add_some {x₁ x₂ y₁ y₂ : F} (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) {h₁ : W.Nonsingular x₁ y₁}
    {h₂ : W.Nonsingular x₂ y₂} : some h₁ + some h₂ = some (nonsingular_add h₁ h₂ hxy)

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
⊢ some h₁ + some h₂ = some ⋯

Tactic:
simp only [add_def, add, dif_neg hxy]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem not_linearIndependent_iff :
    ¬LinearIndependent R v ↔
      ∃ s : Finset ι, ∃ g : ι → R, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ¬LinearIndependent R v ↔ ∃ s g, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0

Tactic:
rw [linearIndependent_iff']

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (¬∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0) ↔
    ∃ s g, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (¬∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0) ↔
    ∃ s g, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0

Tactic:
simp only [exists_prop, not_forall]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkAtomCached_hit_aig (aig : AIG α) {hit} (hcache : aig.cache.get? (.atom var) = some hit) :
    (aig.mkAtomCached var).aig = aig

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hit : CacheHit aig.decls (Decl.atom var)
hcache : aig.cache.get? (Decl.atom var) = some hit
⊢ (aig.mkAtomCached var).aig = aig

Tactic:
simp only [mkAtomCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hit : CacheHit aig.decls (Decl.atom var)
hcache : aig.cache.get? (Decl.atom var) = some hit
⊢ (match aig.cache.get? (Decl.atom var) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
              invariant := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } }).aig =
    aig

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
aig : AIG α
hit : CacheHit aig.decls (Decl.atom var)
hcache : aig.cache.get? (Decl.atom var) = some hit
⊢ (match aig.cache.get? (Decl.atom var) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.atom var), cache := Cache.insert aig.decls aig.cache (Decl.atom var),
              invariant := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } }).aig =
    aig

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem length_add_eq_lengthTRAux (as : List α) (n : Nat) : as.length + n = as.lengthTRAux n

Proof state:
case cons
α : Type u
a : α
as : List α
ih : ∀ (n : Nat), as.length + n = as.lengthTRAux n
n : Nat
⊢ (a :: as).length + n = (a :: as).lengthTRAux n

Tactic:
simp [length, lengthTRAux, ← ih, Nat.succ_add]

Result:
case cons
α : Type u
a : α
as : List α
ih : ∀ (n : Nat), as.length + n = as.lengthTRAux n
n : Nat
⊢ as.length + n + 1 = as.length + (n + 1)

Proof state:
case cons
α : Type u
a : α
as : List α
ih : ∀ (n : Nat), as.length + n = as.lengthTRAux n
n : Nat
⊢ as.length + n + 1 = as.length + (n + 1)

Tactic:
rfl

Result:
no goals

Proof state:
case nil
α : Type u
n : Nat
⊢ nil.length + n = nil.lengthTRAux n

Tactic:
simp [length, lengthTRAux]

Result:
no goals

Proof state:
α : Type u
as : List α
n : Nat
⊢ as.length + n = as.lengthTRAux n

Tactic:
induction as generalizing n with
| nil  => simp [length, lengthTRAux]
| cons a as ih =>
  simp [length, lengthTRAux, ← ih, Nat.succ_add]
  rfl

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Closed.lean
theorem topologyOfClosureOperator_self :
    (topologyOfClosureOperator J₁.closureOperator fun _ _ => J₁.pullback_close) = J₁

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
⊢ topologyOfClosureOperator J₁.closureOperator ⋯ = J₁

Tactic:
ext X S

Result:
case h.h.h
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ (topologyOfClosureOperator J₁.closureOperator ⋯) X ↔ S ∈ J₁ X

Proof state:
case h.h.h
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ (topologyOfClosureOperator J₁.closureOperator ⋯) X ↔ S ∈ J₁ X

Tactic:
apply GrothendieckTopology.close_eq_top_iff_mem

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem eq_of_chain {c : Chain (Part α)} {a b : α} (ha : some a ∈ c) (hb : some b ∈ c) : a = b

Proof state:
case intro.intro.inr
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
⊢ a = b

Tactic:
have := c.monotone hji _ hb

Result:
case intro.intro.inr
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
this : b ∈ c i
⊢ a = b

Proof state:
case intro.intro.inr
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
this : b ∈ c i
⊢ a = b

Tactic:
apply Eq.symm

Result:
case intro.intro.inr.h
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
this : b ∈ c i
⊢ b = a

Proof state:
α : Type u_2
c : Chain (Part α)
a b : α
ha : some a ∈ c
hb : some b ∈ c
⊢ a = b

Tactic:
obtain ⟨i, ha⟩ := ha

Result:
case intro
α : Type u_2
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : some a = c i
⊢ a = b

Proof state:
case intro
α : Type u_2
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : c i = some a
⊢ a = b

Tactic:
obtain ⟨j, hb⟩ := hb

Result:
case intro.intro
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : c i = some a
j : ℕ
hb : some b = c j
⊢ a = b

Proof state:
case intro.intro.inr.h
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
this : b ∈ c i
⊢ b = a

Tactic:
apply mem_unique this ha

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : c i = some a
j : ℕ
hb : c j = some b
⊢ a = b

Tactic:
rw [eq_some_iff] at ha hb

Result:
case intro.intro
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
⊢ a = b

Proof state:
case intro.intro.inl
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hij : i ≤ j
⊢ a = b

Tactic:
have := c.monotone hij _ ha

Result:
case intro.intro.inl
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hij : i ≤ j
this : a ∈ c j
⊢ a = b

Proof state:
case intro
α : Type u_2
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : some a = c i
⊢ a = b

Tactic:
replace ha := ha.symm

Result:
case intro
α : Type u_2
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : c i = some a
⊢ a = b

Proof state:
case intro.intro
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
⊢ a = b

Tactic:
rcases le_total i j with hij | hji

Result:
case intro.intro.inl
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hij : i ≤ j
⊢ a = b

case intro.intro.inr
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
⊢ a = b

Proof state:
case intro.intro
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : c i = some a
j : ℕ
hb : some b = c j
⊢ a = b

Tactic:
replace hb := hb.symm

Result:
case intro.intro
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : c i = some a
j : ℕ
hb : c j = some b
⊢ a = b

Proof state:
case intro.intro.inl
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hij : i ≤ j
this : a ∈ c j
⊢ a = b

Tactic:
apply mem_unique this hb

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem snoc_eraseLast_last {s : CompositionSeries X} (h : IsMaximal s.eraseLast.last s.last) :
    s.eraseLast.snoc s.last h = s :=
  have h : 0 < s.length :=
    Nat.pos_of_ne_zero (fun hs => ne_of_gt (lt_of_isMaximal h) <| by simp [last, Fin.ext_iff, hs])
  (eq_snoc_eraseLast h).symm

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : IsMaximal (eraseLast s).last (last s)
hs : s.length = 0
⊢ last s = (eraseLast s).last

Tactic:
simp [last, Fin.ext_iff, hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zip_eq_zipWith (l₁ : Vector α n) (l₂ : Vector β n) : zip l₁ l₂ = zipWith Prod.mk l₁ l₂

Proof state:
case mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Vector β l₁.size
⊢ { toArray := l₁, size_toArray := ⋯ }.zip l₂ = zipWith Prod.mk { toArray := l₁, size_toArray := ⋯ } l₂

Tactic:
rcases l₂ with ⟨l₂, h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ { toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h } =
    zipWith Prod.mk { toArray := l₁, size_toArray := ⋯ } { toArray := l₂, size_toArray := h }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ { toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h } =
    zipWith Prod.mk { toArray := l₁, size_toArray := ⋯ } { toArray := l₂, size_toArray := h }

Tactic:
simp [Array.zip_eq_zipWith, h]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l₁ : Vector α n
l₂ : Vector β n
⊢ l₁.zip l₂ = zipWith Prod.mk l₁ l₂

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Vector β l₁.size
⊢ { toArray := l₁, size_toArray := ⋯ }.zip l₂ = zipWith Prod.mk { toArray := l₁, size_toArray := ⋯ } l₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_lt_iff_le {x y : BitVec w} : (¬ x < y) ↔ y ≤ x

Proof state:
case mpr
w : Nat
x y : BitVec w
h : y.toNat ≤ x.toNat
⊢ y.toNat ≤ x.toNat

Tactic:
omega

Result:
no goals

Proof state:
case mpr
w : Nat
x y : BitVec w
⊢ y ≤ x → ¬x < y

Tactic:
intro h

Result:
case mpr
w : Nat
x y : BitVec w
h : y ≤ x
⊢ ¬x < y

Proof state:
case mpr
w : Nat
x y : BitVec w
h : y ≤ x
⊢ ¬x < y

Tactic:
simp only [lt_def, Nat.not_lt, le_def] at h ⊢

Result:
case mpr
w : Nat
x y : BitVec w
h : y.toNat ≤ x.toNat
⊢ y.toNat ≤ x.toNat

Proof state:
w : Nat
x y : BitVec w
⊢ ¬x < y ↔ y ≤ x

Tactic:
constructor <;>
  (intro h; simp only [lt_def, Nat.not_lt, le_def] at h ⊢; omega)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Algebra.lean
theorem lipschitz_with_lipschitz_const_mul :
    ∀ p q : β × β, dist (p.1 * p.2) (q.1 * q.2) ≤ LipschitzMul.C β * dist p q

Proof state:
β : Type u_2
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ LipschitzWith (LipschitzMul.C β) fun p => p.1 * p.2

Tactic:
exact lipschitzWith_lipschitz_const_mul_edist

Result:
no goals

Proof state:
β : Type u_2
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ ∀ (p q : β × β), dist (p.1 * p.2) (q.1 * q.2) ≤ ↑(LipschitzMul.C β) * dist p q

Tactic:
rw [← lipschitzWith_iff_dist_le_mul]

Result:
β : Type u_2
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ LipschitzWith (LipschitzMul.C β) fun p => p.1 * p.2
-- Mathlib/Data/Real/Basic.lean
theorem mk_le_of_forall_le {f : CauSeq ℚ abs} {x : ℝ} (h : ∃ i, ∀ j ≥ i, (f j : ℝ) ≤ x) :
    mk f ≤ x

Proof state:
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, ↑(↑f j) ≤ x
j : ℕ
ij : j ≥ i
⊢ -x ≤ ↑(↑(-f) j)

Tactic:
simp [H _ ij]

Result:
no goals

Proof state:
case intro
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, ↑(↑f j) ≤ x
⊢ -x ≤ mk (-f)

Tactic:
exact le_mk_of_forall_le ⟨i, fun j ij => by simp [H _ ij]⟩

Result:
no goals

Proof state:
f : CauSeq ℚ abs
x : ℝ
h : ∃ i, ∀ j ≥ i, ↑(↑f j) ≤ x
⊢ mk f ≤ x

Tactic:
obtain ⟨i, H⟩ := h

Result:
case intro
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, ↑(↑f j) ≤ x
⊢ mk f ≤ x

Proof state:
case intro
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, ↑(↑f j) ≤ x
⊢ mk f ≤ x

Tactic:
rw [← neg_le_neg_iff, ← mk_neg]

Result:
case intro
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, ↑(↑f j) ≤ x
⊢ -x ≤ mk (-f)
-- Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
@[to_additive]
lemma prod_Ioo_mul_left (h : a < b) : (∏ x ∈ Ioo a b, f x) * f a = ∏ x ∈ Ico a b, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a b : α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ (∏ x ∈ Ioo a b, f x) * f a = ∏ x ∈ Ico a b, f x

Tactic:
rw [mul_comm, left_mul_prod_Ioo h]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_inv_triangular (v : ι → E) {i j : ι} (hij : i < j) :
    ⟪gramSchmidt 𝕜 v j, v i⟫ = 0

Proof state:
case h.e'_2.h.e'_6.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
⊢ ∀ x ∈ Iio i, inner (b x) (v i) / ↑‖b x‖ ^ 2 * inner (b j) (b x) = 0

Tactic:
rintro k hki'

Result:
case h.e'_2.h.e'_6.h
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
v : ι → E
i j : ι
hij : i < j
b : ι → E := gramSchmidt 𝕜 v
k : ι
hki' : k ∈ Iio i
⊢ inner (b k) (v i) / ↑‖b k‖ ^ 2 * inner (b j) (b k) = 0
-- Mathlib/Order/Filter/Ultrafilter/Basic.lean
lemma atTop_eq_pure_of_isTop [LinearOrder α] {x : α} (hx : IsTop x) :
    (atTop : Filter α) = pure x

Proof state:
α : Type u
inst✝ : LinearOrder α
x : α
hx : IsTop x
⊢ atTop = pure x

Tactic:
have : Nonempty α := ⟨x⟩

Result:
α : Type u
inst✝ : LinearOrder α
x : α
hx : IsTop x
this : Nonempty α
⊢ atTop = pure x

Proof state:
case h.e'_5
α : Type u
inst✝ : LinearOrder α
x : α
hx : IsTop x
this : Nonempty α
⊢ {x} = Ici x

Tactic:
exact (Ici_eq_singleton_iff_isTop.2 hx).symm

Result:
no goals

Proof state:
α : Type u
inst✝ : LinearOrder α
x : α
hx : IsTop x
this : Nonempty α
⊢ {x} ∈ atTop

Tactic:
convert Ici_mem_atTop x using 1

Result:
case h.e'_5
α : Type u
inst✝ : LinearOrder α
x : α
hx : IsTop x
this : Nonempty α
⊢ {x} = Ici x

Proof state:
α : Type u
inst✝ : LinearOrder α
x : α
hx : IsTop x
this : Nonempty α
⊢ atTop = pure x

Tactic:
apply atTop_neBot.eq_pure_iff.2

Result:
α : Type u
inst✝ : LinearOrder α
x : α
hx : IsTop x
this : Nonempty α
⊢ {x} ∈ atTop
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem monomial_pow (n : ℕ) (r : R) (k : ℕ) : monomial n r ^ k = monomial (n * k) (r ^ k)

Proof state:
case zero
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial n) r ^ 0 = (monomial (n * 0)) (r ^ 0)

Tactic:
simp [pow_zero, monomial_zero_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
k : ℕ
⊢ (monomial n) r ^ k = (monomial (n * k)) (r ^ k)

Tactic:
induction k with
| zero => simp [pow_zero, monomial_zero_one]
| succ k ih => simp [pow_succ, ih, monomial_mul_monomial, mul_add, add_comm]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
k : ℕ
ih : (monomial n) r ^ k = (monomial (n * k)) (r ^ k)
⊢ (monomial n) r ^ (k + 1) = (monomial (n * (k + 1))) (r ^ (k + 1))

Tactic:
simp [pow_succ, ih, monomial_mul_monomial, mul_add, add_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma toAffine_some {X Y : F} (h : W.Nonsingular ![X, Y, 1]) :
    toAffine W ![X, Y, 1] = .some ((nonsingular_some ..).mp h)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
X Y : F
h : W.Nonsingular ![X, Y, 1]
⊢ toAffine W ![X, Y, 1] = Affine.Point.some ⋯

Tactic:
simp only [toAffine_of_Z_ne_zero h one_ne_zero, fin3_def_ext, one_pow, div_one]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
/--
Relation between the completed L-function and the usual one. We state it this way around so
it holds at the poles of the gamma factor as well.
-/
lemma LFunction_eq_completed_div_gammaFactor (χ : DirichletCharacter ℂ N) (s : ℂ)
    (h : s ≠ 0 ∨ N ≠ 1) : LFunction χ s = completedLFunction χ s / gammaFactor χ s

Proof state:
case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Odd
⊢ LFunction χ s = completedLFunction χ s / (s + 1).Gammaℝ

Tactic:
apply LFunction_eq_completed_div_gammaFactor_odd hχ.to_fun

Result:
no goals

Proof state:
case inl
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Even
⊢ LFunction χ s = completedLFunction χ s / s.Gammaℝ

Tactic:
exact LFunction_eq_completed_div_gammaFactor_even hχ.to_fun _ (h.imp_right χ.map_zero')

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s

Tactic:
rcases χ.even_or_odd with hχ | hχ <;>
rw [hχ.gammaFactor_def]

Result:
case inl
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Even
⊢ LFunction χ s = completedLFunction χ s / s.Gammaℝ

case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Odd
⊢ LFunction χ s = completedLFunction χ s / (s + 1).Gammaℝ
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem _root_.exists_prime_orderOf_dvd_card' {G : Type*} [Group G] [Finite G] (p : ℕ)
    [hp : Fact p.Prime] (hdvd : p ∣ Nat.card G) : ∃ x : G, orderOf x = p

Proof state:
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
this : Fintype G
hdvd : p ∣ Fintype.card G
⊢ ∃ x, orderOf x = p

Tactic:
exact exists_prime_orderOf_dvd_card p hdvd

Result:
no goals

Proof state:
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Nat.card G
this : Fintype G
⊢ ∃ x, orderOf x = p

Tactic:
rw [Nat.card_eq_fintype_card] at hdvd

Result:
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
this : Fintype G
hdvd : p ∣ Fintype.card G
⊢ ∃ x, orderOf x = p

Proof state:
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Nat.card G
⊢ ∃ x, orderOf x = p

Tactic:
have := Fintype.ofFinite G

Result:
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Nat.card G
this : Fintype G
⊢ ∃ x, orderOf x = p