harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
theorem AdjoinSimple.isIntegral_gen : IsIntegral F (AdjoinSimple.gen F α) ↔ IsIntegral F α

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ IsIntegral F (gen F α) ↔ IsIntegral F α

Tactic:
conv_rhs => rw [← AdjoinSimple.algebraMap_gen F α]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ IsIntegral F (gen F α) ↔ IsIntegral F ((algebraMap (↥F⟮α⟯) E) (gen F α))

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ IsIntegral F (gen F α) ↔ IsIntegral F ((algebraMap (↥F⟮α⟯) E) (gen F α))

Tactic:
rw [isIntegral_algebraMap_iff (algebraMap F⟮α⟯ E).injective]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Indization.lean
theorem Ind.isSeparating_range_yoneda : IsSeparating (Set.range (Ind.yoneda : C ⥤ _).obj)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : Ind C
f g : X ⟶ Y
h : ∀ G ∈ Set.range Ind.yoneda.obj, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ X.colimitPresentationCompYoneda.hom ≫ f = X.colimitPresentationCompYoneda.hom ≫ g

Tactic:
exact colimit.hom_ext (fun i => by simp [← Category.assoc, h])

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ IsSeparating (Set.range Ind.yoneda.obj)

Tactic:
refine fun X Y f g h => (cancel_epi (Ind.colimitPresentationCompYoneda X).hom).1 ?_

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : Ind C
f g : X ⟶ Y
h : ∀ G ∈ Set.range Ind.yoneda.obj, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ X.colimitPresentationCompYoneda.hom ≫ f = X.colimitPresentationCompYoneda.hom ≫ g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : Ind C
f g : X ⟶ Y
h : ∀ G ∈ Set.range Ind.yoneda.obj, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
i : X.presentation.I
⊢ colimit.ι (X.presentation.F ⋙ Ind.yoneda) i ≫ X.colimitPresentationCompYoneda.hom ≫ f =
    colimit.ι (X.presentation.F ⋙ Ind.yoneda) i ≫ X.colimitPresentationCompYoneda.hom ≫ g

Tactic:
simp [← Category.assoc, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem Functor.monotone_map [LawfulMonad m] (f : γ → m α) (g : α → β) (hmono : monotone f) :
    monotone (fun x => g <$> f x)

Proof state:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : α → β
hmono : monotone f
⊢ monotone fun x => g <$> f x

Tactic:
simp only [← LawfulMonad.bind_pure_comp ]

Result:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : α → β
hmono : monotone f
⊢ monotone fun x => do
    let a ← f x
    pure (g a)

Proof state:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : α → β
hmono : monotone f
⊢ monotone fun x a => pure (g a)

Tactic:
apply monotone_const

Result:
no goals

Proof state:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : α → β
hmono : monotone f
⊢ monotone fun x => do
    let a ← f x
    pure (g a)

Tactic:
apply monotone_bind _ _ _ hmono

Result:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : α → β
hmono : monotone f
⊢ monotone fun x a => pure (g a)
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem restrictScalars_toMatrix [Fintype ι] [DecidableEq ι] {S : Type*} [CommRing S] [Nontrivial S]
    [Algebra R₂ S] [Module S M₂] [IsScalarTower R₂ S M₂] [NoZeroSMulDivisors R₂ S]
    (b : Basis ι S M₂) (v : ι → span R₂ (Set.range b)) :
    (algebraMap R₂ S).mapMatrix ((b.restrictScalars R₂).toMatrix v) =
      b.toMatrix (fun i ↦ (v i : M₂))

Proof state:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
S : Type u_9
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : Algebra R₂ S
inst✝² : Module S M₂
inst✝¹ : IsScalarTower R₂ S M₂
inst✝ : NoZeroSMulDivisors R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range ⇑b))
⊢ (algebraMap R₂ S).mapMatrix ((restrictScalars R₂ b).toMatrix v) = b.toMatrix fun i => ↑(v i)

Tactic:
ext

Result:
case a
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
S : Type u_9
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : Algebra R₂ S
inst✝² : Module S M₂
inst✝¹ : IsScalarTower R₂ S M₂
inst✝ : NoZeroSMulDivisors R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range ⇑b))
i✝ j✝ : ι
⊢ (algebraMap R₂ S).mapMatrix ((restrictScalars R₂ b).toMatrix v) i✝ j✝ = b.toMatrix (fun i => ↑(v i)) i✝ j✝

Proof state:
case a
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
S : Type u_9
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : Algebra R₂ S
inst✝² : Module S M₂
inst✝¹ : IsScalarTower R₂ S M₂
inst✝ : NoZeroSMulDivisors R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range ⇑b))
i✝ j✝ : ι
⊢ (algebraMap R₂ S).mapMatrix ((restrictScalars R₂ b).toMatrix v) i✝ j✝ = b.toMatrix (fun i => ↑(v i)) i✝ j✝

