harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem fst_comp_quotientInfEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    (RingHom.fst _ _).comp
        (quotientInfEquivQuotientProd I J coprime : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J) =
      Ideal.Quotient.factor inf_le_left

Proof state:
case h
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ ((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J)) =
    (factor ⋯).comp (Quotient.mk (I ⊓ J))

Tactic:
ext

Result:
case h.a
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x✝ : R
⊢ (((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J))) x✝ =
    ((factor ⋯).comp (Quotient.mk (I ⊓ J))) x✝

Proof state:
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ (fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = factor ⋯

Tactic:
apply Quotient.ringHom_ext

Result:
case h
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ ((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J)) =
    (factor ⋯).comp (Quotient.mk (I ⊓ J))

Proof state:
case h.a
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x✝ : R
⊢ (((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J))) x✝ =
    ((factor ⋯).comp (Quotient.mk (I ⊓ J))) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem pullback_comp {f : Y ⟶ X} {g : Z ⟶ Y} (S : Sieve X) :
    S.pullback (g ≫ f) = (S.pullback f).pullback g

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
S : Sieve X
⊢ pullback (g ≫ f) S = pullback g (pullback f S)

Tactic:
simp [Sieve.ext_iff]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem map_ofFunction_le {β} (f : α → β) :
    map f (OuterMeasure.ofFunction m m_empty) ≤
      OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty :=
  le_ofFunction.2 fun s => by
    rw [map_apply]
    apply ofFunction_le

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
s : Set β
⊢ (OuterMeasure.ofFunction m m_empty) (f ⁻¹' s) ≤ m (f ⁻¹' s)

Tactic:
apply ofFunction_le

Result:
no goals

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
s : Set β
⊢ ((map f) (OuterMeasure.ofFunction m m_empty)) s ≤ m (f ⁻¹' s)

Tactic:
rw [map_apply]

Result:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
s : Set β
⊢ (OuterMeasure.ofFunction m m_empty) (f ⁻¹' s) ≤ m (f ⁻¹' s)
-- Mathlib/CategoryTheory/Limits/Types.lean
theorem Limit.π_mk (x : ∀ j, F.obj j) (h : ∀ (j j') (f : j ⟶ j'), F.map f (x j) = x j') (j) :
    limit.π F j (Limit.mk F x h) = x j

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x : (j : J) → F.obj j
h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j'
j : J
⊢ limit.π F j (mk F x h) = x j

Tactic:
dsimp [Limit.mk]

Result:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x : (j : J) → F.obj j
h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j'
j : J
⊢ limit.π F j ((limitEquivSections F).symm ⟨x, ⋯⟩) = x j

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x : (j : J) → F.obj j
h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j'
j : J
⊢ limit.π F j ((limitEquivSections F).symm ⟨x, ⋯⟩) = x j

Tactic:
simp

Result:
no goals
-- Mathlib/Order/OrderIsoNat.lean
theorem WellFounded.monotone_chain_condition' [Preorder α] :
    WellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → ¬a n < a m

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ (WellFounded fun x1 x2 => x1 > x2) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Tactic:
rw [← isWellFounded_iff]

Result:
α : Type u_1
inst✝ : Preorder α
⊢ (IsWellFounded α fun x1 x2 => x1 > x2) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ (IsWellFounded α fun x1 x2 => x1 > x2) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Tactic:
exact wellFoundedGT_iff_monotone_chain_condition'

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_zero : (fun _x => (0 : E')) =o[l] g' :=
  IsLittleO.of_bound fun c hc =>
    univ_mem' fun x => by simpa using mul_nonneg hc.le (norm_nonneg <| g' x)

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
c : ℝ
hc : 0 < c
x : α
⊢ x ∈ {x | (fun x => ‖0‖ ≤ c * ‖g' x‖) x}

Tactic:
simpa using mul_nonneg hc.le (norm_nonneg <| g' x)

Result:
no goals
-- Mathlib/Topology/DiscreteQuotient.lean
theorem eq_of_forall_proj_eq [T2Space X] [CompactSpace X] [disc : TotallyDisconnectedSpace X]
    {x y : X} (h : ∀ Q : DiscreteQuotient X, Q.proj x = Q.proj y) : x = y

Proof state:
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
⊢ x = y

Tactic:
rw [← mem_singleton_iff, ← connectedComponent_eq_singleton, connectedComponent_eq_iInter_isClopen,
  mem_iInter]

Result:
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
⊢ ∀ (i : { s // IsClopen s ∧ y ∈ s }), x ∈ ↑i

Proof state:
case mk.intro
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
U : Set X
hU1 : IsClopen U
hU2 : y ∈ U
⊢ x ∈ ↑⟨U, ⋯⟩

Tactic:
exact (Quotient.exact' (h (ofIsClopen hU1))).mpr hU2

Result:
no goals

Proof state:
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
⊢ ∀ (i : { s // IsClopen s ∧ y ∈ s }), x ∈ ↑i

Tactic:
rintro ⟨U, hU1, hU2⟩

Result:
case mk.intro
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
disc : TotallyDisconnectedSpace X
x y : X
h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y
U : Set X
hU1 : IsClopen U
hU2 : y ∈ U
⊢ x ∈ ↑⟨U, ⋯⟩
-- Mathlib/Analysis/InnerProductSpace/Positive.lean
theorem IsPositive.adjoint_conj {T : E →L[𝕜] E} (hT : T.IsPositive) (S : F →L[𝕜] E) :
    (S† ∘L T ∘L S).IsPositive

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : F →L[𝕜] E
⊢ ((adjoint S).comp (T.comp S)).IsPositive

Tactic:
convert hT.conj_adjoint (S†)

Result:
case h.e'_7.h.e'_24.h.e'_24
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : F →L[𝕜] E
⊢ S = adjoint (adjoint S)

Proof state:
case h.e'_7.h.e'_24.h.e'_24
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : F →L[𝕜] E
⊢ S = adjoint (adjoint S)

Tactic:
rw [adjoint_adjoint]

Result:
no goals
-- Mathlib/Data/Finset/Fold.lean
theorem fold_max_lt : s.fold max b f < c ↔ b < c ∧ ∀ x ∈ s, f x < c

Proof state:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x > y ⊔ z ↔ x > y ∧ x > z

Tactic:
intro x y z

Result:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x > y ⊔ z ↔ x > y ∧ x > z

Proof state:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ y ⊔ z < x ↔ x > y ∧ x > z

Tactic:
exact max_lt_iff

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c > fold max b f s ↔ b < c ∧ ∀ x ∈ s, f x < c

Tactic:
apply fold_op_rel_iff_and

Result:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x > y ⊔ z ↔ x > y ∧ x > z

Proof state:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x > y ⊔ z ↔ x > y ∧ x > z

Tactic:
show _ < _ ↔ _

Result:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ y ⊔ z < x ↔ x > y ∧ x > z

Proof state:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s < c ↔ b < c ∧ ∀ x ∈ s, f x < c

Tactic:
show _ > _ ↔ _

Result:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c > fold max b f s ↔ b < c ∧ ∀ x ∈ s, f x < c
-- Mathlib/Algebra/Module/Torsion.lean
@[simp]
lemma infinite_range_add_nsmul_iff [AddCommGroup M] [NoZeroSMulDivisors ℤ M] (x y : M) :
    (Set.range <| fun n : ℕ ↦ x + n • y).Infinite ↔ y ≠ 0

Proof state:
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : NoZeroSMulDivisors ℤ M
x y : M
h : y ≠ 0
r s : ℕ
hrs : x + r • y = x + s • y
⊢ r = s

Tactic:
rw [add_right_inj, ← natCast_zsmul, ← natCast_zsmul] at hrs

Result:
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : NoZeroSMulDivisors ℤ M
x y : M
h : y ≠ 0
r s : ℕ
hrs : ↑r • y = ↑s • y
⊢ r = s

Proof state:
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : NoZeroSMulDivisors ℤ M
x y : M
⊢ (Set.range fun n => x + n • y).Infinite ↔ y ≠ 0

Tactic:
refine ⟨fun h hy ↦ by simp [hy] at h, fun h ↦ Set.infinite_range_of_injective fun r s hrs ↦ ?_⟩

Result:
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : NoZeroSMulDivisors ℤ M
x y : M
h : y ≠ 0
r s : ℕ
hrs : x + r • y = x + s • y
⊢ r = s

Proof state:
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : NoZeroSMulDivisors ℤ M
x y : M
h : y ≠ 0
r s : ℕ
hrs : ↑r • y = ↑s • y
⊢ r = s

Tactic:
simpa using smul_left_injective _ h hrs

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : NoZeroSMulDivisors ℤ M
x y : M
h : (Set.range fun n => x + n • y).Infinite
hy : y = 0
⊢ False

Tactic:
simp [hy] at h

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem coe_image_of_subset {s t : Set α} (h : t ⊆ s) : (↑) '' { x : ↥s | ↑x ∈ t } = t

Proof state:
α : Type u_1
s t : Set α
h : t ⊆ s
⊢ val '' {x | ↑x ∈ t} = t

Tactic:
ext x

Result:
case h
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ x ∈ val '' {x | ↑x ∈ t} ↔ x ∈ t

Proof state:
case h
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ (∃ x_1 ∈ {x | ↑x ∈ t}, ↑x_1 = x) ↔ x ∈ t

Tactic:
exact ⟨fun ⟨_, hx', hx⟩ => hx ▸ hx', fun hx => ⟨⟨x, h hx⟩, hx, rfl⟩⟩

Result:
no goals

Proof state:
case h
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ x ∈ val '' {x | ↑x ∈ t} ↔ x ∈ t

Tactic:
rw [mem_image]

Result:
case h
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ (∃ x_1 ∈ {x | ↑x ∈ t}, ↑x_1 = x) ↔ x ∈ t
-- Mathlib/Algebra/Lie/Submodule.lean
theorem range_eq_top : f.range = ⊤ ↔ Function.Surjective f

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
⊢ LinearMap.range ↑f = ⊤ ↔ Function.Surjective ⇑f

Tactic:
exact LinearMap.range_eq_top

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
⊢ f.range = ⊤ ↔ Function.Surjective ⇑f

Tactic:
rw [← LieSubalgebra.toSubmodule_inj, range_toSubmodule, LieSubalgebra.top_toSubmodule]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
⊢ LinearMap.range ↑f = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib/Algebra/Homology/Single.lean
@[simp]
lemma toSingle₀Equiv_symm_apply_f_zero
    {C : CochainComplex V ℕ} {X : V} (f : C.X 0 ⟶ X) :
    ((toSingle₀Equiv C X).symm f).f 0 = f

Proof state:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : C.X 0 ⟶ X
⊢ ((C.toSingle₀Equiv X).symm f).f 0 = f

Tactic:
simp [toSingle₀Equiv]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
lemma count_ne_zero {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) :
    count K v I = ((Associates.mk v.asIdeal).count (Associates.mk
      (choose (choose_spec (exists_eq_spanSingleton_mul I)))).factors -
      (Associates.mk v.asIdeal).count
        (Associates.mk (Ideal.span {choose (exists_eq_spanSingleton_mul I)})).factors : ℤ)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk (choose ⋯)).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors)

Tactic:
simp only [count, dif_neg hI]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
theorem isSeparated_eq_diagonal_isClosedImmersion :
    @IsSeparated = MorphismProperty.diagonal @IsClosedImmersion

Proof state:
⊢ @IsSeparated = MorphismProperty.diagonal @IsClosedImmersion

Tactic:
ext

Result:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsSeparated x✝ ↔ MorphismProperty.diagonal (@IsClosedImmersion) x✝

Proof state:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsSeparated x✝ ↔ MorphismProperty.diagonal (@IsClosedImmersion) x✝

Tactic:
exact isSeparated_iff _

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_finite_biUnion {s : Set β} (hs : s.Finite) {t : β → Set α} :
    IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ :=
  hs.induction_on _ (by simp) <| by intro a s _ _ hf; simp [hf, or_imp, forall_and]

Proof state:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
s : Set β
hs : s.Finite
t : β → Set α
⊢ ∀ {a : β} {s : Set β},
    a ∉ s →
      s.Finite →
        (IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ) →
          (IntegrableOn f (⋃ i ∈ insert a s, t i) μ ↔ ∀ i ∈ insert a s, IntegrableOn f (t i) μ)

Tactic:
intro a s _ _ hf

Result:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
s✝ : Set β
hs : s✝.Finite
t : β → Set α
a : β
s : Set β
a✝ : a ∉ s
hs✝ : s.Finite
hf : IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ
⊢ IntegrableOn f (⋃ i ∈ insert a s, t i) μ ↔ ∀ i ∈ insert a s, IntegrableOn f (t i) μ

Proof state:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
s✝ : Set β
hs : s✝.Finite
t : β → Set α
a : β
s : Set β
a✝ : a ∉ s
hs✝ : s.Finite
hf : IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, IntegrableOn f (t i) μ
⊢ IntegrableOn f (⋃ i ∈ insert a s, t i) μ ↔ ∀ i ∈ insert a s, IntegrableOn f (t i) μ

Tactic:
simp [hf, or_imp, forall_and]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
s : Set β
hs : s.Finite
t : β → Set α
⊢ IntegrableOn f (⋃ i ∈ ∅, t i) μ ↔ ∀ i ∈ ∅, IntegrableOn f (t i) μ

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem unique_quotient_iff_eq_top : Nonempty (Unique (M ⧸ p)) ↔ p = ⊤ :=
  ⟨fun ⟨h⟩ => subsingleton_quotient_iff_eq_top.mp (@Unique.instSubsingleton _ h),
    by rintro rfl; exact ⟨QuotientTop.unique⟩⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Nonempty (Unique (M ⧸ ⊤))

Tactic:
exact ⟨QuotientTop.unique⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ p = ⊤ → Nonempty (Unique (M ⧸ p))

Tactic:
rintro rfl

Result:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Nonempty (Unique (M ⧸ ⊤))
-- Mathlib/Analysis/Seminorm.lean
theorem neg_ball (p : Seminorm 𝕜 E) (r : ℝ) (x : E) : -ball p x r = ball p (-x) r

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x✝ : E
⊢ x✝ ∈ -p.ball x r ↔ x✝ ∈ p.ball (-x) r

Tactic:
rw [Set.mem_neg, mem_ball, mem_ball, ← neg_add', sub_neg_eq_add, map_neg_eq_map]

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ -p.ball x r = p.ball (-x) r

Tactic:
ext

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x✝ : E
⊢ x✝ ∈ -p.ball x r ↔ x✝ ∈ p.ball (-x) r
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_int_add (z : ℤ) (a : α) : ⌊↑z + a⌋ = z + ⌊a⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌊↑z + a⌋ = z + ⌊a⌋

Tactic:
simpa only [add_comm] using floor_add_int a z

Result:
no goals
-- Mathlib/Order/Part.lean
lemma Monotone.partSeq (hf : Monotone f) (hg : Monotone g) : Monotone fun x ↦ f x <*> g x

Proof state:
α : Type u_1
inst✝ : Preorder α
β γ : Type u_4
f : α → Part (β → γ)
g : α → Part β
hf : Monotone f
hg : Monotone g
⊢ Monotone fun x => f x <*> g x

Tactic:
simpa only [seq_eq_bind_map] using hf.partBind <| Monotone.of_apply₂ fun _ ↦ hg.partMap

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
theorem IsLocalization.algebraMap_mk' (x : R) (y : M) :
    algebraMap Rₘ Sₘ (IsLocalization.mk' Rₘ x y) =
      IsLocalization.mk' Sₘ (algebraMap R S x)
        ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩

Proof state:
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommRing Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ x y) = mk' Sₘ ((algebraMap R S) x) ⟨(algebraMap R S) ↑y, ⋯⟩

Tactic:
rw [IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, ←
  IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R Rₘ Sₘ,
  IsScalarTower.algebraMap_apply R Rₘ Sₘ, ← _root_.map_mul, mul_comm,
  IsLocalization.mul_mk'_eq_mk'_of_mul]

Result:
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommRing Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ (↑y * x) y) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)

Proof state:
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommRing Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ (↑y * x) y) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)

Tactic:
exact congr_arg (algebraMap Rₘ Sₘ) (IsLocalization.mk'_mul_cancel_left x y)

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem map_insert [DecidableEq α] [DecidableEq β] (f : α ↪ β) (a : α) (s : Finset α) :
    (insert a s).map f = insert (f a) (s.map f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α ↪ β
a : α
s : Finset α
⊢ map f (insert a s) = insert (f a) (map f s)

Tactic:
simp only [insert_eq, map_union, map_singleton]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
private lemma exists_lt_mul_left {a b c : ℝ≥0∞} (hc : c < a * b) : ∃ a' < a, c < a' * b

Proof state:
a b c : ℝ≥0∞
hc✝ : c < a * b
a' : ℝ≥0∞
hc : c / b < a'
ha' : a' < a
⊢ b ≠ 0

Tactic:
rintro rfl

Result:
a c a' : ℝ≥0∞
ha' : a' < a
hc✝ : c < a * 0
hc : c / 0 < a'
⊢ False

Proof state:
a b c : ℝ≥0∞
hc : c < a * b
⊢ ∃ a' < a, c < a' * b

Tactic:
obtain ⟨a', hc, ha'⟩ := exists_between (ENNReal.div_lt_of_lt_mul hc)

Result:
case intro.intro
a b c : ℝ≥0∞
hc✝ : c < a * b
a' : ℝ≥0∞
hc : c / b < a'
ha' : a' < a
⊢ ∃ a' < a, c < a' * b

Proof state:
a c a' : ℝ≥0∞
ha' : a' < a
hc✝ : c < a * 0
hc : c / 0 < a'
⊢ False

Tactic:
simp at *

Result:
no goals

Proof state:
a b a' : ℝ≥0∞
ha' : a' < a
hc✝ : ⊤ < a * b
hc : ⊤ / b < a'
⊢ False

Tactic:
simp at *

Result:
no goals

Proof state:
case intro.intro
a b c : ℝ≥0∞
hc✝ : c < a * b
a' : ℝ≥0∞
hc : c / b < a'
ha' : a' < a
⊢ ∃ a' < a, c < a' * b

Tactic:
exact ⟨_, ha', (ENNReal.div_lt_iff (.inl <| by rintro rfl; simp at *)
  (.inr <| by rintro rfl; simp at *)).1 hc⟩

Result:
no goals

Proof state:
a b c : ℝ≥0∞
hc✝ : c < a * b
a' : ℝ≥0∞
hc : c / b < a'
ha' : a' < a
⊢ c ≠ ⊤

Tactic:
rintro rfl

Result:
a b a' : ℝ≥0∞
ha' : a' < a
hc✝ : ⊤ < a * b
hc : ⊤ / b < a'
⊢ False
-- Mathlib/Topology/Constructions.lean
theorem nhdsWithin_subtype_eq_bot_iff {s t : Set X} {x : s} :
    𝓝[((↑) : s → X) ⁻¹' t] x = ⊥ ↔ 𝓝[t] (x : X) ⊓ 𝓟 s = ⊥

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
x : ↑s
⊢ 𝓝[s ↓∩ t] x = ⊥ ↔ 𝓝[t] ↑x ⊓ 𝓟 s = ⊥

Tactic:
rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal,
  nhds_induced]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_add_pos_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x = 0 ∨ y ≠ 0) :
    0 < angle x (x + y)

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ ‖x‖ * ‖x‖ < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
simpa [hx] using h0

Result:
no goals

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
hx : x = 0
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1

Tactic:
simp [hx]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1

Tactic:
by_cases hx : x = 0

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
hx : x = 0
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ 0 < angle x (x + y)

Tactic:
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_pos,
  norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1

Tactic:
rw [div_lt_one (Real.sqrt_pos.2 (Left.add_pos_of_pos_of_nonneg (mul_self_pos.2
  (norm_ne_zero_iff.2 hx)) (mul_self_nonneg _))), Real.lt_sqrt (norm_nonneg _), pow_two]

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ ‖x‖ * ‖x‖ < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