harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem inverse_zero : inverse (0 : M →L[R] M₂) = 0

Proof state:
case pos
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
h : IsInvertible 0
⊢ inverse 0 = 0

Tactic:
rcases isInvertible_zero_iff.1 h with ⟨hM, hM₂⟩

Result:
case pos.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
h : IsInvertible 0
hM : Subsingleton M
hM₂ : Subsingleton M₂
⊢ inverse 0 = 0

Proof state:
case pos.intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
h : IsInvertible 0
hM : Subsingleton M
hM₂ : Subsingleton M₂
⊢ inverse 0 = 0

Tactic:
ext x

Result:
case pos.intro.h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
h : IsInvertible 0
hM : Subsingleton M
hM₂ : Subsingleton M₂
x : M₂
⊢ (inverse 0) x = 0 x

Proof state:
case pos.intro.h
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
h : IsInvertible 0
hM : Subsingleton M
hM₂ : Subsingleton M₂
x : M₂
⊢ (inverse 0) x = 0 x

Tactic:
exact Subsingleton.elim _ _

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ inverse 0 = 0

Tactic:
by_cases h : IsInvertible (0 : M →L[R] M₂)

Result:
case pos
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
h : IsInvertible 0
⊢ inverse 0 = 0

case neg
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
h : ¬IsInvertible 0
⊢ inverse 0 = 0

Proof state:
case neg
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
h : ¬IsInvertible 0
⊢ inverse 0 = 0

Tactic:
exact inverse_of_not_isInvertible h

Result:
no goals
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem insepDegree_self : insepDegree F F = 1

Proof state:
F : Type u
inst✝ : Field F
⊢ insepDegree F F = 1

Tactic:
rw [insepDegree, Subsingleton.elim (separableClosure F F) ⊤, IntermediateField.rank_top]

Result:
no goals
-- Mathlib/Algebra/Algebra/Bilinear.lean
theorem _root_.Algebra.lmul_isUnit_iff {x : A} :
    IsUnit (Algebra.lmul R A x) ↔ IsUnit x

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ IsUnit ((Algebra.lmul R A) x) ↔ IsUnit x

Tactic:
rw [Module.End_isUnit_iff, Iff.comm]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ IsUnit x ↔ Function.Bijective ⇑((Algebra.lmul R A) x)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ IsUnit x ↔ Function.Bijective ⇑((Algebra.lmul R A) x)

Tactic:
exact IsUnit.isUnit_iff_mulLeft_bijective

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) :
    m.isEmpty = true ↔ ∀ a, ¬a ∈ m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ m.isEmpty = true ↔ ∀ (a : α), ¬a ∈ m

Tactic:
simpa [mem_iff_contains] using isEmpty_iff_forall_contains h

Result:
no goals
-- Mathlib/Data/Set/Subsingleton.lean
theorem not_subsingleton_iff : ¬s.Subsingleton ↔ s.Nontrivial

Proof state:
α : Type u
s : Set α
⊢ ¬s.Subsingleton ↔ s.Nontrivial

Tactic:
simp_rw [Set.Subsingleton, Set.Nontrivial, not_forall, exists_prop]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_fract_left' [OrderClosedTopology α] [IsTopologicalAddGroup α] (n : ℤ) :
    Tendsto (fract : α → α) (𝓝[<] n) (𝓝 1)

Proof state:
α : Type u_1
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[<] ↑n) (𝓝 1)

Tactic:
rw [← sub_sub_cancel (n : α) 1]

Result:
α : Type u_1
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[<] ↑n) (𝓝 (↑n - (↑n - 1)))

Proof state:
α : Type u_1
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto (fun x => ↑⌊x⌋) (𝓝[<] ↑n) (𝓝 (↑n - 1))

Tactic:
exact tendsto_floor_left' n

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[<] ↑n) (𝓝 (↑n - (↑n - 1)))

Tactic:
refine (tendsto_id.mono_left nhdsWithin_le_nhds).sub ?_

