harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/IsLUB.lean
theorem exists_seq_strictMono_tendsto [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α]
    (x : α) : ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝 x)

Proof state:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
x : α
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x

Result:
case intro
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Proof state:
case intro
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
rcases exists_seq_strictMono_tendsto' hy with ⟨u, hu_mono, hu_mem, hux⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
u : ℕ → α
hu_mono : StrictMono u
hu_mem : ∀ (n : ℕ), u n ∈ Ioo y x
hux : Tendsto u atTop (𝓝 x)
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
u : ℕ → α
hu_mono : StrictMono u
hu_mem : ∀ (n : ℕ), u n ∈ Ioo y x
hux : Tendsto u atTop (𝓝 x)
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
exact ⟨u, hu_mono, fun n => (hu_mem n).2, hux⟩

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
lemma mem_part (ha : a ∈ s) : a ∈ P.part a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ a ∈ P.part a

Tactic:
simp [part, ha, choose_property (p := fun s => a ∈ s) P.parts (P.existsUnique_mem ha)]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem ext_indep {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E)
    (h : ∀ ⦃I⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)) : M₁ = M₂ :=
  have h' : M₁.Indep = M₂.Indep

Proof state:
case pos
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
rwa [h]

Result:
no goals

Proof state:
case neg
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : ¬I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
exact iff_of_false (fun hi ↦ hI hi.subset_ground)
  (fun hi ↦ hI (hi.subset_ground.trans_eq hE.symm))

Result:
no goals

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
h' : M₁.Indep = M₂.Indep
B : Set α
x✝ : B ⊆ M₁.E
⊢ M₁.IsBase B ↔ M₂.IsBase B

Tactic:
simp_rw [isBase_iff_maximal_indep, h']

Result:
no goals

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
⊢ M₁.Indep = M₂.Indep

Tactic:
ext I

Result:
case h.a
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
⊢ M₁.Indep I ↔ M₂.Indep I

Proof state:
case h.a
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
by_cases hI : I ⊆ M₁.E

Result:
case pos
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

case neg
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : ¬I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_antilipschitzWith_equiv_aux [PseudoEMetricSpace α] [PseudoEMetricSpace β] :
    AntilipschitzWith ((2 : ℝ≥0) ^ (1 / p).toReal) (WithLp.equiv p (α × β))

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y) ^ p.toReal +
        edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y) ^ p.toReal) ^
      (1 / p.toReal) =
    ↑(2 ^ (1 / p.toReal)) * edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y)

Tactic:
simp only [← two_mul, ENNReal.mul_rpow_of_nonneg _ _ nonneg, ← ENNReal.rpow_mul, cancel,
  ENNReal.rpow_one, ENNReal.coe_rpow_of_nonneg _ nonneg, coe_ofNat]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
theorem gelfandTransform_isometry : Isometry (gelfandTransform ℂ A)

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
a : A
⊢ ‖(gelfandTransform ℂ A) a‖ = ‖a‖

Tactic:
have : spectralRadius ℂ (gelfandTransform ℂ A (star a * a)) = spectralRadius ℂ (star a * a) := by
  unfold spectralRadius; rw [spectrum.gelfandTransform_eq]

Result:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
a : A
this : spectralRadius ℂ ((gelfandTransform ℂ A) (star a * a)) = spectralRadius ℂ (star a * a)
⊢ ‖(gelfandTransform ℂ A) a‖ = ‖a‖

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
a : A
this : ‖(gelfandTransform ℂ A) a‖₊ ^ 2 = ‖a‖₊ ^ 2
⊢ ‖(gelfandTransform ℂ A) a‖ = ‖a‖

Tactic:
simpa only [Function.comp_apply, NNReal.sqrt_sq] using
  congr_arg (((↑) : ℝ≥0 → ℝ) ∘ ⇑NNReal.sqrt) this

