harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem finite_of_discr_bdd_of_isComplex :
    {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ F} |
      haveI :  NumberField K := @NumberField.mk _ _ inferInstance K.prop
      {w : InfinitePlace K | IsComplex w}.Nonempty ∧ |discr K| ≤ N }.Finite

Proof state:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈(sqrt (1 + B ^ 2) ⊔ 1) ^ D * ↑(D.choose (D / 2))⌉₊
⊢ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}.Finite

Tactic:
refine finite_of_finite_generating_set A _ (bUnion_roots_finite (algebraMap ℤ A) D
    (Set.finite_Icc (-C : ℤ) C)) (fun ⟨K, hK₀⟩ ⟨hK₁, hK₂⟩ ↦ ?_)

Result:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈(sqrt (1 + B ^ 2) ⊔ 1) ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₁ : {w | w.IsComplex}.Nonempty
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
⊢ ∃
    x ∈
      ⋃ f,
        ⋃ (_ : f.natDegree ≤ D ∧ ∀ (i : ℕ), f.coeff i ∈ Set.Icc (-↑C) ↑C),
          ↑(Polynomial.map (algebraMap ℤ A) f).roots.toFinset,
    ↑⟨K, hK₀⟩ = ℚ⟮x⟯
-- Mathlib/Tactic/NormNum/Inv.lean
theorem isRat_ratCast {R : Type*} [DivisionRing R] [CharZero R] : {q : ℚ} → {n : ℤ} → {d : ℕ} →
    IsRat q n d → IsRat (q : R) n d
  | _, _, _, ⟨⟨qi,_,_⟩, rfl⟩ => ⟨⟨qi, by norm_cast, by norm_cast⟩, by simp only []; norm_cast⟩

Proof state:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑denom✝ * ↑qi = 1

Tactic:
norm_cast

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * ⅟↑denom✝) = ↑num✝ * ⅟↑denom✝

Tactic:
simp only []

Result:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi

Proof state:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi

Tactic:
norm_cast

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑qi * ↑denom✝ = 1

Tactic:
norm_cast

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem eval_at_0 (n ν : ℕ) : (bernsteinPolynomial R n ν).eval 0 = if ν = 0 then 1 else 0

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ Polynomial.eval 0 (↑(n.choose 0) * X ^ 0 * (1 - X) ^ (n - 0)) = 1

Tactic:
simp

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = 0
⊢ Polynomial.eval 0 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0

Tactic:
simp [zero_pow h]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 0 (bernsteinPolynomial R n ν) = if ν = 0 then 1 else 0

Tactic:
rw [bernsteinPolynomial]

Result:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 0 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = if ν = 0 then 1 else 0

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ Polynomial.eval 0 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = if ν = 0 then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν = 0
⊢ Polynomial.eval 0 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 1

case neg
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ¬ν = 0
⊢ Polynomial.eval 0 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 0

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν = 0
⊢ Polynomial.eval 0 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 1

Tactic:
subst h

Result:
case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ Polynomial.eval 0 (↑(n.choose 0) * X ^ 0 * (1 - X) ^ (n - 0)) = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem append_assoc (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs)

Proof state:
α : Type u
as bs cs : List α
⊢ as ++ bs ++ cs = as ++ (bs ++ cs)

Tactic:
induction as with
| nil => rfl
| cons a as ih => simp [ih]

Result:
no goals

Proof state:
case cons
α : Type u
bs cs : List α
a : α
as : List α
ih : as ++ bs ++ cs = as ++ (bs ++ cs)
⊢ a :: as ++ bs ++ cs = a :: as ++ (bs ++ cs)

Tactic:
simp [ih]

Result:
no goals

Proof state:
case nil
α : Type u
bs cs : List α
⊢ nil ++ bs ++ cs = nil ++ (bs ++ cs)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IndYoneda.lean
@[reassoc (attr := simp)]
lemma colimitHomIsoLimitYoneda_hom_comp_π [HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) :
    (colimitHomIsoLimitYoneda F A).hom ≫ limit.π (F.op ⋙ yoneda.obj A) ⟨i⟩ =
      (coyoneda.map (colimit.ι F i).op).app A

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ (colimitHomIsoLimitYoneda F A).hom ≫ limit.π (F.op ⋙ yoneda.obj A) (op i) = (coyoneda.map (colimit.ι F i).op).app A

