harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem LinearEquiv.lift_rank_eq (f : M ≃ₗ[R] M') :
    Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M')

Proof state:
case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')

Tactic:
exact f.toLinearMap.lift_rank_le_of_injective f.injective

Result:
no goals

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')

Tactic:
apply le_antisymm

Result:
case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')

case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)

Proof state:
case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)

Tactic:
exact f.symm.toLinearMap.lift_rank_le_of_injective f.symm.injective

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map_map₂_antidistrib {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' (g₁ b) (g₂ a)) :
    (map₂ f a b).map g = map₂ f' (b.map g₁) (a.map g₂)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
β' : Type u_6
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g₁ b) (Option.map g₂ a)

Tactic:
cases a <;> cases b <;> simp [h_antidistrib]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vectorSpan_eq_span_vsub_set_left_ne {s : Set P} {p : P} (hp : p ∈ s) :
    vectorSpan k s = Submodule.span k ((p -ᵥ ·) '' (s \ {p}))

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (insert (p -ᵥ p) ((fun x => p -ᵥ x) '' (s \ {p}))) =
    Submodule.span k ((fun x => p -ᵥ x) '' (s \ {p}))

Tactic:
simp [Submodule.span_insert_eq_span]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ vectorSpan k s = Submodule.span k ((fun x => p -ᵥ x) '' (s \ {p}))

Tactic:
conv_lhs =>
  rw [vectorSpan_eq_span_vsub_set_left k hp, ← Set.insert_eq_of_mem hp, ←
    Set.insert_diff_singleton, Set.image_insert_eq]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (insert (p -ᵥ p) ((fun x => p -ᵥ x) '' (s \ {p}))) =
    Submodule.span k ((fun x => p -ᵥ x) '' (s \ {p}))
-- Mathlib/Data/Seq/Seq.lean
theorem not_terminates_iff {s : Seq α} : ¬s.Terminates ↔ ∀ n, (s.get? n).isSome

Proof state:
α : Type u
s : Seq α
⊢ ¬s.Terminates ↔ ∀ (n : ℕ), (s.get? n).isSome = true

Tactic:
simp only [Terminates, TerminatedAt, ← Ne.eq_def, Option.ne_none_iff_isSome, not_exists, iff_self]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem Perm.subtypeCongr.apply (a : ε) : ep.subtypeCongr en a =
    if h : p a then (ep ⟨a, h⟩ : ε) else en ⟨a, h⟩

Proof state:
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
⊢ (ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)

