harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Digits.lean
theorem eleven_dvd_of_palindrome (p : (digits 10 n).Palindrome) (h : Even (digits 10 n).length) :
    11 ∣ n

Proof state:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n => ↑n) (digits 10 n)
h : Even dig.length
this : dig.reverse.alternatingSum = (-1) ^ (dig.length + 1) • dig.alternatingSum
⊢ dig.alternatingSum = 0

Tactic:
rw [(p.map _).reverse_eq, _root_.pow_succ', h.neg_one_pow, mul_one, neg_one_zsmul] at this

Result:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n => ↑n) (digits 10 n)
h : Even dig.length
this : (List.map (fun n => ↑n) (digits 10 n)).alternatingSum = -dig.alternatingSum
⊢ dig.alternatingSum = 0

Proof state:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n => ↑n) (digits 10 n)
h : Even dig.length
⊢ dig.alternatingSum = 0

Tactic:
have := dig.alternatingSum_reverse

Result:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n => ↑n) (digits 10 n)
h : Even dig.length
this : dig.reverse.alternatingSum = (-1) ^ (dig.length + 1) • dig.alternatingSum
⊢ dig.alternatingSum = 0

Proof state:
n : ℕ
p : (digits 10 n).Palindrome
h : Even (digits 10 n).length
⊢ 11 ∣ n

Tactic:
let dig := (digits 10 n).map fun n : ℕ => (n : ℤ)

Result:
n : ℕ
p : (digits 10 n).Palindrome
h : Even (digits 10 n).length
dig : List ℤ := List.map (fun n => ↑n) (digits 10 n)
⊢ 11 ∣ n

Proof state:
n : ℕ
p : (digits 10 n).Palindrome
h : Even (digits 10 n).length
dig : List ℤ := List.map (fun n => ↑n) (digits 10 n)
⊢ Even dig.length

Tactic:
rwa [List.length_map]

Result:
no goals

Proof state:
n : ℕ
p : (digits 10 n).Palindrome
h : Even (digits 10 n).length
dig : List ℤ := List.map (fun n => ↑n) (digits 10 n)
⊢ 11 ∣ n

Tactic:
replace h : Even dig.length := by rwa [List.length_map]

Result:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n => ↑n) (digits 10 n)
h : Even dig.length
⊢ 11 ∣ n

Proof state:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n => ↑n) (digits 10 n)
h : Even dig.length
this : (List.map (fun n => ↑n) (digits 10 n)).alternatingSum = -dig.alternatingSum
⊢ dig.alternatingSum = 0

Tactic:
exact eq_zero_of_neg_eq this.symm

Result:
no goals

Proof state:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n => ↑n) (digits 10 n)
h : Even dig.length
⊢ 11 ∣ n

Tactic:
refine eleven_dvd_iff.2 ⟨0, (?_ : dig.alternatingSum = 0)⟩

Result:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n => ↑n) (digits 10 n)
h : Even dig.length
⊢ dig.alternatingSum = 0
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma X_eq_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : P x * Q z = Q x * P z

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun m => m • Q) u x * Q z = Q x * (fun m => m • Q) u z

Tactic:
simp only [Units.smul_def, smul_fin3_ext]

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u * Q x * Q z = Q x * (↑u * Q z)

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P x * Q z = Q x * P z

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun m => m • Q) u x * Q z = Q x * (fun m => m • Q) u z

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u * Q x * Q z = Q x * (↑u * Q z)

Tactic:
ring1

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem to_ofNatMultiset (v : Multiset ℕ) (h) : (ofNatMultiset v h : Multiset ℕ) = v

Proof state:
case h.h
v : Multiset ℕ
h✝ : ∀ p ∈ v, Nat.Prime p
p : ℕ
h : Nat.Prime p
⊢ Coe.coe ⟨p, h⟩ = id p

Tactic:
rfl

Result:
no goals

Proof state:
v : Multiset ℕ
h : ∀ p ∈ v, Nat.Prime p
⊢ (fun p h => Coe.coe ⟨p, h⟩) = fun p x => id p

Tactic:
funext p h

Result:
case h.h
v : Multiset ℕ
h✝ : ∀ p ∈ v, Nat.Prime p
p : ℕ
h : Nat.Prime p
⊢ Coe.coe ⟨p, h⟩ = id p

Proof state:
v : Multiset ℕ
h : ∀ p ∈ v, Nat.Prime p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => ⟨p, hp⟩) v h) = v

