harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_map (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α)
    (f : α → β) : (fromBlocks A B C D).map f =
      fromBlocks (A.map f) (B.map f) (C.map f) (D.map f)

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D).map f i j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks]

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
⊢ (fromBlocks A B C D).map f = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f)

Tactic:
ext i j

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D).map f i j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) i j
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem eq_bot_of_finrank_one (h : finrank F S = 1) [Module.Free F S] : S = ⊥

Proof state:
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : finrank F ↥S = 1
inst✝ : Free F ↥S
⊢ Module.rank F ↥S ≤ 1

Tactic:
rw [finrank, toNat_eq_one] at h

Result:
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S = 1
inst✝ : Free F ↥S
⊢ Module.rank F ↥S ≤ 1

Proof state:
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : finrank F ↥S = 1
inst✝ : Free F ↥S
⊢ S = ⊥

Tactic:
refine Subalgebra.eq_bot_of_rank_le_one ?_

Result:
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : finrank F ↥S = 1
inst✝ : Free F ↥S
⊢ Module.rank F ↥S ≤ 1

Proof state:
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S = 1
inst✝ : Free F ↥S
⊢ Module.rank F ↥S ≤ 1

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp]
lemma nil_append_iff {p : G.Walk u v} {q : G.Walk v w} : (p.append q).Nil ↔ p.Nil ∧ q.Nil

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).Nil ↔ p.Nil ∧ q.Nil

Tactic:
cases p <;> cases q <;> simp

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate'_nil (n : ℕ) : ([] : List α).rotate' n = []

Proof state:
α : Type u
n : ℕ
⊢ [].rotate' n = []

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem j_of_isCharTwoJEqZeroNF_of_char_two [CharP F 2] : W.j = 0

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP F 2
⊢ W.j = 0

Tactic:
rw [j, c₄_of_isCharTwoJEqZeroNF_of_char_two]

Result:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP F 2
⊢ ↑W.Δ'⁻¹ * 0 ^ 3 = 0

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP F 2
⊢ ↑W.Δ'⁻¹ * 0 ^ 3 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem exists_isBasis_subset_isBasis (M : Matroid α) (hXY : X ⊆ Y) (hY : Y ⊆ M.E

Proof state:
case intro.intro.intro
α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.IsBasis I X
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J

Tactic:
exact ⟨_, _, hI, hJ, hIJ⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.IsBasis I X
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans hXY)

Result:
case intro.intro.intro
α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.IsBasis I X
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J

Proof state:
α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis X (hXY.trans hY)

Result:
case intro
α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.IsBasis I X
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_shiftConcat_eq_decide (x : BitVec w) (b : Bool) (i : Nat) :
    (shiftConcat x b).getLsbD i
    = (decide (i < w) && ((decide (i = 0) && b) || (decide (0 < i) && x.getLsbD (i - 1))))

Proof state:
w : Nat
x : BitVec w
b : Bool
i : Nat
⊢ (x.shiftConcat b).getLsbD i = (decide (i < w) && (decide (i = 0) && b || decide (0 < i) && x.getLsbD (i - 1)))

Tactic:
simp only [getLsbD_shiftConcat]

Result:
w : Nat
x : BitVec w
b : Bool
i : Nat
⊢ (decide (i < w) && if i = 0 then b else x.getLsbD (i - 1)) =
    (decide (i < w) && (decide (i = 0) && b || decide (0 < i) && x.getLsbD (i - 1)))

Proof state:
w : Nat
x : BitVec w
b : Bool
i : Nat
h✝ : ¬i = 0
⊢ 0 < i ↔ ¬i = 0

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
b : Bool
i : Nat
⊢ (decide (i < w) && if i = 0 then b else x.getLsbD (i - 1)) =
    (decide (i < w) && (decide (i = 0) && b || decide (0 < i) && x.getLsbD (i - 1)))

Tactic:
split <;> simp [*, show ((0 < i) ↔ ¬(i = 0)) by omega]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- If `A` is connected, the cardinality of `Aut A` is smaller than the cardinality of the
fiber of `A`. -/
lemma card_aut_le_card_fiber_of_connected (A : C) [IsConnected A] :
    Nat.card (Aut A) ≤ Nat.card (F.obj A)

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
⊢ Nat.card (Aut A) ≤ Nat.card (F.obj A).carrier

