harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Filtered/Final.lean
theorem Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful [IsCofilteredOrEmpty D] [F.Full]
    [Faithful F] (h : ∀ d, ∃ c, Nonempty (F.obj c ⟶ d)) : Initial F

Proof state:
case intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
d : Dᵒᵖ
c : C
f : F.obj c ⟶ unop d
⊢ ∃ c, Nonempty (d ⟶ F.op.obj c)

Tactic:
exact ⟨op c, ⟨f.op⟩⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ F.op.Final

Tactic:
refine Functor.final_of_exists_of_isFiltered_of_fullyFaithful F.op (fun d => ?_)

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
d : Dᵒᵖ
⊢ ∃ c, Nonempty (d ⟶ F.op.obj c)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ F.Initial

Tactic:
suffices Final F.op from initial_of_final_op _

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ F.op.Final

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
d : Dᵒᵖ
⊢ ∃ c, Nonempty (d ⟶ F.op.obj c)

Tactic:
obtain ⟨c, ⟨f⟩⟩ := h d.unop

Result:
case intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
d : Dᵒᵖ
c : C
f : F.obj c ⟶ unop d
⊢ ∃ c, Nonempty (d ⟶ F.op.obj c)
-- Mathlib/SetTheory/Game/Nim.lean
theorem nim_def (o : Ordinal) : nim o =
    ⟨o.toType, o.toType,
      fun x => nim ((enumIsoToType o).symm x).val,
      fun x => nim ((enumIsoToType o).symm x).val⟩

Proof state:
o : Ordinal.{u_1}
⊢ nim o = mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)

Tactic:
rw [nim]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem mk_d_1_0 : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 0 1 = d₀

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 0 1 = d₀

Tactic:
change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀

Tactic:
rw [if_pos rfl, Category.comp_id]

Result:
no goals
-- Mathlib/Data/Matrix/DoublyStochastic.lean
/-- Every entry of a doubly stochastic matrix is less than or equal to 1. -/
lemma le_one_of_mem_doublyStochastic (hM : M ∈ doublyStochastic R n) {i j : n} :
    M i j ≤ 1

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
i j : n
⊢ M i j ≤ ∑ j : n, M i j

Tactic:
exact single_le_sum (fun k _ => hM.1 _ k) (mem_univ j)

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
i j : n
⊢ M i j ≤ 1

Tactic:
rw [← sum_row_of_mem_doublyStochastic hM i]

Result:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
i j : n
⊢ M i j ≤ ∑ j : n, M i j
-- Mathlib/Data/Multiset/Basic.lean
theorem strongDownwardInduction_eq {p : Multiset α → Sort*} {n : ℕ}
    (H : ∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁)
    (s : Multiset α) :
    strongDownwardInduction H s = H s fun ht _hst => strongDownwardInduction H _ ht

Proof state:
α : Type u_1
p : Multiset α → Sort u_3
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
s : Multiset α
⊢ strongDownwardInduction H s = H s fun {t₂} ht _hst => strongDownwardInduction H t₂ ht

Tactic:
rw [strongDownwardInduction]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem norm_comp_le_of_le' {g : NormedAddGroupHom V₂ V₃} (C₁ C₂ C₃ : ℝ) (h : C₃ = C₂ * C₁)
    (hg : ‖g‖ ≤ C₂) (hf : ‖f‖ ≤ C₁) : ‖g.comp f‖ ≤ C₃

Proof state:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ C₃ : ℝ
h : C₃ = C₂ * C₁
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖g.comp f‖ ≤ C₃

Tactic:
rw [h]

Result:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ C₃ : ℝ
h : C₃ = C₂ * C₁
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖g.comp f‖ ≤ C₂ * C₁

Proof state:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ C₃ : ℝ
h : C₃ = C₂ * C₁
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖g.comp f‖ ≤ C₂ * C₁

