harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/WellFoundedSet.lean
theorem partiallyWellOrderedOn_sublistForall₂ (r : α → α → Prop) [IsRefl α r] [IsTrans α r]
    {s : Set α} (h : s.PartiallyWellOrderedOn r) :
    { l : List α | ∀ x, x ∈ l → x ∈ s }.PartiallyWellOrderedOn (List.SublistForall₂ r)

Proof state:
case neg
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), (f n).headI ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m < g 0 + n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ False

Tactic:
rw [← Nat.sub_lt_iff_lt_add (le_of_not_lt hm)] at mn

Result:
case neg
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), (f n).headI ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m - g 0 < n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ False

Proof state:
case inr
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
⊢ {l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)

Tactic:
inhabit α

Result:
case inr
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ {l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)
-- Mathlib/RingTheory/TensorProduct/Basic.lean
lemma liftBaseChange_one_tmul (l : M →ₗ[R] N) (y) : l.liftBaseChange A (1 ⊗ₜ y) = l y

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
y : M
⊢ (liftBaseChange A l) (1 ⊗ₜ[R] y) = l y

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem getElem_zero_flatten {L : Vector (Vector α m) n} (h : 0 < n * m) :
    (flatten L)[0] = (L.findSome? fun l => l[0]?).get (getElem_zero_flatten.proof h)

Proof state:
α : Type u_1
m n : Nat
L : Vector (Vector α m) n
h : 0 < n * m
⊢ L.flatten[0] = (findSome? (fun l => l[0]?) L).get ⋯

Tactic:
have t := getElem?_zero_flatten L

Result:
α : Type u_1
m n : Nat
L : Vector (Vector α m) n
h : 0 < n * m
t : L.flatten[0]? = findSome? (fun l => l[0]?) L
⊢ L.flatten[0] = (findSome? (fun l => l[0]?) L).get ⋯

Proof state:
α : Type u_1
m n : Nat
L : Vector (Vector α m) n
h : 0 < n * m
t : some L[0][0] = findSome? (fun l => l[0]?) L
⊢ L.flatten[0] = (findSome? (fun l => l[0]?) L).get ⋯

Tactic:
simp [← t]

Result:
no goals

Proof state:
α : Type u_1
m n : Nat
L : Vector (Vector α m) n
h : 0 < n * m
t : L.flatten[0]? = findSome? (fun l => l[0]?) L
⊢ L.flatten[0] = (findSome? (fun l => l[0]?) L).get ⋯

Tactic:
simp [getElem?_eq_getElem, h] at t

Result:
α : Type u_1
m n : Nat
L : Vector (Vector α m) n
h : 0 < n * m
t : some L[0][0] = findSome? (fun l => l[0]?) L
⊢ L.flatten[0] = (findSome? (fun l => l[0]?) L).get ⋯
-- Mathlib/Data/ZMod/Basic.lean
theorem inv_coe_unit {n : ℕ} (u : (ZMod n)ˣ) : (u : ZMod n)⁻¹ = (u⁻¹ : (ZMod n)ˣ)

Proof state:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
⊢ (↑u)⁻¹ * ↑u = 1

Tactic:
rwa [mul_comm]

Result:
no goals

Proof state:
n : ℕ
u : (ZMod n)ˣ
⊢ (↑u)⁻¹ = ↑u⁻¹

Tactic:
have := congr_arg ((↑) : ℕ → ZMod n) (val_coe_unit_coprime u)

Result:
n : ℕ
u : (ZMod n)ˣ
this : ↑((↑u).val.gcd n) = ↑1
⊢ (↑u)⁻¹ = ↑u⁻¹

Proof state:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := ⋯ }
h : u = u'
⊢ (↑u)⁻¹ = ↑u⁻¹

Tactic:
rw [h]

Result:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := ⋯ }
h : u = u'
⊢ (↑u')⁻¹ = ↑u'⁻¹

Proof state:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := ⋯ }
h : u = u'
⊢ (↑u')⁻¹ = ↑u'⁻¹

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
⊢ (↑u)⁻¹ = ↑u⁻¹

Tactic:
let u' : (ZMod n)ˣ := ⟨u, (u : ZMod n)⁻¹, this, by rwa [mul_comm]⟩

Result:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := ⋯ }
⊢ (↑u)⁻¹ = ↑u⁻¹