Tactic:
have h : Nonempty (F.obj A) := inferInstance

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
h : Nonempty (F.obj A).carrier
⊢ Nat.card (Aut A) ≤ Nat.card (F.obj A).carrier

Proof state:
case intro.hf
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Function.Injective ?intro.f

case intro.f
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Aut A → (F.obj A).carrier

Tactic:
exact evaluation_aut_injective_of_isConnected _ _ a

Result:
no goals

Proof state:
case intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Nat.card (Aut A) ≤ Nat.card (F.obj A).carrier

Tactic:
apply Nat.card_le_card_of_injective

Result:
case intro.hf
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Function.Injective ?intro.f

case intro.f
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Aut A → (F.obj A).carrier

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
h : Nonempty (F.obj A).carrier
⊢ Nat.card (Aut A) ≤ Nat.card (F.obj A).carrier

Tactic:
obtain ⟨a⟩ := h

Result:
case intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
a : (F.obj A).carrier
⊢ Nat.card (Aut A) ≤ Nat.card (F.obj A).carrier
-- Mathlib/Computability/Language.lean
@[simp]
lemma reverse_one : (1 : Language α).reverse = 1

Proof state:
α : Type u_1
⊢ reverse 1 = 1

Tactic:
simp [reverse, ← one_def]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Predicate.lean
theorem comp_liftNatTrans (F₁ F₂ F₃ : C ⥤ E) (F₁' F₂' F₃' : D ⥤ E) [h₁ : Lifting L W F₁ F₁']
    [h₂ : Lifting L W F₂ F₂'] [h₃ : Lifting L W F₃ F₃'] (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃) :
    liftNatTrans L W F₁ F₂ F₁' F₂' τ ≫ liftNatTrans L W F₂ F₃ F₂' F₃' τ' =
      liftNatTrans L W F₁ F₃ F₁' F₃' (τ ≫ τ') :=
  natTrans_ext L W fun X => by
    simp only [NatTrans.comp_app, liftNatTrans_app, assoc, Iso.inv_hom_id_app_assoc]

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{u_5, u_3} E
inst✝ : L.IsLocalization W
F₁ F₂ F₃ : C ⥤ E
F₁' F₂' F₃' : D ⥤ E
h₁ : Lifting L W F₁ F₁'
h₂ : Lifting L W F₂ F₂'
h₃ : Lifting L W F₃ F₃'
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
X : C
⊢ (liftNatTrans L W F₁ F₂ F₁' F₂' τ ≫ liftNatTrans L W F₂ F₃ F₂' F₃' τ').app (L.obj X) =
    (liftNatTrans L W F₁ F₃ F₁' F₃' (τ ≫ τ')).app (L.obj X)

Tactic:
simp only [NatTrans.comp_app, liftNatTrans_app, assoc, Iso.inv_hom_id_app_assoc]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean
@[simp] lemma exp_eq_zero_iff {x : EReal} : exp x = 0 ↔ x = ⊥

Proof state:
x : EReal
⊢ x.exp = 0 ↔ x = ⊥

Tactic:
induction x <;> simp [Real.exp_pos]

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem isAddFundamentalDomain [Finite ι] [MeasurableSpace E] [OpensMeasurableSpace E]
    (μ : Measure E) :
    IsAddFundamentalDomain (span ℤ (Set.range b)) (fundamentalDomain b) μ

Proof state:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : Finite ι
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
val✝ : Fintype ι
⊢ IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑b))) (fundamentalDomain b) μ

Tactic:
exact IsAddFundamentalDomain.mk' (nullMeasurableSet (fundamentalDomain_measurableSet b))
  fun x => exist_unique_vadd_mem_fundamentalDomain b x

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : Finite ι
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
⊢ IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑b))) (fundamentalDomain b) μ

Tactic:
cases nonempty_fintype ι

Result:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : Finite ι
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
val✝ : Fintype ι
⊢ IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑b))) (fundamentalDomain b) μ
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_sub_nonpos : |a - b| ≤ 0 ↔ a = b :=
  ⟨eq_of_abs_sub_nonpos, by rintro rfl; rw [sub_self, abs_zero]⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
⊢ |a - a| ≤ 0