Tactic:
rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
  Basis.restrictScalars_repr_apply, Basis.toMatrix_apply]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/LinearMap.lean
theorem pow_restrict {p : Submodule R M} (n : ℕ) (h : ∀ x ∈ p, f' x ∈ p)
    (h' := pow_apply_mem_of_forall_mem n h) :
    (f'.restrict h) ^ n = (f' ^ n).restrict h'

Proof state:
case h.a
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, f' x ∈ p
h' : optParam (∀ x ∈ p, (f' ^ n) x ∈ p) ⋯
x : ↥p
⊢ ↑((f'.restrict h ^ n) x) = ↑(((f' ^ n).restrict h') x)

Tactic:
have : Semiconj (↑) (f'.restrict h) f' := fun _ ↦ restrict_coe_apply _ _ _

Result:
case h.a
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, f' x ∈ p
h' : optParam (∀ x ∈ p, (f' ^ n) x ∈ p) ⋯
x : ↥p
this : Semiconj Subtype.val ⇑(f'.restrict h) ⇑f'
⊢ ↑((f'.restrict h ^ n) x) = ↑(((f' ^ n).restrict h') x)

Proof state:
case h.a
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, f' x ∈ p
h' : optParam (∀ x ∈ p, (f' ^ n) x ∈ p) ⋯
x : ↥p
this : Semiconj Subtype.val ⇑(f'.restrict h) ⇑f'
⊢ ↑((f'.restrict h ^ n) x) = ↑(((f' ^ n).restrict h') x)

Tactic:
simp [coe_pow, this.iterate_right _ _]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, f' x ∈ p
h' : optParam (∀ x ∈ p, (f' ^ n) x ∈ p) ⋯
⊢ f'.restrict h ^ n = (f' ^ n).restrict h'

Tactic:
ext x

Result:
case h.a
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, f' x ∈ p
h' : optParam (∀ x ∈ p, (f' ^ n) x ∈ p) ⋯
x : ↥p
⊢ ↑((f'.restrict h ^ n) x) = ↑(((f' ^ n).restrict h') x)
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem measurePreserving_div_left (μ : Measure G) [IsInvInvariant μ] [IsMulLeftInvariant μ]
    (g : G) : MeasurePreserving (fun t => g / t) μ μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : DivisionMonoid G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ MeasurePreserving (fun t => g * t⁻¹) μ μ

Tactic:
exact (measurePreserving_mul_left μ g).comp (measurePreserving_inv μ)

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : DivisionMonoid G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ MeasurePreserving (fun t => g / t) μ μ

Tactic:
simp_rw [div_eq_mul_inv]

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : DivisionMonoid G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ MeasurePreserving (fun t => g * t⁻¹) μ μ
-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem restrictNonposSeq_succ (n : ℕ) :
    restrictNonposSeq s i n.succ = someExistsOneDivLT s (i \ ⋃ k ≤ n, restrictNonposSeq s i k)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n.succ =
    MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)

Tactic:
rw [restrictNonposSeq]

Result:
no goals
-- Mathlib/Order/Compare.lean
theorem compares_swap [LT α] {a b : α} {o : Ordering} : o.swap.Compares a b ↔ o.Compares b a

Proof state:
case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LT α
a b : α
o : Ordering
⊢ o.swap.Compares a b ↔ o.Compares b a

Tactic:
cases o

Result:
case lt
α : Type u_1
inst✝ : LT α
a b : α
⊢ lt.swap.Compares a b ↔ lt.Compares b a

case eq
α : Type u_1
inst✝ : LT α
a b : α
⊢ eq.swap.Compares a b ↔ eq.Compares b a

case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a

Proof state:
case lt
α : Type u_1
inst✝ : LT α
a b : α
⊢ lt.swap.Compares a b ↔ lt.Compares b a

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
case eq
α : Type u_1
inst✝ : LT α
a b : α
⊢ eq.swap.Compares a b ↔ eq.Compares b a

Tactic:
exact eq_comm

Result:
no goals
-- Mathlib/Analysis/NormedSpace/MStructure.lean
theorem commute [FaithfulSMul M X] {P Q : M} (h₁ : IsLprojection X P) (h₂ : IsLprojection X Q) :
    Commute P Q

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q)
⊢ Q * P = Q * P * Q

Tactic:
rwa [eq_sub_iff_add_eq, add_right_eq_self, sub_eq_zero] at e1

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)

Tactic:
rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
  mul_smul]

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
QP_eq_QPQ : Q * P = Q * P * Q
⊢ P * Q = Q * P

Tactic:
rw [QP_eq_QPQ, PR_eq_RPR Q h₂]

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖

Tactic:
abel

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0

