harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Coherent/Comparison.lean
theorem extensive_regular_generate_coherent [Preregular C] [FinitaryPreExtensive C] :
    ((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck =
    (coherentTopology C)

Proof state:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk.hS.hS
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i => X i
this :
  generate (Presieve.ofArrows X fun i => Sigma.ι X i) ≤ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))
⊢ (Presieve.ofArrows X fun i => Sigma.ι X i) ∈ (extensiveCoverage C ⊔ regularCoverage C).covering (∐ X)

Tactic:
refine Or.inl ⟨I, inferInstance, _, _, ⟨rfl, ?_⟩⟩

Result:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk.hS.hS
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i => X i
this :
  generate (Presieve.ofArrows X fun i => Sigma.ι X i) ≤ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))
⊢ IsIso (Sigma.desc fun i => Sigma.ι X i)

Proof state:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk.hS
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i => X i
this :
  generate (Presieve.ofArrows X fun i => Sigma.ι X i) ≤ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))
⊢ (extensiveCoverage C ⊔ regularCoverage C).Saturate (∐ X) (generate (Presieve.ofArrows X fun i => Sigma.ι X i))

Tactic:
apply Coverage.Saturate.of

Result:
case h.h.h.refine_2.of.intro.intro.intro.intro.intro.a.intro.intro.intro.intro.mk.hS.hS
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i => X i
this :
  generate (Presieve.ofArrows X fun i => Sigma.ι X i) ≤ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))
⊢ (Presieve.ofArrows X fun i => Sigma.ι X i) ∈ (extensiveCoverage C ⊔ regularCoverage C).covering (∐ X)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
⊢ Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C) = coherentTopology C

Tactic:
ext B S

Result:
case h.h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
⊢ S ∈ (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) B ↔ S ∈ (coherentTopology C) B
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma support_tail_of_not_nil (p : G.Walk u v) (hnp : ¬p.Nil) :
    p.tail.support = p.support.tail

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hnp : ¬nil.Nil
⊢ nil.tail.support = nil.support.tail

Tactic:
simp only [nil_nil, not_true_eq_false] at hnp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hnp : ¬p.Nil
⊢ p.tail.support = p.support.tail

Tactic:
match p with
| .nil => simp only [nil_nil, not_true_eq_false] at hnp
| .cons h q =>
  simp only [tail_cons, getVert_cons_succ, support_copy, support_cons, List.tail_cons]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v✝¹ : V
p : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hnp : ¬(cons h q).Nil
⊢ (cons h q).tail.support = (cons h q).support.tail

Tactic:
simp only [tail_cons, getVert_cons_succ, support_copy, support_cons, List.tail_cons]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem ball_zero_absorbs_ball_zero (p : Seminorm 𝕜 E) {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) :
    Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ p.ball 0 r₂
⊢ x ∈ a • p.ball 0 r₁

Tactic:
rw [smul_ball_zero (norm_pos_iff.1 <| hr₀.trans_le ha), p.mem_ball_zero]

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ p.ball 0 r₂
⊢ p x < ‖a‖ * r₁

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : p x < r₂
⊢ p x < ‖a‖ * r₁

Tactic:
exact hx.trans (hr.trans_le <| by gcongr)

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ p.ball 0 r₂
⊢ p x < ‖a‖ * r₁

Tactic:
rw [p.mem_ball_zero] at hx

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : p x < r₂
⊢ p x < ‖a‖ * r₁

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
⊢ Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)

Tactic:
refine .of_norm ⟨r, fun a ha x hx => ?_⟩

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ p.ball 0 r₂
⊢ x ∈ a • p.ball 0 r₁

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
⊢ Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)

Tactic:
rcases exists_pos_lt_mul hr₁ r₂ with ⟨r, hr₀, hr⟩

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
⊢ Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : p x < r₂
⊢ r * r₁ ≤ ‖a‖ * r₁

Tactic:
gcongr

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem lintegral_norm_eq_lintegral_edist (f : α → β) :
    ∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ = ∫⁻ a, edist (f a) 0 ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ

Tactic:
simp only [ofReal_norm_eq_enorm, edist_zero_eq_enorm]

Result:
no goals
-- Mathlib/FieldTheory/AbelRuffini.lean
theorem induction3 {α : solvableByRad F E} {n : ℕ} (hn : n ≠ 0) (hα : P (α ^ n)) : P α