Proof state:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := ⋯ }
⊢ u = u'

Tactic:
apply Units.ext

Result:
case a
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := ⋯ }
⊢ ↑u = ↑u'

Proof state:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := ⋯ }
⊢ (↑u)⁻¹ = ↑u⁻¹

Tactic:
have h : u = u' := by
  apply Units.ext
  rfl

Result:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := ⋯ }
h : u = u'
⊢ (↑u)⁻¹ = ↑u⁻¹

Proof state:
case a
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
u' : (ZMod n)ˣ := { val := ↑u, inv := (↑u)⁻¹, val_inv := this, inv_val := ⋯ }
⊢ ↑u = ↑u'

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
u : (ZMod n)ˣ
this : ↑((↑u).val.gcd n) = ↑1
⊢ (↑u)⁻¹ = ↑u⁻¹

Tactic:
rw [← mul_inv_eq_gcd, Nat.cast_one] at this

Result:
n : ℕ
u : (ZMod n)ˣ
this : ↑u * (↑u)⁻¹ = 1
⊢ (↑u)⁻¹ = ↑u⁻¹
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem mapQ_pow {f : M →ₗ[R] M} (h : p ≤ p.comap f) (k : ℕ)
    (h' : p ≤ p.comap (f ^ k) := p.le_comap_pow_of_le_comap h k) :
    p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h' : optParam (p ≤ comap (f ^ k) p) ⋯
⊢ p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k

Tactic:
induction k with
| zero => simp [LinearMap.one_eq_id]
| succ k ih =>
  simp only [LinearMap.iterate_succ]
  rw [mapQ_comp, ih]

Result:
no goals

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) ⋯), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : optParam (p ≤ comap (f ^ (k + 1)) p) ⋯
⊢ p.mapQ p ((f ^ k) ∘ₗ f) ⋯ = (p.mapQ p f h ^ k) ∘ₗ p.mapQ p f h

Tactic:
rw [mapQ_comp, ih]

Result:
no goals

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) ⋯), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : optParam (p ≤ comap (f ^ (k + 1)) p) ⋯
⊢ p.mapQ p (f ^ (k + 1)) h' = p.mapQ p f h ^ (k + 1)

Tactic:
simp only [LinearMap.iterate_succ]

Result:
case succ
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) ⋯), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : optParam (p ≤ comap (f ^ (k + 1)) p) ⋯
⊢ p.mapQ p ((f ^ k) ∘ₗ f) ⋯ = (p.mapQ p f h ^ k) ∘ₗ p.mapQ p f h

Proof state:
case zero
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
h' : optParam (p ≤ comap (f ^ 0) p) ⋯
⊢ p.mapQ p (f ^ 0) h' = p.mapQ p f h ^ 0

Tactic:
simp [LinearMap.one_eq_id]

Result:
no goals
-- Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean
theorem comul_tensorObj_tensorObj_right :
    Coalgebra.comul (R := R) (A := (CoalgebraCat.of R M ⊗
      (CoalgebraCat.of R N ⊗ CoalgebraCat.of R P) : CoalgebraCat R))
      = Coalgebra.comul (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
⊢ ModuleCat.Hom.hom ((of R M).toComonObj ⊗ (of R N ⊗ of R P).toComonObj).comul =
    ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ
      map CoalgebraStruct.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul)

Tactic:
simp only [Comon_.monoidal_tensorObj_comul, toComonObj_X, ModuleCat.of_coe, toComonObj_comul]

Result:
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
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗ ModuleCat.ofHom CoalgebraStruct.comul) ≫
        tensorμ (ModuleCat.of R M) (ModuleCat.of R M) (of R N ⊗ of R P).toModuleCat (of R N ⊗ of R P).toModuleCat) =
    ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ
      map CoalgebraStruct.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul)

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
⊢ ModuleCat.Hom.hom
      ((comonEquivalence R).symm.inverse.obj (of R M) ⊗ (comonEquivalence R).symm.inverse.obj (of R N ⊗ of R P)).comul =
    CoalgebraStruct.comul