Tactic:
by_cases h : p a <;> simp [Perm.subtypeCongr, h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem card_roots_le_map_of_injective [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B}
    (hf : Function.Injective f) : Multiset.card p.roots ≤ Multiset.card (p.map f).roots

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hp0 : ¬p = 0
⊢ p.roots.card ≤ (map f p).roots.card

Tactic:
exact card_roots_le_map ((Polynomial.map_ne_zero_iff hf).mpr hp0)

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
⊢ p.roots.card ≤ (map f p).roots.card

Tactic:
by_cases hp0 : p = 0

Result:
case pos
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hp0 : p = 0
⊢ p.roots.card ≤ (map f p).roots.card

case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hp0 : ¬p = 0
⊢ p.roots.card ≤ (map f p).roots.card

Proof state:
case pos
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hp0 : p = 0
⊢ p.roots.card ≤ (map f p).roots.card

Tactic:
simp only [hp0, roots_zero, Polynomial.map_zero, Multiset.card_zero, le_rfl]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Comp.lean
theorem comp_apply_univ_le (κ : Kernel α β) (η : Kernel β γ) [IsFiniteKernel η] (a : α) :
    (η ∘ₖ κ) a Set.univ ≤ κ a Set.univ * IsFiniteKernel.bound η

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝ : IsFiniteKernel η
a : α
Cη : ℝ≥0∞ := IsFiniteKernel.bound η
⊢ ∫⁻ (b : β), (η b) Set.univ ∂κ a ≤ (κ a) Set.univ * IsFiniteKernel.bound η

Tactic:
calc
  ∫⁻ b, η b Set.univ ∂κ a ≤ ∫⁻ _, Cη ∂κ a :=
    lintegral_mono fun b => measure_le_bound η b Set.univ
  _ = Cη * κ a Set.univ := MeasureTheory.lintegral_const Cη
  _ = κ a Set.univ * Cη := mul_comm _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝ : IsFiniteKernel η
a : α
⊢ ∫⁻ (b : β), (η b) Set.univ ∂κ a ≤ (κ a) Set.univ * IsFiniteKernel.bound η

Tactic:
let Cη := IsFiniteKernel.bound η

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝ : IsFiniteKernel η
a : α
Cη : ℝ≥0∞ := IsFiniteKernel.bound η
⊢ ∫⁻ (b : β), (η b) Set.univ ∂κ a ≤ (κ a) Set.univ * IsFiniteKernel.bound η

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝ : IsFiniteKernel η
a : α
⊢ ((η ∘ₖ κ) a) Set.univ ≤ (κ a) Set.univ * IsFiniteKernel.bound η

Tactic:
rw [comp_apply' _ _ _ .univ]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝ : IsFiniteKernel η
a : α
⊢ ∫⁻ (b : β), (η b) Set.univ ∂κ a ≤ (κ a) Set.univ * IsFiniteKernel.bound η
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem eq_of_derivWithin_eq (fdiff : DifferentiableOn ℝ f (Icc a b))
    (gdiff : DifferentiableOn ℝ g (Icc a b))
    (hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)) (hi : f a = g a) :
    ∀ y ∈ Icc a b, f y = g y

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
⊢ ∀ y ∈ Icc a b, f y = g y

Tactic:
have A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y := fun y hy =>
  (fdiff y (mem_Icc_of_Ico hy)).hasDerivWithinAt.mono_of_mem_nhdsWithin
  (Icc_mem_nhdsGE_of_mem hy)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
⊢ ∀ y ∈ Icc a b, f y = g y

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
⊢ ∀ y ∈ Icc a b, f y = g y

Tactic:
have B : ∀ y ∈ Ico a b, HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y := fun y hy =>
  (gdiff y (mem_Icc_of_Ico hy)).hasDerivWithinAt.mono_of_mem_nhdsWithin
  (Icc_mem_nhdsGE_of_mem hy)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
B : ∀ y ∈ Ico a b, HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y
⊢ ∀ y ∈ Icc a b, f y = g y

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
B : ∀ y ∈ Ico a b, HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y
⊢ ∀ y ∈ Icc a b, f y = g y

Tactic:
exact eq_of_has_deriv_right_eq A (fun y hy => (hderiv hy).symm ▸ B y hy) fdiff.continuousOn
  gdiff.continuousOn hi

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem or_of_isNone {o o' : Option α} (h : o.isNone) : o.or o' = o'

Proof state:
α : Type u_1
o o' : Option α
h : o.isNone = true
x✝ : none.isNone = true
⊢ none.or o' = o'

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
o o' : Option α
h : o.isNone = true
⊢ o.or o' = o'

Tactic:
match o, h with
| none, _ => simp

Result:
no goals
-- Mathlib/Data/List/TakeWhile.lean
theorem takeWhile_takeWhile (p q : α → Bool) (l : List α) :
    takeWhile p (takeWhile q l) = takeWhile (fun a => p a ∧ q a) l

Proof state:
case cons
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a => decide (p a = true ∧ q a = true)) tl
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a => decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
by_cases hp : p hd <;> by_cases hq : q hd <;> simp [takeWhile, hp, hq, IH]

Result:
no goals

Proof state:
case nil
α : Type u_1
p q : α → Bool
⊢ takeWhile p (takeWhile q []) = takeWhile (fun a => decide (p a = true ∧ q a = true)) []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p q : α → Bool
l : List α
⊢ takeWhile p (takeWhile q l) = takeWhile (fun a => decide (p a = true ∧ q a = true)) l

Tactic:
induction' l with hd tl IH

Result:
case nil
α : Type u_1
p q : α → Bool
⊢ takeWhile p (takeWhile q []) = takeWhile (fun a => decide (p a = true ∧ q a = true)) []

case cons
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a => decide (p a = true ∧ q a = true)) tl
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a => decide (p a = true ∧ q a = true)) (hd :: tl)
-- Mathlib/Algebra/QuadraticDiscriminant.lean
lemma discrim_eq_sq_of_quadratic_eq_zero {x : R} (h : a * (x * x) + b * x + c = 0) :
    discrim a b c = (2 * a * x + b) ^ 2

Proof state:
R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
⊢ discrim a b c = (2 * a * x + b) ^ 2

Tactic:
rw [discrim]

Result:
R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
⊢ b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2

Proof state:
R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
⊢ b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2

Tactic:
linear_combination -4 * a * h

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem aestronglyMeasurable_condExpIndSMul (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞)
    (x : G) : AEStronglyMeasurable[m] (condExpIndSMul hm hs hμs x) μ

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
⊢ AEStronglyMeasurable (↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))) μ

Tactic:
exact ((toSpanSingleton ℝ x).continuous.comp_aestronglyMeasurable h).congr
  (coeFn_compLpL _ _).symm

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
⊢ AEStronglyMeasurable (↑↑(condExpIndSMul hm hs hμs x)) μ

Tactic:
rw [condExpIndSMul]

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
⊢ AEStronglyMeasurable (↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))) μ

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
⊢ AEStronglyMeasurable (↑↑(condExpIndSMul hm hs hμs x)) μ

