harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/InfiniteSum/Nonarchimedean.lean
theorem Summable.mul_of_complete_nonarchimedean [CompleteSpace R] {f : α → R} {g : β → R}
    (hf : Summable f) (hg : Summable g) : Summable (fun i : α × β ↦ f i.1 * g i.2)

Proof state:
α : Type u_1
β : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : NonarchimedeanRing R
inst✝ : CompleteSpace R
f : α → R
g : β → R
hf : Summable f
hg : Summable g
⊢ Summable fun i => f i.1 * g i.2

Tactic:
rw [NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero] at *

Result:
α : Type u_1
β : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : NonarchimedeanRing R
inst✝ : CompleteSpace R
f : α → R
g : β → R
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
⊢ Tendsto (fun i => f i.1 * g i.2) cofinite (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : NonarchimedeanRing R
inst✝ : CompleteSpace R
f : α → R
g : β → R
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
⊢ Tendsto (fun i => f i.1 * g i.2) cofinite (𝓝 0)

Tactic:
exact tendsto_mul_cofinite_nhds_zero hf hg

Result:
no goals
-- Mathlib/Order/Filter/EventuallyConst.lean
theorem EventuallyEq.eventuallyConst_iff {g : α → β} (h : f =ᶠ[l] g) :
    EventuallyConst f l ↔ EventuallyConst g l

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
f g : α → β
h : f =ᶠ[l] g
⊢ EventuallyConst f l ↔ EventuallyConst g l

Tactic:
simp only [EventuallyConst, map_congr h]

Result:
no goals
-- Mathlib/Algebra/Module/SpanRank.lean
lemma spanRank_sup_le_sum_spanRank {p q : Submodule R M} :
    (p ⊔ q).spanRank ≤ p.spanRank + q.spanRank

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
⊢ (p ⊔ q).spanRank ≤ p.spanRank + q.spanRank

Tactic:
apply (FG.spanRank_le_iff_exists_span_set_card_le (p ⊔ q)).mpr

Result:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
⊢ ∃ s, #↑s ≤ p.spanRank + q.spanRank ∧ span R s = p ⊔ q

Proof state:
case intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
q : Submodule R M
sp : Set M
hp₁ : #↑sp = (span R sp).spanRank
⊢ ∃ s, #↑s ≤ (span R sp).spanRank + q.spanRank ∧ span R s = span R sp ⊔ q

Tactic:
obtain ⟨sq, ⟨hq₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank q

Result:
case intro.intro.intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
sp : Set M
hp₁ : #↑sp = (span R sp).spanRank
sq : Set M
hq₁ : #↑sq = (span R sq).spanRank
⊢ ∃ s, #↑s ≤ (span R sp).spanRank + (span R sq).spanRank ∧ span R s = span R sp ⊔ span R sq

Proof state:
case intro.intro.intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
sp : Set M
hp₁ : #↑sp = (span R sp).spanRank
sq : Set M
hq₁ : #↑sq = (span R sq).spanRank
⊢ ∃ s, #↑s ≤ (span R sp).spanRank + (span R sq).spanRank ∧ span R s = span R sp ⊔ span R sq

Tactic:
exact ⟨sp ∪ sq, ⟨hp₁ ▸ hq₁ ▸ (Cardinal.mk_union_le sp sq), span_union sp sq⟩⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
⊢ ∃ s, #↑s ≤ p.spanRank + q.spanRank ∧ span R s = p ⊔ q

Tactic:
obtain ⟨sp, ⟨hp₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank p

Result:
case intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
q : Submodule R M
sp : Set M
hp₁ : #↑sp = (span R sp).spanRank
⊢ ∃ s, #↑s ≤ (span R sp).spanRank + q.spanRank ∧ span R s = span R sp ⊔ q
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma pow_lt_iff_lt_log (hx : 0 < x) (hy : 0 < y) : x ^ n < y ↔ n * log x < log y

Proof state:
x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
⊢ x ^ n < y ↔ ↑n * log x < log y

Tactic:
rw [← rpow_lt_iff_lt_log hx hy, rpow_natCast]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Matrix.lean
/-- Eigenvalues of a diagonal linear operator are the diagonal entries. -/
lemma hasEigenvalue_toLin_diagonal_iff (d : n → R) {μ : R} [NoZeroSMulDivisors R M]
    (b : Basis n R M) : HasEigenvalue (toLin b b (diagonal d)) μ ↔ ∃ i, d i = μ

Proof state:
case mp
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this✝ : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
h_iSup : ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ = ⊤
hμ_not_mem : μ ∉ Set.range d
this : Disjoint (eigenspace ((toLin b b) (diagonal d)) μ) (⨆ i ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) i)
⊢ False

