harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem set_eq_take_append_cons_drop (l : List α) (n : Nat) (a : α) :
    l.set n a = if n < l.length then l.take n ++ a :: l.drop (n + 1) else l

Proof state:
case neg
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
h''' : n < m
⊢ (take n l).length ≤ m

Tactic:
rw [length_take]

Result:
case neg
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
h''' : n < m
⊢ min n l.length ≤ m

Proof state:
case pos
α : Type u_1
l : List α
a : α
m : Nat
h : m < l.length
h' : ¬m < m
⊢ (take m l).length ≤ m

Tactic:
rw [length_take]

Result:
case pos
α : Type u_1
l : List α
a : α
m : Nat
h : m < l.length
h' : ¬m < m
⊢ min m l.length ≤ m

Proof state:
case neg
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
h''' : n < m
⊢ min n l.length ≤ m

Tactic:
exact Nat.le_trans (Nat.min_le_left _ _) (by omega)

Result:
no goals

Proof state:
case isFalse.h
α : Type u_1
l : List α
n : Nat
a : α
h : ¬n < l.length
⊢ l.length ≤ n

Tactic:
omega

Result:
no goals

Proof state:
case neg
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
⊢ (l.set n a)[m]? = (take n l ++ a :: drop (n + 1) l)[m]?

Tactic:
have h''' : n < m := by omega