Tactic:
have h : AEStronglyMeasurable[m] (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) μ :=
  aestronglyMeasurable_condExpL2 _ _

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
⊢ AEStronglyMeasurable (↑↑(condExpIndSMul hm hs hμs x)) μ
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_add_two : ∀ n, T R (n + 2) = 2 * X * T R (n + 1) - T R n
  | (k : ℕ) => T.eq_3 R k
  | -(k + 1 : ℕ) => by linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) T.eq_4 R k

Proof state:
case a.a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ T R (-↑(k + 1) + 2) + (2 * X * T R (-↑k) - T R (-↑k + 1)) -
      (2 * X * T R (-↑(k + 1) + 1) - T R (-↑(k + 1)) + T R (Int.negSucc k)) =
    0

Tactic:
simp [Int.negSucc_eq]

Result:
case a.a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ T R (-1 + -↑k + 2) + (2 * X * T R (-↑k) - T R (-↑k + 1)) - 2 * X * T R (-↑k) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ T R (-↑(k + 1) + 2) = 2 * X * T R (-↑(k + 1) + 1) - T R (-↑(k + 1))

Tactic:
linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) T.eq_4 R k

Result:
no goals

Proof state:
case a.a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ T R (-1 + -↑k + 2) + (2 * X * T R (-↑k) - T R (-↑k + 1)) - 2 * X * T R (-↑k) = 0

Tactic:
ring_nf

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem not_isComplex_iff_isReal {w : InfinitePlace K} : ¬IsComplex w ↔ IsReal w

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
⊢ ¬w.IsComplex ↔ w.IsReal

Tactic:
rw [isComplex_iff, isReal_iff, not_not]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem min?_reverse (t : RBNode α) : t.reverse.min? = t.max?

Proof state:
α : Type u_1
t : RBNode α
⊢ t.reverse.min? =
    match t with
    | nil => none
    | node c l v nil => some v
    | node c l v r => r.max?

Tactic:
split <;> simp [RBNode.min?]

Result:
case h_3
α : Type u_1
x✝¹ : RBNode α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : r✝ = nil → False
⊢ (node c✝ r✝.reverse v✝ l✝.reverse).min? = r✝.max?

Proof state:
case h_3.x
α : Type u_1
x✝¹ : RBNode α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : r✝ = nil → False
⊢ r✝.reverse = nil → False

Tactic:
simpa [reverse_eq_iff]

Result:
no goals

Proof state:
α : Type u_1
t : RBNode α
⊢ t.reverse.min? = t.max?

Tactic:
unfold RBNode.max?

Result:
α : Type u_1
t : RBNode α
⊢ t.reverse.min? =
    match t with
    | nil => none
    | node c l v nil => some v
    | node c l v r => r.max?

Proof state:
case h_3
α : Type u_1
x✝¹ : RBNode α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : r✝ = nil → False
⊢ r✝.reverse.min? = r✝.max?

Tactic:
apply min?_reverse

Result:
no goals

Proof state:
case h_3
α : Type u_1
x✝¹ : RBNode α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : r✝ = nil → False
⊢ (node c✝ r✝.reverse v✝ l✝.reverse).min? = r✝.max?

Tactic:
unfold RBNode.min?

Result:
case h_3
α : Type u_1
x✝¹ : RBNode α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : r✝ = nil → False
⊢ (match node c✝ r✝.reverse v✝ l✝.reverse with
    | nil => none
    | node c nil v r => some v
    | node c l v r => l.min?) =
    r✝.max?

Proof state:
case h_3
α : Type u_1
x✝¹ : RBNode α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : r✝ = nil → False
⊢ (match node c✝ r✝.reverse v✝ l✝.reverse with
    | nil => none
    | node c nil v r => some v
    | node c l v r => l.min?) =
    r✝.max?

Tactic:
rw [min?.match_1.eq_3]

Result:
case h_3
α : Type u_1
x✝¹ : RBNode α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : r✝ = nil → False
⊢ r✝.reverse.min? = r✝.max?

case h_3.x
α : Type u_1
x✝¹ : RBNode α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : r✝ = nil → False
⊢ r✝.reverse = nil → False
-- Mathlib/Algebra/Polynomial/Derivation.lean
lemma mkDerivation_one_eq_derivative' : mkDerivation R (1 : R[X]) = derivative'

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
⊢ ((mkDerivation R) 1) X = derivative' X

