harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem rightInvSeq_drop (ω : List B) (j : ℕ) :
    ris (ω.drop j) = (ris ω).drop j

Proof state:
case succ.nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
⊢ cs.rightInvSeq (drop (j + 1) []) = drop (j + 1) (cs.rightInvSeq [])

Tactic:
simp

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)

Tactic:
induction' j with j ih₁ generalizing ω

Result:
case zero
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ cs.rightInvSeq (drop 0 ω) = drop 0 (cs.rightInvSeq ω)

case succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
ω : List B
⊢ cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)

Proof state:
case zero
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ cs.rightInvSeq (drop 0 ω) = drop 0 (cs.rightInvSeq ω)

Tactic:
simp

Result:
no goals

Proof state:
case succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
ω : List B
⊢ cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)

Tactic:
induction' ω with k ω _

Result:
case succ.nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
⊢ cs.rightInvSeq (drop (j + 1) []) = drop (j + 1) (cs.rightInvSeq [])

case succ.cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
k : B
ω : List B
tail_ih✝ : cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
⊢ cs.rightInvSeq (drop (j + 1) (k :: ω)) = drop (j + 1) (cs.rightInvSeq (k :: ω))

Proof state:
case succ.cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
k : B
ω : List B
tail_ih✝ : cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
⊢ cs.rightInvSeq (drop (j + 1) (k :: ω)) = drop (j + 1) (cs.rightInvSeq (k :: ω))

Tactic:
rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_cons]

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem ext_iff_mulSupport {f g : α → M} :
    f = g ↔ f.mulSupport = g.mulSupport ∧ ∀ x ∈ f.mulSupport, f x = g x :=
  ⟨fun h ↦ h ▸ ⟨rfl, fun _ _ ↦ rfl⟩, fun ⟨h₁, h₂⟩ ↦ funext fun x ↦ by
    if hx : x ∈ f.mulSupport then exact h₂ x hx
    else rw [nmem_mulSupport.1 hx, nmem_mulSupport.1 (mt (Set.ext_iff.1 h₁ x).2 hx)]⟩

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
f g : α → M
x✝ : mulSupport f = mulSupport g ∧ ∀ x ∈ mulSupport f, f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ x ∈ mulSupport f, f x = g x
x : α
⊢ f x = g x

Tactic:
if hx : x ∈ f.mulSupport then exact h₂ x hx
else rw [nmem_mulSupport.1 hx, nmem_mulSupport.1 (mt (Set.ext_iff.1 h₁ x).2 hx)]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
f g : α → M
x✝ : mulSupport f = mulSupport g ∧ ∀ x ∈ mulSupport f, f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ x ∈ mulSupport f, f x = g x
x : α
hx : x ∈ mulSupport f
⊢ f x = g x

Tactic:
exact h₂ x hx

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
f g : α → M
x✝ : mulSupport f = mulSupport g ∧ ∀ x ∈ mulSupport f, f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ x ∈ mulSupport f, f x = g x
x : α
hx : x ∉ mulSupport f
⊢ f x = g x

Tactic:
rw [nmem_mulSupport.1 hx, nmem_mulSupport.1 (mt (Set.ext_iff.1 h₁ x).2 hx)]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
lemma eval₂ (hφ : φ.IsHomogeneous m) (f : R →+* MvPolynomial τ S) (g : σ → MvPolynomial τ S)
    (hf : ∀ r, (f r).IsHomogeneous 0) (hg : ∀ i, (g i).IsHomogeneous n) :
    (eval₂ f g φ).IsHomogeneous (n * m)

Proof state:
case h.e'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : φ i ≠ 0
⊢ (n * i.sum fun i c => c • 1 i) = n * ∑ i_1 ∈ i.support, i i_1

Tactic:
simp_rw [smul_eq_mul, Finsupp.sum, Pi.one_apply, mul_one]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/RingHom.lean
/-- `p` is in the image of `Spec S → Spec R` if and only if `p` extended to `S` and
restricted back to `R` is `p`. -/
lemma PrimeSpectrum.mem_range_comap_iff {p : PrimeSpectrum R} :
    p ∈ Set.range f.specComap ↔ (p.asIdeal.map f).comap f = p.asIdeal

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : PrimeSpectrum R
⊢ (∃ q, q.IsPrime ∧ Ideal.comap f q = p.asIdeal) → p ∈ Set.range f.specComap

Tactic:
rintro ⟨q, _, hq⟩

Result:
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : PrimeSpectrum R
q : Ideal S
left✝ : q.IsPrime
hq : Ideal.comap f q = p.asIdeal
⊢ p ∈ Set.range f.specComap

Proof state:
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : PrimeSpectrum R
q : Ideal S
left✝ : q.IsPrime
hq : Ideal.comap f q = p.asIdeal
⊢ p ∈ Set.range f.specComap

