harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_eq_isSome_get? [LawfulBEq α] (h : m.1.WF) {a : α} :
    m.contains a = (m.get? a).isSome

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
⊢ m.contains a = (m.get? a).isSome

Tactic:
simp_to_model using List.containsKey_eq_isSome_getValueCast?

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
lemma optionEquivLeft_X_some (x : S₁) : optionEquivLeft R S₁ (X (some x)) = Polynomial.C (X x)

Proof state:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ (optionEquivLeft R S₁) (X (Option.some x)) = Polynomial.C (X x)

Tactic:
simp [optionEquivLeft_apply, aeval_X]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem toMatrix_self [DecidableEq ι] : e.toMatrix e = 1

Proof state:
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
inst✝ : DecidableEq ι
⊢ (fun i j => (e.repr (e j)) i) = 1

Tactic:
ext i j

Result:
case a
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
inst✝ : DecidableEq ι
i j : ι
⊢ (e.repr (e j)) i = 1 i j

Proof state:
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
inst✝ : DecidableEq ι
⊢ e.toMatrix ⇑e = 1

Tactic:
unfold Basis.toMatrix

Result:
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
inst✝ : DecidableEq ι
⊢ (fun i j => (e.repr (e j)) i) = 1

Proof state:
case a
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
inst✝ : DecidableEq ι
i j : ι
⊢ (e.repr (e j)) i = 1 i j

