harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Regular/Basic.lean
theorem not_isLeftRegular_zero_iff : ¬IsLeftRegular (0 : R) ↔ Nontrivial R

Proof state:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y

Tactic:
push_neg

Result:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y

Proof state:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : MulZeroClass R
⊢ ¬IsLeftRegular 0 ↔ Nontrivial R

Tactic:
rw [nontrivial_iff, not_iff_comm, isLeftRegular_zero_iff_subsingleton, subsingleton_iff]

Result:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
lemma add_left_iff {μ₁ μ₂ ν : Measure α} :
    μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
⊢ ∀ (s : Set α), ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0

Tactic:
intro s hs0

Result:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
s : Set α
hs0 : ν s = 0
⊢ μ₁ s = 0 ∧ μ₂ s = 0

Proof state:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
this : ∀ (s : Set α), ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0
⊢ μ₁ ≪ ν ∧ μ₂ ≪ ν

Tactic:
exact ⟨fun s hs0 ↦ (this s hs0).1, fun s hs0 ↦ (this s hs0).2⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ 2 • ν ≪ ν

Tactic:
exact AbsolutelyContinuous.rfl.smul_left 2

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
s : Set α
hs0 : ν s = 0
⊢ μ₁ s = 0 ∧ μ₂ s = 0

Tactic:
simpa using h hs0

Result:
no goals

Proof state:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
⊢ μ₁ ≪ ν ∧ μ₂ ≪ ν

Tactic:
have : ∀ s, ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0 := by intro s hs0; simpa using h hs0

Result:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
this : ∀ (s : Set α), ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0
⊢ μ₁ ≪ ν ∧ μ₂ ≪ ν

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
⊢ μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ (h.1.add h.2).trans ?_⟩

Result:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
⊢ μ₁ ≪ ν ∧ μ₂ ≪ ν

case refine_2
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ ν + ν ≪ ν

Proof state:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ ν + ν ≪ ν

Tactic:
rw [← two_smul ℝ≥0]