Result:
α : Type u_1
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto (fun x => ↑⌊x⌋) (𝓝[<] ↑n) (𝓝 (↑n - 1))
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem memP_reverse {t : RBNode α} : MemP cut t.reverse ↔ MemP (cut · |>.swap) t

Proof state:
α : Type u_1
cut : α → Ordering
t : RBNode α
⊢ MemP cut t.reverse ↔ MemP (fun x => (cut x).swap) t

Tactic:
simp [MemP]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
theorem ae_nonneg_restrict_of_forall_setIntegral_nonneg {f : α → ℝ}
    (hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
    (hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → 0 ≤ ∫ x in s, f x ∂μ) {t : Set α}
    (ht : MeasurableSet t) (hμt : μ t ≠ ∞) : 0 ≤ᵐ[μ.restrict t] f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f

Tactic:
refine
  ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter
    (hf_int_finite t ht (lt_top_iff_ne_top.mpr hμt)) fun s hs _ => ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
s : Set α
hs : MeasurableSet s
x✝ : μ (s ∩ t) < ⊤
⊢ 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
s : Set α
hs : MeasurableSet s
x✝ : μ (s ∩ t) < ⊤
⊢ μ (s ∩ t) < ⊤

Tactic:
exact (measure_mono Set.inter_subset_right).trans_lt (lt_top_iff_ne_top.mpr hμt)

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
s : Set α
hs : MeasurableSet s
x✝ : μ (s ∩ t) < ⊤
⊢ 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ

Tactic:
refine hf_zero (s ∩ t) (hs.inter ht) ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
s : Set α
hs : MeasurableSet s
x✝ : μ (s ∩ t) < ⊤
⊢ μ (s ∩ t) < ⊤
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma rnDeriv_withDensity_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
    μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᵐ[μ] μ.rnDeriv ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae μ] μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)

Tactic:
refine (absolutelyContinuous_withDensity_rnDeriv hμν).ae_eq ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae (μ.withDensity (ν.rnDeriv μ))]
    μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae (μ.withDensity (ν.rnDeriv μ))]
    μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)

Tactic:
exact (rnDeriv_add_right_of_mutuallySingular
  (Measure.mutuallySingular_singularPart ν μ).symm.withDensity).symm

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae μ] μ.rnDeriv ν

Tactic:
conv_rhs => rw [ν.haveLebesgueDecomposition_add μ, add_comm]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᶠ[ae μ] μ.rnDeriv (μ.withDensity (ν.rnDeriv μ) + ν.singularPart μ)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_of_isEmpty [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] :
    m.1.isEmpty = true → m.get! a = default

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
a : α
inst✝ : Inhabited (β a)
⊢ m.val.isEmpty = true → m.get! a = default

Tactic:
simp_to_model

Result:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
a : α
inst✝ : Inhabited (β a)
⊢ (toListModel m.val.buckets).isEmpty = true → getValueCast! a (toListModel m.val.buckets) = default

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
a : α
inst✝ : Inhabited (β a)
⊢ (toListModel m.val.buckets).isEmpty = true → getValueCast! a (toListModel m.val.buckets) = default

Tactic:
empty

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem mem_insertEntry_of_key_beq_eq_false [BEq α] [EquivBEq α] {a : α} {b : β a}
    {l : List ((a : α) × β a)} (p : (a : α) × β a)
    (hne : (p.1 == a) = false) : p ∈ insertEntry a b l ↔ p ∈ l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
l : List ((a : α) × β a)
p : (a : α) × β a
hne : (p.fst == a) = false
⊢ p ∈ insertEntry a b l ↔ p ∈ l

Tactic:
simp only [insertEntry, cond_eq_if]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
l : List ((a : α) × β a)
p : (a : α) × β a
hne : (p.fst == a) = false
⊢ (p ∈ if containsKey a l = true then replaceEntry a b l else ⟨a, b⟩ :: l) ↔ p ∈ l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
l : List ((a : α) × β a)
p : (a : α) × β a
hne : (p.fst == a) = false
⊢ (p ∈ if containsKey a l = true then replaceEntry a b l else ⟨a, b⟩ :: l) ↔ p ∈ l

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
l : List ((a : α) × β a)
p : (a : α) × β a
hne : (p.fst == a) = false
h✝ : containsKey a l = true
⊢ p ∈ replaceEntry a b l ↔ p ∈ l