Tactic:
have : (fun p h => (Coe.coe : Nat.Primes → ℕ) ⟨p, h⟩) = fun p _ => id p := by
  funext p h
  rfl

Result:
v : Multiset ℕ
h : ∀ p ∈ v, Nat.Prime p
this : (fun p h => Coe.coe ⟨p, h⟩) = fun p x => id p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => ⟨p, hp⟩) v h) = v

Proof state:
v : Multiset ℕ
h : ∀ p ∈ v, Nat.Prime p
this : (fun p h => Coe.coe ⟨p, h⟩) = fun p x => id p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => ⟨p, hp⟩) v h) = v

Tactic:
rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]

Result:
no goals

Proof state:
v : Multiset ℕ
h : ∀ p ∈ v, Nat.Prime p
⊢ (ofNatMultiset v h).toNatMultiset = v

Tactic:
dsimp [ofNatMultiset, toNatMultiset]

Result:
v : Multiset ℕ
h : ∀ p ∈ v, Nat.Prime p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => ⟨p, hp⟩) v h) = v
-- Mathlib/Algebra/Homology/Embedding/TruncGE.lean
@[simp]
lemma truncGE'Map_id : truncGE'Map (𝟙 K) e = 𝟙 _

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : e.BoundaryGE i
⊢ (truncGE'Map (𝟙 K) e).f i = (𝟙 (K.truncGE' e)).f i

Tactic:
simp [truncGE'Map_f_eq_opcyclesMap _ _ hi rfl]

Result:
no goals

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ (truncGE'Map (𝟙 K) e).f i = (𝟙 (K.truncGE' e)).f i

Tactic:
simp [truncGE'Map_f_eq _ _ hi rfl]

Result:
no goals

Proof state:
case h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
⊢ (truncGE'Map (𝟙 K) e).f i = (𝟙 (K.truncGE' e)).f i

Tactic:
by_cases hi : e.BoundaryGE i

Result:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : e.BoundaryGE i
⊢ (truncGE'Map (𝟙 K) e).f i = (𝟙 (K.truncGE' e)).f i

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ (truncGE'Map (𝟙 K) e).f i = (𝟙 (K.truncGE' e)).f i

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
⊢ truncGE'Map (𝟙 K) e = 𝟙 (K.truncGE' e)

Tactic:
ext i

Result:
case h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
⊢ (truncGE'Map (𝟙 K) e).f i = (𝟙 (K.truncGE' e)).f i
-- Mathlib/Data/List/Basic.lean
theorem map_erase [DecidableEq β] {f : α → β} (finj : Injective f) {a : α} (l : List α) :
    map f (l.erase a) = (map f l).erase (f a)

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x => a == x) = fun x => f a == f x
⊢ map f (l.erase a) = (map f l).erase (f a)

Tactic:
rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_map, this]

Result:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x => a == x) = fun x => f a == f x
⊢ map f (eraseP (fun x => f a == f x) l) = map f (eraseP ((fun x => f a == x) ∘ f) l)

Proof state:
case h
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
b : α
⊢ (a == b) = (f a == f b)

Tactic:
simp [beq_eq_decide, finj.eq_iff]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x => a == x) = fun x => f a == f x
⊢ map f (eraseP (fun x => f a == f x) l) = map f (eraseP ((fun x => f a == x) ∘ f) l)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
⊢ (fun x => a == x) = fun x => f a == f x

Tactic:
ext b

Result:
case h
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
a : α
l : List α
b : α
⊢ (a == b) = (f a == f b)
-- Mathlib/Algebra/MvPolynomial/Funext.lean
theorem funext_iff {σ : Type*} {p q : MvPolynomial σ R} :
    p = q ↔ ∀ x : σ → R, eval x p = eval x q :=
  ⟨by rintro rfl; simp only [forall_const, eq_self_iff_true], funext⟩

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p : MvPolynomial σ R
⊢ ∀ (x : σ → R), (eval x) p = (eval x) p

Tactic:
simp only [forall_const, eq_self_iff_true]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
⊢ p = q → ∀ (x : σ → R), (eval x) p = (eval x) q

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p : MvPolynomial σ R
⊢ ∀ (x : σ → R), (eval x) p = (eval x) p
-- Mathlib/Algebra/Group/AddChar.lean
lemma _root_.MonoidHom.compAddChar_injective_right (f : M →* N) (hf : Injective f) :
    Injective fun ψ : AddChar B M ↦ f.compAddChar ψ