Tactic:
rw [le_antisymm_iff]

Result:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ ≤ 0 ∧ 0 ≤ ‖(P * R) • x - (R * P * R) • x‖

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
QP_eq_QPQ : Q * P = Q * P * Q
⊢ Commute P Q

Tactic:
show P * Q = Q * P

Result:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
QP_eq_QPQ : Q * P = Q * P * Q
⊢ P * Q = Q * P
-- Mathlib/Topology/Compactness/Compact.lean
theorem Set.Finite.isCompact_sUnion {S : Set (Set X)} (hf : S.Finite) (hc : ∀ s ∈ S, IsCompact s) :
    IsCompact (⋃₀ S)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
⊢ IsCompact (⋃ i ∈ S, i)

Tactic:
exact hf.isCompact_biUnion hc

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
⊢ IsCompact (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]

Result:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
⊢ IsCompact (⋃ i ∈ S, i)
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem factor_comp (H1 : p ≤ p') (H2 : p' ≤ p'') :
    (factor H2).comp (factor H1) = factor (H1.trans H2)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
⊢ factor H2 ∘ₗ factor H1 = factor ⋯

Tactic:
ext

Result:
case h.h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x✝ : M
⊢ ((factor H2 ∘ₗ factor H1) ∘ₗ p.mkQ) x✝ = (factor ⋯ ∘ₗ p.mkQ) x✝

Proof state:
case h.h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x✝ : M
⊢ ((factor H2 ∘ₗ factor H1) ∘ₗ p.mkQ) x✝ = (factor ⋯ ∘ₗ p.mkQ) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_pop {v : Vector α n} {i : Nat} (h : i < n - 1) : (v.pop)[i] = v[i]

Proof state:
case mk
α : Type u_1
i : Nat
data : Array α
h : i < data.size - 1
⊢ { toArray := data, size_toArray := ⋯ }.pop[i] = { toArray := data, size_toArray := ⋯ }[i]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
h : i < n - 1
⊢ v.pop[i] = v[i]

Tactic:
rcases v with ⟨data, rfl⟩

