harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobject_zero_arrow : (imageSubobject (0 : X ⟶ Y)).arrow = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ (imageSubobjectIso 0).hom ≫ image.ι 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ (imageSubobject 0).arrow = 0

Tactic:
rw [← imageSubobject_arrow]

Result:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ (imageSubobjectIso 0).hom ≫ image.ι 0 = 0
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_iSup_le_lift {ι} {f : ι → Ordinal} (H : ∀ i, f i < iSup f) :
    cof (iSup f) ≤ Cardinal.lift.{v, u} #ι

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
H : sup f = lsub f
⊢ (sup f).cof ≤ Cardinal.lift.{v, u} #ι

Tactic:
rw [H]

Result:
ι : Type u
f : ι → Ordinal.{max u v}
H : sup f = lsub f
⊢ (lsub f).cof ≤ Cardinal.lift.{v, u} #ι

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
H : sup f = lsub f
⊢ (lsub f).cof ≤ Cardinal.lift.{v, u} #ι

Tactic:
exact cof_lsub_le_lift f

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
⊢ (iSup f).cof ≤ Cardinal.lift.{v, u} #ι

Tactic:
rw [← Ordinal.sup] at *

Result:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < sup f
⊢ (sup f).cof ≤ Cardinal.lift.{v, u} #ι

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < sup f
⊢ (sup f).cof ≤ Cardinal.lift.{v, u} #ι

Tactic:
rw [← sup_eq_lsub_iff_lt_sup.{u, v}] at H

Result:
ι : Type u
f : ι → Ordinal.{max u v}
H : sup f = lsub f
⊢ (sup f).cof ≤ Cardinal.lift.{v, u} #ι
-- Mathlib/Data/Real/Hyperreal.lean
theorem Infinitesimal.add {x y : ℝ*} (hx : Infinitesimal x) (hy : Infinitesimal y) :
    Infinitesimal (x + y)

Proof state:
x y : ℝ*
hx : x.Infinitesimal
hy : y.Infinitesimal
⊢ (x + y).Infinitesimal

Tactic:
simpa only [add_zero] using hx.add hy

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem relindex_inf_le : (H ⊓ K).relindex L ≤ H.relindex L * K.relindex L

Proof state:
case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : H.relindex L = 0
⊢ (H ⊓ K).relindex L ≤ H.relindex L * K.relindex L

Tactic:
exact (le_of_eq (relindex_eq_zero_of_le_left inf_le_left h)).trans (zero_le _)

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relindex L = 0
⊢ H.relindex (K ⊓ L) * K.relindex L ≤ H.relindex L * K.relindex L

Tactic:
exact mul_le_mul_right' (relindex_le_of_le_right inf_le_right h) (K.relindex L)

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relindex L = 0
⊢ (H ⊓ K).relindex L ≤ H.relindex L * K.relindex L

Tactic:
rw [← inf_relindex_right, inf_assoc, ← relindex_mul_relindex _ _ L inf_le_right inf_le_right,
  inf_relindex_right, inf_relindex_right]

Result:
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relindex L = 0
⊢ H.relindex (K ⊓ L) * K.relindex L ≤ H.relindex L * K.relindex L

Proof state:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ (H ⊓ K).relindex L ≤ H.relindex L * K.relindex L

Tactic:
by_cases h : H.relindex L = 0

Result:
case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : H.relindex L = 0
⊢ (H ⊓ K).relindex L ≤ H.relindex L * K.relindex L

case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relindex L = 0
⊢ (H ⊓ K).relindex L ≤ H.relindex L * K.relindex L
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem Heap.realSize_tail (le) (s : Heap α) : (s.tail le).realSize = s.realSize - 1

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ (tail le s).realSize = s.realSize - 1

Tactic:
simp only [Heap.tail]

Result:
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ ((tail? le s).getD nil).realSize = s.realSize - 1

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
eq : tail? le s = none
⊢ (none.getD nil).realSize = s.realSize - 1

Tactic:
cases s with cases eq | nil => rfl

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s tl : Heap α
eq : tail? le s = some tl
⊢ ((some tl).getD nil).realSize = s.realSize - 1

Tactic:
simp [Heap.realSize_tail? eq]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ ((tail? le s).getD nil).realSize = s.realSize - 1

Tactic:
match eq : s.tail? le with
| none => cases s with cases eq | nil => rfl
| some tl => simp [Heap.realSize_tail? eq]

Result:
no goals

Proof state:
case nil.refl
α : Type u_1
le : α → α → Bool
⊢ (none.getD nil).realSize = nil.realSize - 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem quotientEquiv.symm_apply [Fintype ι] (x : fundamentalDomain b) :
    (quotientEquiv b).symm x = Submodule.Quotient.mk ↑x

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : ↑(fundamentalDomain b)
⊢ (quotientEquiv b).symm x = Submodule.Quotient.mk ↑x