Tactic:
dsimp only [Equivalence.symm_inverse, comonEquivalence_functor, toComon_obj,
  instCoalgebraStruct_comul]

Result:
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
⊢ ModuleCat.Hom.hom ((of R M).toComonObj ⊗ (of R N ⊗ of R P).toComonObj).comul =
    ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ
      map CoalgebraStruct.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul)
-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
lemma hasDerivAt_fourierChar (x : ℝ) : HasDerivAt (𝐞 · : ℝ → ℂ) (2 * π * I * 𝐞 x) x

Proof state:
x : ℝ
⊢ HasDerivAt (fun x => ↑(𝐞 x)) (2 * ↑π * I * ↑(𝐞 x)) x

Tactic:
have h1 (y : ℝ) : 𝐞 y = fourier 1 (y : UnitAddCircle) := by
  rw [fourierChar_apply, fourier_coe_apply]
  push_cast
  ring_nf

Result:
x : ℝ
h1 : ∀ (y : ℝ), ↑(𝐞 y) = (fourier 1) ↑y
⊢ HasDerivAt (fun x => ↑(𝐞 x)) (2 * ↑π * I * ↑(𝐞 x)) x

Proof state:
x y : ℝ
⊢ ↑(𝐞 y) = (fourier 1) ↑y

Tactic:
rw [fourierChar_apply, fourier_coe_apply]

Result:
x y : ℝ
⊢ cexp (↑(2 * π * y) * I) = cexp (2 * ↑π * I * ↑1 * ↑y / ↑1)

Proof state:
x y : ℝ
⊢ cexp (2 * ↑π * ↑y * I) = cexp (2 * ↑π * I * 1 * ↑y / 1)

Tactic:
ring_nf

Result:
no goals

Proof state:
x : ℝ
h1 : ∀ (y : ℝ), ↑(𝐞 y) = (fourier 1) ↑y
⊢ HasDerivAt (fun x => ↑(𝐞 x)) (2 * ↑π * I * ↑(𝐞 x)) x

Tactic:
simpa only [h1, Int.cast_one, ofReal_one, div_one, mul_one] using hasDerivAt_fourier 1 1 x

Result:
no goals

Proof state:
x y : ℝ
⊢ cexp (↑(2 * π * y) * I) = cexp (2 * ↑π * I * ↑1 * ↑y / ↑1)

Tactic:
push_cast

Result:
x y : ℝ
⊢ cexp (2 * ↑π * ↑y * I) = cexp (2 * ↑π * I * 1 * ↑y / 1)
-- Mathlib/Computability/PostTuringMachine.lean
theorem tr_supports {S : Finset Λ} (ss : TM1.Supports M S) :
    TM0.Supports (tr M) ↑(trStmts M S)

Proof state:
case left
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ default.1 ∈ TM1.stmts M S ∧ default.2 ∈ Finset.univ

Tactic:
constructor

Result:
case left.left
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ default.1 ∈ TM1.stmts M S

case left.right
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ default.2 ∈ Finset.univ