Tactic:
simp [Basis.equivFun, Matrix.one_apply, Finsupp.single_apply, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma nilRankAux_le [Nontrivial R] (b : Basis ι R L) (b' : Basis ι' R L) :
    nilRankAux φ b ≤ nilRankAux φ b'

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ φ.nilRankAux b ≤ φ.nilRankAux b'

Tactic:
apply Polynomial.natTrailingDegree_le_of_ne_zero

Result:
case h
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ (φ.polyCharpoly b).coeff (φ.nilRankAux b') ≠ 0

Proof state:
case h
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ (φ.polyCharpoly b).coeff (φ.nilRankAux b') ≠ 0

Tactic:
rw [Ne, (polyCharpoly_coeff_eq_zero_iff_of_basis φ b b' _).not]

Result:
case h
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ ¬(φ.polyCharpoly b').coeff (φ.nilRankAux b') = 0

Proof state:
case h
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ ¬(φ.polyCharpoly b').coeff (φ.nilRankAux b') = 0

Tactic:
apply polyCharpoly_coeff_nilRankAux_ne_zero

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
theorem zero_at_infty_comp_ofComplex [CuspFormClass F Γ k] : ZeroAtFilter I∞ (f ∘ ofComplex)

Proof state:
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup SL(2, ℤ)
f : F
inst✝ : CuspFormClass F Γ k
⊢ I∞.ZeroAtFilter (⇑f ∘ ↑ofComplex)

Tactic:
simpa only [SlashAction.slash_one, toSlashInvariantForm_coe]
  using (zero_at_infty f 1).comp tendsto_comap_im_ofComplex

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem Finset.norm_prod_le {α : Type*} [NormedCommRing α] [NormOneClass α] (s : Finset ι)
    (f : ι → α) : ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖

Proof state:
case mk.mk
ι : Type u_4
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
⊢ ‖∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, f i‖ ≤
    ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, ‖f i‖

Tactic:
simpa using (l.map f).norm_prod_le

Result:
no goals

Proof state:
ι : Type u_4
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
s : Finset ι
f : ι → α
⊢ ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖

Tactic:
rcases s with ⟨⟨l⟩, hl⟩

Result:
case mk.mk
ι : Type u_4
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
⊢ ‖∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, f i‖ ≤
    ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, ‖f i‖
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_eq_of_inf_eq (h : A ⊓ C = B ⊓ C) : relrank A C = relrank B C

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h : A ⊓ C = B ⊓ C
⊢ Module.rank ↥(A ⊓ C) ↥(extendScalars ⋯) = Module.rank ↥(B ⊓ C) ↥(extendScalars ⋯)

Tactic:
congr!

Result:
no goals

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h : A ⊓ C = B ⊓ C
⊢ A.relrank C = B.relrank C

Tactic:
simp_rw [relrank]

Result:
E : Type v
inst✝ : Field E
A B C : Subfield E
h : A ⊓ C = B ⊓ C
⊢ Module.rank ↥(A ⊓ C) ↥(extendScalars ⋯) = Module.rank ↥(B ⊓ C) ↥(extendScalars ⋯)
-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem splitEpiCategoryImpOfIsEquivalence [IsEquivalence F] [SplitEpiCategory C] :
    SplitEpiCategory D :=
  ⟨fun {X} {Y} f => by
    intro
    rw [← F.inv.isSplitEpi_iff f]
    apply isSplitEpi_of_epi⟩

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.IsEquivalence
inst✝¹ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
inst✝ : Epi f
⊢ IsSplitEpi (F.inv.map f)

Tactic:
apply isSplitEpi_of_epi

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✝² : F.IsEquivalence
inst✝¹ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
inst✝ : Epi f
⊢ IsSplitEpi f

Tactic:
rw [← F.inv.isSplitEpi_iff f]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.IsEquivalence
inst✝¹ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
inst✝ : Epi f
⊢ IsSplitEpi (F.inv.map f)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.IsEquivalence
inst✝ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
⊢ ∀ [inst : Epi f], IsSplitEpi f

Tactic:
intro

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.IsEquivalence
inst✝¹ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
inst✝ : Epi f
⊢ IsSplitEpi f
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem congr (p : FormalMultilinearSeries 𝕜 E F) {m n : ℕ} {v : Fin m → E} {w : Fin n → E}
    (h1 : m = n) (h2 : ∀ (i : ℕ) (him : i < m) (hin : i < n), v ⟨i, him⟩ = w ⟨i, hin⟩) :
    p m v = p n w

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
m n : ℕ
v : Fin m → E
w : Fin n → E
h1 : m = n
h2 : ∀ (i : ℕ) (him : i < m) (hin : i < n), v ⟨i, him⟩ = w ⟨i, hin⟩
⊢ (p m) v = (p n) w

Tactic:
subst n

Result:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
m : ℕ
v w : Fin m → E
h2 : ∀ (i : ℕ) (him hin : i < m), v ⟨i, him⟩ = w ⟨i, hin⟩
⊢ (p m) v = (p m) w

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
m : ℕ
v w : Fin m → E
h2 : ∀ (i : ℕ) (him hin : i < m), v ⟨i, him⟩ = w ⟨i, hin⟩
⊢ (p m) v = (p m) w

Tactic:
congr with ⟨i, hi⟩

Result:
case h.e_6.h.h.mk
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
m : ℕ
v w : Fin m → E
h2 : ∀ (i : ℕ) (him hin : i < m), v ⟨i, him⟩ = w ⟨i, hin⟩
i : ℕ
hi : i < m
⊢ v ⟨i, hi⟩ = w ⟨i, hi⟩

Proof state:
case h.e_6.h.h.mk
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
m : ℕ
v w : Fin m → E
h2 : ∀ (i : ℕ) (him hin : i < m), v ⟨i, him⟩ = w ⟨i, hin⟩
i : ℕ
hi : i < m
⊢ v ⟨i, hi⟩ = w ⟨i, hi⟩

Tactic:
exact h2 i hi hi

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_inf_mul_relfinrank :
    A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
simpa using congr(toNat $(relrank_inf_mul_relrank A B C))

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem zip_eq (s₁ : Stream' α) (s₂ : Stream' β) :
    zip f s₁ s₂ = f (head s₁) (head s₂)::zip f (tail s₁) (tail s₂)

Proof state:
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ (zip f s₁ s₂).head :: (zip f s₁ s₂).tail = f s₁.head s₂.head :: zip f s₁.tail s₂.tail

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ zip f s₁ s₂ = f s₁.head s₂.head :: zip f s₁.tail s₂.tail

Tactic:
rw [← Stream'.eta (zip f s₁ s₂)]

Result:
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ (zip f s₁ s₂).head :: (zip f s₁ s₂).tail = f s₁.head s₂.head :: zip f s₁.tail s₂.tail
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem card_le_of {α : Type u} {n : ℕ} (H : ∀ s : Finset α, s.card ≤ n) : #α ≤ n

Proof state:
α : Type u
n : ℕ
H : ∀ (s : Finset α), s.card ≤ n
⊢ #α ≤ ↑n

Tactic:
contrapose! H

Result:
α : Type u
n : ℕ
H : ↑n < #α
⊢ ∃ s, n < s.card

Proof state:
α : Type u
n : ℕ
H : ↑n < #α
⊢ ↑(n + 1) ≤ #α

Tactic:
simpa only [nat_succ, succ_le_iff] using H

Result:
no goals

Proof state:
α : Type u
n : ℕ
H : ↑n < #α
⊢ ∃ s, n < s.card

Tactic:
apply exists_finset_le_card α (n+1)

Result:
α : Type u
n : ℕ
H : ↑n < #α
⊢ ↑(n + 1) ≤ #α
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem one : padicValRat p 1 = 0

Proof state:
p : ℕ
⊢ padicValRat p 1 = 0

Tactic:
simp [padicValRat]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
lemma affineSpan_insert_zero (s : Set V) :
    (affineSpan k (insert 0 s) : Set V) = Submodule.span k s

Proof state:
case a.h
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ insert 0 s ⊆ insert 0 s -ᵥ insert 0 s

Tactic:
exact subset_sub_left <| mem_insert ..

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(Submodule.span k (insert 0 s)) ⊆ ↑(Submodule.span k (insert 0 s -ᵥ insert 0 s))

Tactic:
gcongr

Result:
case a.h
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ insert 0 s ⊆ insert 0 s -ᵥ insert 0 s

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(affineSpan k (insert 0 s)) = ↑(Submodule.span k (insert 0 s))

Tactic:
refine affineSpan_subset_span.antisymm ?_

Result:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(Submodule.span k (insert 0 s)) ⊆ ↑(affineSpan k (insert 0 s))

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(Submodule.span k (insert 0 s)) ⊆ ↑(Submodule.span k (insert 0 s -ᵥ insert 0 s)) + insert 0 s

Tactic:
refine Subset.trans ?_ <| subset_add_left _ <| mem_insert ..

Result:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(Submodule.span k (insert 0 s)) ⊆ ↑(Submodule.span k (insert 0 s -ᵥ insert 0 s))

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(affineSpan k (insert 0 s)) = ↑(Submodule.span k s)

Tactic:
rw [← Submodule.span_insert_zero]

Result:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(affineSpan k (insert 0 s)) = ↑(Submodule.span k (insert 0 s))

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(Submodule.span k (insert 0 s)) ⊆ ↑(affineSpan k (insert 0 s))

Tactic:
rw [← vectorSpan_add_self, vectorSpan_def]

Result:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(Submodule.span k (insert 0 s)) ⊆ ↑(Submodule.span k (insert 0 s -ᵥ insert 0 s)) + insert 0 s
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_filter_lt_of_right_le [DecidablePred (· < c)] (hbc : b ≤ c) :
    ((Ico a b).filter fun x => x < c) = Ico a b

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => x < c
hbc : b ≤ c
⊢ filter (fun x => x < c) (Ico a b) = Ico a b

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_right_le hbc]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem Filter.EventuallyEq.congr_continuousWithinAt (h : f =ᶠ[𝓝[s] x] g) (hx : f x = g x) :
    ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s : Set α
x : α
h : f =ᶠ[𝓝[s] x] g
hx : f x = g x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x

Tactic:
rw [ContinuousWithinAt, hx, tendsto_congr' h, ContinuousWithinAt]

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem ZMod.pow_totient {n : ℕ} (x : (ZMod n)ˣ) : x ^ φ n = 1

Proof state:
case zero
x : (ZMod 0)ˣ
⊢ x ^ φ 0 = 1

Tactic:
rw [Nat.totient_zero, pow_zero]

Result:
no goals

Proof state:
case succ
n✝ : ℕ
x : (ZMod (n✝ + 1))ˣ
⊢ x ^ φ (n✝ + 1) = 1

Tactic:
rw [← card_units_eq_totient, pow_card_eq_one]

Result:
no goals

Proof state:
n : ℕ
x : (ZMod n)ˣ
⊢ x ^ φ n = 1

Tactic:
cases n

Result:
case zero
x : (ZMod 0)ˣ
⊢ x ^ φ 0 = 1

case succ
n✝ : ℕ
x : (ZMod (n✝ + 1))ˣ
⊢ x ^ φ (n✝ + 1) = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_flatten (f : α → Option β) (L : List (List α)) :
    filterMap f (flatten L) = flatten (map (filterMap f) L)

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
L : List (List α)
⊢ filterMap f L.flatten = (map (filterMap f) L).flatten

Tactic:
induction L <;> simp [*, filterMap_append]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem grundyValue_iff_equiv_zero (G : PGame) [G.Impartial] : grundyValue G = 0 ↔ G ≈ 0

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ G.grundyValue = 0 ↔ G ≈ 0

Tactic:
rw [← grundyValue_eq_iff_equiv, grundyValue_zero]

Result:
no goals
-- Mathlib/Topology/GDelta/Basic.lean
theorem IsGδ.biInter {s : Set ι} (hs : s.Countable) {t : ∀ i ∈ s, Set X}
    (ht : ∀ (i) (hi : i ∈ s), IsGδ (t i hi)) : IsGδ (⋂ i ∈ s, t i ‹_›)

Proof state:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ i, ⋂ (h : i ∈ s), t i h)

Tactic:
rw [biInter_eq_iInter]

Result:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ x, t ↑x ⋯)

Proof state:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
this : Countable ↑s
⊢ IsGδ (⋂ x, t ↑x ⋯)

Tactic:
exact .iInter fun x => ht x x.2

Result:
no goals

Proof state:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ x, t ↑x ⋯)

Tactic:
haveI := hs.to_subtype

Result:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
this : Countable ↑s
⊢ IsGδ (⋂ x, t ↑x ⋯)
-- Mathlib/Data/Fin/Basic.lean
theorem one_lt_last [NeZero n] : 1 < last (n + 1)

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ n ≠ 0

Tactic:
exact NeZero.ne n

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ 1 < last (n + 1)

Tactic:
rw [lt_iff_val_lt_val, val_one, val_last, Nat.lt_add_left_iff_pos, Nat.pos_iff_ne_zero]

Result:
n : ℕ
inst✝ : NeZero n
⊢ n ≠ 0
-- Mathlib/Analysis/Normed/Field/InfiniteSum.lean
theorem Summable.mul_of_nonneg {f : ι → ℝ} {g : ι' → ℝ} (hf : Summable f) (hg : Summable g)
    (hf' : 0 ≤ f) (hg' : 0 ≤ g) : Summable fun x : ι × ι' => f x.1 * g x.2 :=
  (summable_prod_of_nonneg fun _ ↦ mul_nonneg (hf' _) (hg' _)).2 ⟨fun x ↦ hg.mul_left (f x),
    by simpa only [hg.tsum_mul_left _] using hf.mul_right (∑' x, g x)⟩

Proof state:
ι : Type u_2
ι' : Type u_3
f : ι → ℝ
g : ι' → ℝ
hf : Summable f
hg : Summable g
hf' : 0 ≤ f
hg' : 0 ≤ g
⊢ Summable fun x => ∑' (y : ι'), f (x, y).1 * g (x, y).2

Tactic:
simpa only [hg.tsum_mul_left _] using hf.mul_right (∑' x, g x)

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
lemma Topology.IsInducing.withSeminorms [hι : Nonempty ι] {q : SeminormFamily 𝕜₂ F ι}
    (hq : WithSeminorms q) [TopologicalSpace E] {f : E →ₛₗ[σ₁₂] F} (hf : IsInducing f) :
    WithSeminorms (q.comp f)

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : TopologicalSpace F
hι : Nonempty ι
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
inst✝ : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : IsInducing ⇑f
⊢ WithSeminorms (q.comp f)

Tactic:
exact f.withSeminorms_induced hq

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
lemma truncateToReal_eq_toReal {t x : ℝ≥0∞} (t_ne_top : t ≠ ∞) (x_le : x ≤ t) :
    truncateToReal t x = x.toReal

Proof state:
t x : ℝ≥0∞
t_ne_top : t ≠ ⊤
x_le : x ≤ t
x_lt_top : x < ⊤
⊢ t ⊓ x ≠ ⊤

Tactic:
simp_all only [ne_eq, min_eq_top, false_and, not_false_eq_true]

Result:
no goals

Proof state:
t x : ℝ≥0∞
t_ne_top : t ≠ ⊤
x_le : x ≤ t
x_lt_top : x < ⊤
obs : t ⊓ x ≠ ⊤
⊢ t.truncateToReal x = x.toReal

Tactic:
exact (ENNReal.toReal_eq_toReal obs x_lt_top.ne).mpr (min_eq_right x_le)

Result:
no goals

Proof state:
t x : ℝ≥0∞
t_ne_top : t ≠ ⊤
x_le : x ≤ t
x_lt_top : x < ⊤
⊢ t.truncateToReal x = x.toReal

Tactic:
have obs : min t x ≠ ∞ := by
  simp_all only [ne_eq, min_eq_top, false_and, not_false_eq_true]

Result:
t x : ℝ≥0∞
t_ne_top : t ≠ ⊤
x_le : x ≤ t
x_lt_top : x < ⊤
obs : t ⊓ x ≠ ⊤
⊢ t.truncateToReal x = x.toReal

Proof state:
t x : ℝ≥0∞
t_ne_top : t ≠ ⊤
x_le : x ≤ t
⊢ t.truncateToReal x = x.toReal

Tactic:
have x_lt_top : x < ∞ := lt_of_le_of_lt x_le t_ne_top.lt_top

Result:
t x : ℝ≥0∞
t_ne_top : t ≠ ⊤
x_le : x ≤ t
x_lt_top : x < ⊤
⊢ t.truncateToReal x = x.toReal
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem fill_eq {w : Nat} {v : Bool} : fill w v = if v = true then allOnes w else 0#w

Proof state:
case neg
w : Nat
v : Bool
h : ¬v = true
⊢ fill w false = if false = true then allOnes w else 0#w

Tactic:
ext

Result:
case neg.pred
w : Nat
v : Bool
h : ¬v = true
i✝ : Nat
a✝ : i✝ < w
⊢ (fill w false).getLsbD i✝ = (if false = true then allOnes w else 0#w).getLsbD i✝

Proof state:
case neg
w : Nat
v : Bool
h : ¬v = true
⊢ fill w v = if v = true then allOnes w else 0#w

Tactic:
simp only [h]

Result:
case neg
w : Nat
v : Bool
h : ¬v = true
⊢ fill w false = if false = true then allOnes w else 0#w

Proof state:
w : Nat
v : Bool
⊢ fill w v = if v = true then allOnes w else 0#w

Tactic:
by_cases h : v <;> (simp only [h] ; ext ; simp)

Result:
no goals

Proof state:
case neg.pred
w : Nat
v : Bool
h : ¬v = true
i✝ : Nat
a✝ : i✝ < w
⊢ (fill w false).getLsbD i✝ = (if false = true then allOnes w else 0#w).getLsbD i✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem filter_not (s : Finset α) : (s.filter fun a => ¬p a) = s \ s.filter p :=
  ext fun a => by
    simp only [Bool.decide_coe, Bool.not_eq_true', mem_filter, and_comm, mem_sdiff, not_and_or,
      Bool.not_eq_true, and_or_left, and_not_self, or_false]

Proof state:
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ a ∈ filter (fun a => ¬p a) s ↔ a ∈ s \ filter p s

Tactic:
simp only [Bool.decide_coe, Bool.not_eq_true', mem_filter, and_comm, mem_sdiff, not_and_or,
  Bool.not_eq_true, and_or_left, and_not_self, or_false]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Basic.lean
theorem eq_natCast' [AddMonoidHomClass F ℕ A] (f : F) (h1 : f 1 = 1) : ∀ n : ℕ, f n = n
  | 0 => by simp [map_zero f]
  | n + 1 => by rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]

Proof state:
A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : f 1 = 1
⊢ f 0 = ↑0

Tactic:
simp [map_zero f]

Result:
no goals

Proof state:
A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : f 1 = 1
n : ℕ
⊢ f (n + 1) = ↑(n + 1)

Tactic:
rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]

Result:
no goals
-- Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean
theorem ZeroAtFilter.neg [TopologicalSpace β] [AddGroup β] [ContinuousNeg β] {l : Filter α}
    {f : α → β} (hf : ZeroAtFilter l f) : ZeroAtFilter l (-f)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : ContinuousNeg β
l : Filter α
f : α → β
hf : l.ZeroAtFilter f
⊢ l.ZeroAtFilter (-f)

Tactic:
simpa using hf.neg

Result:
no goals