Tactic:
rw [Equiv.symm_apply_eq, quotientEquiv_apply_mk b ↑x, Subtype.ext_iff, fractRestrict_apply]

Result:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : ↑(fundamentalDomain b)
⊢ ↑x = fract b ↑x

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : ↑(fundamentalDomain b)
⊢ ↑x = fract b ↑x

Tactic:
exact (fract_eq_self.mpr x.prop).symm

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_eq_one_iff (hl : Nodup l) : formPerm l = 1 ↔ l.length ≤ 1

Proof state:
case cons.mp
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 → (hd :: tl).formPerm hd = hd

Tactic:
simp +contextual

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 ↔ (hd :: tl).formPerm hd = hd

Tactic:
constructor

Result:
case cons.mp
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 → (hd :: tl).formPerm hd = hd

case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm hd = hd → (hd :: tl).formPerm = 1

Proof state:
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
h : (hd :: tl).formPerm hd = hd
⊢ (hd :: tl).formPerm = 1

Tactic:
simp only [(hd :: tl).formPerm_apply_mem_eq_self_iff hl hd (mem_cons_self hd tl),
  add_le_iff_nonpos_left, length, nonpos_iff_eq_zero, length_eq_zero] at h

Result:
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
h : tl = []
⊢ (hd :: tl).formPerm = 1

Proof state:
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm hd = hd → (hd :: tl).formPerm = 1

Tactic:
intro h

Result:
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
h : (hd :: tl).formPerm hd = hd
⊢ (hd :: tl).formPerm = 1

Proof state:
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
h : tl = []
⊢ (hd :: tl).formPerm = 1

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
⊢ l.formPerm = 1 ↔ l.length ≤ 1

Tactic:
rcases l with - | ⟨hd, tl⟩

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
hl : [].Nodup
⊢ [].formPerm = 1 ↔ [].length ≤ 1

case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 ↔ (hd :: tl).length ≤ 1

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 ↔ (hd :: tl).length ≤ 1

Tactic:
rw [← formPerm_apply_mem_eq_self_iff _ hl hd (mem_cons_self _ _)]

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 ↔ (hd :: tl).formPerm hd = hd

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
hl : [].Nodup
⊢ [].formPerm = 1 ↔ [].length ≤ 1

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem isSeparatedFor_top (P : Cᵒᵖ ⥤ Type w) : IsSeparatedFor P (⊤ : Presieve X) :=
  fun x t₁ t₂ h₁ h₂ => by
  have q₁ := h₁ (𝟙 X) (by tauto)
  have q₂ := h₂ (𝟙 X) (by tauto)
  simp only [op_id, FunctorToTypes.map_id_apply] at q₁ q₂
  rw [q₁, q₂]

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
q₁ : P.map (𝟙 X).op t₁ = x (𝟙 X) trivial
⊢ ⊤ (𝟙 X)

Tactic:
tauto

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂

Tactic:
have q₁ := h₁ (𝟙 X) (by tauto)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
q₁ : P.map (𝟙 X).op t₁ = x (𝟙 X) trivial
⊢ t₁ = t₂

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
q₁ : P.map (𝟙 X).op t₁ = x (𝟙 X) trivial
q₂ : P.map (𝟙 X).op t₂ = x (𝟙 X) trivial
⊢ t₁ = t₂

Tactic:
simp only [op_id, FunctorToTypes.map_id_apply] at q₁ q₂

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
q₁ : t₁ = x (𝟙 X) trivial
q₂ : t₂ = x (𝟙 X) trivial
⊢ t₁ = t₂

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
q₁ : t₁ = x (𝟙 X) trivial
q₂ : t₂ = x (𝟙 X) trivial
⊢ t₁ = t₂

Tactic:
rw [q₁, q₂]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
⊢ ⊤ (𝟙 X)

Tactic:
tauto

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
q₁ : P.map (𝟙 X).op t₁ = x (𝟙 X) trivial
⊢ t₁ = t₂

Tactic:
have q₂ := h₂ (𝟙 X) (by tauto)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
q₁ : P.map (𝟙 X).op t₁ = x (𝟙 X) trivial
q₂ : P.map (𝟙 X).op t₂ = x (𝟙 X) trivial
⊢ t₁ = t₂
-- Mathlib/Topology/Category/Compactum.lean
theorem str_incl (X : Compactum) (x : X) : X.str (X.incl x) = x

Proof state:
X : Compactum
x : X.A
⊢ X.str (X.incl x) = x