Proof state:
case right.mk.some.mk.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : ((some val✝, v'), s) ∈ tr M (some q, v) a
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
simp only [tr, Option.mem_def] at h₁

Result:
case right.mk.some.mk.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : some (trAux M a q v) = some ((some val✝, v'), s)
⊢ some val✝ ∈ TM1.stmts M S
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem monic_restriction {p : R[X]} : Monic (restriction p) ↔ Monic p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
H : p.restriction.coeff p.natDegree = 1
⊢ ↑(p.restriction.coeff p.natDegree) = 1

Tactic:
rw [H, OneMemClass.coe_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.Monic ↔ p.Monic

Tactic:
simp only [Monic, leadingCoeff, natDegree_restriction]

Result:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.coeff p.natDegree = 1 ↔ p.coeff p.natDegree = 1

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.coeff p.natDegree = 1 ↔ p.coeff p.natDegree = 1

Tactic:
rw [← @coeff_restriction _ _ p]

Result:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.coeff p.natDegree = 1 ↔ ↑(p.restriction.coeff p.natDegree) = 1

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.coeff p.natDegree = 1 ↔ ↑(p.restriction.coeff p.natDegree) = 1

Tactic:
exact ⟨fun H => by rw [H, OneMemClass.coe_one], fun H => Subtype.coe_injective H⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
theorem MeasureTheory.volume_sum_rpow_lt_one (hp : 1 ≤ p) :
    volume {x : ι → ℝ | ∑ i, |x i| ^ p < 1} =
      .ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (card ι / p + 1))

Proof state:
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
⊢ volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have eq_norm := fun x : ι → ℝ => (PiLp.norm_eq_sum (p := .ofReal p) (f := x)
  ((toReal_ofReal (le_of_lt h₁)).symm ▸ h₁))

Result:
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ i : ι, ‖x i‖ ^ (ENNReal.ofReal p).toReal) ^ (1 / (ENNReal.ofReal p).toReal)
⊢ volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Proof state:
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : ‖0‖ = 0
eq_zero : ∀ (x : ι → ℝ), ‖x‖ = 0 ↔ x = 0
nm_neg : ∀ (x : ι → ℝ), ‖-x‖ = ‖x‖
nm_add : ∀ (x y : ι → ℝ), ‖x + y‖ ≤ ‖x‖ + ‖y‖
⊢ volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
simp_rw [eq_norm] at eq_zero nm_zero nm_neg nm_add

Result:
ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
h₂ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
eq_norm : ∀ (x : ι → ℝ), ‖x‖ = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℝ), (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ x : ι, |0 x| ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℝ), (∑ x_1 : ι, |(-x) x_1| ^ p) ^ (1 / p) = (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p)
nm_add :
  ∀ (x y : ι → ℝ),
    (∑ x_1 : ι, |(x + y) x_1| ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, |x x_1| ^ p) ^ (1 / p) + (∑ x : ι, |y x| ^ p) ^ (1 / p)
⊢ volume {x | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_forIn'_loop {α : Type uu}
    (as : List α) (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)) (as' : List α) (b : β)
    (p : Exists (fun bs => bs ++ as' = as)) (hmono : monotone f) :
    monotone (fun x => List.forIn'.loop as (f x) as' b p)

Proof state:
case cons.hmono₂.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ ∀ (y : ForInStep β),
    monotone fun x =>
      match y with
      | ForInStep.done b => pure b
      | ForInStep.yield b =>
        let_fun this := ⋯;
        List.forIn'.loop as (f x) as' b this

Tactic:
intro y

Result:
case cons.hmono₂.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
y : ForInStep β
⊢ monotone fun x =>
    match y with
    | ForInStep.done b => pure b
    | ForInStep.yield b =>
      let_fun this := ⋯;
      List.forIn'.loop as (f x) as' b this

Proof state:
case cons.hmono₁.h.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ monotone fun x => f x a

Tactic:
apply monotone_apply

Result:
case cons.hmono₁.h.h.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
a : α
as' : List α
ih : ∀ (b : β) (p : ∃ bs, bs ++ as' = as), monotone fun x => List.forIn'.loop as (f x) as' b p
b : β
p : ∃ bs, bs ++ a :: as' = as
⊢ monotone f

Proof state:
case nil
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : List α
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
b : β
p : ∃ bs, bs ++ [] = as
⊢ monotone fun x => List.forIn'.loop as (f x) [] b p

Tactic:
apply monotone_const

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem edist_lt_coe {x y : α} {c : ℝ≥0} : edist x y < c ↔ nndist x y < c

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
c : ℝ≥0
⊢ edist x y < ↑c ↔ nndist x y < c

Tactic:
rw [edist_nndist, ENNReal.coe_lt_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_le_of_le_add {a b c : Nat} (h : a ≤ c + b) : a - b ≤ c

Proof state:
a b c : Nat
h : a ≤ c + b
d : Nat
hd✝ : a + d = c + b
hge : b ≤ a
hd : a + d - b = c
⊢ a - b + d = c

Tactic:
rw [Nat.add_comm, ← Nat.add_sub_assoc hge, Nat.add_comm]

Result:
a b c : Nat
h : a ≤ c + b
d : Nat
hd✝ : a + d = c + b
hge : b ≤ a
hd : a + d - b = c
⊢ a + d - b = c

Proof state:
a b c : Nat
h : a ≤ c + b
x✝ : Exists fun k => a + k = c + b
hle : a ≤ b
⊢ 0 ≤ c

Tactic:
apply Nat.zero_le

Result:
no goals

Proof state:
a b c : Nat
h : a ≤ c + b
d : Nat
hd : a + d = c + b
hge : b ≤ a
⊢ a - b + d = c

Tactic:
have hd := Nat.sub_eq_of_eq_add hd

Result:
a b c : Nat
h : a ≤ c + b
d : Nat
hd✝ : a + d = c + b
hge : b ≤ a
hd : a + d - b = c
⊢ a - b + d = c

Proof state:
a b c : Nat
h : a ≤ c + b
d : Nat
hd✝ : a + d = c + b
hge : b ≤ a
hd : a + d - b = c
⊢ a + d - b = c

Tactic:
exact hd

Result:
no goals

Proof state:
a b c : Nat
h : a ≤ c + b
⊢ a - b ≤ c

Tactic:
match le.dest h, Nat.le_total a b with
| _, Or.inl hle =>
  rw [Nat.sub_eq_zero_of_le hle]
  apply Nat.zero_le
| ⟨d, hd⟩, Or.inr hge =>
  apply @le.intro _ _ d
  have hd := Nat.sub_eq_of_eq_add hd
  rw [Nat.add_comm, ← Nat.add_sub_assoc hge, Nat.add_comm]
  exact hd

Result:
no goals

Proof state:
a b c : Nat
h : a ≤ c + b
x✝ : Exists fun k => a + k = c + b
hle : a ≤ b
⊢ a - b ≤ c

Tactic:
rw [Nat.sub_eq_zero_of_le hle]

Result:
a b c : Nat
h : a ≤ c + b
x✝ : Exists fun k => a + k = c + b
hle : a ≤ b
⊢ 0 ≤ c

Proof state:
a b c : Nat
h : a ≤ c + b
d : Nat
hd : a + d = c + b
hge : b ≤ a
⊢ a - b ≤ c

Tactic:
apply @le.intro _ _ d

Result:
a b c : Nat
h : a ≤ c + b
d : Nat
hd : a + d = c + b
hge : b ≤ a
⊢ a - b + d = c
-- Mathlib/GroupTheory/Finiteness.lean
theorem Subgroup.fg_iff_add_fg (P : Subgroup G) : P.FG ↔ P.toAddSubgroup.FG

Proof state:
G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG ↔ (toAddSubgroup P).FG

Tactic:
exact (Subgroup.toSubmonoid P).fg_iff_add_fg

Result:
no goals
-- Mathlib/Data/Multiset/Replicate.lean
theorem replicate_le_replicate (a : α) {k n : ℕ} : replicate k a ≤ replicate n a ↔ k ≤ n :=
  _root_.trans (by rw [← replicate_le_coe, coe_replicate]) (List.replicate_sublist_replicate a)

Proof state:
α : Type u_1
a : α
k n : ℕ
⊢ replicate k a ≤ replicate n a ↔ List.replicate k a <+ List.replicate n a

Tactic:
rw [← replicate_le_coe, coe_replicate]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem TopologicalSpace.ext_iff_isClosed {X} {t₁ t₂ : TopologicalSpace X} :
    t₁ = t₂ ↔ ∀ s, IsClosed[t₁] s ↔ IsClosed[t₂] s

Proof state:
X : Type u_3
t₁ t₂ : TopologicalSpace X
⊢ (∀ (x : Set X), IsOpen xᶜ ↔ IsOpen xᶜ) ↔ ∀ (s : Set X), IsClosed s ↔ IsClosed s

Tactic:
simp only [@isOpen_compl_iff _ _ t₁, @isOpen_compl_iff _ _ t₂]

Result:
no goals

Proof state:
X : Type u_3
t₁ t₂ : TopologicalSpace X
⊢ t₁ = t₂ ↔ ∀ (s : Set X), IsClosed s ↔ IsClosed s

Tactic:
rw [TopologicalSpace.ext_iff, compl_surjective.forall]

Result:
X : Type u_3
t₁ t₂ : TopologicalSpace X
⊢ (∀ (x : Set X), IsOpen xᶜ ↔ IsOpen xᶜ) ↔ ∀ (s : Set X), IsClosed s ↔ IsClosed s