Tactic:
exact norm_comp_le_of_le hg hf

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_int_mod (s : Finset α) (n : ℤ) (f : α → ℤ) :
    (∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n :=
  (Multiset.prod_int_mod _ _).trans <| by rw [Finset.prod, Multiset.map_map]; rfl

Proof state:
α : Type u_3
s : Finset α
n : ℤ
f : α → ℤ
⊢ (Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val).prod % n = (Multiset.map (fun i => f i % n) s.val).prod % n

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
s : Finset α
n : ℤ
f : α → ℤ
⊢ (Multiset.map (fun x => x % n) (Multiset.map (fun i => f i) s.val)).prod % n = (∏ i ∈ s, f i % n) % n

Tactic:
rw [Finset.prod, Multiset.map_map]

Result:
α : Type u_3
s : Finset α
n : ℤ
f : α → ℤ
⊢ (Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val).prod % n = (Multiset.map (fun i => f i % n) s.val).prod % n
-- Mathlib/Data/Complex/Norm.lean
theorem dist_conj_self (z : ℂ) : dist (conj z) z = 2 * |z.im|

Proof state:
z : ℂ
⊢ dist ((starRingEnd ℂ) z) z = 2 * |z.im|

Tactic:
rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul,
  _root_.abs_mul, abs_of_pos (zero_lt_two' ℝ)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modifyHead_id : modifyHead (id : α → α) = id

Proof state:
case h
α : Type u_1
l : List α
⊢ modifyHead id l = id l

Tactic:
cases l <;> simp

Result:
no goals

Proof state:
α : Type u_1
⊢ modifyHead id = id

Tactic:
funext l

Result:
case h
α : Type u_1
l : List α
⊢ modifyHead id l = id l
-- Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
theorem Function.Injective.hasProd_iff {g : γ → β} (hg : Injective g)
    (hf : ∀ x, x ∉ Set.range g → f x = 1) : HasProd (f ∘ g) a ↔ HasProd f a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ HasProd (f ∘ g) a ↔ HasProd f a

Tactic:
simp only [HasProd, Tendsto, comp_apply, hg.map_atTop_finset_prod_eq hf]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem isUnit_iff {z : ℤ_[p]} : IsUnit z ↔ ‖z‖ = 1 :=
  ⟨fun h => by
    rcases isUnit_iff_dvd_one.1 h with ⟨w, eq⟩
    refine le_antisymm (norm_le_one _) ?_
    have := mul_le_mul_of_nonneg_left (norm_le_one w) (norm_nonneg z)
    rwa [mul_one, ← norm_mul, ← eq, norm_one] at this, fun h =>
    ⟨⟨z, z.inv, mul_inv h, inv_mul h⟩, rfl⟩⟩

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
⊢ ‖z‖ = 1

Tactic:
rcases isUnit_iff_dvd_one.1 h with ⟨w, eq⟩

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ ‖z‖ = 1

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ 1 ≤ ‖z‖

Tactic:
have := mul_le_mul_of_nonneg_left (norm_le_one w) (norm_nonneg z)

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
this : ‖z‖ * ‖w‖ ≤ ‖z‖ * 1
⊢ 1 ≤ ‖z‖

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ ‖z‖ = 1

Tactic:
refine le_antisymm (norm_le_one _) ?_

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ 1 ≤ ‖z‖

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
this : ‖z‖ * ‖w‖ ≤ ‖z‖ * 1
⊢ 1 ≤ ‖z‖

Tactic:
rwa [mul_one, ← norm_mul, ← eq, norm_one] at this

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem NormedCommGroup.uniformity_basis_dist :
    (𝓤 E).HasBasis (fun ε : ℝ => 0 < ε) fun ε => { p : E × E | ‖p.fst / p.snd‖ < ε }

Proof state:
case h.e'_5
E : Type u_5
inst✝ : SeminormedGroup E
⊢ (fun ε => {p | ‖p.1 / p.2‖ < ε}) = fun ε => {p | dist p.1 p.2 < ε}

Tactic:
simp [dist_eq_norm_div]

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ (𝓤 E).HasBasis (fun ε => 0 < ε) fun ε => {p | ‖p.1 / p.2‖ < ε}

Tactic:
convert Metric.uniformity_basis_dist (α := E) using 1

Result:
case h.e'_5
E : Type u_5
inst✝ : SeminormedGroup E
⊢ (fun ε => {p | ‖p.1 / p.2‖ < ε}) = fun ε => {p | dist p.1 p.2 < ε}
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.sameCycle (hf : IsCycle f) (hx : f x ≠ x) (hy : f y ≠ y) :
    SameCycle f x y :=
  let ⟨g, hg⟩ := hf
  let ⟨a, ha⟩ := hg.2 hx
  let ⟨b, hb⟩ := hg.2 hy
  ⟨b - a, by rw [← ha, ← mul_apply, ← zpow_add, sub_add_cancel, hb]⟩

Proof state:
α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
g : α
hg : f g ≠ g ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a) g = x
b : ℤ
hb : (f ^ b) g = y
⊢ (f ^ (b - a)) x = y

Tactic:
rw [← ha, ← mul_apply, ← zpow_add, sub_add_cancel, hb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_dvd_pow_iff_le_right {x k l : Nat} (w : 1 < x) : x ^ k ∣ x ^ l ↔ k ≤ l

Proof state:
x k l : Nat
w : 1 < x
⊢ x ^ k ∣ x ^ l ↔ k ≤ l

Tactic:
rw [pow_dvd_pow_iff_pow_le_pow (lt_of_succ_lt w), Nat.pow_le_pow_iff_right w]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
theorem le_or_le_of_add_eq_add_pred (h : a + c = b + d - 1) : b ≤ a ∨ d ≤ c

Proof state:
a b c d : ℕ
h : a + c = b + d - 1
⊢ b ≤ a ∨ d ≤ c

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
theorem evenToNeg_comp_evenToNeg (Q' : QuadraticForm R M) (h : Q' = -Q) (h' : Q = -Q') :
    (evenToNeg Q' Q h').comp (evenToNeg Q Q' h) = AlgHom.id R _

Proof state:
case h.bilin.h.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
h' : Q = -Q'
m₁ m₂ : M
⊢ (((even.ι Q).compr₂ ((evenToNeg Q' Q h').comp (evenToNeg Q Q' h))).bilin m₁) m₂ =
    (((even.ι Q).compr₂ (AlgHom.id R ↥(even Q))).bilin m₁) m₂

Tactic:
simp [evenToNeg_ι]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
h' : Q = -Q'
⊢ (evenToNeg Q' Q h').comp (evenToNeg Q Q' h) = AlgHom.id R ↥(even Q)

Tactic:
ext m₁ m₂ : 4

Result:
case h.bilin.h.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
h' : Q = -Q'
m₁ m₂ : M
⊢ (((even.ι Q).compr₂ ((evenToNeg Q' Q h').comp (evenToNeg Q Q' h))).bilin m₁) m₂ =
    (((even.ι Q).compr₂ (AlgHom.id R ↥(even Q))).bilin m₁) m₂
-- Mathlib/RingTheory/Ideal/Maximal.lean
theorem maximal_of_no_maximal {P : Ideal α}
    (hmax : ∀ m : Ideal α, P < m → ¬IsMaximal m) (J : Ideal α) (hPJ : P < J) : J = ⊤

Proof state:
α : Type u
inst✝ : Semiring α
P : Ideal α
hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal
J : Ideal α
hPJ : P < J
hnonmax : ¬J = ⊤
⊢ False

Tactic:
rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩

Result:
case intro.intro
α : Type u
inst✝ : Semiring α
P : Ideal α
hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal
J : Ideal α
hPJ : P < J
hnonmax : ¬J = ⊤
M : Ideal α
hM1 : M.IsMaximal
hM2 : J ≤ M
⊢ False

Proof state:
α : Type u
inst✝ : Semiring α
P : Ideal α
hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal
J : Ideal α
hPJ : P < J
⊢ J = ⊤

Tactic:
by_contra hnonmax

Result:
α : Type u
inst✝ : Semiring α
P : Ideal α
hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal
J : Ideal α
hPJ : P < J
hnonmax : ¬J = ⊤
⊢ False

Proof state:
case intro.intro
α : Type u
inst✝ : Semiring α
P : Ideal α
hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal
J : Ideal α
hPJ : P < J
hnonmax : ¬J = ⊤
M : Ideal α
hM1 : M.IsMaximal
hM2 : J ≤ M
⊢ False

Tactic:
exact hmax M (lt_of_lt_of_le hPJ hM2) hM1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem dropLast_concat_getLast : ∀ {l : List α} (h : l ≠ []), dropLast l ++ [getLast l h] = l
  | [], h => absurd rfl h
  | [_], _ => rfl
  | _ :: b :: l, _ => by
    rw [dropLast_cons₂, cons_append, getLast_cons (cons_ne_nil _ _)]
    congr
    exact dropLast_concat_getLast (cons_ne_nil b l)

Proof state:
α : Type u_1
head✝ b : α
l : List α
x✝ : head✝ :: b :: l ≠ []
⊢ head✝ :: ((b :: l).dropLast ++ [(b :: l).getLast ⋯]) = head✝ :: b :: l

Tactic:
congr

Result:
case e_tail
α : Type u_1
head✝ b : α
l : List α
x✝ : head✝ :: b :: l ≠ []
⊢ (b :: l).dropLast ++ [(b :: l).getLast ⋯] = b :: l

Proof state:
case e_tail
α : Type u_1
head✝ b : α
l : List α
x✝ : head✝ :: b :: l ≠ []
⊢ (b :: l).dropLast ++ [(b :: l).getLast ⋯] = b :: l

Tactic:
exact dropLast_concat_getLast (cons_ne_nil b l)

Result:
no goals

Proof state:
α : Type u_1
head✝ b : α
l : List α
x✝ : head✝ :: b :: l ≠ []
⊢ (head✝ :: b :: l).dropLast ++ [(head✝ :: b :: l).getLast x✝] = head✝ :: b :: l

Tactic:
rw [dropLast_cons₂, cons_append, getLast_cons (cons_ne_nil _ _)]

Result:
α : Type u_1
head✝ b : α
l : List α
x✝ : head✝ :: b :: l ≠ []
⊢ head✝ :: ((b :: l).dropLast ++ [(b :: l).getLast ⋯]) = head✝ :: b :: l
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem lcs_le_iff (k : ℕ) : N₁.lcs k ≤ N₂ ↔ N₁ ≤ N₂.ucs k

Proof state:
case h.e'_1.h.e'_3.h.e'_10
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₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ k = 0 + k

Tactic:
rw [zero_add]

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₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ lcs k N₁ ≤ N₂ ↔ N₁ ≤ ucs k N₂

Tactic:
convert lcs_add_le_iff (R := R) (L := L) (M := M) 0 k

Result:
case h.e'_1.h.e'_3.h.e'_10
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₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ k = 0 + k
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.add_left_eq_self (a b : BitVec w) : (a + b == b) = (a == 0#w)

Proof state:
w : Nat
a b : BitVec w
⊢ (a + b == b) = true ↔ (a == 0#w) = true

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
a b : BitVec w
⊢ (a + b == b) = (a == 0#w)

Tactic:
rw [Bool.eq_iff_iff]

Result:
w : Nat
a b : BitVec w
⊢ (a + b == b) = true ↔ (a == 0#w) = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_cons (a b : α) (l : List α) :
    count a (b :: l) = count a l + if b == a then 1 else 0

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
⊢ count a (b :: l) = count a l + if (b == a) = true then 1 else 0

Tactic:
simp [count, countP_cons]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem padicNormE_lim_le {f : CauSeq ℚ_[p] norm} {a : ℝ} (ha : 0 < a) (hf : ∀ i, ‖f i‖ ≤ a) :
    ‖f.lim‖ ≤ a

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ j ≥ N, ‖↑(const norm f.lim - f) j‖ < a
⊢ ‖f.lim‖ ≤ a

Tactic:
calc
  ‖f.lim‖ = ‖f.lim - f N + f N‖ := by simp
  _ ≤ max ‖f.lim - f N‖ ‖f N‖ := padicNormE.nonarchimedean _ _
  _ ≤ a := max_le (le_of_lt (hN _ le_rfl)) (hf _)

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ j ≥ N, ‖↑(const norm f.lim - f) j‖ < a
⊢ ‖f.lim‖ = ‖f.lim - ↑f N + ↑f N‖

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
⊢ ‖f.lim‖ ≤ a

Tactic:
obtain ⟨N, hN⟩ := Setoid.symm (CauSeq.equiv_lim f) _ ha

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ j ≥ N, ‖↑(const norm f.lim - f) j‖ < a
⊢ ‖f.lim‖ ≤ a
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem hom_ext_iff {P Q : Karoubi C} {f g : P ⟶ Q} : f = g ↔ f.f = g.f

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
h : f = g
⊢ f.f = g.f

Tactic:
rw [h]

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g

Tactic:
apply Hom.ext

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g ↔ f.f = g.f

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g → f.f = g.f

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f = g.f → f = g

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f = g → f.f = g.f

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f g : P ⟶ Q
h : f = g
⊢ f.f = g.f
-- Mathlib/Data/Nat/Init.lean
@[simp] lemma max_eq_zero_iff : max m n = 0 ↔ m = 0 ∧ n = 0

Proof state:
m n : ℕ
⊢ max m n = 0 ↔ m = 0 ∧ n = 0

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem eq_divRadical {a x : E} (h : radical a * x = a) : x = divRadical a

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a x : E
h : radical a * x = a
⊢ x * radical a = a

Tactic:
rwa [mul_comm]

Result:
no goals

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a x : E
h : radical a * x = a
⊢ x = divRadical a

Tactic:
apply EuclideanDomain.eq_div_of_mul_eq_left (radical_ne_zero a)

Result:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a x : E
h : radical a * x = a
⊢ x * radical a = a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : Array β₁) (init : α) :
    (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init

Proof state:
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g : α → β₂ → α
l : Array β₁
init : α
⊢ foldl g init (map f l) = foldl (fun x y => g x (f y)) init l

Tactic:
cases l

Result:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g : α → β₂ → α
init : α
toList✝ : List β₁
⊢ foldl g init (map f { toList := toList✝ }) = foldl (fun x y => g x (f y)) init { toList := toList✝ }

Proof state:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g : α → β₂ → α
init : α
toList✝ : List β₁
⊢ foldl g init (map f { toList := toList✝ }) = foldl (fun x y => g x (f y)) init { toList := toList✝ }

Tactic:
simp [List.foldl_map]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem ofReal_toReal_ae_eq {f : α → ℝ≥0∞} (hf : ∀ᵐ x ∂μ, f x < ∞) :
    (fun x => ENNReal.ofReal (f x).toReal) =ᵐ[μ] f

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ ∀ (a : α), f a < ⊤ → ENNReal.ofReal (f a).toReal = f a

Tactic:
intro x hx

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
x : α
hx : f x < ⊤
⊢ ENNReal.ofReal (f x).toReal = f x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ (fun x => ENNReal.ofReal (f x).toReal) =ᶠ[ae μ] f

Tactic:
filter_upwards [hf]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ ∀ (a : α), f a < ⊤ → ENNReal.ofReal (f a).toReal = f a

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
x : α
hx : f x < ⊤
⊢ ENNReal.ofReal (f x).toReal = f x

Tactic:
simp only [hx.ne, ofReal_toReal, Ne, not_false_iff]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_right_fderiv {f : F → G} {x : E} :
    fderiv 𝕜 (f ∘ iso) x = (fderiv 𝕜 f (iso x)).comp (iso : E →L[𝕜] F)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
x : E
⊢ UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' univ) x

Tactic:
exact uniqueDiffWithinAt_univ

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
x : E
⊢ fderiv 𝕜 (f ∘ ⇑iso) x = (fderiv 𝕜 f (iso x)).comp ↑iso

Tactic:
rw [← fderivWithin_univ, ← fderivWithin_univ, ← iso.comp_right_fderivWithin, preimage_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
x : E
⊢ UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' univ) x