Proof state:
case hq.refine_2.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
⊢ IsSolvable (Multiset.map (fun p_1 => p_1.comp (X ^ n)) (Multiset.map (fun a => X - C a) s)).prod.Gal

Tactic:
apply gal_prod_isSolvable

Result:
case hq.refine_2.intro.hs
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
⊢ ∀ p_1 ∈ Multiset.map (fun p_2 => p_2.comp (X ^ n)) (Multiset.map (fun a => X - C a) s), IsSolvable p_1.Gal

Proof state:
case hq.refine_2.intro.hs.intro.intro.intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
q : p.SplittingField
left✝ : q ∈ s
⊢ IsSolvable (X ^ n - C q).Gal

Tactic:
exact gal_X_pow_sub_C_isSolvable n q

Result:
no goals

Proof state:
case hq.refine_2.intro.hs
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
q : p.SplittingField[X]
hq : q ∈ Multiset.map (fun p_1 => p_1.comp (X ^ n)) (Multiset.map (fun a => X - C a) s)
⊢ IsSolvable q.Gal

Tactic:
rw [Multiset.mem_map] at hq

Result:
case hq.refine_2.intro.hs
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : ↥(solvableByRad F E)
n : ℕ
hn : n ≠ 0
hα : P (α ^ n)
p : F[X] := minpoly F (α ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  Polynomial.map (algebraMap F p.SplittingField) p =
    C ((algebraMap F p.SplittingField) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
q : p.SplittingField[X]
hq : ∃ a ∈ Multiset.map (fun a => X - C a) s, a.comp (X ^ n) = q
⊢ IsSolvable q.Gal
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Pairwise.lean
theorem map_getElem_sublist {l : List α} {is : List (Fin l.length)} (h : is.Pairwise (· < ·)) :
    is.map (l[·]) <+ l

Proof state:
case cons
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
this : map (fun x => l[x]) tl <+ drop (↑hd + 1) l
his : n ≤ ↑hd
⊢ l[↑hd] :: map (fun x => l[↑x]) tl <+ drop n l

Tactic:
have := (drop_eq_getElem_cons ..).symm ▸ this.cons₂ (get l hd)

Result:
case cons
α : Type u_1
l : List α
hd : Fin l.length
tl : List (Fin l.length)
IH :
  Pairwise (fun x1 x2 => x1 < x2) tl →
    ∀ (n : Nat), (∀ (i : Fin l.length), i ∈ tl → n ≤ ↑i) → map (fun x => l[x]) tl <+ drop n l
h : Pairwise (fun x1 x2 => x1 < x2) (hd :: tl)
n : Nat
this✝ : map (fun x => l[x]) tl <+ drop (↑hd + 1) l
his : n ≤ ↑hd
this : l.get hd :: map (fun x => l[x]) tl <+ drop (↑hd) l
⊢ l[↑hd] :: map (fun x => l[↑x]) tl <+ drop n l
-- Mathlib/Control/Traversable/Lemmas.lean
theorem pure_traverse (x : t α) : traverse pure x = (pure x : F (t α))

Proof state:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α : Type u
x : t α
this : traverse pure x = pure (traverse pure x)
⊢ traverse pure x = pure x

Tactic:
rwa [id_traverse] at this

Result:
no goals

Proof state:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α : Type u
x : t α
⊢ traverse pure x = pure x

Tactic:
have : traverse pure x = pure (traverse (m := Id) pure x) :=
    (naturality (PureTransformation F) pure x).symm

Result:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α : Type u
x : t α
this : traverse pure x = pure (traverse pure x)
⊢ traverse pure x = pure x
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_zero : cof 0 = 0

Proof state:
⊢ cof 0 ≤ 0

Tactic:
rw [← card_zero]

Result:
⊢ cof 0 ≤ card 0

Proof state:
⊢ cof 0 ≤ card 0

Tactic:
exact cof_le_card 0

Result:
no goals

Proof state:
⊢ cof 0 = 0

Tactic:
refine LE.le.antisymm  ?_ (Cardinal.zero_le _)

Result:
⊢ cof 0 ≤ 0
-- Mathlib/Order/KrullDimension.lean
lemma krullDim_eq_top [InfiniteDimensionalOrder α] :
    krullDim α = ⊤ :=
  le_antisymm le_top <| le_iSup_iff.mpr <| fun m hm ↦ match m, hm with
  | ⊥, hm => False.elim <| by
    haveI : Inhabited α := ⟨LTSeries.withLength _ 0 0⟩
    exact not_le_of_lt (WithBot.bot_lt_coe _ : ⊥ < (0 : WithBot (WithTop ℕ))) <| hm default
  | some ⊤, _ => le_refl _
  | some (some m), hm => by
    refine (not_lt_of_le (hm (LTSeries.withLength _ (m + 1))) ?_).elim
    rw [WithBot.some_eq_coe, ← WithBot.coe_natCast, WithBot.coe_lt_coe,
      WithTop.some_eq_coe, ← WithTop.coe_natCast, WithTop.coe_lt_coe]
    simp

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m✝ : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝
m : ℕ
hm : ∀ (i : LTSeries α), ↑i.length ≤ some (some m)
⊢ m < ↑(LTSeries.withLength α (m + 1)).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m
hm : ∀ (i : LTSeries α), ↑i.length ≤ ⊥
⊢ False

Tactic:
haveI : Inhabited α := ⟨LTSeries.withLength _ 0 0⟩

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m
hm : ∀ (i : LTSeries α), ↑i.length ≤ ⊥
this : Inhabited α
⊢ False

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m
hm : ∀ (i : LTSeries α), ↑i.length ≤ ⊥
this : Inhabited α
⊢ False

Tactic:
exact not_le_of_lt (WithBot.bot_lt_coe _ : ⊥ < (0 : WithBot (WithTop ℕ))) <| hm default

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m✝ : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝
m : ℕ
hm : ∀ (i : LTSeries α), ↑i.length ≤ some (some m)
⊢ ⊤ ≤ some (some m)

Tactic:
refine (not_lt_of_le (hm (LTSeries.withLength _ (m + 1))) ?_).elim

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m✝ : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝
m : ℕ
hm : ∀ (i : LTSeries α), ↑i.length ≤ some (some m)
⊢ some (some m) < ↑(LTSeries.withLength α (m + 1)).length

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m✝ : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝
m : ℕ
hm : ∀ (i : LTSeries α), ↑i.length ≤ some (some m)
⊢ some (some m) < ↑(LTSeries.withLength α (m + 1)).length

Tactic:
rw [WithBot.some_eq_coe, ← WithBot.coe_natCast, WithBot.coe_lt_coe,
  WithTop.some_eq_coe, ← WithTop.coe_natCast, WithTop.coe_lt_coe]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m✝ : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝
m : ℕ
hm : ∀ (i : LTSeries α), ↑i.length ≤ some (some m)
⊢ m < ↑(LTSeries.withLength α (m + 1)).length
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem Complex.Gamma_one_half_eq : Complex.Gamma (1 / 2) = (π : ℂ) ^ (1 / 2 : ℂ)

Proof state:
case h.e'_3

⊢ ↑π ^ (1 / 2) = ↑√π

Tactic:
rw [sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_ofNat, ofReal_one]

Result:
no goals

Proof state:
⊢ Gamma (1 / 2) = ↑π ^ (1 / 2)

Tactic:
convert congr_arg ((↑) : ℝ → ℂ) Real.Gamma_one_half_eq

Result:
case h.e'_2

⊢ Gamma (1 / 2) = ↑(Real.Gamma (1 / 2))

case h.e'_3

⊢ ↑π ^ (1 / 2) = ↑√π

Proof state:
case h.e'_2

⊢ Gamma (1 / 2) = ↑(Real.Gamma (1 / 2))

Tactic:
simpa only [one_div, ofReal_inv, ofReal_ofNat] using Gamma_ofReal (1 / 2)

Result:
no goals
-- Mathlib/RingTheory/Fintype.lean
lemma Finset.univ_of_card_le_three (h : Fintype.card R ≤ 3) :
    (univ : Finset R) = {0, 1, -1}

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝¹ : Fintype.card R ≤ 3
h✝ : Fintype.card R = 3
this : Nontrivial R
h : 0 ∈ {1, -1}
⊢ False

Tactic:
simp only [mem_insert, mem_singleton, zero_eq_neg] at h

Result:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝¹ : Fintype.card R ≤ 3
h✝ : Fintype.card R = 3
this : Nontrivial R
h : 0 = 1 ∨ 1 = 0
⊢ False

Proof state:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : 2 = 0
⊢ False

Tactic:
replace H : ((2 : ℕ) : ZMod 3) = 0 := H

Result:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
H : ↑2 = 0
⊢ False

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ Nontrivial R

Tactic:
refine Fintype.one_lt_card_iff_nontrivial.1 ?_

Result:
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ 1 < Fintype.card R

Proof state:
case inl.a
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
⊢ {0, 1} ⊆ {0, 1, -1}

Tactic:
intro a ha

Result:
case inl.a
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
a : R
ha : a ∈ {0, 1}
⊢ a ∈ {0, 1, -1}
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
lemma dynEntourage_mem_uniformity [UniformSpace X] {T : X → X} (h : UniformContinuous T)
    {U : Set (X × X)} (U_uni : U ∈ 𝓤 X) (n : ℕ) :
    dynEntourage T U n ∈ 𝓤 X

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
k : ↑(Ico 0 n)
⊢ map T^[↑k] T^[↑k] ⁻¹' U ∈ 𝓤 X

Tactic:
exact uniformContinuous_def.1 (UniformContinuous.iterate T k h) U U_uni

Result:
no goals

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
k : ↑(Ico 0 n)
⊢ (map T T)^[↑k] ⁻¹' U ∈ 𝓤 X

Tactic:
rw [map_iterate T T k]

Result:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
k : ↑(Ico 0 n)
⊢ map T^[↑k] T^[↑k] ⁻¹' U ∈ 𝓤 X

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ dynEntourage T U n ∈ 𝓤 X

Tactic:
rw [dynEntourage_eq_inter_Ico T U n]

Result:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ ⋂ k, (map T T)^[↑k] ⁻¹' U ∈ 𝓤 X

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ ⋂ k, (map T T)^[↑k] ⁻¹' U ∈ 𝓤 X

Tactic:
refine Filter.iInter_mem.2 fun k ↦ ?_

Result:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
k : ↑(Ico 0 n)
⊢ (map T T)^[↑k] ⁻¹' U ∈ 𝓤 X
-- Mathlib/Algebra/GroupWithZero/InjSurj.lean
theorem Function.Injective.noZeroDivisors [NoZeroDivisors M₀'] : NoZeroDivisors M₀ where
  eq_zero_or_eq_zero_of_mul_eq_zero {a b} H :=
    have : f a * f b = 0

Proof state:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H✝ : a * b = 0
this : f a * f b = 0
H : f b = 0
⊢ f b = f 0

Tactic:
rwa [zero]

Result:
no goals

Proof state:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H : a * b = 0
⊢ f a * f b = 0

Tactic:
rw [← mul, H, zero]

Result:
no goals

Proof state:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H✝ : a * b = 0
this : f a * f b = 0
H : f a = 0
⊢ f a = f 0

Tactic:
rwa [zero]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_union_Ici (h : c ≤ max a b) : Icc a b ∪ Ici c = Ici (min a c)

Proof state:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b < a
h : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (a ⊓ c)

Tactic:
have hca : c ≤ a := h.trans hab.le

Result:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b < a
h : c ≤ b
hca : c ≤ a
⊢ Icc a b ∪ Ici c = Ici (a ⊓ c)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b < a
h : c ≤ a ∨ c ≤ b
⊢ Icc a b ∪ Ici c = Ici (a ⊓ c)

Tactic:
rcases h with h | h

Result:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b < a
h : c ≤ a
⊢ Icc a b ∪ Ici c = Ici (a ⊓ c)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b < a
h : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (a ⊓ c)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : c ≤ a ⊔ b
⊢ Icc a b ∪ Ici c = Ici (a ⊓ c)

Tactic:
rcases le_or_lt a b with hab | hab <;> simp [hab] at h

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
h : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (a ⊓ c)

case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b < a
h : c ≤ a ∨ c ≤ b
⊢ Icc a b ∪ Ici c = Ici (a ⊓ c)

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
h : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (a ⊓ c)

Tactic:
exact Icc_union_Ici' h

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b < a
h : c ≤ b
hca : c ≤ a
⊢ Icc a b ∪ Ici c = Ici (a ⊓ c)

Tactic:
simp [*]

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b < a
h : c ≤ a
⊢ Icc a b ∪ Ici c = Ici (a ⊓ c)

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma antitone_of_succ_le (hf : ∀ a, ¬ IsMax a → f (succ a) ≤ f a) : Antitone f

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) ≤ f a
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f (succ a) ≤ f a

Tactic:
simpa using hf

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) ≤ f a
⊢ Antitone f

Tactic:
simpa using antitoneOn_of_succ_le Set.ordConnected_univ (by simpa using hf)

Result:
no goals