Tactic:
simp [derivative']

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ (mkDerivation R) 1 = derivative'

Tactic:
ext : 1

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
⊢ ((mkDerivation R) 1) X = derivative' X
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
lemma maximumClique_exists [Fintype α] : ∃ (s : Finset α), G.IsMaximumClique s

Proof state:
case intro
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
snc : G.IsNClique G.cliqueNum s
⊢ ∃ s, G.IsMaximumClique s

Tactic:
exact ⟨s, ⟨snc.isClique, fun t ht => snc.card_eq.symm ▸ ht.card_le_cliqueNum⟩⟩

Result:
no goals

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
⊢ ∃ s, G.IsMaximumClique s

Tactic:
obtain ⟨s, snc⟩ := G.exists_isNClique_cliqueNum

Result:
case intro
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
snc : G.IsNClique G.cliqueNum s
⊢ ∃ s, G.IsMaximumClique s
-- Mathlib/Combinatorics/Quiver/Prefunctor.lean
theorem congr_map {U V : Type*} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} {f g : X ⟶ Y}
    (h : f = g) : F.map f = F.map g

Proof state:
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Probability/ConditionalProbability.lean
theorem cond_apply' (ht : MeasurableSet t) (μ : Measure Ω) : μ[t|s] = (μ s)⁻¹ * μ (s ∩ t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
ht : MeasurableSet t
μ : Measure Ω
⊢ μ[t | s] = (μ s)⁻¹ * μ (s ∩ t)

Tactic:
rw [cond, Measure.smul_apply, Measure.restrict_apply ht, Set.inter_comm, smul_eq_mul]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem coe_real_preimage_closedBall_eq_iUnion (x ε : ℝ) :
    (↑) ⁻¹' closedBall (x : AddCircle p) ε = ⋃ z : ℤ, closedBall (x + z • p) ε

Proof state:
case inr.h.intro
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |y - x - ↑n * p| ≤ ε
⊢ |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε

Tactic:
rw [← mul_le_mul_left (abs_pos.mpr <| inv_ne_zero hp), ← abs_mul, mul_sub, mul_comm _ p,
  inv_mul_cancel_left₀ hp] at hn ⊢

Result:
case inr.h.intro
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |p⁻¹ * (y - x) - ↑n| ≤ |p⁻¹| * ε
⊢ |p⁻¹ * (y - x) - ↑(round (p⁻¹ * (y - x)))| ≤ |p⁻¹| * ε

Proof state:
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ (∃ i, |y - x - ↑i * p| ≤ ε) → |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε

Tactic:
rintro ⟨n, hn⟩

Result:
case inr.h.intro
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |y - x - ↑n * p| ≤ ε
⊢ |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε

Proof state:
p x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ z, closedBall (x + z • p) ε

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)

Result:
case inl
x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ z, closedBall (x + z • 0) ε

case inr
p x ε : ℝ
hp : p ≠ 0
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ z, closedBall (x + z • p) ε

Proof state:
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ ⋃ z, closedBall (x + z • p) ε

Tactic:
simp only [dist_eq_norm, mem_preimage, mem_closedBall, zsmul_eq_mul, mem_iUnion, Real.norm_eq_abs,
  ← QuotientAddGroup.mk_sub, norm_eq, ← sub_sub]

Result:
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε ↔ ∃ i, |y - x - ↑i * p| ≤ ε

Proof state:
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε ↔ ∃ i, |y - x - ↑i * p| ≤ ε

Tactic:
refine ⟨fun h => ⟨round (p⁻¹ * (y - x)), h⟩, ?_⟩

Result:
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ (∃ i, |y - x - ↑i * p| ≤ ε) → |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε

Proof state:
case inr
p x ε : ℝ
hp : p ≠ 0
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ z, closedBall (x + z • p) ε

Tactic:
ext y

Result:
case inr.h
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ ⋃ z, closedBall (x + z • p) ε

Proof state:
case inr.h.intro
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |p⁻¹ * (y - x) - ↑n| ≤ |p⁻¹| * ε
⊢ |p⁻¹ * (y - x) - ↑(round (p⁻¹ * (y - x)))| ≤ |p⁻¹| * ε

Tactic:
exact (round_le (p⁻¹ * (y - x)) n).trans hn

Result:
no goals

Proof state:
case inl
x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ z, closedBall (x + z • 0) ε

Tactic:
simp [iUnion_const]

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem sorted_last_eq_max' {s : Finset α}
    {h : (s.sort (· ≤ ·)).length - 1 < (s.sort (· ≤ ·)).length} :
    (s.sort (· ≤ ·))[(s.sort (· ≤ ·)).length - 1] =
      s.max' (by rw [length_sort] at h; exact card_pos.1 (lt_of_le_of_lt bot_le h)) :=
  sorted_last_eq_max'_aux _ h _

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : #s - 1 < #s
⊢ s.Nonempty

Tactic:
exact card_pos.1 (lt_of_le_of_lt bot_le h)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : (sort (fun x1 x2 => x1 ≤ x2) s).length - 1 < (sort (fun x1 x2 => x1 ≤ x2) s).length
⊢ s.Nonempty

Tactic:
rw [length_sort] at h

Result:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : #s - 1 < #s
⊢ s.Nonempty