Result:
no goals

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
a : A
this : ↑‖star ((gelfandTransform ℂ A) a) * (gelfandTransform ℂ A) a‖₊ = ↑‖star a * a‖₊
⊢ ‖(gelfandTransform ℂ A) a‖ = ‖a‖

Tactic:
simp only [ENNReal.coe_inj, CStarRing.nnnorm_star_mul_self, ← sq] at this

Result:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
a : A
this : ‖(gelfandTransform ℂ A) a‖₊ ^ 2 = ‖a‖₊ ^ 2
⊢ ‖(gelfandTransform ℂ A) a‖ = ‖a‖

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
⊢ Isometry ⇑(gelfandTransform ℂ A)

Tactic:
nontriviality A

Result:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
⊢ Isometry ⇑(gelfandTransform ℂ A)

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
a : A
⊢ ⨆ k ∈ spectrum ℂ ((gelfandTransform ℂ A) (star a * a)), ↑‖k‖₊ = ⨆ k ∈ spectrum ℂ (star a * a), ↑‖k‖₊

Tactic:
rw [spectrum.gelfandTransform_eq]

Result:
no goals

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
a : A
this : spectralRadius ℂ ((gelfandTransform ℂ A) (star a * a)) = spectralRadius ℂ (star a * a)
⊢ ‖(gelfandTransform ℂ A) a‖ = ‖a‖

Tactic:
rw [map_mul, (IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, gelfandTransform_map_star,
  (IsSelfAdjoint.star_mul_self (gelfandTransform ℂ A a)).spectralRadius_eq_nnnorm] at this

Result:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
a : A
this : ↑‖star ((gelfandTransform ℂ A) a) * (gelfandTransform ℂ A) a‖₊ = ↑‖star a * a‖₊
⊢ ‖(gelfandTransform ℂ A) a‖ = ‖a‖

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
⊢ Isometry ⇑(gelfandTransform ℂ A)

Tactic:
refine AddMonoidHomClass.isometry_of_norm (gelfandTransform ℂ A) fun a => ?_

Result:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
a : A
⊢ ‖(gelfandTransform ℂ A) a‖ = ‖a‖

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
a : A
⊢ spectralRadius ℂ ((gelfandTransform ℂ A) (star a * a)) = spectralRadius ℂ (star a * a)

Tactic:
unfold spectralRadius

Result:
A : Type u_1
inst✝ : CommCStarAlgebra A
a✝ : Nontrivial A
a : A
⊢ ⨆ k ∈ spectrum ℂ ((gelfandTransform ℂ A) (star a * a)), ↑‖k‖₊ = ⨆ k ∈ spectrum ℂ (star a * a), ↑‖k‖₊
-- Mathlib/Topology/Algebra/Algebra.lean
theorem _root_.DenseRange.topologicalClosure_map_subalgebra
    [IsTopologicalSemiring B] {f : A →A[R] B} (hf' : DenseRange f) {s : Subalgebra R A}
    (hs : s.topologicalClosure = ⊤) : (s.map (f : A →ₐ[R] B)).topologicalClosure = ⊤

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsTopologicalSemiring A
inst✝ : IsTopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : s.topologicalClosure = ⊤
⊢ (Subalgebra.map (↑f) s).topologicalClosure = ⊤

Tactic:
rw [SetLike.ext'_iff] at hs ⊢

Result:
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsTopologicalSemiring A
inst✝ : IsTopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(Subalgebra.map (↑f) s).topologicalClosure = ↑⊤

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsTopologicalSemiring A
inst✝ : IsTopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : Dense ↑s
⊢ Dense ((fun a => f a) '' ↑s)

Tactic:
exact hf'.dense_image f.continuous hs

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsTopologicalSemiring A
inst✝ : IsTopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(Subalgebra.map (↑f) s).topologicalClosure = ↑⊤

Tactic:
simp only [Subalgebra.topologicalClosure_coe, coe_top, ← dense_iff_closure_eq, Subalgebra.coe_map,
  AlgHom.coe_coe] at hs ⊢

Result:
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsTopologicalSemiring A
inst✝ : IsTopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : Dense ↑s
⊢ Dense ((fun a => f a) '' ↑s)
-- Mathlib/Data/Finsupp/Ext.lean
theorem mulHom_ext [MulOneClass N] ⦃f g : Multiplicative (α →₀ M) →* N⦄
    (H : ∀ x y, f (Multiplicative.ofAdd <| single x y) = g (Multiplicative.ofAdd <| single x y)) :
    f = g :=
  MonoidHom.ext <|
    DFunLike.congr_fun <| by
      have := @addHom_ext α M (Additive N) _ _
        (MonoidHom.toAdditive'' f) (MonoidHom.toAdditive'' g) H
      ext
      rw [DFunLike.ext_iff] at this
      apply this

Proof state:
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))
⊢ f = g

Tactic:
have := @addHom_ext α M (Additive N) _ _
  (MonoidHom.toAdditive'' f) (MonoidHom.toAdditive'' g) H

Result:
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))
this : MonoidHom.toAdditive'' f = MonoidHom.toAdditive'' g
⊢ f = g