Proof state:
B : Type u_2
M : Type u_3
N : Type u_4
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Injective ⇑f
ψ χ : AddChar B M
h : ⇑((fun ψ => f.compAddChar ψ) ψ) = ⇑((fun ψ => f.compAddChar ψ) χ)
⊢ ⇑ψ = ⇑χ

Tactic:
exact hf.comp_left h

Result:
no goals

Proof state:
B : Type u_2
M : Type u_3
N : Type u_4
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Injective ⇑f
⊢ Injective fun ψ => f.compAddChar ψ

Tactic:
rintro ψ χ h

Result:
B : Type u_2
M : Type u_3
N : Type u_4
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Injective ⇑f
ψ χ : AddChar B M
h : (fun ψ => f.compAddChar ψ) ψ = (fun ψ => f.compAddChar ψ) χ
⊢ ψ = χ

Proof state:
B : Type u_2
M : Type u_3
N : Type u_4
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Injective ⇑f
ψ χ : AddChar B M
h : (fun ψ => f.compAddChar ψ) ψ = (fun ψ => f.compAddChar ψ) χ
⊢ ψ = χ

Tactic:
rw [DFunLike.ext'_iff] at h ⊢

Result:
B : Type u_2
M : Type u_3
N : Type u_4
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Injective ⇑f
ψ χ : AddChar B M
h : ⇑((fun ψ => f.compAddChar ψ) ψ) = ⇑((fun ψ => f.compAddChar ψ) χ)
⊢ ⇑ψ = ⇑χ
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem ContinuousLinearMap.norm_map_tail_le
    (f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei i.succ) G) (m : ∀ i, Ei i) :
    ‖f (m 0) (tail m)‖ ≤ ‖f‖ * ∏ i, ‖m i‖ :=
  calc
    ‖f (m 0) (tail m)‖ ≤ ‖f (m 0)‖ * ∏ i, ‖(tail m) i‖ := (f (m 0)).le_opNorm _
    _ ≤ ‖f‖ * ‖m 0‖ * ∏ i, ‖tail m i‖ := mul_le_mul_of_nonneg_right (f.le_opNorm _) <| by positivity
    _ = ‖f‖ * (‖m 0‖ * ∏ i, ‖(tail m) i‖)

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G
m : (i : Fin n.succ) → Ei i
⊢ 0 ≤ ∏ i : Fin n, ‖tail m i‖

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G
m : (i : Fin n.succ) → Ei i
⊢ ‖f‖ * (‖m 0‖ * ∏ i : Fin n, ‖tail m i‖) = ‖f‖ * (‖m 0‖ * ∏ i : Fin n, ‖m i.succ‖)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G
m : (i : Fin n.succ) → Ei i
⊢ ‖f‖ * ‖m 0‖ * ∏ i : Fin n, ‖tail m i‖ = ‖f‖ * (‖m 0‖ * ∏ i : Fin n, ‖tail m i‖)

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G
m : (i : Fin n.succ) → Ei i
⊢ ‖f‖ * (‖m 0‖ * ∏ i : Fin n, ‖tail m i‖) = ‖f‖ * ∏ i : Fin n.succ, ‖m i‖

Tactic:
rw [prod_univ_succ]

Result:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G
m : (i : Fin n.succ) → Ei i
⊢ ‖f‖ * (‖m 0‖ * ∏ i : Fin n, ‖tail m i‖) = ‖f‖ * (‖m 0‖ * ∏ i : Fin n, ‖m i.succ‖)
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem MeasureTheory.setIntegral_support : ∫ x in support F, F x ∂ν = ∫ x, F x ∂ν

Proof state:
X : Type u_1
M : Type u_5
inst✝¹ : NormedAddCommGroup M
inst✝ : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
⊢ ∫ (x : X) in support F, F x ∂ν = ∫ (x : X) in univ, F x ∂ν

Tactic:
rw [setIntegral_eq_of_subset_of_forall_diff_eq_zero MeasurableSet.univ (subset_univ (support F))]

Result:
X : Type u_1
M : Type u_5
inst✝¹ : NormedAddCommGroup M
inst✝ : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
⊢ ∀ x ∈ univ \ support F, F x = 0

Proof state:
X : Type u_1
M : Type u_5
inst✝¹ : NormedAddCommGroup M
inst✝ : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
⊢ ∀ x ∈ univ \ support F, F x = 0

Tactic:
exact fun _ hx => nmem_support.mp <| not_mem_of_mem_diff hx

Result:
no goals

Proof state:
X : Type u_1
M : Type u_5
inst✝¹ : NormedAddCommGroup M
inst✝ : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
⊢ ∫ (x : X) in support F, F x ∂ν = ∫ (x : X), F x ∂ν