Tactic:
simp only [colimitHomIsoLimitYoneda, Iso.trans_hom, Iso.app_hom, Category.assoc]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).hom.app A ≫
      (limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) A).hom ≫ limit.π (F.op ⋙ yoneda.obj A) (op i) =
    (coyoneda.map (colimit.ι F i).op).app A

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ ((coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ limit.π (F.op ⋙ coyoneda) (op i)).app A =
    (coyoneda.map (colimit.ι F i).op).app A

Tactic:
rw [coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π]

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).hom.app A ≫ (limit.π (F.op ⋙ coyoneda) (op i)).app A =
    (coyoneda.map (colimit.ι F i).op).app A

Tactic:
change ((coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ _).app A = _

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ ((coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ limit.π (F.op ⋙ coyoneda) (op i)).app A =
    (coyoneda.map (colimit.ι F i).op).app A

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).hom.app A ≫
      (limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) A).hom ≫ limit.π (F.op ⋙ yoneda.obj A) (op i) =
    (coyoneda.map (colimit.ι F i).op).app A

Tactic:
erw [limitObjIsoLimitCompEvaluation_hom_π]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).hom.app A ≫ (limit.π (F.op ⋙ coyoneda) (op i)).app A =
    (coyoneda.map (colimit.ι F i).op).app A
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem restrict_boxes_of_le (π : Prepartition I) (h : I ≤ J) : (π.restrict J).boxes = π.boxes

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ (π.boxes.biUnion fun a => Option.toFinset (↑J ⊓ ↑a)) = π.boxes

Tactic:
refine (Finset.biUnion_congr rfl ?_).trans Finset.biUnion_singleton_eq_self

Result:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ ∀ a ∈ π.boxes, Option.toFinset (↑J ⊓ ↑a) = {a}

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
J' : Box ι
hJ' : J' ∈ π.boxes
⊢ Option.toFinset (↑J ⊓ ↑J') = {J'}

Tactic:
rw [inf_of_le_right, ← WithBot.some_eq_coe, Option.toFinset_some]

Result:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
J' : Box ι
hJ' : J' ∈ π.boxes
⊢ ↑J' ≤ ↑J

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ (π.restrict J).boxes = π.boxes