Proof state:
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))
this : MonoidHom.toAdditive'' f = MonoidHom.toAdditive'' g
⊢ f = g

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))
this : MonoidHom.toAdditive'' f = MonoidHom.toAdditive'' g
x✝ : Multiplicative (α →₀ M)
⊢ f x✝ = g x✝

Proof state:
case h
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))
this : ∀ (x : α →₀ M), (MonoidHom.toAdditive'' f) x = (MonoidHom.toAdditive'' g) x
x✝ : Multiplicative (α →₀ M)
⊢ f x✝ = g x✝

Tactic:
apply this

Result:
no goals

Proof state:
case h
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))
this : MonoidHom.toAdditive'' f = MonoidHom.toAdditive'' g
x✝ : Multiplicative (α →₀ M)
⊢ f x✝ = g x✝

Tactic:
rw [DFunLike.ext_iff] at this

Result:
case h
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))
this : ∀ (x : α →₀ M), (MonoidHom.toAdditive'' f) x = (MonoidHom.toAdditive'' g) x
x✝ : Multiplicative (α →₀ M)
⊢ f x✝ = g x✝
-- Mathlib/.lake/packages/lean4/src/lean/lake/Lake/Util/Name.lean
theorem quickCmp_rfl {n : Name} : n.quickCmp n = .eq

Proof state:
n : Name
⊢ (match compare n.hash n.hash with
    | Ordering.eq => n.quickCmpAux n
    | ord => ord) =
    Ordering.eq

Tactic:
split <;> exact cmp_rfl

Result:
no goals

Proof state:
n : Name
⊢ n.quickCmp n = Ordering.eq

Tactic:
unfold Name.quickCmp

Result:
n : Name
⊢ (match compare n.hash n.hash with
    | Ordering.eq => n.quickCmpAux n
    | ord => ord) =
    Ordering.eq
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem sum_const' (ι : Type u) (a : Cardinal.{u}) : (sum fun _ : ι => a) = #ι * a

Proof state:
ι : Type u
a : Cardinal.{u}
⊢ (sum fun x => a) = #ι * a

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem null_iff_of_isMulLeftInvariant [Regular μ] {s : Set G} (hs : IsOpen s) :
    μ s = 0 ↔ s = ∅ ∨ μ = 0

Proof state:
case inr
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.Regular
s : Set G
hs : IsOpen s
hμ : NeZero μ
⊢ μ s = 0 ↔ s = ∅ ∨ μ = 0

Tactic:
simp only [or_false, hs.measure_eq_zero_iff μ, NeZero.ne μ]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.Regular
s : Set G
hs : IsOpen s
⊢ μ s = 0 ↔ s = ∅ ∨ μ = 0