Tactic:
nth_rw 2 [← setIntegral_univ]

Result:
X : Type u_1
M : Type u_5
inst✝¹ : NormedAddCommGroup M
inst✝ : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
⊢ ∫ (x : X) in support F, F x ∂ν = ∫ (x : X) in univ, F x ∂ν
-- Mathlib/Data/Nat/Nth.lean
theorem filter_range_nth_eq_insert {k : ℕ}
    (hlt : ∀ hf : (setOf p).Finite, k + 1 < #hf.toFinset) :
    {n ∈ range (nth p (k + 1)) | p n} = insert (nth p k) {n ∈ range (nth p k) | p n}

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
a : ℕ
ha : a = nth p k ∨ a < nth p k ∧ p a
this : nth p k < nth p (k + 1)
⊢ a < nth p (k + 1) ∧ p a

Tactic:
rcases ha with (rfl | ⟨hlt, hpa⟩)

Result:
case inl
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
this : nth p k < nth p (k + 1)
⊢ nth p k < nth p (k + 1) ∧ p (nth p k)

case inr.intro
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt✝ : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
a : ℕ
this : nth p k < nth p (k + 1)
hlt : a < nth p k
hpa : p a
⊢ a < nth p (k + 1) ∧ p a

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
a : ℕ
ha : a ∈ insert (nth p k) (filter (fun n => p n) (range (nth p k)))
⊢ a ∈ filter (fun n => p n) (range (nth p (k + 1)))

Tactic:
simp only [mem_insert, mem_filter, mem_range] at ha ⊢

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
a : ℕ
ha : a = nth p k ∨ a < nth p k ∧ p a
⊢ a < nth p (k + 1) ∧ p a

Proof state:
case inr.intro
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt✝ : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
a : ℕ
this : nth p k < nth p (k + 1)
hlt : a < nth p k
hpa : p a
⊢ a < nth p (k + 1) ∧ p a

Tactic:
exact ⟨hlt.trans this, hpa⟩

Result:
no goals

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
⊢ filter (fun n => p n) (range (nth p (k + 1))) = insert (nth p k) (filter (fun n => p n) (range (nth p k)))

Tactic:
refine (filter_range_nth_subset_insert p k).antisymm fun a ha => ?_

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
a : ℕ
ha : a ∈ insert (nth p k) (filter (fun n => p n) (range (nth p k)))
⊢ a ∈ filter (fun n => p n) (range (nth p (k + 1)))

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
a : ℕ
ha : a = nth p k ∨ a < nth p k ∧ p a
⊢ a < nth p (k + 1) ∧ p a

Tactic:
have : nth p k < nth p (k + 1) := nth_lt_nth' k.lt_succ_self hlt

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
a : ℕ
ha : a = nth p k ∨ a < nth p k ∧ p a
this : nth p k < nth p (k + 1)
⊢ a < nth p (k + 1) ∧ p a

Proof state:
case inl
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (setOf p).Finite), k + 1 < #hf.toFinset
this : nth p k < nth p (k + 1)
⊢ nth p k < nth p (k + 1) ∧ p (nth p k)

Tactic:
exact ⟨this, nth_mem _ fun hf => k.lt_succ_self.trans (hlt hf)⟩

Result:
no goals
-- Mathlib/GroupTheory/Coset/Defs.lean
theorem preimage_image_mk_eq_mul (N : Subgroup α) (s : Set α) :
    mk ⁻¹' ((mk : α → α ⧸ N) '' s) = s * N

Proof state:
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ ⋃ x, ⋃ (hx : x ∈ N), (fun x_1 => x_1 * ↑⟨x, hx⟩) '' s = ⋃ b ∈ ↑N, (fun x => x * b) '' s

Tactic:
simp only [SetLike.mem_coe]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ mk ⁻¹' (mk '' s) = s * ↑N

Tactic:
rw [preimage_image_mk_eq_iUnion_image, iUnion_subtype, ← image2_mul, ← iUnion_image_right]

Result:
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ ⋃ x, ⋃ (hx : x ∈ N), (fun x_1 => x_1 * ↑⟨x, hx⟩) '' s = ⋃ b ∈ ↑N, (fun x => x * b) '' s
-- Mathlib/Data/Fin/Basic.lean
@[simp]
lemma succ_predAbove_zero [NeZero n] {j : Fin (n + 1)} (h : j ≠ 0) : succ (predAbove 0 j) = j