Tactic:
classical
simp only [restrict, ofWithBot, eraseNone_eq_biUnion]
refine Finset.image_biUnion.trans ?_
refine (Finset.biUnion_congr rfl ?_).trans Finset.biUnion_singleton_eq_self
intro J' hJ'
rw [inf_of_le_right, ← WithBot.some_eq_coe, Option.toFinset_some]
exact WithBot.coe_le_coe.2 ((π.le_of_mem hJ').trans h)

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ (Finset.image (fun J' => ↑J ⊓ ↑J') π.boxes).biUnion Option.toFinset = π.boxes

Tactic:
refine Finset.image_biUnion.trans ?_

Result:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ (π.boxes.biUnion fun a => Option.toFinset (↑J ⊓ ↑a)) = π.boxes

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ (π.restrict J).boxes = π.boxes

Tactic:
simp only [restrict, ofWithBot, eraseNone_eq_biUnion]

Result:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ (Finset.image (fun J' => ↑J ⊓ ↑J') π.boxes).biUnion Option.toFinset = π.boxes

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
⊢ ∀ a ∈ π.boxes, Option.toFinset (↑J ⊓ ↑a) = {a}

Tactic:
intro J' hJ'

Result:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
J' : Box ι
hJ' : J' ∈ π.boxes
⊢ Option.toFinset (↑J ⊓ ↑J') = {J'}

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
h : I ≤ J
J' : Box ι
hJ' : J' ∈ π.boxes
⊢ ↑J' ≤ ↑J

Tactic:
exact WithBot.coe_le_coe.2 ((π.le_of_mem hJ').trans h)

Result:
no goals
-- Mathlib/NumberTheory/GaussSum.lean
theorem MulChar.IsQuadratic.gaussSum_frob_iter (n : ℕ) (hp : IsUnit (p : R)) {χ : MulChar R R'}
    (hχ : IsQuadratic χ) (ψ : AddChar R R') :
    gaussSum χ ψ ^ p ^ n = χ ((p : R) ^ n) * gaussSum χ ψ

Proof state:
case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p ^ 0 = χ (↑p ^ 0) * gaussSum χ ψ

Tactic:
rw [pow_zero, pow_one, pow_zero, MulChar.map_one, one_mul]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
n : ℕ
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ

Tactic:
induction n with
| zero => rw [pow_zero, pow_one, pow_zero, MulChar.map_one, one_mul]
| succ n ih =>
  rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul,
    ← pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ
⊢ gaussSum χ ψ ^ p ^ (n + 1) = χ (↑p ^ (n + 1)) * gaussSum χ ψ

Tactic:
rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul,
  ← pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} {h} : getValueCast a (insertEntryIfNew k v l) h =
    if h' : k == a ∧ containsKey k l = false then
      cast (congrArg β (eq_of_beq h'.1)) v
    else
      getValueCast a l (containsKey_of_containsKey_insertEntryIfNew' h h')

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (insertEntryIfNew k v l) = true
⊢ (if h : (k == a) = true ∧ containsKey k l = false then some (cast ⋯ v) else getValueCast? a l) =
    if h : (k == a) = true ∧ containsKey k l = false then some (cast ⋯ v) else some (getValueCast a l ⋯)

Tactic:
simp only [← getValueCast?_eq_some_getValueCast]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (insertEntryIfNew k v l) = true
⊢ getValueCast a (insertEntryIfNew k v l) h =
    if h' : (k == a) = true ∧ containsKey k l = false then cast ⋯ v else getValueCast a l ⋯

Tactic:
rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, apply_dite Option.some,
  getValueCast?_insertEntryIfNew]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (insertEntryIfNew k v l) = true
⊢ (if h : (k == a) = true ∧ containsKey k l = false then some (cast ⋯ v) else getValueCast? a l) =
    if h : (k == a) = true ∧ containsKey k l = false then some (cast ⋯ v) else some (getValueCast a l ⋯)
-- Mathlib/LinearAlgebra/TensorPower/Basic.lean
theorem algebraMap₀_eq_smul_one (r : R) : (algebraMap₀ r : (⨂[R]^0) M) = r • ₜ1

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ r • (tprod R) isEmptyElim = r • GradedMonoid.GOne.one

Tactic:
congr

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ algebraMap₀ r = r • GradedMonoid.GOne.one

Tactic:
simp [algebraMap₀]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ r • (tprod R) isEmptyElim = r • GradedMonoid.GOne.one
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem weightedSMul_empty {m : MeasurableSpace α} (μ : Measure α) :
    weightedSMul μ ∅ = (0 : F →L[ℝ] F)

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
⊢ (μ ∅).toReal • x = 0 x

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
⊢ (weightedSMul μ ∅) x = 0 x

Tactic:
rw [weightedSMul_apply]

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
⊢ (μ ∅).toReal • x = 0 x

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
⊢ weightedSMul μ ∅ = 0

Tactic:
ext1 x

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
⊢ (weightedSMul μ ∅) x = 0 x
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_neg : sinh (-x) = -sinh x

Proof state:
x : ℝ
⊢ sinh (-x) = -sinh x

Tactic:
simp [sinh, exp_neg, (neg_div _ _).symm, add_mul]

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem isNilpotent_of_ker_le_center {H : Type*} [Group H] (f : G →* H) (hf1 : f.ker ≤ center G)
    (hH : IsNilpotent H) : IsNilpotent G

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
⊢ IsNilpotent G

Tactic:
rw [nilpotent_iff_lowerCentralSeries] at *

Result:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : ∃ n, lowerCentralSeries H n = ⊥
⊢ ∃ n, lowerCentralSeries G n = ⊥

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ Subgroup.map f (lowerCentralSeries G n) = ⊥

Tactic:
exact eq_bot_iff.mpr (hn ▸ lowerCentralSeries.map f n)

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ lowerCentralSeries G (n + 1) = ⊥

Tactic:
refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)

Result:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ Subgroup.map f (lowerCentralSeries G n) = ⊥

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ ∃ n, lowerCentralSeries G n = ⊥

Tactic:
use n + 1

Result:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ lowerCentralSeries G (n + 1) = ⊥

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : ∃ n, lowerCentralSeries H n = ⊥
⊢ ∃ n, lowerCentralSeries G n = ⊥

Tactic:
rcases hH with ⟨n, hn⟩

Result:
case intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ ∃ n, lowerCentralSeries G n = ⊥
-- Mathlib/Data/List/Rotate.lean
theorem length_cyclicPermutations_cons (x : α) (l : List α) :
    length (cyclicPermutations (x :: l)) = length l + 1

Proof state:
α : Type u
x : α
l : List α
⊢ (x :: l).cyclicPermutations.length = l.length + 1

Tactic:
simp [cyclicPermutations_cons]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem lt_castPred_succ_iff {a b : Fin (n + 1)} (ha : succ a ≠ last (n + 1)) :
    b < (succ a).castPred ha ↔ b ≤ a

Proof state:
n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ b < a.succ.castPred ha ↔ b ≤ a

Tactic:
rw [lt_castPred_iff, castSucc_lt_succ_iff]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem bind_congr {f g : α → Option β} {x : Option α}
    (h : ∀ a ∈ x, f a = g a) : x.bind f = x.bind g

Proof state:
α : Type u_1
β : Type u_2
f g : α → Option β
x : Option α
h : ∀ (a : α), a ∈ x → f a = g a
⊢ x.bind f = x.bind g

Tactic:
cases x <;> simp only [some_bind, none_bind, mem_def, h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exponential.lean
theorem hasFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕊)
    (htx : t • x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasFDerivAt (fun u : 𝕊 => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smulRight x) t

Proof state:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
⊢ HasFDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) t

Tactic:
rw [hasFDerivAt_iff_isLittleO_nhds_zero]

Result:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
hpos : 0 < (expSeries 𝕂 𝔸).radius
⊢ (fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h) =o[𝓝 0]
    fun h => h
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem card_edgeFinset_top_eq_card_choose_two [DecidableEq V] :
    #(⊤ : SimpleGraph V).edgeFinset = (Fintype.card V).choose 2

Proof state:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ #⊤.edgeFinset = (Fintype.card V).choose 2

Tactic:
simp_rw [Set.toFinset_card, edgeSet_top, Set.coe_setOf, ← Sym2.card_subtype_not_diag]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
theorem pow_div_pow_eventuallyEq_atTop {p q : ℕ} :
    (fun x : 𝕜 => x ^ p / x ^ q) =ᶠ[atTop] fun x => x ^ ((p : ℤ) - q)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ (fun x => x ^ p / x ^ q) =ᶠ[atTop] fun x => x ^ (↑p - ↑q)

Tactic:
apply (eventually_gt_atTop (0 : 𝕜)).mono fun x hx => _

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ ∀ (x : 𝕜), 0 < x → (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
x : 𝕜
hx : 0 < x
⊢ (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x

Tactic:
simp [zpow_sub₀ hx.ne']

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ ∀ (x : 𝕜), 0 < x → (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x

Tactic:
intro x hx

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
x : 𝕜
hx : 0 < x
⊢ (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_natCast (n : ℕ) : (n : R[X]).smeval x = n • x ^ 0

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
n : ℕ
⊢ (↑n).smeval x = n • x ^ 0

Tactic:
induction n with
| zero => simp only [smeval_zero, Nat.cast_zero, zero_smul]
| succ n ih => rw [n.cast_succ, smeval_add, ih, smeval_one, ← add_nsmul]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
n : ℕ
ih : (↑n).smeval x = n • x ^ 0
⊢ (↑(n + 1)).smeval x = (n + 1) • x ^ 0

Tactic:
rw [n.cast_succ, smeval_add, ih, smeval_one, ← add_nsmul]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
⊢ (↑0).smeval x = 0 • x ^ 0

Tactic:
simp only [smeval_zero, Nat.cast_zero, zero_smul]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem norm_expSeries_div_summable_of_mem_ball (x : 𝔸)
    (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    Summable fun n => ‖x ^ n / (n ! : 𝔸)‖

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n => (expSeries 𝕂 𝔸 n) fun x_1 => x)

Tactic:
exact norm_expSeries_summable_of_mem_ball x hx

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable fun n => ‖x ^ n / ↑n !‖

Tactic:
change Summable (norm ∘ _)

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n => x ^ n / ↑n !)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n => x ^ n / ↑n !)

Tactic:
rw [← expSeries_apply_eq_div' (𝕂 := 𝕂) x]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n => (expSeries 𝕂 𝔸 n) fun x_1 => x)
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.add {t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s + t)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 ((fun x => x.1 + x.2) '' s ×ˢ t)

Tactic:
exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s + t)

Tactic:
rw [← add_image_prod]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 ((fun x => x.1 + x.2) '' s ×ˢ t)