Result:
case mk
α : Type u_1
i : Nat
data : Array α
h : i < data.size - 1
⊢ { toArray := data, size_toArray := ⋯ }.pop[i] = { toArray := data, size_toArray := ⋯ }[i]
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp]
lemma sq_eq_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b := pow_left_inj₀ ha hb (by decide)

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a b : M₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 2 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem MulAction.isClosedMap_quotient [CompactSpace α] :
    letI := orbitRel α β
    IsClosedMap (Quotient.mk' : β → Quotient (orbitRel α β))

Proof state:
α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed t
⊢ IsClosed (⋃ g, (fun x => g • x) '' t)

Tactic:
convert ht.smul_left_of_isCompact (isCompact_univ (X := α))

Result:
case h.e'_3
α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed t
⊢ ⋃ g, (fun x => g • x) '' t = univ • t

Proof state:
case h.e'_3
α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed t
⊢ ⋃ x ∈ univ, (fun x_1 => x • x_1) '' t = ⋃ a ∈ univ, a • t

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
⊢ IsClosedMap Quotient.mk'

Tactic:
intro t ht

Result:
α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed t
⊢ IsClosed (Quotient.mk' '' t)

Proof state:
α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed t
⊢ IsClosed (Quotient.mk' '' t)

Tactic:
rw [← isQuotientMap_quotient_mk'.isClosed_preimage,
  MulAction.quotient_preimage_image_eq_union_mul]

Result:
α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed t
⊢ IsClosed (⋃ g, (fun x => g • x) '' t)

Proof state:
case h.e'_3
α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed t
⊢ ⋃ g, (fun x => g • x) '' t = univ • t

Tactic:
rw [← biUnion_univ, ← iUnion_smul_left_image]

Result:
case h.e'_3
α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed t
⊢ ⋃ x ∈ univ, (fun x_1 => x • x_1) '' t = ⋃ a ∈ univ, a • t
-- Mathlib/Probability/BorelCantelli.lean
theorem iIndepSet.condExp_indicator_filtrationOfSet_ae_eq (hsm : ∀ n, MeasurableSet (s n))
    (hs : iIndepSet s μ) (hij : i < j) :
    μ[(s j).indicator (fun _ => 1 : Ω → ℝ)|filtrationOfSet hsm i] =ᵐ[μ]
    fun _ => (μ (s j)).toReal

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst✝ : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ (fun x => (μ (s j)).toReal) =ᶠ[ae μ] fun x => (μ (s j)).toReal

Tactic:
rfl

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst✝ : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ μ[(s j).indicator fun x => 1|↑(Filtration.natural (fun i => (s i).indicator fun x => 1) ⋯) i] =ᶠ[ae μ] fun x =>
    (μ (s j)).toReal

Tactic:
refine (iIndepFun.condExp_natural_ae_eq_of_lt _ hs.iIndepFun_indicator hij).trans ?_

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst✝ : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ (fun x => ∫ (x : Ω), (s j).indicator (fun _ω => 1) x ∂μ) =ᶠ[ae μ] fun x => (μ (s j)).toReal

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst✝ : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ (fun x => ∫ (x : Ω), (s j).indicator (fun _ω => 1) x ∂μ) =ᶠ[ae μ] fun x => (μ (s j)).toReal

Tactic:
simp only [integral_indicator_const _ (hsm _), Algebra.id.smul_eq_mul, mul_one]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst✝ : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ (fun x => (μ (s j)).toReal) =ᶠ[ae μ] fun x => (μ (s j)).toReal

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst✝ : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ μ[(s j).indicator fun x => 1|↑(filtrationOfSet hsm) i] =ᶠ[ae μ] fun x => (μ (s j)).toReal

Tactic:
rw [Filtration.filtrationOfSet_eq_natural (β := ℝ) hsm]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst✝ : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ μ[(s j).indicator fun x => 1|↑(Filtration.natural (fun i => (s i).indicator fun x => 1) ⋯) i] =ᶠ[ae μ] fun x =>
    (μ (s j)).toReal
-- Mathlib/Algebra/RingQuot.lean
theorem pow_quot {a} {n : ℕ} : (⟨Quot.mk _ a⟩ ^ n : RingQuot r) = ⟨Quot.mk _ (a ^ n)⟩

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a : R
n : ℕ
⊢ RingQuot.npow r n { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (a ^ n) }

Tactic:
rw [npow_def]

Result:
no goals

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a : R
n : ℕ
⊢ { toQuot := Quot.mk (Rel r) a } ^ n = { toQuot := Quot.mk (Rel r) (a ^ n) }

Tactic:
show npow r _ _ = _

Result:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a : R
n : ℕ
⊢ RingQuot.npow r n { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (a ^ n) }
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_sub_le (x y : Game) : (x - y).birthday ≤ x.birthday ♯ y.birthday

Proof state:
x y : Game
⊢ x.birthday ♯ (-y).birthday = x.birthday ♯ y.birthday

Tactic:
rw [birthday_neg]

Result:
no goals

Proof state:
x y : Game
⊢ (x - y).birthday ≤ x.birthday ♯ y.birthday

Tactic:
apply (birthday_add_le x _).trans_eq

Result:
x y : Game
⊢ x.birthday ♯ (-y).birthday = x.birthday ♯ y.birthday
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem uniformGroup_of_commGroup : UniformGroup G

Proof state:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ UniformGroup G

Tactic:
constructor

Result:
case uniformContinuous_div
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ UniformContinuous fun p => p.1 / p.2

Proof state:
case uniformContinuous_div
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ Tendsto (fun x => x.1.2 / x.1.1 / (x.2.2 / x.2.1)) (comap (fun p => (p.1.2 / p.1.1, p.2.2 / p.2.1)) (𝓝 1)) (𝓝 1)

Tactic:
exact (continuous_div'.tendsto' 1 1 (div_one 1)).comp tendsto_comap

Result:
no goals

Proof state:
case uniformContinuous_div
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ UniformContinuous fun p => p.1 / p.2

Tactic:
simp only [UniformContinuous, uniformity_prod_eq_prod, uniformity_eq_comap_nhds_one',
  tendsto_comap_iff, tendsto_map'_iff, prod_comap_comap_eq, Function.comp_def,
  div_div_div_comm _ (Prod.snd (Prod.snd _)), ← nhds_prod_eq, Prod.mk_one_one]

Result:
case uniformContinuous_div
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ Tendsto (fun x => x.1.2 / x.1.1 / (x.2.2 / x.2.1)) (comap (fun p => (p.1.2 / p.1.1, p.2.2 / p.2.1)) (𝓝 1)) (𝓝 1)
-- Mathlib/Data/Finset/Sum.lean
@[gcongr]
lemma toLeft_subset_toLeft : u ⊆ v → u.toLeft ⊆ v.toLeft :=
  fun h _ => by simpa only [mem_toLeft] using @h _

Proof state:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
h : u ⊆ v
x✝ : α
⊢ x✝ ∈ u.toLeft → x✝ ∈ v.toLeft

Tactic:
simpa only [mem_toLeft] using @h _

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem range_one [Nonempty α] [One β] : (1 : α →ₛ β).range = {1} :=
  Finset.ext fun x => by simp [eq_comm]

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Nonempty α
inst✝ : One β
x : β
⊢ x ∈ SimpleFunc.range 1 ↔ x ∈ {1}

Tactic:
simp [eq_comm]

Result:
no goals