case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
l : List ((a : α) × β a)
p : (a : α) × β a
hne : (p.fst == a) = false
h✝ : ¬containsKey a l = true
⊢ p ∈ ⟨a, b⟩ :: l ↔ p ∈ l

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
l : List ((a : α) × β a)
p : (a : α) × β a
hne : (p.fst == a) = false
h✝ : ¬containsKey a l = true
⊢ p.fst = a ∧ HEq p.snd b → p ∈ l

Tactic:
rw [← Bool.not_eq_true] at hne

Result:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
l : List ((a : α) × β a)
p : (a : α) × β a
hne : ¬(p.fst == a) = true
h✝ : ¬containsKey a l = true
⊢ p.fst = a ∧ HEq p.snd b → p ∈ l

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
l : List ((a : α) × β a)
p : (a : α) × β a
hne : ¬(p.fst == a) = true
h✝ : ¬containsKey a l = true
⊢ p.fst = a ∧ HEq p.snd b → p ∈ l

Tactic:
exact fun x => hne (beq_of_eq x.1) |> False.elim

Result:
no goals

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
l : List ((a : α) × β a)
p : (a : α) × β a
hne : (p.fst == a) = false
h✝ : containsKey a l = true
⊢ p ∈ replaceEntry a b l ↔ p ∈ l

Tactic:
exact mem_replaceEntry_of_beq_eq_false p hne

Result:
no goals

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
l : List ((a : α) × β a)
p : (a : α) × β a
hne : (p.fst == a) = false
h✝ : ¬containsKey a l = true
⊢ p ∈ ⟨a, b⟩ :: l ↔ p ∈ l

Tactic:
simp only [List.mem_cons, or_iff_right_iff_imp, Sigma.ext_iff]

Result:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
a : α
b : β a
l : List ((a : α) × β a)
p : (a : α) × β a
hne : (p.fst == a) = false
h✝ : ¬containsKey a l = true
⊢ p.fst = a ∧ HEq p.snd b → p ∈ l
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_neg_iff (h : 0 < x) : log x < 0 ↔ x < 1

Proof state:
x : ℝ
h : 0 < x
⊢ log x < log 1 ↔ x < 1

Tactic:
exact log_lt_log_iff h zero_lt_one

Result:
no goals

Proof state:
x : ℝ
h : 0 < x
⊢ log x < 0 ↔ x < 1

Tactic:
rw [← log_one]

Result:
x : ℝ
h : 0 < x
⊢ log x < log 1 ↔ x < 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofBool_or_ofBool : ofBool b ||| ofBool b' = ofBool (b || b')

Proof state:
b b' : Bool
⊢ ofBool b ||| ofBool b' = ofBool (b || b')

Tactic:
cases b <;> cases b' <;> rfl

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean
theorem id_φ : (id X n).φ = 𝟙 _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f (n + 1) ≫ (id X n).a + ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev =
    (P (n + 1)).f (n + 1) + (Q (n + 1)).f (n + 1)

Tactic:
congr 1

Result:
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f (n + 1) ≫ (id X n).a = (P (n + 1)).f (n + 1)

case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev = (Q (n + 1)).f (n + 1)

Proof state:
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f (n + 1) ≫ (id X n).a = (P (n + 1)).f (n + 1)

Tactic:
simp only [id, PInfty_f, P_f_idem]

Result:
no goals

Proof state:
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev = (Q (n + 1)).f (n + 1)

Tactic:
exact Eq.trans (by congr; simp) (decomposition_Q n (n + 1)).symm

Result:
no goals

Proof state:
case e_s
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ Finset.univ = Finset.filter (fun i => ↑i < n + 1) Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev =
    ∑ i ∈ Finset.filter (fun i => ↑i < n + 1) Finset.univ, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
congr

Result:
case e_s
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ Finset.univ = Finset.filter (fun i => ↑i < n + 1) Finset.univ

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (id X n).φ = 𝟙 (X _⦋n + 1⦌)