Tactic:
exact ⟨⟨q, inferInstance⟩, PrimeSpectrum.ext hq⟩

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : PrimeSpectrum R
x✝ : p ∈ Set.range f.specComap
q : PrimeSpectrum S
hq : f.specComap q = p
⊢ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal

Tactic:
simp [← hq]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : PrimeSpectrum R
⊢ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal → p ∈ Set.range f.specComap

Tactic:
rw [Ideal.comap_map_eq_self_iff_of_isPrime]

Result:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : PrimeSpectrum R
⊢ (∃ q, q.IsPrime ∧ Ideal.comap f q = p.asIdeal) → p ∈ Set.range f.specComap

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : PrimeSpectrum R
⊢ p ∈ Set.range f.specComap ↔ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal

Tactic:
refine ⟨fun ⟨q, hq⟩ ↦ by simp [← hq], ?_⟩

Result:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : PrimeSpectrum R
⊢ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal → p ∈ Set.range f.specComap
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem diagonalObjPullbackFstIso_inv_fst_fst {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    (diagonalObjPullbackFstIso f g).inv ≫ pullback.fst _ _ ≫ pullback.fst _ _ =
      pullback.snd _ _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).inv ≫
      fst (fst f g) (fst f g) ≫ fst f g =
    snd (snd g g ≫ g) f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).inv ≫ fst (fst f g) (fst f g) ≫ fst f g = snd (snd g g ≫ g) f

Tactic:
delta diagonalObjPullbackFstIso

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackRightPullbackFstIso f g (fst f g) ≪≫
          congrHom ⋯ ⋯ ≪≫ pullbackAssoc f g g g ≪≫ pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom ⋯ ⋯).inv ≫
      fst (fst f g) (fst f g) ≫ fst f g =
    snd (snd g g ≫ g) f
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_union_Ioi' (h₁ : c < b) : Ioo a b ∪ Ioi c = Ioi (min a c)

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c < b
x : α
hc : ¬c < x
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x

Tactic:
have hxb : x < b := (le_of_not_gt hc).trans_lt h₁

Result:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c < b
x : α
hc : ¬c < x
hxb : x < b
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c < b
x : α
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x

Tactic:
by_cases hc : c < x

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c < b
x : α
hc : c < x
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x

case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c < b
x : α
hc : ¬c < x
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c < b
x : α
⊢ x ∈ Ioo a b ∪ Ioi c ↔ x ∈ Ioi (a ⊓ c)

Tactic:
simp_rw [mem_union, mem_Ioo, mem_Ioi, min_lt_iff]

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c < b
x : α
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c < b
⊢ Ioo a b ∪ Ioi c = Ioi (a ⊓ c)

Tactic:
ext1 x

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c < b
x : α
⊢ x ∈ Ioo a b ∪ Ioi c ↔ x ∈ Ioi (a ⊓ c)

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c < b
x : α
hc : c < x
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x

Tactic:
simp only [hc, or_true]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c < b
x : α
hc : ¬c < x
hxb : x < b
⊢ a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x

Tactic:
simp only [hxb, and_true]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem weightedSMul_add_measure {m : MeasurableSpace α} (μ ν : Measure α) {s : Set α}
    (hμs : μ s ≠ ∞) (hνs : ν s ≠ ∞) :
    (weightedSMul (μ + ν) s : F →L[ℝ] F) = weightedSMul μ s + weightedSMul ν s

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ⊤
hνs : ν s ≠ ⊤
x : F
⊢ ((μ + ν) s).toReal • x = (μ s).toReal • x + (ν s).toReal • x

Tactic:
push_cast

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ⊤
hνs : ν s ≠ ⊤
x : F
⊢ ((⇑μ + ⇑ν) s).toReal • x = (μ s).toReal • x + (ν s).toReal • x

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ⊤
hνs : ν s ≠ ⊤
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s

Tactic:
ext1 x

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ⊤
hνs : ν s ≠ ⊤
x : F
⊢ (weightedSMul (μ + ν) s) x = (weightedSMul μ s + weightedSMul ν s) x

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ⊤
hνs : ν s ≠ ⊤
x : F
⊢ (weightedSMul (μ + ν) s) x = (⇑(weightedSMul μ s) + ⇑(weightedSMul ν s)) x

Tactic:
simp_rw [Pi.add_apply, weightedSMul_apply]

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ⊤
hνs : ν s ≠ ⊤
x : F
⊢ ((μ + ν) s).toReal • x = (μ s).toReal • x + (ν s).toReal • x

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ⊤
hνs : ν s ≠ ⊤
x : F
⊢ ((⇑μ + ⇑ν) s).toReal • x = (μ s).toReal • x + (ν s).toReal • x

Tactic:
rw [Pi.add_apply, ENNReal.toReal_add hμs hνs, add_smul]