Tactic:
rcases eq_zero_or_neZero μ with rfl|hμ

Result:
case inl
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
s : Set G
hs : IsOpen s
inst✝¹ : IsMulLeftInvariant 0
inst✝ : Regular 0
⊢ 0 s = 0 ↔ s = ∅ ∨ 0 = 0

case inr
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.Regular
s : Set G
hs : IsOpen s
hμ : NeZero μ
⊢ μ s = 0 ↔ s = ∅ ∨ μ = 0

Proof state:
case inl
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
s : Set G
hs : IsOpen s
inst✝¹ : IsMulLeftInvariant 0
inst✝ : Regular 0
⊢ 0 s = 0 ↔ s = ∅ ∨ 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem setOfIdeal_open [T2Space R] (I : Ideal C(X, R)) : IsOpen (setOfIdeal I)

Proof state:
X : Type u_1
R : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : T2Space R
I : Ideal C(X, R)
⊢ IsClosed (⋂ i ∈ I, {x | i x = 0})

Tactic:
exact
  isClosed_iInter fun f =>
    isClosed_iInter fun _ => isClosed_eq (map_continuous f) continuous_const

Result:
no goals

Proof state:
X : Type u_1
R : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : T2Space R
I : Ideal C(X, R)
⊢ IsOpen (setOfIdeal I)

Tactic:
simp only [setOfIdeal, Set.setOf_forall, isOpen_compl_iff]

Result:
X : Type u_1
R : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : T2Space R
I : Ideal C(X, R)
⊢ IsClosed (⋂ i ∈ I, {x | i x = 0})
-- Mathlib/GroupTheory/FreeAbelianGroup.lean
theorem of (x : α) : lift f (of x) = f x

Proof state:
α : Type u
β : Type v
inst✝ : AddCommGroup β
f : α → β
x : α
⊢ (lift f) (of x) = f x

Tactic:
convert Abelianization.lift.of
   (FreeGroup.lift f (β := Multiplicative β)) (FreeGroup.of x) using 1

Result:
case h.e'_3.h
α : Type u
β : Type v
inst✝ : AddCommGroup β
f : α → β
x : α
e_1✝ : β = Multiplicative β
⊢ f x = (FreeGroup.lift f) (FreeGroup.of x)

Proof state:
case h.e'_3.h
α : Type u
β : Type v
inst✝ : AddCommGroup β
f : α → β
x : α
e_1✝ : β = Multiplicative β
⊢ f x = (FreeGroup.lift f) (FreeGroup.of x)