Tactic:
rw [sub_self, abs_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ a = b → |a - b| ≤ 0

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
⊢ |a - a| ≤ 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem replicate_congr (n : Nat) (w : Nat) (expr expr' : BitVec w) (h : expr' = expr) :
    BitVec.replicate n expr' = BitVec.replicate n expr

Proof state:
n w : Nat
expr expr' : BitVec w
h : expr' = expr
⊢ BitVec.replicate n expr' = BitVec.replicate n expr

Tactic:
simp[*]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem cardFactors_apply_prime_pow {p k : ℕ} (hp : p.Prime) : Ω (p ^ k) = k

Proof state:
p k : ℕ
hp : Nat.Prime p
⊢ Ω (p ^ k) = k

Tactic:
rw [cardFactors_apply, hp.primeFactorsList_pow, List.length_replicate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_eq_false_iff_exists_isSome_getValue? [BEq α] [ReflBEq α] {l : List ((_ : α) × β)} :
    l.isEmpty = false ↔ ∃ a, (getValue? a l).isSome

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : ReflBEq α
l : List ((_ : α) × β)
⊢ l.isEmpty = false ↔ ∃ a, (getValue? a l).isSome = true

Tactic:
simp [isEmpty_eq_false_iff_exists_isSome_getEntry?, getValue?_eq_getEntry?]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_subset [Fintype s] {t : Finset α} : s.toFinset ⊆ t ↔ s ⊆ t

Proof state:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ s.toFinset ⊆ t ↔ s ⊆ ↑t

Tactic:
rw [← Finset.coe_subset, coe_toFinset]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem Bool.symmDiff_eq_xor : ∀ p q : Bool, p ∆ q = xor p q

Proof state:
⊢ ∀ (p q : Bool), p ∆ q = (p ^^ q)

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst) :
    (insertMany m l).getKey? k' = some k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
⊢ (insertMany m l).getKey? k' = some k

Tactic:
simp_to_raw using Raw₀.Const.getKey?_insertMany_list_of_mem

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
/--
Variant of `map_yonedaEquiv` with general `g`. This is technically strictly more general
than `map_yonedaEquiv`, but `map_yonedaEquiv` is sometimes preferable because it
can avoid the "motive is not type correct" error.
-/
lemma map_yonedaEquiv' {X Y : Cᵒᵖ} {F : Sheaf J (Type v)} (f : J.yoneda.obj (unop X) ⟶ F)
    (g : X ⟶ Y) : F.val.map g (J.yonedaEquiv f) = f.val.app Y g.unop

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
F : Sheaf J (Type v)
f : J.yoneda.obj (unop X) ⟶ F
g : X ⟶ Y
⊢ F.val.map g (J.yonedaEquiv f) = f.val.app Y g.unop

Tactic:
rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
@[reassoc (attr := simp)]
lemma ι_descMapObj {A : C} {j : J}
    (φ : ∀ (i : I) (_ : p i = j), X i ⟶ A) (i : I) (hi : p i = j) :
    X.ιMapObj p i j hi ≫ X.descMapObj p φ = φ i hi

Proof state:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝¹ : Category.{u_5, u_4} C
X : GradedObject I C
p : I → J
inst✝ : X.HasMap p
A : C
j : J
φ : (i : I) → p i = j → (X i ⟶ A)
i : I
hi : p i = j
⊢ X.ιMapObj p i j hi ≫ X.descMapObj p φ = φ i hi

Tactic:
apply Cofan.IsColimit.fac

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem reverse_eq_iff {as bs : Vector α n} : as.reverse = bs ↔ as = bs.reverse

Proof state:
α : Type u_1
n : Nat
as bs : Vector α n
⊢ as.reverse = bs ↔ as = bs.reverse

Tactic:
constructor <;> (rintro rfl; simp)

Result:
no goals

Proof state:
case mpr
α : Type u_1
n : Nat
as bs : Vector α n
⊢ as = bs.reverse → as.reverse = bs

Tactic:
rintro rfl

Result:
case mpr
α : Type u_1
n : Nat
bs : Vector α n
⊢ bs.reverse.reverse = bs

Proof state:
case mpr
α : Type u_1
n : Nat
bs : Vector α n
⊢ bs.reverse.reverse = bs

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem diam_eq {s : Set ℝ} (h : Bornology.IsBounded s) : Metric.diam s = sSup s - sInf s

Proof state:
s : Set ℝ
h : Bornology.IsBounded s
⊢ 0 ≤ sSup s - sInf s

Tactic:
exact sub_nonneg.2 (Real.sInf_le_sSup s h.bddBelow h.bddAbove)

Result:
no goals

Proof state:
s : Set ℝ
h : Bornology.IsBounded s
⊢ Metric.diam s = sSup s - sInf s

Tactic:
rw [Metric.diam, Real.ediam_eq h, ENNReal.toReal_ofReal]

Result:
s : Set ℝ
h : Bornology.IsBounded s
⊢ 0 ≤ sSup s - sInf s
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem toList_erase [BEq α] {l : AssocList α β} {a : α} :
    (l.erase a).toList = eraseKey a l.toList

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (erase a tail✝).toList = eraseKey a tail✝.toList
⊢ (erase a (cons key✝ value✝ tail✝)).toList = eraseKey a (cons key✝ value✝ tail✝).toList

Tactic:
next k v t ih => cases h : k == a <;> simp_all [erase, List.eraseKey_cons]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a k : α
v : β k
t : AssocList α β
ih : (erase a t).toList = eraseKey a t.toList
⊢ (erase a (cons k v t)).toList = eraseKey a (cons k v t).toList

Tactic:
cases h : k == a <;> simp_all [erase, List.eraseKey_cons]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
⊢ (erase a nil).toList = eraseKey a nil.toList

Tactic:
simp [erase]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : AssocList α β
a : α
⊢ (erase a l).toList = eraseKey a l.toList

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
⊢ (erase a nil).toList = eraseKey a nil.toList

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (erase a tail✝).toList = eraseKey a tail✝.toList
⊢ (erase a (cons key✝ value✝ tail✝)).toList = eraseKey a (cons key✝ value✝ tail✝).toList
-- Mathlib/.lake/packages/lean4/src/lean/Lean/Data/PersistentHashMap.lean
theorem size_push {ks : Array α} {vs : Array β} (h : ks.size = vs.size) (k : α) (v : β) : (ks.push k).size = (vs.push v).size

Proof state:
α : Type u_1
β : Type u_2
ks : Array α
vs : Array β
h : ks.size = vs.size
k : α
v : β
⊢ (ks.push k).size = (vs.push v).size

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
@[to_additive (attr := simp)]
lemma prod_attach_univ [Fintype ι] (f : {i // i ∈ @univ ι _} → α) :
    ∏ i ∈ univ.attach, f i = ∏ i, f ⟨i, mem_univ _⟩ :=
  Fintype.prod_equiv (Equiv.subtypeUnivEquiv mem_univ) _ _ <| by simp

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommMonoid α
inst✝ : Fintype ι
f : { i // i ∈ univ } → α
⊢ ∀ (x : Subtype (Membership.mem univ)), f x = f ⟨(Equiv.subtypeUnivEquiv ⋯) x, ⋯⟩

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem map_lowerCentralSeries_le (f : M →ₗ⁅R,L⁆ M₂) :
    (lowerCentralSeries R L M k).map f ≤ lowerCentralSeries R L M₂ k

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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k

Tactic:
induction k with
| zero => simp only [lowerCentralSeries_zero, le_top]
| succ k ih =>
  simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
  exact LieSubmodule.mono_lie_right ⊤ 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
k✝ : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
ih : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
⊢ LieSubmodule.map f (lowerCentralSeries R L M (k + 1)) ≤ lowerCentralSeries R L M₂ (k + 1)

Tactic:
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]

Result:
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
k✝ : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
ih : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
⊢ ⁅⊤, LieSubmodule.map f (lowerCentralSeries R L M k)⁆ ≤ ⁅⊤, lowerCentralSeries R L M₂ k⁆

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
k✝ : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
ih : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
⊢ ⁅⊤, LieSubmodule.map f (lowerCentralSeries R L M k)⁆ ≤ ⁅⊤, lowerCentralSeries R L M₂ k⁆

Tactic:
exact LieSubmodule.mono_lie_right ⊤ ih

Result:
no goals

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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map f (lowerCentralSeries R L M 0) ≤ lowerCentralSeries R L M₂ 0

Tactic:
simp only [lowerCentralSeries_zero, le_top]

Result:
no goals