Tactic:
change ((β ).η.app _ ≫ X.a) _ = _

Result:
X : Compactum
x : X.A
⊢ (β.η.app X.A ≫ X.a) x = x

Proof state:
X : Compactum
x : X.A
⊢ 𝟙 X.A x = x

Tactic:
rfl

Result:
no goals

Proof state:
X : Compactum
x : X.A
⊢ (β.η.app X.A ≫ X.a) x = x

Tactic:
rw [Monad.Algebra.unit]

Result:
X : Compactum
x : X.A
⊢ 𝟙 X.A x = x
-- Mathlib/Data/Fintype/Quotient.lean
@[simp]
lemma finRecOn_mk {C : (∀ i, Trunc (α i)) → Sort*}
    (a : ∀ i, α i) :
    finRecOn (C := C) (⟦a ·⟧) = fun f _ ↦ f a

Proof state:
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Sort u_2
C : ((i : ι) → Trunc (α i)) → Sort u_4
a : (i : ι) → α i
⊢ (fun f h => Quotient.finRecOn (fun x => ⟦a x⟧) (fun x => f x) ⋯) = fun f x => f a

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Sort u_2
C : ((i : ι) → Trunc (α i)) → Sort u_4
a : (i : ι) → α i
⊢ (finRecOn fun x => ⟦a x⟧) = fun f x => f a

Tactic:
unfold finRecOn

Result:
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Sort u_2
C : ((i : ι) → Trunc (α i)) → Sort u_4
a : (i : ι) → α i
⊢ (fun f h => Quotient.finRecOn (fun x => ⟦a x⟧) (fun x => f x) ⋯) = fun f x => f a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem tail_range (n : Nat) : (range n).tail = range' 1 (n - 1)

Proof state:
n : Nat
⊢ (range n).tail = range' 1 (n - 1)

Tactic:
rw [range_eq_range', tail_range']

Result:
no goals
-- Mathlib/Tactic/Module.lean
theorem sub_eq_eval₂ [Ring R] [AddCommGroup M] [Module R M] (r₁ r₂ : R) (x : M) {l₁ l₂ l : NF R M}
    (h : l₁.eval - l₂.eval = l.eval) :
    ((r₁, x) ::ᵣ l₁).eval - ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval

Proof state:
case h.e'_6
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ l₁.eval + (-(r₂ • x) + -l₂.eval) = -(r₂ • x) + (l₁.eval + -l₂.eval)

Tactic:
simp only [← add_assoc]

Result:
case h.e'_6
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ l₁.eval + -(r₂ • x) + -l₂.eval = -(r₂ • x) + l₁.eval + -l₂.eval

Proof state:
case h.e'_6.h.e'_5
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ l₁.eval + -(r₂ • x) = -(r₂ • x) + l₁.eval

Tactic:
rw [add_comm]

Result:
no goals

Proof state:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ r₁ • x + (l₁.eval + (-(r₂ • x) + -l₂.eval)) = r₁ • x + (-(r₂ • x) + (l₁.eval + -l₂.eval))

Tactic:
congr! 1

Result:
case h.e'_6
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ l₁.eval + (-(r₂ • x) + -l₂.eval) = -(r₂ • x) + (l₁.eval + -l₂.eval)

Proof state:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ ((r₁, x) ::ᵣ l₁).eval - ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval

Tactic:
simp only [← h, eval_cons, sub_smul, sub_eq_add_neg, neg_add, add_smul, neg_smul, add_assoc]

Result:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ r₁ • x + (l₁.eval + (-(r₂ • x) + -l₂.eval)) = r₁ • x + (-(r₂ • x) + (l₁.eval + -l₂.eval))

Proof state:
case h.e'_6
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ l₁.eval + -(r₂ • x) + -l₂.eval = -(r₂ • x) + l₁.eval + -l₂.eval

Tactic:
congr! 1