Tactic:
rw [h_iSup, disjoint_top] at this

Result:
case mp
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this✝ : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
h_iSup : ⨆ μ ∈ Set.range d, eigenspace ((toLin b b) (diagonal d)) μ = ⊤
hμ_not_mem : μ ∉ Set.range d
this : eigenspace ((toLin b b) (diagonal d)) μ = ⊥
⊢ False

Proof state:
case intro
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
i : n
⊢ b i ∈ ⨆ (_ : d i ∈ Set.range d), eigenspace ((toLin b b) (diagonal d)) (d i)

Tactic:
apply Submodule.mem_iSup_of_mem ⟨i, rfl⟩

Result:
case intro
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
i : n
⊢ b i ∈ eigenspace ((toLin b b) (diagonal d)) (d i)

Proof state:
case intro
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
inst✝ : NoZeroSMulDivisors R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue ((toLin b b) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue ((toLin b b) (diagonal d)) μ
i : n
⊢ ((toLin b b) (diagonal d)) (b i) = d i • b i

Tactic:
exact (hasEigenvector_toLin_diagonal d i b).apply_eq_smul

Result:
no goals
-- Mathlib/Combinatorics/Additive/CovBySMul.lean
@[to_additive]
lemma CovBySMul.mono (hKL : K ≤ L) : CovBySMul M K A B → CovBySMul M L A B

Proof state:
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K L : ℝ
A B : Set X
hKL : K ≤ L
⊢ CovBySMul M K A B → CovBySMul M L A B

Tactic:
rintro ⟨F, hF, hFAB⟩

Result:
case intro.intro
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K L : ℝ
A B : Set X
hKL : K ≤ L
F : Finset M
hF : ↑(#F) ≤ K
hFAB : A ⊆ ↑F • B
⊢ CovBySMul M L A B

Proof state:
case intro.intro
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K L : ℝ
A B : Set X
hKL : K ≤ L
F : Finset M
hF : ↑(#F) ≤ K
hFAB : A ⊆ ↑F • B
⊢ CovBySMul M L A B

Tactic:
exact ⟨F, hF.trans hKL, hFAB⟩

Result:
no goals
-- Mathlib/Topology/Sheaves/SheafCondition/Sites.lean
lemma Topology.IsOpenEmbedding.functor_isContinuous (h : IsOpenEmbedding f) :
    h.isOpenMap.functor.IsContinuous (Opens.grothendieckTopology X)
      (Opens.grothendieckTopology Y)

Proof state:
case hF₁
X Y : TopCat
f : X ⟶ Y
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) ⋯.functor

Tactic:
exact h.compatiblePreserving

Result:
no goals

Proof state:
case hF₂
X Y : TopCat
f : X ⟶ Y
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) ⋯.functor

Tactic:
exact h.isOpenMap.coverPreserving

Result:
no goals

Proof state:
X Y : TopCat
f : X ⟶ Y
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ ⋯.functor.IsContinuous (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y)

Tactic:
apply Functor.isContinuous_of_coverPreserving

Result:
case hF₁
X Y : TopCat
f : X ⟶ Y
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) ⋯.functor