Result:
case neg
α : Type u_1
l : List α
n : Nat
a : α
h : n < l.length
m : Nat
h' : ¬m < n
h'' : ¬m = n
h''' : n < m
⊢ (l.set n a)[m]? = (take n l ++ a :: drop (n + 1) l)[m]?
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_relabel {t : L.Term α} {g : α → β} {v : β → M} :
    (t.relabel g).realize v = t.realize (v ∘ g)

Proof state:
case var
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α → β
v : β → M
a✝ : α
⊢ realize v (relabel g (var a✝)) = realize (v ∘ g) (var a✝)

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
t : L.Term α
g : α → β
v : β → M
⊢ realize v (relabel g t) = realize (v ∘ g) t

Tactic:
induction' t with _ n f ts ih

Result:
case var
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α → β
v : β → M
a✝ : α
⊢ realize v (relabel g (var a✝)) = realize (v ∘ g) (var a✝)

case func
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α → β
v : β → M
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n), realize v (relabel g (ts a)) = realize (v ∘ g) (ts a)
⊢ realize v (relabel g (func f ts)) = realize (v ∘ g) (func f ts)

Proof state:
case func
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α → β
v : β → M
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n), realize v (relabel g (ts a)) = realize (v ∘ g) (ts a)
⊢ realize v (relabel g (func f ts)) = realize (v ∘ g) (func f ts)

Tactic:
simp [ih]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/FilteredColimits.lean
theorem colimitInvAux_eq_of_rel (x y : Σ j, F.obj j)
    (h : Types.FilteredColimit.Rel (F ⋙ forget Grp) x y) :
    colimitInvAux.{v, u} F x = colimitInvAux F y

Proof state:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ Grp
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget Grp) x y
⊢ colimitInvAux F x = colimitInvAux F y

Tactic:
apply G.mk_eq

Result:
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ Grp
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget Grp) x y
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) ⟨x.fst, x.snd⁻¹⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, y.snd⁻¹⟩.snd

Proof state:
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ Grp
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget Grp).map f x.snd = (F ⋙ forget Grp).map g y.snd
⊢ (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd

Tactic:
exact hfg

Result:
no goals

Proof state:
case h.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ Grp
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget Grp).map f x.snd = (F ⋙ forget Grp).map g y.snd
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) ⟨x.fst, x.snd⁻¹⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, y.snd⁻¹⟩.snd

Tactic:
use k, f, g

Result:
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ Grp
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget Grp).map f x.snd = (F ⋙ forget Grp).map g y.snd
⊢ (ConcreteCategory.hom (F.map f)) ⟨x.fst, x.snd⁻¹⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, y.snd⁻¹⟩.snd

Proof state:
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ Grp
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget Grp).map f x.snd = (F ⋙ forget Grp).map g y.snd
⊢ (ConcreteCategory.hom (F.map f)) ⟨x.fst, x.snd⁻¹⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, y.snd⁻¹⟩.snd

Tactic:
rw [MonoidHom.map_inv, MonoidHom.map_inv, inv_inj]

Result:
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ Grp
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget Grp).map f x.snd = (F ⋙ forget Grp).map g y.snd
⊢ (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd

Proof state:
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ Grp
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget Grp) x y
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) ⟨x.fst, x.snd⁻¹⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, y.snd⁻¹⟩.snd

Tactic:
obtain ⟨k, f, g, hfg⟩ := h

Result:
case h.intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ Grp
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (F ⋙ forget Grp).map f x.snd = (F ⋙ forget Grp).map g y.snd
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) ⟨x.fst, x.snd⁻¹⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨y.fst, y.snd⁻¹⟩.snd
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_radius_eq_top_of_tendsto (hc : ∀ᶠ n in atTop, c n ≠ 0)
    (hc' : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)) : (ofScalars E c).radius = ⊤

Proof state:
case neg.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
⊢ Summable fun n => ‖‖c n‖ * ↑r' ^ n‖

Tactic:
apply summable_of_ratio_test_tendsto_lt_one zero_lt_one (hc.mp (Eventually.of_forall ?_))

Result:
case neg.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
⊢ Tendsto (fun n => ‖‖‖c (n + 1)‖ * ↑r' ^ (n + 1)‖‖ / ‖‖‖c n‖ * ↑r' ^ n‖‖) atTop (𝓝 0)

𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
⊢ ∀ (x : ℕ), c x ≠ 0 → ‖‖c x‖ * ↑r' ^ x‖ ≠ 0

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
n : ℕ
hn : n ≠ 0
⊢ ‖ofScalars E c n‖ * ↑r' ^ n ≤ ‖c n‖ * ↑r' ^ n

Tactic:
gcongr

Result:
case h.h
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
n : ℕ
hn : n ≠ 0
⊢ ‖ofScalars E c n‖ ≤ ‖c n‖
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Find.lean
theorem find?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {b : α} :
    xs.find? p = some b ↔ p b ∧ ∃ i h, xs[i] = b ∧ ∀ j : Nat, (hj : j < i) → !p xs[j]

Proof state:
case mp.intro.intro.intro.refine_3
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
j : Nat
h' : j < as.length
⊢ p (as ++ b :: bs)[j] = false

Tactic:
rw [getElem_append_left h']

Result:
case mp.intro.intro.intro.refine_3
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
j : Nat
h' : j < as.length
⊢ p as[j] = false

Proof state:
case mp
α : Type u_1
xs : List α
p : α → Bool
b : α
w : p b = true
⊢ (∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false) →
    ∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), p xs[j] = false

Tactic:
rintro ⟨as, ⟨bs, rfl⟩, h⟩

Result:
case mp.intro.intro.intro
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
⊢ ∃ i h, (as ++ b :: bs)[i] = b ∧ ∀ (j : Nat) (hj : j < i), p (as ++ b :: bs)[j] = false

Proof state:
case mpr.intro.intro.intro.refine_2
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
a : α
m : ∃ i_1 hm, xs[i_1] = a
⊢ p a = false

Tactic:
obtain ⟨j, h, rfl⟩ := m

Result:
case mpr.intro.intro.intro.refine_2.intro.intro
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h✝ : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
j : Nat
h : j < min i xs.length
⊢ p xs[j] = false

Proof state:
case mp.intro.intro.intro.refine_1
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
⊢ as.length < as.length + (bs.length + 1)

Tactic:
refine Nat.lt_add_of_pos_right (zero_lt_succ bs.length)

Result:
no goals

Proof state:
α : Type u_1
xs : List α
p : α → Bool
b : α
⊢ (p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α), a ∈ as → (!p a) = true) ↔
    p b = true ∧ ∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), (!p xs[j]) = true

Tactic:
simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]

Result:
α : Type u_1
xs : List α
p : α → Bool
b : α
⊢ p b = true →
    ((∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false) ↔
      ∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), p xs[j] = false)
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- The L-series of the von Mangoldt function restricted to the prime residue class `a` mod `q`
is continuous on `re s ≥ 1` except for a simple pole at `s = 1` with residue `(q.totient)⁻¹`.
The statement as given here in terms of `ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux`
is equivalent. -/
lemma continuousOn_LFunctionResidueClassAux :
    ContinuousOn (LFunctionResidueClassAux a) {s | 1 ≤ s.re}

Proof state:
case inr
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | 1 ≤ s.re}
hs₁ : s ≠ 1
⊢ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0

Tactic:
exact fun χ ↦ LFunction_ne_zero_of_one_le_re χ (.inr hs₁) <| Set.mem_setOf.mp hs

Result:
no goals

Proof state:
case inl
q : ℕ
a : ZMod q
inst✝ : NeZero q
hs : 1 ∈ {s | 1 ≤ s.re}
⊢ 1 ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
simp only [ne_eq, Set.mem_setOf_eq, true_or]

Result:
no goals

Proof state:
case inr
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | 1 ≤ s.re}
hs₁ : s ≠ 1
⊢ s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
simp only [ne_eq, Set.mem_setOf_eq, hs₁, false_or]

Result:
case inr
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | 1 ≤ s.re}
hs₁ : s ≠ 1
⊢ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (LFunctionResidueClassAux a) {s | 1 ≤ s.re}

Tactic:
refine (continuousOn_LFunctionResidueClassAux' a).mono fun s hs ↦ ?_

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | 1 ≤ s.re}
⊢ s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | 1 ≤ s.re}
⊢ s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
rcases eq_or_ne s 1 with rfl | hs₁

Result:
case inl
q : ℕ
a : ZMod q
inst✝ : NeZero q
hs : 1 ∈ {s | 1 ≤ s.re}
⊢ 1 ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

case inr
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | 1 ≤ s.re}
hs₁ : s ≠ 1
⊢ s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
-- Mathlib/Algebra/Free.lean
theorem length_mul (x y : FreeSemigroup α) : (x * y).length = x.length + y.length

Proof state:
α : Type u
x y : FreeSemigroup α
⊢ (x * y).length = x.length + y.length

Tactic:
simp [length, Nat.add_right_comm, List.length, List.length_append]

Result:
no goals
-- Mathlib/RepresentationTheory/FDRep.lean
theorem forget₂_ρ (V : FDRep R G) : ((forget₂ (FDRep R G) (Rep R G)).obj V).ρ = V.ρ

Proof state:
R G : Type u
inst✝¹ : CommRing R
inst✝ : Monoid G
V : FDRep R G
⊢ ((forget₂ (FDRep R G) (Rep R G)).obj V).ρ = V.ρ

Tactic:
ext g v

Result:
case h.h
R G : Type u
inst✝¹ : CommRing R
inst✝ : Monoid G
V : FDRep R G
g : G
v : ↑((forget₂ (FDRep R G) (Rep R G)).obj V).V
⊢ (((forget₂ (FDRep R G) (Rep R G)).obj V).ρ g) v = (V.ρ g) v

Proof state:
case h.h
R G : Type u
inst✝¹ : CommRing R
inst✝ : Monoid G
V : FDRep R G
g : G
v : ↑((forget₂ (FDRep R G) (Rep R G)).obj V).V
⊢ (((forget₂ (FDRep R G) (Rep R G)).obj V).ρ g) v = (V.ρ g) v

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[simp]
lemma map_f' : (h.map F).f' = F.map h.f'

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
⊢ (h.map F).f' = F.map h.f'

Tactic:
rw [← cancel_mono (h.map F).i, f'_i, map_f, map_i, ← F.map_comp, f'_i]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_eq_three : s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Proof state:
case refine_2
α : Type u_1
s : Set α
h : s.encard = 3
⊢ ↑s.encard.toNat = 3

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
⊢ ↑s.encard.toNat = 3 ↔ s.encard = 3

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
α : Type u_1
s : Set α
h : ↑s.encard.toNat = 3
⊢ s.encard = 3

case refine_2
α : Type u_1
s : Set α
h : s.encard = 3
⊢ ↑s.encard.toNat = 3

Proof state:
case refine_1
α : Type u_1
s : Set α
h : ↑s.encard.toNat = 3
⊢ s.encard = 3

Tactic:
rwa [ENat.coe_toNat] at h

Result:
case refine_1
α : Type u_1
s : Set α
h : ↑s.encard.toNat = 3
⊢ s.encard ≠ ⊤

Proof state:
case refine_1
α : Type u_1
s : Set α
h : ↑s.encard.toNat = 3
h' : s.encard = ⊤
⊢ False

Tactic:
simp [h'] at h

Result:
no goals

Proof state:
case refine_1
α : Type u_1
s : Set α
h : ↑s.encard.toNat = 3
⊢ s.encard ≠ ⊤

Tactic:
rintro h'

Result:
case refine_1
α : Type u_1
s : Set α
h : ↑s.encard.toNat = 3
h' : s.encard = ⊤
⊢ False

Proof state:
α : Type u_1
s : Set α
⊢ s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
rw [← encard_eq_three, ncard_def, ← Nat.cast_inj (R := ℕ∞), Nat.cast_ofNat]

Result:
α : Type u_1
s : Set α
⊢ ↑s.encard.toNat = 3 ↔ s.encard = 3
-- Mathlib/Topology/Basic.lean
theorem le_nhds_iff {f} : f ≤ 𝓝 x ↔ ∀ s : Set X, x ∈ s → IsOpen s → s ∈ f

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
f : Filter X
⊢ f ≤ 𝓝 x ↔ ∀ (s : Set X), x ∈ s → IsOpen s → s ∈ f

Tactic:
simp [nhds_def]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma smul_univ₀' [Fintype β] {s : Finset α} (hs : s.Nontrivial) : s • (univ : Finset β) = univ :=
  coe_injective <| by push_cast; exact Set.smul_univ₀' hs

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nontrivial
⊢ ↑s • Set.univ = Set.univ

Tactic:
exact Set.smul_univ₀' hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nontrivial
⊢ ↑(s • univ) = ↑univ

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nontrivial
⊢ ↑s • Set.univ = Set.univ
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
@[simp] lemma divInt_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a /. b

Proof state:
case inl
a : ℤ
ha : 0 ≤ a
hb : 0 ≤ 0
⊢ 0 ≤ 0

Tactic:
rfl

Result:
no goals

Proof state:
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a /. b

Tactic:
obtain rfl | hb := hb.eq_or_lt

Result:
case inl
a : ℤ
ha : 0 ≤ a
hb : 0 ≤ 0
⊢ 0 ≤ a /. 0

case inr
a b : ℤ
ha : 0 ≤ a
hb✝ : 0 ≤ b
hb : 0 < b
⊢ 0 ≤ a /. b

Proof state:
case inl
a : ℤ
ha : 0 ≤ a
hb : 0 ≤ 0
⊢ 0 ≤ a /. 0

Tactic:
simp

Result:
case inl
a : ℤ
ha : 0 ≤ a
hb : 0 ≤ 0
⊢ 0 ≤ 0

Proof state:
case inr
a b : ℤ
ha : 0 ≤ a
hb✝ : 0 ≤ b
hb : 0 < b
⊢ 0 ≤ a /. b

Tactic:
rwa [divInt_nonneg_iff_of_pos_right hb]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean
theorem differentiableAt_GammaAux (s : ℂ) (n : ℕ) (h1 : 1 - s.re < n) (h2 : ∀ m : ℕ, s ≠ -m) :
    DifferentiableAt ℂ (GammaAux n) s

Proof state:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑n + 1
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
⊢ 1 - (s + 1).re < ↑n

Tactic:
rw [Complex.add_re, Complex.one_re]

Result:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑n + 1
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
⊢ 1 - (s.re + 1) < ↑n

Proof state:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
m : ℕ
⊢ s + 1 ≠ -↑m

Tactic:
have := h2 (1 + m)

Result:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
m : ℕ
this : s ≠ -↑(1 + m)
⊢ s + 1 ≠ -↑m

Proof state:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
⊢ 1 - (s + 1).re < ↑n

Tactic:
rw [Nat.cast_succ] at h1

Result:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑n + 1
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
⊢ 1 - (s + 1).re < ↑n

Proof state:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑n + 1
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
⊢ 1 - (s.re + 1) < ↑n

Tactic:
linarith

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem IsSeparable.of_algebra_isSeparable_of_isSeparable [Algebra E K] [IsScalarTower F E K]
    [Algebra.IsSeparable F E] {x : K} (hsep : IsSeparable E x) : IsSeparable F x

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝¹ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝ : Algebra.IsSeparable F ↥E'
this : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
⊢ IsSeparable F x

Tactic:
haveI := adjoin.finiteDimensional halg

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝² : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝¹ : Algebra.IsSeparable F ↥E'
this✝ : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
this : FiniteDimensional ↥E' ↥(↥E')⟮x⟯
⊢ IsSeparable F x

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
⊢ IsSeparable F x

Tactic:
let E' : IntermediateField F E := adjoin F f.coeffs

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
⊢ IsSeparable F x

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this : FiniteDimensional F ↥E'
⊢ IsSeparable F x

Tactic:
let g : E'[X] := f.toSubring E'.toSubring (subset_adjoin F _)

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this : FiniteDimensional F ↥E'
g : (↥E')[X] := f.toSubring E'.toSubring ⋯
⊢ IsSeparable F x
-- Mathlib/Data/PFunctor/Multivariate/W.lean
theorem comp_wPathCasesOn {α β : TypeVec n} (h : α ⟹ β) {a : P.A} {f : P.last.B a → P.last.W}
    (g' : P.drop.B a ⟹ α) (g : ∀ j : P.last.B a, P.WPath (f j) ⟹ α) :
    h ⊚ P.wPathCasesOn g' g = P.wPathCasesOn (h ⊚ g') fun i => h ⊚ g i

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
⊢ h ⊚ P.wPathCasesOn g' g = P.wPathCasesOn (h ⊚ g') fun i => h ⊚ g i

Tactic:
ext i x

Result:
case a.h
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk a f) i
⊢ (h ⊚ P.wPathCasesOn g' g) i x = P.wPathCasesOn (h ⊚ g') (fun i => h ⊚ g i) i x

Proof state:
case a.h
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk a f) i
⊢ (h ⊚ P.wPathCasesOn g' g) i x = P.wPathCasesOn (h ⊚ g') (fun i => h ⊚ g i) i x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem unzip_toArray (as : List (α × β)) :
    as.toArray.unzip = Prod.map List.toArray List.toArray as.unzip

Proof state:
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ as.toArray.unzip = Prod.map toArray toArray as.unzip

Tactic:
ext1 <;> simp

Result:
no goals