Tactic:
exact (FreeGroup.lift.of (β := Multiplicative β)).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array (AssocList α β))
    (target : {d : Array (AssocList α β) // 0 < d.size}) : expand.go 0 source target =
      (toListModel source).foldl (fun acc p => reinsertAux hash acc p.1 p.2) target

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
source : Array (AssocList α β)
target : { d // 0 < d.size }
⊢ go 0 source target = foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (toListModel source)

Tactic:
suffices ∀ i, expand.go i source target =
  ((source.toList.drop i).flatMap AssocList.toList).foldl
    (fun acc p => reinsertAux hash acc p.1 p.2) target by
  simpa using this 0

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
source : Array (AssocList α β)
target : { d // 0 < d.size }
⊢ ∀ (i : Nat),
    go i source target =
      foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (flatMap AssocList.toList (drop i source.toList))

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
source : Array (AssocList α β)
target : { d // 0 < d.size }
this :
  ∀ (i : Nat),
    go i source target =
      foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (flatMap AssocList.toList (drop i source.toList))
⊢ go 0 source target = foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (toListModel source)

Tactic:
simpa using this 0

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
theorem sized_shadow_iff (h : ∅ ∉ 𝒜) :
    (∂ 𝒜 : Set (Finset α)).Sized r ↔ (𝒜 : Set (Finset α)).Sized (r + 1)

Proof state:
case intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
h𝒜 : Set.Sized r ↑(∂ 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
a : α
ha : a ∈ s
⊢ #s = r + 1

Tactic:
rw [← h𝒜 (erase_mem_shadow hs ha), card_erase_add_one ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
h𝒜 : Set.Sized r ↑(∂ 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
⊢ #s = r + 1

Tactic:
obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 (ne_of_mem_of_not_mem hs h)

Result:
case intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
h𝒜 : Set.Sized r ↑(∂ 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
a : α
ha : a ∈ s
⊢ #s = r + 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
⊢ Set.Sized r ↑(∂ 𝒜) ↔ Set.Sized (r + 1) ↑𝒜

Tactic:
refine ⟨fun h𝒜 s hs => ?_, Set.Sized.shadow⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h : ∅ ∉ 𝒜
h𝒜 : Set.Sized r ↑(∂ 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
⊢ #s = r + 1
-- Mathlib/Data/Nat/ModEq.lean
theorem odd_mul_odd_div_two {m n : ℕ} (hm1 : m % 2 = 1) (hn1 : n % 2 = 1) :
    m * n / 2 = m * (n / 2) + m / 2 :=
  have hn0 : 0 < n := Nat.pos_of_ne_zero fun h => by simp_all
  mul_right_injective₀ two_ne_zero <| by
    dsimp
    rw [mul_add, two_mul_odd_div_two hm1, mul_left_comm, two_mul_odd_div_two hn1,
      two_mul_odd_div_two (Nat.odd_mul_odd hm1 hn1), Nat.mul_sub, mul_one, ←
      Nat.add_sub_assoc (by omega), Nat.sub_add_cancel (Nat.le_mul_of_pos_right m hn0)]

Proof state:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ (fun x => 2 * x) (m * n / 2) = (fun x => 2 * x) (m * (n / 2) + m / 2)

Tactic:
dsimp

Result:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)

Proof state:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ 1 ≤ m

Tactic:
omega

Result:
no goals

Proof state:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)

Tactic:
rw [mul_add, two_mul_odd_div_two hm1, mul_left_comm, two_mul_odd_div_two hn1,
  two_mul_odd_div_two (Nat.odd_mul_odd hm1 hn1), Nat.mul_sub, mul_one, ←
  Nat.add_sub_assoc (by omega), Nat.sub_add_cancel (Nat.le_mul_of_pos_right m hn0)]

Result:
no goals

Proof state:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
h : n = 0
⊢ False

Tactic:
simp_all

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
/-- If the comparison morphism `colimit (F ⋙ G) ⟶ G.obj (colimit F)` is an isomorphism, then `G`
    preserves colimits of `F`. -/
lemma preservesColimit_of_isIso_post [IsIso (colimit.post F G)] : PreservesColimit F G :=
  preservesColimit_of_preserves_colimit_cocone (colimit.isColimit F) (by
    convert IsColimit.ofPointIso (colimit.isColimit (F ⋙ G))
    assumption)

Proof state:
case convert_2
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : HasColimit F
inst✝¹ : HasColimit (F ⋙ G)
inst✝ : IsIso (colimit.post F G)
⊢ IsIso ((colimit.isColimit (F ⋙ G)).desc (G.mapCocone (colimit.cocone F)))

Tactic:
assumption

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : HasColimit F
inst✝¹ : HasColimit (F ⋙ G)
inst✝ : IsIso (colimit.post F G)
⊢ IsColimit (G.mapCocone (colimit.cocone F))

Tactic:
convert IsColimit.ofPointIso (colimit.isColimit (F ⋙ G))

Result:
case convert_2
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : HasColimit F
inst✝¹ : HasColimit (F ⋙ G)
inst✝ : IsIso (colimit.post F G)
⊢ IsIso ((colimit.isColimit (F ⋙ G)).desc (G.mapCocone (colimit.cocone F)))