harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_const_smul_left {c : 𝕜} (hc : c ≠ 0) :
    (fun x => c • f' x) =o[l] g ↔ f' =o[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x => ‖c • f' x‖) =o[l] g ↔ f' =o[l] g

Tactic:
simp only [norm_smul]

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x => ‖c‖ * ‖f' x‖) =o[l] g ↔ f' =o[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
⊢ (fun x => c • f' x) =o[l] g ↔ f' =o[l] g

Tactic:
have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x => c • f' x) =o[l] g ↔ f' =o[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x => c • f' x) =o[l] g ↔ f' =o[l] g

Tactic:
rw [← isLittleO_norm_left]

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x => ‖c • f' x‖) =o[l] g ↔ f' =o[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (fun x => ‖c‖ * ‖f' x‖) =o[l] g ↔ f' =o[l] g

Tactic:
rw [isLittleO_const_mul_left_iff cne0, isLittleO_norm_left]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[simp] lemma ofIsLimitKernelFork_f' (hf : S.f = 0) (c : KernelFork S.g) (hc : IsLimit c) :
    (ofIsLimitKernelFork S hf c hc).f' = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ (ofIsLimitKernelFork S hf c hc).f' = 0

Tactic:
rw [← cancel_mono (ofIsLimitKernelFork S hf c hc).i, f'_i, hf, zero_comp]

Result:
no goals
-- Mathlib/Topology/Category/Stonean/Basic.lean
lemma projective_of_extrDisc {X : Profinite.{u}} (hX : ExtremallyDisconnected X) :
    Projective X

Proof state:
X : Profinite
hX : ExtremallyDisconnected ↑X.toTop
⊢ Projective X

Tactic:
show Projective (Stonean.toProfinite.obj ⟨X.toTop, inferInstance⟩)

Result:
X : Profinite
hX : ExtremallyDisconnected ↑X.toTop
⊢ Projective (Stonean.toProfinite.obj (CompHausLike.mk X.toTop ⋯))

Proof state:
X : Profinite
hX : ExtremallyDisconnected ↑X.toTop
⊢ Projective (Stonean.toProfinite.obj (CompHausLike.mk X.toTop ⋯))

Tactic:
exact inferInstance

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma norm_smul_basis (p q : R[X]) :
    Algebra.norm R[X] (p • (1 : W.CoordinateRing) + q • mk W Y) =
      p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) -
        q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ (Algebra.norm R[X]) (p • 1 + q • (mk W) Y) =
    p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)

Tactic:
simp_rw [Algebra.norm_eq_matrix_det <| CoordinateRing.basis W, Matrix.det_fin_two,
  Algebra.leftMulMatrix_eq_repr_mul, basis_zero, mul_one, basis_one, smul_basis_mul_Y, map_add,
  Finsupp.add_apply, map_smul, Finsupp.smul_apply, ← basis_zero, ← basis_one,
  Basis.repr_self_apply, if_pos, one_ne_zero, if_false, smul_eq_mul]

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ (p * 1 + q * 0) *
        ((q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) * if 0 = 1 then 1 else 0) +
          (p - q * (C W.a₁ * X + C W.a₃)) * 1) -
      (q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) * 1 + (p - q * (C W.a₁ * X + C W.a₃)) * 0) *
        ((p * if 0 = 1 then 1 else 0) + q * 1) =
    p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ (p * 1 + q * 0) *
        ((q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) * if 0 = 1 then 1 else 0) +
          (p - q * (C W.a₁ * X + C W.a₃)) * 1) -
      (q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) * 1 + (p - q * (C W.a₁ * X + C W.a₃)) * 0) *
        ((p * if 0 = 1 then 1 else 0) + q * 1) =
    p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)

Tactic:
ring1

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem outerMeasure_exists_compact {U : Opens G} (hU : μ.outerMeasure U ≠ ∞) {ε : ℝ≥0}
    (hε : ε ≠ 0) : ∃ K : Compacts G, (K : Set G) ⊆ U ∧ μ.outerMeasure U ≤ μ.outerMeasure K + ε

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : Opens G
hU : μ.outerMeasure ↑U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure ↑K + ↑ε

Tactic:
rw [μ.outerMeasure_opens] at hU ⊢

Result:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : Opens G
hU : μ.innerContent U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ.outerMeasure ↑K + ↑ε

Proof state:
case intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : Opens G
hU : μ.innerContent U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
K : Compacts G
h1K : ↑K ⊆ ↑U
h2K : μ.innerContent U ≤ μ K + ↑ε
⊢ ∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ.outerMeasure ↑K + ↑ε

Tactic:
exact ⟨K, h1K, le_trans h2K <| add_le_add_right (μ.le_outerMeasure_compacts K) _⟩

Result:
no goals

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : Opens G
hU : μ.innerContent U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ.outerMeasure ↑K + ↑ε

Tactic:
rcases μ.innerContent_exists_compact hU hε with ⟨K, h1K, h2K⟩

Result:
case intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : Opens G
hU : μ.innerContent U ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
K : Compacts G
h1K : ↑K ⊆ ↑U
h2K : μ.innerContent U ≤ μ K + ↑ε
⊢ ∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ.outerMeasure ↑K + ↑ε
-- Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
theorem isIntegrallyClosed_eq_field_fractions' [IsDomain S] [Algebra K S] [IsScalarTower R K S]
    {s : S} (hs : IsIntegral R s) : minpoly K s = (minpoly R s).map (algebraMap R K)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain R
inst✝⁷ : Algebra R S
K : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
inst✝¹ : Algebra K S
inst✝ : IsScalarTower R K S
s : S
hs : IsIntegral R s
⊢ minpoly K s = map (algebraMap R K) (minpoly R s)

Tactic:
let L := FractionRing S

Result:
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain R
inst✝⁷ : Algebra R S
K : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
inst✝¹ : Algebra K S
inst✝ : IsScalarTower R K S
s : S
hs : IsIntegral R s
L : Type u_2 := FractionRing S
⊢ minpoly K s = map (algebraMap R K) (minpoly R s)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain R
inst✝⁷ : Algebra R S
K : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
inst✝¹ : Algebra K S
inst✝ : IsScalarTower R K S
s : S
hs : IsIntegral R s
L : Type u_2 := FractionRing S
⊢ minpoly K s = map (algebraMap R K) (minpoly R s)

Tactic:
rw [← isIntegrallyClosed_eq_field_fractions K L hs, algebraMap_eq (IsFractionRing.injective S L)]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem HasMFDerivWithinAt.congr_of_eventuallyEq (h : HasMFDerivWithinAt I I' f s x f')
    (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : HasMFDerivWithinAt I I' f₁ s x f'

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f f₁ : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivWithinAt I I' f s x f'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
this : ↑(extChartAt I x).symm ⁻¹' {y | f₁ y = f y} ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x
⊢ ∀ y ∈ ↑(extChartAt I x).symm ⁻¹' {y | f₁ y = f y},
    y ∈ {x_1 | (fun x_2 => writtenInExtChartAt I I' x f₁ x_2 = writtenInExtChartAt I I' x f x_2) x_1}

Tactic:
simp +contextual only [hx, mfld_simps]

Result:
no goals

Proof state:
case hx
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f f₁ : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivWithinAt I I' f s x f'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ writtenInExtChartAt I I' x f₁ (↑(extChartAt I x) x) = writtenInExtChartAt I I' x f (↑(extChartAt I x) x)

Tactic:
simp only [hx, mfld_simps]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_eq_zero' {a b : Ordinal} : a * b = 0 ↔ a = 0 ∨ b = 0 :=
  inductionOn a fun α _ _ =>
    inductionOn b fun β _ _ => by
      simp_rw [← type_prod_lex, type_eq_zero_iff_isEmpty]
      rw [or_comm]
      exact isEmpty_prod

Proof state:
a b : Ordinal.{u_4}
α : Type u_4
x✝³ : α → α → Prop
x✝² : IsWellOrder α x✝³
β : Type u_4
x✝¹ : β → β → Prop
x✝ : IsWellOrder β x✝¹
⊢ IsEmpty (β × α) ↔ IsEmpty α ∨ IsEmpty β

Tactic:
rw [or_comm]

Result:
a b : Ordinal.{u_4}
α : Type u_4
x✝³ : α → α → Prop
x✝² : IsWellOrder α x✝³
β : Type u_4
x✝¹ : β → β → Prop
x✝ : IsWellOrder β x✝¹
⊢ IsEmpty (β × α) ↔ IsEmpty β ∨ IsEmpty α

Proof state:
a b : Ordinal.{u_4}
α : Type u_4
x✝³ : α → α → Prop
x✝² : IsWellOrder α x✝³
β : Type u_4
x✝¹ : β → β → Prop
x✝ : IsWellOrder β x✝¹
⊢ IsEmpty (β × α) ↔ IsEmpty β ∨ IsEmpty α

Tactic:
exact isEmpty_prod

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
α : Type u_4
x✝³ : α → α → Prop
x✝² : IsWellOrder α x✝³
β : Type u_4
x✝¹ : β → β → Prop
x✝ : IsWellOrder β x✝¹
⊢ type x✝³ * type x✝¹ = 0 ↔ type x✝³ = 0 ∨ type x✝¹ = 0

Tactic:
simp_rw [← type_prod_lex, type_eq_zero_iff_isEmpty]

Result:
a b : Ordinal.{u_4}
α : Type u_4
x✝³ : α → α → Prop
x✝² : IsWellOrder α x✝³
β : Type u_4
x✝¹ : β → β → Prop
x✝ : IsWellOrder β x✝¹
⊢ IsEmpty (β × α) ↔ IsEmpty α ∨ IsEmpty β
-- Mathlib/SetTheory/Game/Basic.lean
theorem rightMoves_mul_cases {x y : PGame} (k) {P : (x * y).RightMoves → Prop}
    (hl : ∀ ix jy, P <| toRightMovesMul (Sum.inl ⟨ix, jy⟩))
    (hr : ∀ jx iy, P <| toRightMovesMul (Sum.inr ⟨jx, iy⟩)) : P k

Proof state:
case inl.mk
x y : PGame
k : (x * y).RightMoves
P : (x * y).RightMoves → Prop
hl : ∀ (ix : x.LeftMoves) (jy : y.RightMoves), P (toRightMovesMul (Sum.inl (ix, jy)))
hr : ∀ (jx : x.RightMoves) (iy : y.LeftMoves), P (toRightMovesMul (Sum.inr (jx, iy)))
ix : x.LeftMoves
iy : y.RightMoves
⊢ P (toRightMovesMul (Sum.inl (ix, iy)))

Tactic:
apply hl

Result:
no goals

Proof state:
x y : PGame
k : (x * y).RightMoves
P : (x * y).RightMoves → Prop
hl : ∀ (ix : x.LeftMoves) (jy : y.RightMoves), P (toRightMovesMul (Sum.inl (ix, jy)))
hr : ∀ (jx : x.RightMoves) (iy : y.LeftMoves), P (toRightMovesMul (Sum.inr (jx, iy)))
⊢ P (toRightMovesMul (toRightMovesMul.symm k))

Tactic:
rcases toRightMovesMul.symm k with (⟨ix, iy⟩ | ⟨jx, jy⟩)

Result:
case inl.mk
x y : PGame
k : (x * y).RightMoves
P : (x * y).RightMoves → Prop
hl : ∀ (ix : x.LeftMoves) (jy : y.RightMoves), P (toRightMovesMul (Sum.inl (ix, jy)))
hr : ∀ (jx : x.RightMoves) (iy : y.LeftMoves), P (toRightMovesMul (Sum.inr (jx, iy)))
ix : x.LeftMoves
iy : y.RightMoves
⊢ P (toRightMovesMul (Sum.inl (ix, iy)))

case inr.mk
x y : PGame
k : (x * y).RightMoves
P : (x * y).RightMoves → Prop
hl : ∀ (ix : x.LeftMoves) (jy : y.RightMoves), P (toRightMovesMul (Sum.inl (ix, jy)))
hr : ∀ (jx : x.RightMoves) (iy : y.LeftMoves), P (toRightMovesMul (Sum.inr (jx, iy)))
jx : x.RightMoves
jy : y.LeftMoves
⊢ P (toRightMovesMul (Sum.inr (jx, jy)))

Proof state:
x y : PGame
k : (x * y).RightMoves
P : (x * y).RightMoves → Prop
hl : ∀ (ix : x.LeftMoves) (jy : y.RightMoves), P (toRightMovesMul (Sum.inl (ix, jy)))
hr : ∀ (jx : x.RightMoves) (iy : y.LeftMoves), P (toRightMovesMul (Sum.inr (jx, iy)))
⊢ P k

Tactic:
rw [← toRightMovesMul.apply_symm_apply k]

Result:
x y : PGame
k : (x * y).RightMoves
P : (x * y).RightMoves → Prop
hl : ∀ (ix : x.LeftMoves) (jy : y.RightMoves), P (toRightMovesMul (Sum.inl (ix, jy)))
hr : ∀ (jx : x.RightMoves) (iy : y.LeftMoves), P (toRightMovesMul (Sum.inr (jx, iy)))
⊢ P (toRightMovesMul (toRightMovesMul.symm k))

Proof state:
case inr.mk
x y : PGame
k : (x * y).RightMoves
P : (x * y).RightMoves → Prop
hl : ∀ (ix : x.LeftMoves) (jy : y.RightMoves), P (toRightMovesMul (Sum.inl (ix, jy)))
hr : ∀ (jx : x.RightMoves) (iy : y.LeftMoves), P (toRightMovesMul (Sum.inr (jx, iy)))
jx : x.RightMoves
jy : y.LeftMoves
⊢ P (toRightMovesMul (Sum.inr (jx, jy)))

Tactic:
apply hr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem size_unattach {p : α → Prop} {l : Array { x // p x }} :
    l.unattach.size = l.size

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
⊢ (map (fun x => x.val) l).size = l.size

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
⊢ l.unattach.size = l.size

Tactic:
unfold unattach

Result:
α : Type u_1
p : α → Prop
l : Array { x // p x }
⊢ (map (fun x => x.val) l).size = l.size
-- Mathlib/Data/Rat/Defs.lean
@[simp] lemma mk'_pow (num : ℤ) (den : ℕ) (hd hdn) (n : ℕ) :
    mk' num den hd hdn ^ n = mk' (num ^ n) (den ^ n)
      (by simp [Nat.pow_eq_zero, hd]) (by rw [Int.natAbs_pow]; exact hdn.pow _ _) := rfl

Proof state:
q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ den ^ n ≠ 0

Tactic:
simp [Nat.pow_eq_zero, hd]

Result:
no goals

Proof state:
q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ (num.natAbs ^ n).Coprime (den ^ n)

Tactic:
exact hdn.pow _ _

Result:
no goals

Proof state:
q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ (num ^ n).natAbs.Coprime (den ^ n)

Tactic:
rw [Int.natAbs_pow]

Result:
q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ (num.natAbs ^ n).Coprime (den ^ n)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem lookup_cons_self  {k : α} : ((k,b) :: es).lookup k = some b

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β✝ : Type u_1
b : β✝
es : List (α × β✝)
k : α
⊢ lookup k ((k, b) :: es) = some b

Tactic:
simp [lookup_cons]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Ring.lean
lemma two_mul_sq_add_one_le_two_pow_two_mul (k : ℕ) : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)

Proof state:
k : ℕ
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)

Tactic:
induction k with
| zero => simp
| succ k hk =>
  rw [add_pow_two, one_pow, mul_one, add_assoc, mul_add, add_right_comm]
  refine (add_le_add_right hk _).trans ?_
  rw [mul_add 2 k, pow_add, mul_one, pow_two, ← mul_assoc, mul_two, mul_two, add_assoc]
  gcongr
  rw [← two_mul, ← pow_succ']
  exact le_add_of_le_right (mul_le_pow (by simp) _)

Result:
no goals

Proof state:
case succ
k : ℕ
hk : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
⊢ 2 ^ (2 * k) + 2 * (2 * k + 1) ≤ 2 ^ (2 * (k + 1))

Tactic:
rw [mul_add 2 k, pow_add, mul_one, pow_two, ← mul_assoc, mul_two, mul_two, add_assoc]

Result:
case succ
k : ℕ
hk : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
⊢ 2 ^ (2 * k) + 2 * (2 * k + 1) ≤ 2 ^ (2 * k) + (2 ^ (2 * k) + (2 ^ (2 * k) + 2 ^ (2 * k)))

Proof state:
case succ
k : ℕ
hk : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
⊢ 2 * (k + 1) ^ 2 + 1 ≤ 2 ^ (2 * (k + 1))

Tactic:
rw [add_pow_two, one_pow, mul_one, add_assoc, mul_add, add_right_comm]

Result:
case succ
k : ℕ
hk : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
⊢ 2 * k ^ 2 + 1 + 2 * (2 * k + 1) ≤ 2 ^ (2 * (k + 1))

Proof state:
case succ
k : ℕ
hk : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
⊢ 2 ^ (2 * k) + 2 * (2 * k + 1) ≤ 2 ^ (2 * k) + (2 ^ (2 * k) + (2 ^ (2 * k) + 2 ^ (2 * k)))

Tactic:
gcongr

Result:
case succ.bc
k : ℕ
hk : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
⊢ 2 * (2 * k + 1) ≤ 2 ^ (2 * k) + (2 ^ (2 * k) + 2 ^ (2 * k))

Proof state:
case succ
k : ℕ
hk : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
⊢ 2 * k ^ 2 + 1 + 2 * (2 * k + 1) ≤ 2 ^ (2 * (k + 1))

Tactic:
refine (add_le_add_right hk _).trans ?_

Result:
case succ
k : ℕ
hk : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
⊢ 2 ^ (2 * k) + 2 * (2 * k + 1) ≤ 2 ^ (2 * (k + 1))

Proof state:
k : ℕ
hk : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
⊢ 2 ≠ 1

Tactic:
simp

Result:
no goals

Proof state:
case succ.bc
k : ℕ
hk : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
⊢ 2 * (2 * k + 1) ≤ 2 ^ (2 * k) + 2 ^ (2 * k).succ

Tactic:
exact le_add_of_le_right (mul_le_pow (by simp) _)

Result:
no goals

Proof state:
case zero

⊢ 2 * 0 ^ 2 + 1 ≤ 2 ^ (2 * 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ.bc
k : ℕ
hk : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
⊢ 2 * (2 * k + 1) ≤ 2 ^ (2 * k) + (2 ^ (2 * k) + 2 ^ (2 * k))

Tactic:
rw [← two_mul, ← pow_succ']

Result:
case succ.bc
k : ℕ
hk : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
⊢ 2 * (2 * k + 1) ≤ 2 ^ (2 * k) + 2 ^ (2 * k).succ
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem hasSum_at_zero (a : ℕ → E) : HasSum (fun n => (0 : 𝕜) ^ n • a n) (a 0)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a : ℕ → E
⊢ HasSum (fun n => 0 ^ n • a n) (a 0)

Tactic:
convert hasSum_single (α := E) 0 fun b h ↦ _ <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem ucs_eq_self_of_normalizer_eq_self (h : N₁.normalizer = N₁) (k : ℕ) : N₁.ucs k = N₁

Proof state:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
⊢ ucs 0 N₁ = N₁

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ucs k N₁ = N₁

Tactic:
induction k with
| zero => simp
| succ k ih => rwa [ucs_succ, ih]

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
ih : ucs k N₁ = N₁
⊢ ucs (k + 1) N₁ = N₁

Tactic:
rwa [ucs_succ, ih]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem congr_hom {F G : C ⥤ D} (h : F = G) {X Y} (f : X ⟶ Y) :
    F.map f = eqToHom (congr_obj h X) ≫ G.map f ≫ eqToHom (congr_obj h Y).symm

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F = G
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
subst h

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/StoneCech.lean
theorem continuous_ultrafilter_extend (f : α → γ) : Continuous (Ultrafilter.extend f)

Proof state:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ univ ∈ ↑(Ultrafilter.map f b)

Tactic:
exact univ_mem

Result:
no goals

Proof state:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
⊢ Continuous (Ultrafilter.extend f)

Tactic:
have h (b : Ultrafilter α) : ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c) :=
  let ⟨c, _, h'⟩ :=
    isCompact_univ.ultrafilter_le_nhds (b.map f) (by rw [le_principal_iff]; exact univ_mem)
  ⟨c, le_trans (map_mono (ultrafilter_comap_pure_nhds _)) h'⟩

Result:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
⊢ Continuous (Ultrafilter.extend f)

Proof state:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ ↑(Ultrafilter.map f b) ≤ 𝓟 univ

Tactic:
rw [le_principal_iff]

Result:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ univ ∈ ↑(Ultrafilter.map f b)

Proof state:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
⊢ Continuous (Ultrafilter.extend f)

Tactic:
let _ : TopologicalSpace α := ⊥

Result:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
x✝ : TopologicalSpace α := ⊥
⊢ Continuous (Ultrafilter.extend f)

Proof state:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
x✝ : TopologicalSpace α := ⊥
⊢ Continuous (Ultrafilter.extend f)

Tactic:
exact isDenseInducing_pure.continuous_extend h

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem exists_isBasis_union_inter_isBasis (M : Matroid α) (X Y : Set α)
    (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
X Y : Set α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
J : Set α
hJ : M.IsBasis J Y
I : Set α
hI : M.IsBasis I (X ∪ Y) ∧ I ∩ Y = J
⊢ M.IsBasis (I ∩ Y) Y

Tactic:
rwa [hI.2]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem coe_true_iff_false  : ∀{a b : Bool}, (a ↔ b = false) ↔ a = (!b)

Proof state:
⊢ ∀ {a b : Bool}, (a = true ↔ b = false) ↔ a = !b

Tactic:
decide

Result:
no goals