Tactic:
simp only [← P_add_Q_f (n + 1) (n + 1), φ]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f (n + 1) ≫ (id X n).a + ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ (id X n).b i.rev =
    (P (n + 1)).f (n + 1) + (Q (n + 1)).f (n + 1)
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem of_subsingleton [Subsingleton A] (a : A) : spectrum R a = ∅

Proof state:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Subsingleton A
a : A
⊢ σ a = ∅

Tactic:
rw [spectrum, resolventSet_of_subsingleton, Set.compl_univ]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem Set.maximal_iff_forall_insert (hP : ∀ ⦃s t⦄, P t → s ⊆ t → P s) :
    Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬ P (insert x s)

Proof state:
α : Type u_1
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ (x : α), P (insert x s) → x ∈ s

Tactic:
exact ⟨fun h ↦ ⟨h.1, fun x ↦ h.mem_of_prop_insert⟩,
  fun h ↦ ⟨h.1, fun t ht hst x hxt ↦ h.2 x (hP ht <| insert_subset hxt hst)⟩⟩

Result:
no goals

Proof state:
α : Type u_1
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)

Tactic:
simp only [not_imp_not]

Result:
α : Type u_1
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ (x : α), P (insert x s) → x ∈ s
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.closure_openCell_eq_closedCell [RelCWComplex C D] [T2Space X] {n : ℕ}
    {j : cell C n} : closure (openCell n j) = closedCell n j

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ closure (openCell n j) = closedCell n j

Tactic:
apply subset_antisymm (isClosed_closedCell.closure_subset_iff.2 (openCell_subset_closedCell n j))

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ closedCell n j ⊆ closure (openCell n j)

Proof state:
case hf
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ContinuousOn (↑(map n j)) (closedBall 0 1)

Tactic:
exact continuousOn n j

Result:
no goals

Proof state:
case hf
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ContinuousOn (↑(map n j)) (closure (ball 0 1))

Tactic:
rw [closure_ball 0 (by exact one_ne_zero)]

Result:
case hf
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ContinuousOn (↑(map n j)) (closedBall 0 1)

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ↑(map n j) '' closure (ball 0 1) ⊆ closure (openCell n j)

Tactic:
apply ContinuousOn.image_closure

Result:
case hf
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ContinuousOn (↑(map n j)) (closure (ball 0 1))

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ closedCell n j ⊆ closure (openCell n j)

Tactic:
rw [closedCell, ← closure_ball 0 (by exact one_ne_zero)]

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ↑(map n j) '' closure (ball 0 1) ⊆ closure (openCell n j)

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem _root_.Function.LeftInverse.list_map {f : α → β} {g : β → α} (h : LeftInverse f g) :
    LeftInverse (map f) (map g)
  | [] => by simp_rw [map_nil]
  | x :: xs => by simp_rw [map_cons, h x, h.list_map xs]

Proof state:
α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse f g
x : β
xs : List β
⊢ map f (map g (x :: xs)) = x :: xs

Tactic:
simp_rw [map_cons, h x, h.list_map xs]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse f g
⊢ map f (map g []) = []

Tactic:
simp_rw [map_nil]

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem _root_.Associated.primeFactors_eq {a b : M} (h : Associated a b) :
    primeFactors a = primeFactors b

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : Associated a b
⊢ (normalizedFactors a).toFinset = (normalizedFactors b).toFinset

Tactic:
rw [h.normalizedFactors_eq]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : Associated a b
⊢ primeFactors a = primeFactors b

Tactic:
unfold primeFactors

Result:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : Associated a b
⊢ (normalizedFactors a).toFinset = (normalizedFactors b).toFinset
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem rotateRight_def {x : BitVec w} {r : Nat} :
    x.rotateRight r = (x >>> (r % w)) ||| (x <<< (w - r % w))

Proof state:
w : Nat
x : BitVec w
r : Nat
⊢ x.rotateRight r = x >>> (r % w) ||| x <<< (w - r % w)

Tactic:
simp only [rotateRight, rotateRightAux]

Result:
no goals