case hF₂
X Y : TopCat
f : X ⟶ Y
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) ⋯.functor
-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
protected
lemma Scheme.IsGermInjective.Spec
    (H : ∀ I : Ideal R, I.IsPrime →
      ∃ f : R, f ∉ I ∧ ∀ (x y : R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0) :
    (Spec R).IsGermInjective

Proof state:
case intro.intro.refine_2.intro.intro
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
      ((CommRingCat.Hom.hom (StructureSheaf.toOpen (↑R) (Opposite.unop (Opposite.op (PrimeSpectrum.basicOpen f))))) x) =
    0
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0

Tactic:
erw [StructureSheaf.germ_toOpen] at hx

Result:
case intro.intro.refine_2.intro.intro
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx : (ConcreteCategory.hom (StructureSheaf.toStalk (↑R) p)) x = 0
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0

Proof state:
case intro.intro.refine_1
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ IsAffineOpen ((Spec R).basicOpen ((ConcreteCategory.hom (ΓSpecIso R).inv) f))

Tactic:
exact (isAffineOpen_top (Spec R)).basicOpen _

Result:
no goals

Proof state:
R : CommRingCat
H : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
⊢ ∃ U, ∃ (hx : p ∈ U), IsAffineOpen U ∧ Function.Injective ⇑(ConcreteCategory.hom ((Spec R).presheaf.germ U p hx))

Tactic:
obtain ⟨f, hf, H⟩ := H p.asIdeal p.2

Result:
case intro.intro
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ ∃ U, ∃ (hx : p ∈ U), IsAffineOpen U ∧ Function.Injective ⇑(ConcreteCategory.hom ((Spec R).presheaf.germ U p hx))

Proof state:
R : CommRingCat
H : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
⊢ (Spec R).IsGermInjective

Tactic:
refine fun p ↦ ⟨?_⟩

Result:
R : CommRingCat
H : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
⊢ ∃ U, ∃ (hx : p ∈ U), IsAffineOpen U ∧ Function.Injective ⇑(ConcreteCategory.hom ((Spec R).presheaf.germ U p hx))
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.add_const [AddCommSemigroup α] [Neg β] (h : Antiperiodic f c) (a : α) :
    Antiperiodic (fun x => f (x + a)) c := fun x => by
  simpa only [add_right_comm] using h (x + a)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddCommSemigroup α
inst✝ : Neg β
h : Antiperiodic f c
a x : α
⊢ (fun x => f (x + a)) (x + c) = -(fun x => f (x + a)) x

Tactic:
simpa only [add_right_comm] using h (x + a)

Result:
no goals
-- Mathlib/Algebra/Group/Translate.lean
lemma translate_add (a b : G) (f : G → α) : τ (a + b) f = τ a (τ b f)

Proof state:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ (a + b) f = τ a (τ b f)

Tactic:
ext

Result:
case h
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
x✝ : G
⊢ τ (a + b) f x✝ = τ a (τ b f) x✝

Proof state:
case h
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
x✝ : G
⊢ τ (a + b) f x✝ = τ a (τ b f) x✝

Tactic:
simp [sub_sub]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem le_tsub_iff_right (ha : AddLECancellable a) (h : a ≤ c) :
    b ≤ c - a ↔ b + a ≤ c

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ b + a ≤ c

Tactic:
rw [add_comm]

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ a + b ≤ c

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ a + b ≤ c

Tactic:
exact ha.le_tsub_iff_left h

Result:
no goals
-- Mathlib/Combinatorics/Young/SemistandardTableau.lean
theorem col_weak {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i1 i2 j : ℕ} (hi : i1 ≤ i2)
    (cell : (i2, j) ∈ μ) : T i1 j ≤ T i2 j

Proof state:
case inl
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 = i2
⊢ T i1 j ≤ T i2 j

Tactic:
rw [h]

Result:
no goals

Proof state:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
⊢ T i1 j ≤ T i2 j

Tactic:
rcases eq_or_lt_of_le hi with h | h

Result:
case inl
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 = i2
⊢ T i1 j ≤ T i2 j

case inr
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ T i1 j ≤ T i2 j

Proof state:
case inr
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ T i1 j ≤ T i2 j

Tactic:
exact le_of_lt (T.col_strict h cell)

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem bne_eq_xor : bne = xor

Proof state:
⊢ bne = xor

Tactic:
funext a b

Result:
case h.h
a b : Bool
⊢ (a != b) = (a ^^ b)

Proof state:
case h.h

⊢ ∀ (a b : Bool), (a != b) = (a ^^ b)

Tactic:
decide

Result:
no goals

Proof state:
case h.h
a b : Bool
⊢ (a != b) = (a ^^ b)

Tactic:
revert a b

Result:
case h.h

⊢ ∀ (a b : Bool), (a != b) = (a ^^ b)
-- Mathlib/Data/List/Sublists.lean
theorem map_pure_sublist_sublists (l : List α) : map pure l <+ sublists l

Proof state:
α : Type u
l : List α
⊢ map pure l <+ l.sublists

Tactic:
induction' l using reverseRecOn with l a ih <;> simp only [map, map_append, sublists_concat]

Result:
case nil
α : Type u
⊢ [] <+ [].sublists

case append_singleton
α : Type u
l : List α
a : α
ih : map pure l <+ l.sublists
⊢ map pure l ++ [pure a] <+ l.sublists ++ map (fun x => x ++ [a]) l.sublists

Proof state:
case nil
α : Type u
⊢ [] <+ [].sublists

Tactic:
simp only [sublists_nil, sublist_cons_self]

Result:
no goals

Proof state:
α : Type u
l : List α
a : α
ih : map pure l <+ l.sublists
⊢ [] ++ [a] = pure a

Tactic:
rfl

Result:
no goals

Proof state:
case append_singleton
α : Type u
l : List α
a : α
ih : map pure l <+ l.sublists
⊢ map pure l ++ [pure a] <+ l.sublists ++ map (fun x => x ++ [a]) l.sublists

Tactic:
exact ((append_sublist_append_left _).2 <|
            singleton_sublist.2 <| mem_map.2 ⟨[], mem_sublists.2 (nil_sublist _), by rfl⟩).trans
        ((append_sublist_append_right _).2 ih)

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem trunc_succ (f : R⟦X⟧) (n : ℕ) :
    trunc n.succ f = trunc n f + Polynomial.monomial n (coeff R n f)

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ trunc n.succ f = trunc n f + (Polynomial.monomial n) ((coeff R n) f)

Tactic:
rw [trunc, Ico_zero_eq_range, sum_range_succ, trunc, Ico_zero_eq_range]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem castNum_shiftRight (m : Num) (n : Nat) : ↑(m >>> n) = (m : ℕ) >>> (n : ℕ)

Proof state:
case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit0) >>> (n + 1)