Proof state:
n : ℕ
inst✝ : NeZero n
j : Fin (n + 1)
h : j ≠ 0
⊢ (predAbove 0 j).succ = j

Tactic:
rcases exists_succ_eq_of_ne_zero h with ⟨k, rfl⟩

Result:
case intro
n : ℕ
inst✝ : NeZero n
k : Fin n
h : k.succ ≠ 0
⊢ (predAbove 0 k.succ).succ = k.succ

Proof state:
case intro
n : ℕ
inst✝ : NeZero n
k : Fin n
h : k.succ ≠ 0
⊢ (predAbove 0 k.succ).succ = k.succ

Tactic:
rw [predAbove_zero_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_neg_of_pos {x : BitVec n} (h : 0#n < x) :
    (- x).toNat = 2^n - x.toNat

Proof state:
n : Nat
x : BitVec n
h : 0#n < x
⊢ (-x).toNat = 2 ^ n - x.toNat

Tactic:
change 0 < x.toNat at h

Result:
n : Nat
x : BitVec n
h : 0 < x.toNat
⊢ (-x).toNat = 2 ^ n - x.toNat

Proof state:
n : Nat
x : BitVec n
h : 0 < x.toNat
⊢ (-x).toNat = 2 ^ n - x.toNat

Tactic:
rw [toNat_neg, Nat.mod_eq_of_lt]

Result:
n : Nat
x : BitVec n
h : 0 < x.toNat
⊢ 2 ^ n - x.toNat < 2 ^ n

Proof state:
n : Nat
x : BitVec n
h : 0 < x.toNat
⊢ 2 ^ n - x.toNat < 2 ^ n

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem lt_to_nat {m n : Num} : (m : ℕ) < n ↔ m < n :=
  show (m : ℕ) < n ↔ cmp m n = Ordering.lt from
    match cmp m n, cmp_to_nat m n with
    | Ordering.lt, h => by simp only at h; simp [h]
    | Ordering.eq, h => by simp only at h; simp [h, lt_irrefl]
    | Ordering.gt, h => by simp [not_lt_of_gt h]

Proof state:
m n : Num
h : ↑m < ↑n
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Tactic:
simp [h]

Result:
no goals

Proof state:
m n : Num
h : Ordering.casesOn Ordering.lt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Tactic:
simp only at h

Result:
m n : Num
h : ↑m < ↑n
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Proof state:
m n : Num
h : m = n
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Tactic:
simp [h, lt_irrefl]

Result:
no goals

Proof state:
m n : Num
h : Ordering.casesOn Ordering.eq (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Tactic:
simp only at h

Result:
m n : Num
h : m = n
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Proof state:
m n : Num
h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.gt = Ordering.lt

Tactic:
simp [not_lt_of_gt h]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_eq_neg_self : |a| = -a ↔ a ≤ 0

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
⊢ |a| = -a ↔ a ≤ 0

Tactic:
rw [abs_eq_max_neg, max_eq_right_iff, le_neg_self_iff]

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem LieEquiv.nilpotent_iff_equiv_nilpotent (e : L ≃ₗ⁅R⁆ L') :
    IsNilpotent L ↔ IsNilpotent L'

Proof state:
case mpr
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
h : LieRing.IsNilpotent L'
⊢ LieRing.IsNilpotent L

Tactic:
exact e.injective.lieAlgebra_isNilpotent

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
⊢ LieRing.IsNilpotent L ↔ LieRing.IsNilpotent L'

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
h : LieRing.IsNilpotent L
⊢ LieRing.IsNilpotent L'

case mpr
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
h : LieRing.IsNilpotent L'
⊢ LieRing.IsNilpotent L

Proof state:
case mp
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
h : LieRing.IsNilpotent L
⊢ LieRing.IsNilpotent L'

Tactic:
exact e.symm.injective.lieAlgebra_isNilpotent

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
theorem Icc_mul_Icc_subset' [LocallyFiniteOrder α] (a b c d : α) :
    Icc a b * Icc c d ⊆ Icc (a * c) (b * d) :=
  Finset.coe_subset.mp <| by simpa using Set.Icc_mul_Icc_subset' _ _ _ _

Proof state:
α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : Preorder α
inst✝³ : DecidableEq α
inst✝² : MulLeftMono α
inst✝¹ : MulRightMono α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ ↑(Icc a b * Icc c d) ⊆ ↑(Icc (a * c) (b * d))

Tactic:
simpa using Set.Icc_mul_Icc_subset' _ _ _ _

Result:
no goals