Result:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ 2 • ν ≪ ν
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem exists_SL2_smul_eq_of_apply_zero_one_ne_zero (g : SL(2, ℝ)) (hc : g 1 0 ≠ 0) :
    ∃ (u : { x : ℝ // 0 < x }) (v w : ℝ),
      (g • · : ℍ → ℍ) =
        (w +ᵥ ·) ∘ (ModularGroup.S • · : ℍ → ℍ) ∘ (v +ᵥ · : ℍ → ℍ) ∘ (u • · : ℍ → ℍ)

Proof state:
case h.h.mk.h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹

Tactic:
replace hc : (c : ℂ) ≠ 0 := by norm_cast

Result:
case h.h.mk.h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹

Proof state:
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0
⊢ ↑a * ↑d - ↑b * ↑c = 1

Tactic:
norm_cast

Result:
no goals

Proof state:
case h.h.mk.h
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹

Tactic:
replace h : (a * d - b * c : ℂ) = (1 : ℂ) := by norm_cast

Result:
case h.h.mk.h
a b c d : ℝ
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0
h : ↑a * ↑d - ↑b * ↑c = 1
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹

Proof state:
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
⊢ ↑c * z + ↑d ≠ 0

Tactic:
simpa using h_denom ⟨z, hz⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem map_roots_le [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (h : p.map f ≠ 0) :
    p.roots.map f ≤ (p.map f).roots

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
b : B
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

Tactic:
apply count_map_roots h

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
⊢ Multiset.map (⇑f) p.roots ≤ (map f p).roots

Tactic:
exact Multiset.le_iff_count.2 fun b => by
  rw [count_roots]
  apply count_map_roots h

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
b : B
⊢ count b (Multiset.map (⇑f) p.roots) ≤ count b (map f p).roots

Tactic:
rw [count_roots]

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
b : B
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
⊢ Multiset.map (⇑f) p.roots ≤ (map f p).roots

Tactic:
classical
exact Multiset.le_iff_count.2 fun b => by
  rw [count_roots]
  apply count_map_roots h

Result:
no goals
-- Mathlib/ModelTheory/Syntax.lean
theorem distinctConstantsTheory_mono {s t : Set α} (h : s ⊆ t) :
    L.distinctConstantsTheory s ⊆ L.distinctConstantsTheory t

Proof state:
L : Language
α : Type u'
s t : Set α
h : s ⊆ t
⊢ L.distinctConstantsTheory s ⊆ L.distinctConstantsTheory t

Tactic:
unfold distinctConstantsTheory

Result:
L : Language
α : Type u'
s t : Set α
h : s ⊆ t
⊢ (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) ⊆
    (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (t ×ˢ t ∩ (diagonal α)ᶜ)

Proof state:
L : Language
α : Type u'
s t : Set α
h : s ⊆ t
⊢ (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) ⊆
    (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (t ×ˢ t ∩ (diagonal α)ᶜ)

Tactic:
gcongr

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
    preserves binary coproducts. -/
lemma preservesBinaryCoproduct_of_preservesBinaryBiproduct {X Y : C}
    [PreservesBinaryBiproduct X Y F] :
    PreservesColimit (pair X Y) F where
  preserves {c} hc :=
    ⟨IsColimit.ofIsoColimit
        ((IsColimit.precomposeHomEquiv (diagramIsoPair _) _).symm
          (isBinaryBilimitOfPreserves F
              (binaryBiconeIsBilimitOfColimitCoconeOfIsColimit hc)).isColimit) <|
      Cocones.ext (by dsimp; rfl) fun j => by
        rcases j with ⟨⟨⟩⟩ <;> simp⟩

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
j : Discrete WalkingPair
⊢ ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
              (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)).toCocone).ι.app
        j ≫
      (id (Iso.refl (F.obj c.pt))).hom =
    (F.mapCocone c).ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
⊢ F.obj c.pt ≅ F.obj c.pt

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
⊢ ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
        (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)).toCocone).pt ≅
    (F.mapCocone c).pt

Tactic:
dsimp

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
⊢ F.obj c.pt ≅ F.obj c.pt
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Erase.lean
theorem eraseIdx_length_sub_one (l : List α) :
    (l.eraseIdx (l.length - 1)) = l.dropLast

Proof state:
case h
α : Type u_1
l : List α
n : Nat
h₁ : n < (l.eraseIdx (l.length - 1)).length
h₂ : n < l.dropLast.length
⊢ (l.eraseIdx (l.length - 1))[n] = l.dropLast[n]

Tactic:
rw [getElem_eraseIdx_of_lt, getElem_dropLast]

Result:
case h.h'
α : Type u_1
l : List α
n : Nat
h₁ : n < (l.eraseIdx (l.length - 1)).length
h₂ : n < l.dropLast.length
⊢ n < l.length - 1

Proof state:
case h
α : Type u_1
l : List α
⊢ ∀ (i : Nat) (h₁ : i < (l.eraseIdx (l.length - 1)).length) (h₂ : i < l.dropLast.length),
    (l.eraseIdx (l.length - 1))[i] = l.dropLast[i]

Tactic:
intro n h₁ h₂

Result:
case h
α : Type u_1
l : List α
n : Nat
h₁ : n < (l.eraseIdx (l.length - 1)).length
h₂ : n < l.dropLast.length
⊢ (l.eraseIdx (l.length - 1))[n] = l.dropLast[n]

Proof state:
α : Type u_1
l : List α
⊢ l.eraseIdx (l.length - 1) = l.dropLast

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
l : List α
⊢ (l.eraseIdx (l.length - 1)).length = l.dropLast.length

case h
α : Type u_1
l : List α
⊢ ∀ (i : Nat) (h₁ : i < (l.eraseIdx (l.length - 1)).length) (h₂ : i < l.dropLast.length),
    (l.eraseIdx (l.length - 1))[i] = l.dropLast[i]

Proof state:
case h.h'
α : Type u_1
l : List α
n : Nat
h₁ : n < (l.eraseIdx (l.length - 1)).length
h₂ : n < l.dropLast.length
⊢ n < l.length - 1

Tactic:
simp_all

Result:
no goals

Proof state:
case hl
α : Type u_1
l : List α
⊢ l.length ≤ l.length - 1 → l.length = l.length - 1

Tactic:
omega

Result:
no goals

Proof state:
case hl
α : Type u_1
l : List α
⊢ (l.eraseIdx (l.length - 1)).length = l.dropLast.length

Tactic:
simp [length_eraseIdx]

Result:
case hl
α : Type u_1
l : List α
⊢ l.length ≤ l.length - 1 → l.length = l.length - 1
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem ediam_image (s : Set α) : EMetric.diam ((f : α → β) '' s) = ratio f * EMetric.diam s

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ EMetric.diam (⇑f '' s) = ↑(ratio f) * EMetric.diam s

Tactic:
refine ((lipschitz f).ediam_image_le s).antisymm ?_

Result:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ↑(ratio f) * EMetric.diam s ≤ EMetric.diam (⇑f '' s)

Proof state:
case h
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ EMetric.diam s ≤ ↑(ratio f)⁻¹ * EMetric.diam (⇑f '' s)

case h
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ratio f ≠ 0

Tactic:
exacts [(antilipschitz f).le_mul_ediam_image s, ratio_ne_zero f]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ↑(ratio f) * EMetric.diam s ≤ EMetric.diam (⇑f '' s)

Tactic:
apply ENNReal.mul_le_of_le_div'

Result:
case h
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ EMetric.diam s ≤ EMetric.diam (⇑f '' s) / ↑(ratio f)

Proof state:
case h
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ EMetric.diam s ≤ EMetric.diam (⇑f '' s) / ↑(ratio f)

Tactic:
rw [div_eq_mul_inv, mul_comm, ← ENNReal.coe_inv]

Result:
case h
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ EMetric.diam s ≤ ↑(ratio f)⁻¹ * EMetric.diam (⇑f '' s)

case h
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ratio f ≠ 0
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem oangle_rotation_oangle_right (x y : V) : o.oangle y (o.rotation (o.oangle x y) x) = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ -o.oangle ((o.rotation (o.oangle x y)) x) y = 0

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle y ((o.rotation (o.oangle x y)) x) = 0

Tactic:
rw [oangle_rev]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ -o.oangle ((o.rotation (o.oangle x y)) x) y = 0
-- Mathlib/Order/Interval/Finset/Basic.lean
/-- In a locally finite preorder, `≤` is the transitive closure of `⩿`. -/
lemma le_iff_transGen_wcovBy [Preorder α] [LocallyFiniteOrder α] {x y : α} :
    x ≤ y ↔ TransGen (· ⩿ ·) x y

Proof state:
case single
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y b✝ : α
h : x ⩿ b✝
⊢ x ≤ b✝

Tactic:
exact h.le

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
h : TransGen (fun x1 x2 => x1 ⩿ x2) x y
⊢ x ≤ y

Tactic:
induction h with
| single h => exact h.le
| tail _ h₁ h₂ => exact h₂.trans h₁.le

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
⊢ x ≤ y ↔ TransGen (fun x1 x2 => x1 ⩿ x2) x y

Tactic:
refine ⟨transGen_wcovBy_of_le, fun h ↦ ?_⟩

Result:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
h : TransGen (fun x1 x2 => x1 ⩿ x2) x y
⊢ x ≤ y

Proof state:
case tail
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y b✝ c✝ : α
a✝ : TransGen (fun x1 x2 => x1 ⩿ x2) x b✝
h₁ : b✝ ⩿ c✝
h₂ : x ≤ b✝
⊢ x ≤ c✝

Tactic:
exact h₂.trans h₁.le

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem measure_toMeasurable (s : Set α) : μ (toMeasurable μ s) = μ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ (toMeasurable μ s) = μ s

Tactic:
rw [toMeasurable_def]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ
      (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then h.choose
      else
        if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose
        else ⋯.choose) =
    μ s

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ μ h's.choose = μ s

Tactic:
simpa only [inter_univ] using h's.choose_spec.2.2 univ MeasurableSet.univ

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ
      (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then h.choose
      else
        if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose
        else ⋯.choose) =
    μ s

Tactic:
split_ifs with hs h's

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ μ hs.choose = μ s

case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ μ h's.choose = μ s

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's : ¬∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ μ ⋯.choose = μ s

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ μ hs.choose = μ s

Tactic:
exact measure_congr hs.choose_spec.2.2

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's : ¬∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ μ ⋯.choose = μ s

Tactic:
exact (exists_measurable_superset μ s).choose_spec.2.2

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem lipschitzWith_compLp [Fact (1 ≤ p)] (hg : LipschitzWith c g) (g0 : g 0 = 0) :
    LipschitzWith c (hg.compLp g0 : Lp E p μ → Lp F p μ) :=
  -- squeezed for performance reasons
  LipschitzWith.of_dist_le_mul fun f g => by simp only [dist_eq_norm, norm_compLp_sub_le]

Proof state:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g✝ : E → F
c : ℝ≥0
inst✝ : Fact (1 ≤ p)
hg : LipschitzWith c g✝
g0 : g✝ 0 = 0
f g : ↥(Lp E p μ)
⊢ dist (hg.compLp g0 f) (hg.compLp g0 g) ≤ ↑c * dist f g

Tactic:
simp only [dist_eq_norm, norm_compLp_sub_le]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem yang_baxter (X Y Z : C) :
    (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫
    Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom =
      X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫
      (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ X Y Z).inv ≫
      (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom

Tactic:
rw [← braiding_tensor_right_assoc X Y Z, ← cancel_mono (α_ Z Y X).inv]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom) ≫ (α_ Z Y X).inv =
    (X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom) ≫ (α_ Z Y X).inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom ≫ (α_ Z Y X).inv

Tactic:
rw [Iso.hom_inv_id, comp_id, ← braiding_naturality_right, braiding_tensor_right]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom) ≫ (α_ Z Y X).inv =
    (X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom) ≫ (α_ Z Y X).inv

Tactic:
repeat rw [assoc]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom ≫ (α_ Z Y X).inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ ((α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom) ≫ (α_ Z Y X).inv

Tactic:
rw [assoc]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom ≫ (α_ Z Y X).inv =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom ≫ (α_ Z Y X).inv
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem conGen_idem (r : M → M → Prop) : conGen (conGen r) = conGen r

Proof state:
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
⊢ conGen ⇑(conGen r) = conGen r

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Weierstrass.lean
theorem exists_polynomial_near_continuousMap (a b : ℝ) (f : C(Set.Icc a b, ℝ)) (ε : ℝ)
    (pos : 0 < ε) : ∃ p : ℝ[X], ‖p.toContinuousMapOn _ - f‖ < ε

Proof state:
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(↑(Set.Icc a b), ℝ)) in nhds f, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring
⊢ ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Tactic:
rw [Metric.nhds_basis_ball.frequently_iff] at w

Result:
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring
⊢ ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Proof state:
case intro.intro.intro.intro
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring
m : ℝ[X]
H : ↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m ∈ Metric.ball f ε
⊢ ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Tactic:
rw [Metric.mem_ball, dist_eq_norm] at H

Result:
case intro.intro.intro.intro
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring
m : ℝ[X]
H : ‖↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m - f‖ < ε
⊢ ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Proof state:
case intro.intro.intro.intro
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring
m : ℝ[X]
H : ‖↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m - f‖ < ε
⊢ ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Tactic:
exact ⟨m, H⟩

Result:
no goals

Proof state:
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring
⊢ ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Tactic:
obtain ⟨-, H, ⟨m, ⟨-, rfl⟩⟩⟩ := w ε pos

Result:
case intro.intro.intro.intro
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring
m : ℝ[X]
H : ↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m ∈ Metric.ball f ε
⊢ ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Proof state:
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

Tactic:
have w := mem_closure_iff_frequently.mp (continuousMap_mem_polynomialFunctions_closure _ _ f)

Result:
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(↑(Set.Icc a b), ℝ)) in nhds f, x ∈ ↑(polynomialFunctions (Set.Icc a b)).toSubsemiring
⊢ ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε