harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean
lemma equiv_chgUniv (L : C ⥤ D) [L.IsLocalization W] [L.CommShift M] {X Y : C} {m : M}
    [HasSmallLocalizedShiftedHom.{w} W M X Y]
    [HasSmallLocalizedShiftedHom.{w''} W M X Y]
    (e : SmallShiftedHom.{w} W X Y m) :
    equiv W L (chgUniv.{w''} e) = equiv W L e

Proof state:
case h.e_6.h
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
L : C ⥤ D
inst✝³ : L.IsLocalization W
inst✝² : L.CommShift M
X Y : C
m : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M X Y
e : SmallShiftedHom W X Y m
⊢ (SmallHom.equiv W L) (chgUniv e) = (SmallHom.equiv W L) e

Tactic:
apply SmallHom.equiv_chgUniv

Result:
no goals

Proof state:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
L : C ⥤ D
inst✝³ : L.IsLocalization W
inst✝² : L.CommShift M
X Y : C
m : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M X Y
e : SmallShiftedHom W X Y m
⊢ ((L.commShiftIso m).app Y).homToEquiv ((SmallHom.equiv W L) (chgUniv e)) =
    ((L.commShiftIso m).app Y).homToEquiv ((SmallHom.equiv W L) e)

Tactic:
congr

Result:
case h.e_6.h
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
L : C ⥤ D
inst✝³ : L.IsLocalization W
inst✝² : L.CommShift M
X Y : C
m : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M X Y
e : SmallShiftedHom W X Y m
⊢ (SmallHom.equiv W L) (chgUniv e) = (SmallHom.equiv W L) e

Proof state:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
L : C ⥤ D
inst✝³ : L.IsLocalization W
inst✝² : L.CommShift M
X Y : C
m : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M X Y
e : SmallShiftedHom W X Y m
⊢ (equiv W L) (chgUniv e) = (equiv W L) e

Tactic:
dsimp [equiv]

Result:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
L : C ⥤ D
inst✝³ : L.IsLocalization W
inst✝² : L.CommShift M
X Y : C
m : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M X Y
e : SmallShiftedHom W X Y m
⊢ ((L.commShiftIso m).app Y).homToEquiv ((SmallHom.equiv W L) (chgUniv e)) =
    ((L.commShiftIso m).app Y).homToEquiv ((SmallHom.equiv W L) e)
-- Mathlib/Topology/TietzeExtension.lean
theorem ContinuousMap.exists_extension' (he : IsClosedEmbedding e) (f : C(X₁, Y)) :
    ∃ (g : C(X, Y)), g ∘ e = f :=
  f.exists_extension he |>.imp fun g hg ↦ by ext x; congrm($(hg) x)

Proof state:
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
g : C(X, Y)
hg : g.comp { toFun := e, continuous_toFun := ⋯ } = f
⊢ ⇑g ∘ e = ⇑f

Tactic:
ext x

Result:
case h
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
g : C(X, Y)
hg : g.comp { toFun := e, continuous_toFun := ⋯ } = f
x : X₁
⊢ (⇑g ∘ e) x = f x

Proof state:
case h
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
g : C(X, Y)
hg : g.comp { toFun := e, continuous_toFun := ⋯ } = f
x : X₁
⊢ (⇑g ∘ e) x = f x

Tactic:
congrm($(hg) x)

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma intCast_val_sub_eq_sub_add_ite {n : ℕ} (a b : Fin n) :
    ((a - b).val : ℤ) = a.val - b.val + if b ≤ a then 0 else n

Proof state:
n : ℕ
a b : Fin n
⊢ ↑↑(a - b) = ↑↑a - ↑↑b + ↑(if b ≤ a then 0 else n)

Tactic:
split <;> fin_omega

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Lemmas.lean
lemma parallelComp_id_right_comp_parallelComp {η : Kernel α' γ} [IsSFiniteKernel η]
    {ξ : Kernel γ δ} [IsSFiniteKernel ξ] :
    (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = (ξ ∘ₖ η) ∥ₖ κ

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
α' : Type u_5
mα' : MeasurableSpace α'
inst✝² : IsSFiniteKernel κ
η : Kernel α' γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel γ δ
inst✝ : IsSFiniteKernel ξ
a : α' × α
s✝ : Set (δ × β)
a✝ : MeasurableSet s✝
⊢ ((ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ)) a) s✝ = ((ξ ∘ₖ η ∥ₖ κ) a) s✝

Tactic:
rw [parallelComp_apply, comp_apply, comp_apply, parallelComp_apply, Measure.prod_comp_left]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
α' : Type u_5
mα' : MeasurableSpace α'
inst✝² : IsSFiniteKernel κ
η : Kernel α' γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel γ δ
inst✝ : IsSFiniteKernel ξ
⊢ ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ) = ξ ∘ₖ η ∥ₖ κ