Result:
case h.e'_6.h.e'_5
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ l₁.eval + -(r₂ • x) = -(r₂ • x) + l₁.eval
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
/-- A simple sufficient condition for bounding `levyProkhorovEDist` between probability measures
from above. The condition involves only one of two natural bounds, the other bound is for free. -/
lemma levyProkhorovEDist_le_of_forall_le
    (μ ν : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (δ : ℝ≥0∞)
    (h : ∀ ε B, δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε) :
    levyProkhorovEDist μ ν ≤ δ

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
⊢ ν B ≤ μ (thickening ε.toReal B) + ε

Tactic:
apply (measure_mono (μ := ν) B_subset).trans

Result:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
⊢ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ ≤ μ (thickening ε.toReal B) + ε
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_prod_of_pairwise_disjoint (l : List (Perm α)) (h : l.Pairwise Disjoint) :
    l.prod.support = (l.map support).foldr (· ⊔ ·) ⊥

Proof state:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → tl.prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
h : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
⊢ (hd :: tl).prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Tactic:
have : Disjoint hd tl.prod := disjoint_prod_right _ h.left

Result:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → tl.prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
h : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
this : hd.Disjoint tl.prod
⊢ (hd :: tl).prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Proof state:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → tl.prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
h : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
this : hd.Disjoint tl.prod
⊢ (hd :: tl).prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Tactic:
simp [this.support_mul, hl h.right]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → tl.prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
h : List.Pairwise Disjoint (hd :: tl)
⊢ (hd :: tl).prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Tactic:
rw [List.pairwise_cons] at h

Result:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → tl.prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
h : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
⊢ (hd :: tl).prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
h : List.Pairwise Disjoint l
⊢ l.prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support l)

Tactic:
induction' l with hd tl hl

Result:
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : List.Pairwise Disjoint []
⊢ [].prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support [])

case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → tl.prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
h : List.Pairwise Disjoint (hd :: tl)
⊢ (hd :: tl).prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Proof state:
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : List.Pairwise Disjoint []
⊢ [].prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support [])

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
theorem ordConnectedProj_eq {x y : s} :
    ordConnectedProj s x = ordConnectedProj s y ↔ [[(x : α), y]] ⊆ s

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
⊢ s.ordConnectedProj x = s.ordConnectedProj y ↔ [[↑x, ↑y]] ⊆ s

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : s.ordConnectedProj x = s.ordConnectedProj y
⊢ [[↑x, ↑y]] ⊆ s

case mpr
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : [[↑x, ↑y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y

Proof state:
case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : s.ordConnectedProj x = s.ordConnectedProj y
⊢ [[↑x, ↑y]] ⊆ s

Tactic:
rw [← mem_ordConnectedComponent, ← ordConnectedComponent_ordConnectedProj, h,
  ordConnectedComponent_ordConnectedProj, self_mem_ordConnectedComponent]

Result:
case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : s.ordConnectedProj x = s.ordConnectedProj y
⊢ ↑y ∈ s

Proof state:
case mpr
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : [[↑x, ↑y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y

Tactic:
simp only [ordConnectedProj, ordConnectedComponent_eq h]

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : s.ordConnectedProj x = s.ordConnectedProj y
⊢ ↑y ∈ s

Tactic:
exact y.2

Result:
no goals
-- Mathlib/Algebra/Lie/SkewAdjoint.lean
theorem mem_skewAdjointMatricesLieSubalgebra_unit_smul (u : Rˣ) (J A : Matrix n n R) :
    A ∈ skewAdjointMatricesLieSubalgebra (u • J) ↔ A ∈ skewAdjointMatricesLieSubalgebra J

Proof state:
case mpr
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u : Rˣ
J A : Matrix n n R
h : Aᵀ * J = J * -A
⊢ Aᵀ * u • J = u • J * -A

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u : Rˣ
J A : Matrix n n R
⊢ A ∈ skewAdjointMatricesLieSubalgebra (u • J) ↔ A ∈ skewAdjointMatricesLieSubalgebra J

Tactic:
change A ∈ skewAdjointMatricesSubmodule (u • J) ↔ A ∈ skewAdjointMatricesSubmodule J

Result:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u : Rˣ
J A : Matrix n n R
⊢ A ∈ skewAdjointMatricesSubmodule (u • J) ↔ A ∈ skewAdjointMatricesSubmodule J

Proof state:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u : Rˣ
J A : Matrix n n R
⊢ A ∈ skewAdjointMatricesSubmodule (u • J) ↔ A ∈ skewAdjointMatricesSubmodule J

Tactic:
simp only [mem_skewAdjointMatricesSubmodule, Matrix.IsSkewAdjoint, Matrix.IsAdjointPair]

Result:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * u • J = u • J * -A ↔ Aᵀ * J = J * -A

Proof state:
case mp
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u : Rˣ
J A : Matrix n n R
h : Aᵀ * u • J = u • J * -A
⊢ Aᵀ * J = J * -A

Tactic:
simpa using congr_arg (fun B => u⁻¹ • B) h

Result:
no goals

Proof state:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * u • J = u • J * -A ↔ Aᵀ * J = J * -A

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u : Rˣ
J A : Matrix n n R
h : Aᵀ * u • J = u • J * -A
⊢ Aᵀ * J = J * -A

case mpr
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u : Rˣ
J A : Matrix n n R
h : Aᵀ * J = J * -A
⊢ Aᵀ * u • J = u • J * -A