Result:
no goals

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ⊤
hνs : ν s ≠ ⊤
x : F
⊢ (weightedSMul (μ + ν) s) x = (weightedSMul μ s + weightedSMul ν s) x

Tactic:
push_cast

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ⊤
hνs : ν s ≠ ⊤
x : F
⊢ (weightedSMul (μ + ν) s) x = (⇑(weightedSMul μ s) + ⇑(weightedSMul ν s)) x
-- Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
theorem coeff_hermite_of_lt {n k : ℕ} (hnk : n < k) : coeff (hermite n) k = 0

Proof state:
case intro
n k : ℕ
hnk : n < n + k + 1
⊢ (hermite n).coeff (n + k + 1) = 0

Tactic:
clear hnk

Result:
case intro
n k : ℕ
⊢ (hermite n).coeff (n + k + 1) = 0

Proof state:
case intro
n k : ℕ
⊢ (hermite n).coeff (n + k + 1) = 0

Tactic:
induction n generalizing k with
| zero => exact coeff_C
| succ n ih =>
  have : n + k + 1 + 2 = n + (k + 2) + 1 := by ring
  rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]

Result:
no goals

Proof state:
n k : ℕ
hnk : n < k
⊢ (hermite n).coeff k = 0

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hnk

Result:
case intro
n k : ℕ
hnk : n < n + k + 1
⊢ (hermite n).coeff (n + k + 1) = 0

Proof state:
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
⊢ n + k + 1 + 2 = n + (k + 2) + 1

Tactic:
ring

Result:
no goals

Proof state:
case intro.succ
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0

Tactic:
rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]

Result:
no goals

Proof state:
case intro.zero
k : ℕ
⊢ (hermite 0).coeff (0 + k + 1) = 0

Tactic:
exact coeff_C

Result:
no goals

Proof state:
case intro.succ
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0

Tactic:
have : n + k + 1 + 2 = n + (k + 2) + 1 := by ring

Result:
case intro.succ
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
⊢ (hermite (n + 1)).coeff (n + 1 + k + 1) = 0
-- Mathlib/Data/Nat/Nth.lean
theorem nth_count_eq_sInf (n : ℕ) : nth p (count p n) = sInf {i : ℕ | p i ∧ n ≤ i}

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ nth p (count p n) = sInf {i | p i ∧ n ≤ i}

Tactic:
refine (nth_eq_sInf _ _).trans (congr_arg sInf ?_)

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ {x | p x ∧ ∀ k < count p n, nth p k < x} = {i | p i ∧ n ≤ i}

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
⊢ (∀ k < count p n, nth p k < a) ↔ n ≤ a

Tactic:
refine ⟨fun h => not_lt.1 fun ha => ?_, fun hn k hk => lt_of_lt_of_le (nth_lt_of_lt_count hk) hn⟩

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
⊢ False

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ {x | p x ∧ ∀ k < count p n, nth p k < x} = {i | p i ∧ n ≤ i}

Tactic:
refine Set.ext fun a => and_congr_right fun hpa => ?_

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
⊢ (∀ k < count p n, nth p k < a) ↔ n ≤ a

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
⊢ False

Tactic:
have hn : nth p (count p a) < a := h _ (count_strict_mono hpa ha)

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
hn : nth p (count p a) < a
⊢ False

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
hn : nth p (count p a) < a
⊢ False

Tactic:
rwa [nth_count hpa, lt_self_iff_false] at hn

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem stirlingSeq_has_pos_limit_a : ∃ a : ℝ, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)

Proof state:
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto stirlingSeq atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))

Tactic:
rw [← Filter.tendsto_add_atTop_iff_nat 1]

Result:
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto (fun n => stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))

Proof state:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
⊢ x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))

Tactic:
simpa [lowerBounds] using hx

Result:
no goals

Proof state:
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)

Tactic:
obtain ⟨x, x_pos, hx⟩ := stirlingSeq'_bounded_by_pos_constant

Result:
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)

Proof state:
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)

Tactic:
refine ⟨_, lt_of_lt_of_le x_pos (le_csInf (Set.range_nonempty _) hx'), ?_⟩

Result:
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto stirlingSeq atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))

Proof state:
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)

Tactic:
have hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ)) := by simpa [lowerBounds] using hx

Result:
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)

Proof state:
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto (fun n => stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))

Tactic:
exact tendsto_atTop_ciInf stirlingSeq'_antitone ⟨x, hx'⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem colorable_chromaticNumber_of_fintype (G : SimpleGraph V) [Finite V] :
    G.Colorable (ENat.toNat G.chromaticNumber)

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
exact colorable_chromaticNumber G.colorable_of_fintype

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
cases nonempty_fintype V

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ G.Colorable G.chromaticNumber.toNat
-- Mathlib/Combinatorics/Schnirelmann.lean
@[simp] lemma schnirelmannDensity_empty : schnirelmannDensity ∅ = 0 :=
  schnirelmannDensity_eq_zero_of_one_not_mem (by simp)

Proof state:
⊢ 1 ∉ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/ZetaValues.lean
theorem hasSum_zeta_four : HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 4) (π ^ 4 / 90)

Proof state:
case h.e'_6

⊢ π ^ 4 / 90 = 8 * π ^ 4 * (1 / 30) / 24

Tactic:
field_simp

Result:
case h.e'_6

⊢ π ^ 4 * (30 * 24) = 8 * π ^ 4 * 90

Proof state:
case h.e'_6

⊢ π ^ 4 * (30 * 24) = 8 * π ^ 4 * 90

Tactic:
ring

Result:
no goals

Proof state:
⊢ HasSum (fun n => 1 / ↑n ^ 4) (π ^ 4 / 90)

Tactic:
convert hasSum_zeta_nat two_ne_zero using 1

Result:
case h.e'_6

⊢ π ^ 4 / 90 = (-1) ^ (2 + 1) * 2 ^ (2 * 2 - 1) * π ^ (2 * 2) * ↑(bernoulli (2 * 2)) / ↑(2 * 2)!

Proof state:
case h.e'_6

⊢ π ^ 4 / 90 = -(8 * π ^ 4 * ↑(-1 / 30)) / ↑4!

Tactic:
norm_num [Nat.factorial]

Result:
case h.e'_6

⊢ π ^ 4 / 90 = 8 * π ^ 4 * (1 / 30) / 24

Proof state:
case h.e'_6

⊢ π ^ 4 / 90 = (-1) ^ (2 + 1) * 2 ^ (2 * 2 - 1) * π ^ (2 * 2) * ↑(bernoulli (2 * 2)) / ↑(2 * 2)!

Tactic:
norm_num

Result:
case h.e'_6

⊢ π ^ 4 / 90 = -(8 * π ^ 4 * ↑(bernoulli 4)) / ↑4!

Proof state:
case h.e'_6

⊢ 4 ≠ 1

Tactic:
decide

Result:
no goals

Proof state:
case h.e'_6

⊢ π ^ 4 / 90 = -(8 * π ^ 4 * ↑(bernoulli 4)) / ↑4!

Tactic:
rw [bernoulli_eq_bernoulli'_of_ne_one, bernoulli'_four]

Result:
case h.e'_6

⊢ π ^ 4 / 90 = -(8 * π ^ 4 * ↑(-1 / 30)) / ↑4!

case h.e'_6

⊢ 4 ≠ 1
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem clift_self (h : proj e.1 = γ i) :
    T.clift (e, γ) i = e

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
T : Trivialization F proj
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : LocallyCompactPair ι ↑T.baseSet
γ : C(ι, ↑T.baseSet)
i : ι
e : ↑T.source
h : proj ↑e = ↑(γ i)
⊢ proj ↑e ∈ T.baseSet

Tactic:
simp [h]

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
T : Trivialization F proj
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : LocallyCompactPair ι ↑T.baseSet
γ : C(ι, ↑T.baseSet)
i : ι
e : ↑T.source
h : proj ↑e = ↑(γ i)
⊢ (T.clift (e, γ)) i = e

Tactic:
have : proj e ∈ T.baseSet := by simp [h]

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
T : Trivialization F proj
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : LocallyCompactPair ι ↑T.baseSet
γ : C(ι, ↑T.baseSet)
i : ι
e : ↑T.source
h : proj ↑e = ↑(γ i)
this : proj ↑e ∈ T.baseSet
⊢ (T.clift (e, γ)) i = e

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
T : Trivialization F proj
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : LocallyCompactPair ι ↑T.baseSet
γ : C(ι, ↑T.baseSet)
i : ι
e : ↑T.source
h : proj ↑e = ↑(γ i)
this : proj ↑e ∈ T.baseSet
⊢ (T.clift (e, γ)) i = e

Tactic:
simp [clift, liftCM, ← h, lift_self, this]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Power.lean
theorem Odd.zpow_neg_iff (hn : Odd n) : a ^ n < 0 ↔ a < 0

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a < 0
k : ℤ
⊢ a ^ (2 * k + 1) < 0

Tactic:
rw [zpow_add_one₀ ha.ne]

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a < 0
k : ℤ
⊢ a ^ (2 * k) * a < 0

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a < 0
k : ℤ
⊢ a ^ (2 * k) * a < 0

Tactic:
exact mul_neg_of_pos_of_neg (Even.zpow_pos (even_two_mul _) ha.ne) ha

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
n : ℤ
hn : Odd n
ha : a < 0
⊢ a ^ n < 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a < 0
k : ℤ
⊢ a ^ (2 * k + 1) < 0