Tactic:
ext a

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
α' : Type u_5
mα' : MeasurableSpace α'
inst✝² : IsSFiniteKernel κ
η : Kernel α' γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel γ δ
inst✝ : IsSFiniteKernel ξ
a : α' × α
s✝ : Set (δ × β)
a✝ : MeasurableSet s✝
⊢ ((ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ)) a) s✝ = ((ξ ∘ₖ η ∥ₖ κ) a) s✝
-- Mathlib/Topology/Order.lean
theorem map_nhds_induced_of_mem {a : α} (h : range f ∈ 𝓝 (f a)) :
    map f (@nhds α (induced f t) a) = 𝓝 (f a)

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
h : range f ∈ 𝓝 (f a)
⊢ map f (𝓝 a) = 𝓝 (f a)

Tactic:
rw [nhds_induced, Filter.map_comap_of_mem h]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem exists_finite_card_le_of_finite_of_linearIndependent_of_span (ht : t.Finite)
    (hs : LinearIndepOn K id s) (hst : s ⊆ span K t) :
    ∃ h : s.Finite, h.toFinset.card ≤ ht.toFinset.card :=
  have : s ⊆ (span K ↑ht.toFinset : Submodule K V)

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑ht.toFinset)
u : Finset V
_hust : ↑u ⊆ s ∪ ↑ht.toFinset
hsu : s ⊆ ↑u
Eq : u.card = ht.toFinset.card
this : s.Finite
⊢ this.toFinset.card ≤ u.card

Tactic:
exact Finset.card_le_card <| Finset.coe_subset.mp <| by simp [hsu]

Result:
no goals

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
⊢ s ⊆ ↑(span K ↑ht.toFinset)

Tactic:
simpa

Result:
no goals

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑ht.toFinset)
u : Finset V
_hust : ↑u ⊆ s ∪ ↑ht.toFinset
hsu : s ⊆ ↑u
Eq : u.card = ht.toFinset.card
this : s.Finite
⊢ ↑this.toFinset ⊆ ↑u

Tactic:
simp [hsu]

Result:
no goals

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑ht.toFinset)
u : Finset V
_hust : ↑u ⊆ s ∪ ↑ht.toFinset
hsu : s ⊆ ↑u
Eq : u.card = ht.toFinset.card
this : s.Finite
⊢ this.toFinset.card ≤ ht.toFinset.card

Tactic:
rw [← Eq]

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑ht.toFinset)
u : Finset V
_hust : ↑u ⊆ s ∪ ↑ht.toFinset
hsu : s ⊆ ↑u
Eq : u.card = ht.toFinset.card
this : s.Finite
⊢ this.toFinset.card ≤ u.card
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem cauchySeq_iff_tendsto [Nonempty β] [SemilatticeSup β] {u : β → α} :
    CauchySeq u ↔ Tendsto (Prod.map u u) atTop (𝓤 α) :=
  cauchy_map_iff'.trans <| by simp only [prod_atTop_atTop_eq, Prod.map_def]

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun p => (u p.1, u p.2)) (atTop ×ˢ atTop) (𝓤 α) ↔ Tendsto (Prod.map u u) atTop (𝓤 α)

Tactic:
simp only [prod_atTop_atTop_eq, Prod.map_def]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
lemma rootSpace_two_smul (hα : α.IsNonZero) : rootSpace H (2 • α) = ⊥

Proof state:
case inr
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
hα : α.IsNonZero
h✝ : Nontrivial L
⊢ rootSpace H (2 • ⇑α) = ⊥

Tactic:
simpa [chainTopCoeff_zero_right α hα] using
  genWeightSpace_chainTopCoeff_add_one_nsmul_add α (0 : Weight K H L) hα

Result:
no goals

Proof state:
case inl
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
hα : α.IsNonZero
h✝ : Subsingleton L
⊢ rootSpace H (2 • ⇑α) = ⊥

Tactic:
exact IsEmpty.elim inferInstance α

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ rootSpace H (2 • ⇑α) = ⊥

Tactic:
cases subsingleton_or_nontrivial L

Result:
case inl
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
hα : α.IsNonZero
h✝ : Subsingleton L
⊢ rootSpace H (2 • ⇑α) = ⊥

case inr
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
hα : α.IsNonZero
h✝ : Nontrivial L
⊢ rootSpace H (2 • ⇑α) = ⊥
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma NonUnitalStarAlgHom.ext_continuousMap [UniqueHom R A]
    (a : A) [CompactSpace (σₙ R a)] (φ ψ : C(σₙ R a, R)₀ →⋆ₙₐ[R] A)
    (hφ : Continuous φ) (hψ : Continuous ψ)
    (h : φ ⟨.restrict (σₙ R a) <| .id R, rfl⟩ = ψ ⟨.restrict (σₙ R a) <| .id R, rfl⟩) :
    φ = ψ :=
  UniqueHom.eq_of_continuous_of_map_id _ (by simp) φ ψ hφ hψ h