Tactic:
trans

Result:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ?m.195607

n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ?m.195607 = ↑(pos m.bit0) >>> (n + 1)

n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ℕ
-- Mathlib/GroupTheory/Nilpotent.lean
theorem ascending_central_series_le_upper (H : ℕ → Subgroup G) (hH : IsAscendingCentralSeries H) :
    ∀ n : ℕ, H n ≤ upperCentralSeries G n
  | 0 => hH.1.symm ▸ le_refl ⊥
  | n + 1 => by
    intro x hx
    rw [mem_upperCentralSeries_succ_iff]
    exact fun y => ascending_central_series_le_upper H hH n (hH.2 x n hx y)

Proof state:
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ x ∈ upperCentralSeries G (n + 1)

Tactic:
rw [mem_upperCentralSeries_succ_iff]

Result:
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ upperCentralSeries G n

Proof state:
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ upperCentralSeries G n

Tactic:
exact fun y => ascending_central_series_le_upper H hH n (hH.2 x n hx y)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
⊢ H (n + 1) ≤ upperCentralSeries G (n + 1)

Tactic:
intro x hx

Result:
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ x ∈ upperCentralSeries G (n + 1)
-- Mathlib/Data/Multiset/Pi.lean
theorem cons_eta {m : Multiset α} {a : α} (f : ∀ a' ∈ a ::ₘ m, δ a') :
    (cons m a (f _ (mem_cons_self _ _)) fun a' ha' => f a' (mem_cons_of_mem ha')) = f

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a' : α
f : (a'_1 : α) → a'_1 ∈ a' ::ₘ m → δ a'_1
h' : a' ∈ a' ::ₘ m
⊢ cons m a' (f a' ⋯) (fun a'_1 ha' => f a'_1 ⋯) a' h' = f a' h'

Tactic:
rw [Pi.cons_same]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ cons m a (f a ⋯) (fun a' ha' => f a' ⋯) a' h' = f a' h'

Tactic:
rw [Pi.cons_ne _ h]

Result:
no goals

Proof state:
case h.h
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
⊢ cons m a (f a ⋯) (fun a' ha' => f a' ⋯) a' h' = f a' h'

Tactic:
by_cases h : a' = a

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : a' = a
⊢ cons m a (f a ⋯) (fun a' ha' => f a' ⋯) a' h' = f a' h'

case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ cons m a (f a ⋯) (fun a' ha' => f a' ⋯) a' h' = f a' h'

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : a' = a
⊢ cons m a (f a ⋯) (fun a' ha' => f a' ⋯) a' h' = f a' h'

Tactic:
subst h

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a' : α
f : (a'_1 : α) → a'_1 ∈ a' ::ₘ m → δ a'_1
h' : a' ∈ a' ::ₘ m
⊢ cons m a' (f a' ⋯) (fun a'_1 ha' => f a'_1 ⋯) a' h' = f a' h'

Proof state:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
⊢ (cons m a (f a ⋯) fun a' ha' => f a' ⋯) = f

Tactic:
ext a' h'

Result:
case h.h
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
⊢ cons m a (f a ⋯) (fun a' ha' => f a' ⋯) a' h' = f a' h'
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_smul (r : R) (m : M) (s : S) : mk' f (r • m) s = r • mk' f m s

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
r : R
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (r • m) s) = r • (fromLocalizedModule S f) (LocalizedModule.mk m s)

Tactic:
rw [← LocalizedModule.smul'_mk, LinearMap.map_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
r : R
m : M
s : ↥S
⊢ mk' f (r • m) s = r • mk' f m s

Tactic:
delta mk'

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
r : R
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (r • m) s) = r • (fromLocalizedModule S f) (LocalizedModule.mk m s)
-- Mathlib/Algebra/Polynomial/GroupRingAction.lean
theorem smul_eval_smul (m : M) (f : S[X]) (x : S) : (m • f).eval (m • x) = m • f.eval x :=
  Polynomial.induction_on f (fun r ↦ by rw [smul_C, eval_C, eval_C])
    (fun f g ihf ihg ↦ by rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]) fun n r _ ↦ by
    rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_pow, eval_X, eval_mul, eval_C,
      eval_pow, eval_X, smul_mul', smul_pow']

Proof state:
M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x r : S
⊢ eval (m • x) (m • C r) = m • eval x (C r)

Tactic:
rw [smul_C, eval_C, eval_C]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f✝ : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
⊢ eval (m • x) (m • (f + g)) = m • eval x (f + g)

Tactic:
rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)
⊢ eval (m • x) (m • (C r * X ^ (n + 1))) = m • eval x (C r * X ^ (n + 1))

Tactic:
rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_pow, eval_X, eval_mul, eval_C,
  eval_pow, eval_X, smul_mul', smul_pow']

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean
theorem pullbackObjIso_hom_comp_fst (f : F ⟶ H) (g : G ⟶ H) (d : D) :
    (pullbackObjIso f g d).hom ≫ pullback.fst (f.app d) (g.app d) = (pullback.fst f g).app d

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G H : D ⥤ C
inst✝ : HasPullbacks C
f : F ⟶ H
g : G ⟶ H
d : D
⊢ (pullbackObjIso f g d).hom ≫ pullback.fst (f.app d) (g.app d) = (pullback.fst f g).app d

Tactic:
simp [pullbackObjIso]

Result:
no goals