Proof state:
R : Type u_1
A : Type u_2
inst✝¹³ : CommSemiring R
inst✝¹² : Nontrivial R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : UniqueHom R A
a : A
inst✝ : CompactSpace ↑(σₙ R a)
φ ψ : C(↑(σₙ R a), R)₀ →⋆ₙₐ[R] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h :
  φ { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } =
    ψ { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ }
⊢ ↑0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertMany_empty_list_nil :
    (insertMany empty ([] : List ((a : α) × (β a)))).1 = empty

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ (empty.insertMany []).val = empty

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem pow_gcd_card_eq_one_iff : x ^ n = 1 ↔ x ^ gcd n (Fintype.card G) = 1 :=
  ⟨fun h => pow_gcd_eq_one _ h <| pow_card_eq_one, fun h => by
    let ⟨m, hm⟩ := gcd_dvd_left n (Fintype.card G)
    rw [hm, pow_mul, h, one_pow]⟩

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
n : ℕ
h : x ^ n.gcd (card G) = 1
m : ℕ
hm : n = n.gcd (card G) * m
⊢ x ^ n = 1

Tactic:
rw [hm, pow_mul, h, one_pow]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
n : ℕ
h : x ^ n.gcd (card G) = 1
⊢ x ^ n = 1

Tactic:
let ⟨m, hm⟩ := gcd_dvd_left n (Fintype.card G)

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
n : ℕ
h : x ^ n.gcd (card G) = 1
m : ℕ
hm : n = n.gcd (card G) * m
⊢ x ^ n = 1
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteArray.lean
theorem get_append_right {a b : ByteArray} (hle : a.size ≤ i) (h : i < (a ++ b).size)
    (h' : i - a.size < b.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
    (a ++ b)[i] = b[i - a.size]

Proof state:
i : Nat
a b : ByteArray
hle : a.size ≤ i
h : i < (a ++ b).size
h' : optParam (i - a.size < b.size) ⋯
⊢ (a.data ++ b.data)[i] = b.data[i - a.size]

Tactic:
exact Array.getElem_append_right hle

Result:
no goals

Proof state:
i : Nat
a b : ByteArray
hle : a.size ≤ i
h : i < (a ++ b).size
h' : optParam (i - a.size < b.size) ⋯
⊢ (a ++ b)[i] = b[i - a.size]

Tactic:
simp [getElem_eq_data_getElem]

Result:
i : Nat
a b : ByteArray
hle : a.size ≤ i
h : i < (a ++ b).size
h' : optParam (i - a.size < b.size) ⋯
⊢ (a.data ++ b.data)[i] = b.data[i - a.size]
-- Mathlib/Topology/Order/Compact.lean
theorem Continuous.exists_forall_le' [ClosedIicTopology α] {f : β → α} (hf : Continuous f)
    (x₀ : β) (h : ∀ᶠ x in cocompact β, f x₀ ≤ f x) : ∃ x : β, ∀ y : β, f x ≤ f y :=
  let ⟨x, _, hx⟩ := hf.continuousOn.exists_isMinOn' isClosed_univ (mem_univ x₀)
    (by rwa [principal_univ, inf_top_eq])
  ⟨x, fun y => hx (mem_univ y)⟩

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
f : β → α
hf : Continuous f
x₀ : β
h : ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x
⊢ ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 univ, f x₀ ≤ f x

Tactic:
rwa [principal_univ, inf_top_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseIdx_eq_take_drop_succ :
    ∀ (l : List α) (i : Nat), l.eraseIdx i = l.take i ++ l.drop (i + 1)
  | nil, _ => by simp
  | a::l, 0 => by simp
  | a::l, i + 1 => by simp [eraseIdx_eq_take_drop_succ l i]

Proof state:
α : Type u_1
x✝ : Nat
⊢ [].eraseIdx x✝ = take x✝ [] ++ drop (x✝ + 1) []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
l : List α
i : Nat
⊢ (a :: l).eraseIdx (i + 1) = take (i + 1) (a :: l) ++ drop (i + 1 + 1) (a :: l)

Tactic:
simp [eraseIdx_eq_take_drop_succ l i]

Result:
no goals

Proof state:
α : Type u_1
a : α
l : List α
⊢ (a :: l).eraseIdx 0 = take 0 (a :: l) ++ drop (0 + 1) (a :: l)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Multiset.lean
lemma nsmul_singleton (a : α) (n) : n • ({a} : Multiset α) = replicate n a

Proof state:
α : Type u_1
a : α
n : ℕ
⊢ n • {a} = replicate n a

Tactic:
rw [← replicate_one, nsmul_replicate, mul_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem range_inr : range (inr R M M₂) = ker (fst R M M₂)

Proof state:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ x ∈ range (inr R M M₂) ↔ x ∈ ker (fst R M M₂)

Tactic:
simp only [mem_ker, mem_range]

Result:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inr R M M₂) y = x) ↔ (fst R M M₂) x = 0

Proof state:
case h.mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
h : (fst R M M₂) x = 0
⊢ ∃ y, (inr R M M₂) y = x

Tactic:
exact ⟨x.snd, Prod.ext h.symm rfl⟩

Result:
no goals

Proof state:
case h.mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inr R M M₂) y = x) → (fst R M M₂) x = 0

Tactic:
rintro ⟨y, rfl⟩

Result:
case h.mp.intro
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
y : M₂
⊢ (fst R M M₂) ((inr R M M₂) y) = 0

Proof state:
case h.mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (fst R M M₂) x = 0 → ∃ y, (inr R M M₂) y = x

Tactic:
intro h

Result:
case h.mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
h : (fst R M M₂) x = 0
⊢ ∃ y, (inr R M M₂) y = x

Proof state:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inr R M M₂) y = x) ↔ (fst R M M₂) x = 0

Tactic:
constructor

Result:
case h.mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inr R M M₂) y = x) → (fst R M M₂) x = 0

case h.mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (fst R M M₂) x = 0 → ∃ y, (inr R M M₂) y = x

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ range (inr R M M₂) = ker (fst R M M₂)

Tactic:
ext x

Result:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ x ∈ range (inr R M M₂) ↔ x ∈ ker (fst R M M₂)

Proof state:
case h.mp.intro
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
y : M₂
⊢ (fst R M M₂) ((inr R M M₂) y) = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} {v : β k} :
    (m.insert k v).getKeyD a fallback =
      if k == a then k else m.getKeyD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a fallback : α
v : β k
⊢ (m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback

Tactic:
simp_to_raw using Raw₀.getKeyD_insert

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem comm_symm :
    (TensorProduct.comm R A B).symm = TensorProduct.comm R B A

Proof state:
case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a✝ : B ⊗[R] A
⊢ (TensorProduct.comm R A B).symm a✝ = (TensorProduct.comm R B A) a✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ (TensorProduct.comm R A B).symm = TensorProduct.comm R B A

Tactic:
ext

Result:
case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a✝ : B ⊗[R] A
⊢ (TensorProduct.comm R A B).symm a✝ = (TensorProduct.comm R B A) a✝
-- Mathlib/CategoryTheory/Iso.lean
theorem cancel_iso_inv_right_assoc {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
    (g' : X' ⟶ Y) (h : Z ≅ Y) : f ≫ g ≫ h.inv = f' ≫ g' ≫ h.inv ↔ f ≫ g = f' ≫ g'

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W X X' Y Z : C
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
h : Z ≅ Y
⊢ f ≫ g ≫ h.inv = f' ≫ g' ≫ h.inv ↔ f ≫ g = f' ≫ g'

Tactic:
simp only [← Category.assoc, cancel_mono]

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem clog_anti_left {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : clog b n ≤ clog c n

Proof state:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ clog b n ≤ clog c n

Tactic:
rw [← le_pow_iff_clog_le (lt_of_lt_of_le hc hb)]

Result:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ n ≤ b ^ clog c n

Proof state:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ n ≤ b ^ clog c n

Tactic:
calc
  n ≤ c ^ clog c n := le_pow_clog hc _
  _ ≤ b ^ clog c n := Nat.pow_le_pow_left hb _

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem pow_one : M ^ 1 = M

Proof state:
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
⊢ M ^ 1 = M

Tactic:
rw [Submodule.pow_succ, Submodule.pow_zero, Submodule.one_mul]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem blsub_lt_ord_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c)
    (ho : o.card < c) : (∀ i hi, f i hi < c.ord) → Ordinal.blsub o f < c.ord :=
  blsub_lt_ord (by rwa [hc.cof_eq])

Proof state:
o : Ordinal.{max u_1 u_2}
f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
ho : o.card < c
⊢ o.card < c.ord.cof

Tactic:
rwa [hc.cof_eq]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem add_left_aux2 (x y z : E) : ‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖
    = 2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)

Tactic:
convert parallelogram_identity (x + y - z) (x + z) using 4 <;> abel

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem edgeDensity_nonneg (s : Finset α) (t : Finset β) : 0 ≤ edgeDensity r s t

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ edgeDensity r s t

Tactic:
apply div_nonneg <;> exact mod_cast Nat.zero_le _

Result:
no goals