harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Pi.lean
theorem ker_pi (f : (i : ι) → M₂ →ₗ[R] φ i) : ker (pi f) = ⨅ i : ι, ker (f i)

Proof state:
case h
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
⊢ c ∈ ker (pi f) ↔ c ∈ ⨅ i, ker (f i)

Tactic:
simp [funext_iff]

Result:
no goals

Proof state:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M₂ →ₗ[R] φ i
⊢ ker (pi f) = ⨅ i, ker (f i)

Tactic:
ext c

Result:
case h
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
⊢ c ∈ ker (pi f) ↔ c ∈ ⨅ i, ker (f i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem swap_then (o₁ o₂ : Ordering) : (o₁.then o₂).swap = o₁.swap.then o₂.swap

Proof state:
o₁ o₂ : Ordering
⊢ (o₁.then o₂).swap = o₁.swap.then o₂.swap

Tactic:
cases o₁ <;> rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_mul_diff' (hst : s ⊆ t) (ht : (t ∩ mulSupport f).Finite) :
    ((∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t \ s, f i) = ∏ᶠ i ∈ t, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hst : s ⊆ t
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
rw [← finprod_mem_inter_mul_diff' _ ht, inter_eq_self_of_subset_right hst]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mem_zipIdx_iff_getElem? {x : α × Nat} {l : List α} : x ∈ zipIdx l ↔ l[x.2]? = some x.1

Proof state:
case mk
α : Type u_1
l : List α
fst✝ : α
snd✝ : Nat
⊢ (fst✝, snd✝) ∈ l.zipIdx ↔ l[(fst✝, snd✝).snd]? = some (fst✝, snd✝).fst

Tactic:
simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]

Result:
no goals

Proof state:
α : Type u_1
x : α × Nat
l : List α
⊢ x ∈ l.zipIdx ↔ l[x.snd]? = some x.fst

Tactic:
cases x

Result:
case mk
α : Type u_1
l : List α
fst✝ : α
snd✝ : Nat
⊢ (fst✝, snd✝) ∈ l.zipIdx ↔ l[(fst✝, snd✝).snd]? = some (fst✝, snd✝).fst
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@[simp]
lemma restrictionLE_map {k₁ k₂ : Set.Iic i} (φ : k₁ ⟶ k₂) :
    (restrictionLE F hi).map φ = F.map (homOfLE (by simpa using leOfHom φ)) := rfl

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : PartialOrder J
j : J
F : ↑(Set.Iic j) ⥤ C
i : J
hi : i ≤ j
k₁ k₂ : ↑(Set.Iic i)
φ : k₁ ⟶ k₂
⊢ ⋯.functor.obj k₁ ≤ ⋯.functor.obj k₂

Tactic:
simpa using leOfHom φ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/FinRange.lean
theorem length_finRange (n) : (List.finRange n).length = n

Proof state:
n : Nat
⊢ (finRange n).length = n

Tactic:
simp [List.finRange]

Result:
no goals
-- Mathlib/Algebra/Group/Operations.lean
@[to_additive]
lemma dite_mul_dite (a : P → α) (b : ¬ P → α) (c : P → α) (d : ¬ P → α) :
    ((if h : P then a h else b h) * if h : P then c h else d h) =
      if h : P then a h * c h else b h * d h

Proof state:
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
⊢ ((if h : P then a h else b h) * if h : P then c h else d h) = if h : P then a h * c h else b h * d h

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_equal {t₁ t₂ : L.Term α} {x : α → M} :
    (t₁.equal t₂).Realize x ↔ t₁.realize x = t₂.realize x

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
t₁ t₂ : L.Term α
x : α → M
⊢ (t₁.equal t₂).Realize x ↔ Term.realize x t₁ = Term.realize x t₂

Tactic:
simp [Term.equal, Realize]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem subset_union {H K L : S} : (H : Set G) ⊆ K ∪ L ↔ H ≤ K ∨ H ≤ L

Proof state:
G : Type u_1
inst✝² : Group G
S : Type u_4
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
H K L : S
h : ↑H ⊆ ↑K ∪ ↑L
⊢ H ≤ K ∨ H ≤ L

Tactic:
rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]

Result:
G : Type u_1
inst✝² : Group G
S : Type u_4
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
H K L : S
h : ↑H ⊆ ↑K ∪ ↑L
⊢ (∃ x ∈ H, x ∉ K) → H ≤ L
-- Mathlib/RingTheory/Radical.lean
theorem _root_.IsCoprime.divRadical {a b : E} (h : IsCoprime a b) :
    IsCoprime (divRadical a) (divRadical b)

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
h : IsCoprime (radical a * EuclideanDomain.divRadical a) b
⊢ IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)

Tactic:
rw [← radical_mul_divRadical b] at h

Result:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
h : IsCoprime (radical a * EuclideanDomain.divRadical a) (radical b * EuclideanDomain.divRadical b)
⊢ IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
h : IsCoprime (radical a * EuclideanDomain.divRadical a) (radical b * EuclideanDomain.divRadical b)
⊢ IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)

Tactic:
exact h.of_mul_left_right.of_mul_right_right

Result:
no goals

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
h : IsCoprime a b
⊢ IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)

Tactic:
rw [← radical_mul_divRadical a] at h

Result:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
h : IsCoprime (radical a * EuclideanDomain.divRadical a) b
⊢ IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- The Hurwitz zeta function is differentiable everywhere except at `s = 1`. This is true
even in the delicate case `a = 0` and `s = 0` (where the completed zeta has a pole, but this is
cancelled out by the Gamma factor). -/
lemma differentiableAt_hurwitzZetaEven (a : UnitAddCircle) {s : ℂ} (hs' : s ≠ 1) :
    DifferentiableAt ℂ (hurwitzZetaEven a) s

Proof state:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ
    (Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0)) s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
exact this

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
have := differentiableAt_update_of_residue
  (fun t ht ht' ↦ differentiableAt_completedHurwitzZetaEven a (Or.inl ht) ht')
  (completedHurwitzZetaEven_residue_zero a) s hs'

Result:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ
    (Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 ((if a = 0 then -1 else 0) / 2)) s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Proof state:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ
    (Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 ((if a = 0 then -1 else 0) / 2)) s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
simp_rw [div_eq_mul_inv, ite_mul, zero_mul, ← div_eq_mul_inv] at this

Result:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ
    (Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0)) s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem map_edgeFinset_induce_of_support_subset (h : G.support ⊆ s) :
    (G.induce s).edgeFinset.map (Embedding.subtype s).sym2Map = G.edgeFinset

Proof state:
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.support ⊆ s
⊢ map (Embedding.subtype s).sym2Map (induce s G).edgeFinset = G.edgeFinset

Tactic:
simpa [map_edgeFinset_induce] using edgeFinset_subset_sym2_of_support_subset h

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem mem_sum {f : α → Multiset β} (s : Finset α) (b : β) :
    (b ∈ ∑ x ∈ s, f x) ↔ ∃ a ∈ s, b ∈ f a

Proof state:
case empty
α : Type u_3
β : Type u_4
f : α → Multiset β
b : β
⊢ b ∈ ∑ x ∈ ∅, f x ↔ ∃ a ∈ ∅, b ∈ f a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
f : α → Multiset β
s : Finset α
b : β
⊢ b ∈ ∑ x ∈ s, f x ↔ ∃ a ∈ s, b ∈ f a

Tactic:
induction s using Finset.cons_induction with
| empty => simp
| cons a t hi ih => simp [sum_cons, ih, or_and_right, exists_or]

Result:
no goals

Proof state:
case cons
α : Type u_3
β : Type u_4
f : α → Multiset β
b : β
a : α
t : Finset α
hi : a ∉ t
ih : b ∈ ∑ x ∈ t, f x ↔ ∃ a ∈ t, b ∈ f a
⊢ b ∈ ∑ x ∈ cons a t hi, f x ↔ ∃ a_1 ∈ cons a t hi, b ∈ f a_1

Tactic:
simp [sum_cons, ih, or_and_right, exists_or]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKeyD_alter_self [LawfulBEq α] [Inhabited α] {k : α} {fallback : α}
    {f : Option (β k) → Option (β k)} :
    (m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome then k else fallback

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k fallback : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome = true then k else fallback

Tactic:
simp [getKeyD_alter]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem hom_inv_id_tensor' {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
    (f ⊗ g) ≫ (inv f ⊗ h) = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ 𝟙 V ⊗ g ≫ h = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)

Tactic:
simp [id_tensorHom]

Result:
no goals

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f ⊗ g) ≫ (inv f ⊗ h) = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)

Tactic:
rw [← tensor_comp, IsIso.hom_inv_id]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ 𝟙 V ⊗ g ≫ h = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem hom_ext (h : IsLimit t) {W : C} {f f' : W ⟶ t.pt}
    (w : ∀ j, f ≫ t.π.app j = f' ≫ t.π.app j) :
    f = f'

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ h.lift { pt := W, π := { app := fun b => f ≫ t.π.app b, naturality := ⋯ } } =
    h.lift { pt := W, π := { app := fun b => f' ≫ t.π.app b, naturality := ⋯ } }

Tactic:
congr

Result:
case h.e_8.h.e_π.e_app
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ (fun b => f ≫ t.π.app b) = fun b => f' ≫ t.π.app b

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ f = f'

Tactic:
rw [h.hom_lift f, h.hom_lift f']

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ h.lift { pt := W, π := { app := fun b => f ≫ t.π.app b, naturality := ⋯ } } =
    h.lift { pt := W, π := { app := fun b => f' ≫ t.π.app b, naturality := ⋯ } }

Proof state:
case h.e_8.h.e_π.e_app
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ (fun b => f ≫ t.π.app b) = fun b => f' ≫ t.π.app b

Tactic:
exact funext w

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem one_lt_gold : 1 < φ

Proof state:
⊢ 1 < φ

Tactic:
refine lt_of_mul_lt_mul_left ?_ (le_of_lt gold_pos)

Result:
⊢ φ * 1 < φ * φ

Proof state:
⊢ φ * 1 < φ * φ

Tactic:
simp [← sq, gold_pos, zero_lt_one]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Lean/Except.lean
theorem map_pmap (g : β → γ) (x : Except ε α) (f : (a : α) → x = .ok a → β) :
    g <$> x.pmap f = x.pmap fun a h => g (f a h)

Proof state:
β γ : Type u_1
ε : Type u_2
α : Type u_1
g : β → γ
x : Except ε α
f : (a : α) → x = ok a → β
⊢ g <$> x.pmap f = x.pmap fun a h => g (f a h)

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem lintegral_coeFn (f : α →ₘ[μ] ℝ≥0∞) : ∫⁻ a, f a ∂μ = f.lintegral

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α →ₘ[μ] ℝ≥0∞
⊢ ∫⁻ (a : α), ↑f a ∂μ = f.lintegral

Tactic:
rw [← lintegral_mk, mk_coeFn]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_eq_const {f : α → ℝ≥0∞} (hf : Measurable f) (r : ℝ≥0∞) :
    ∫⁻ x in { x | f x = r }, f x ∂μ = r * μ { x | f x = r }

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ ∫⁻ (x : α) in {x | f x = r}, f x ∂μ = r * μ {x | f x = r}

Tactic:
rw [setLIntegral_congr_fun _ this]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ ∫⁻ (x : α) in {x | f x = r}, r ∂μ = r * μ {x | f x = r}

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ MeasurableSet {x | f x = r}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ MeasurableSet {x | f x = r}

Tactic:
exact hf (measurableSet_singleton r)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ ∫⁻ (x : α) in {x | f x = r}, r ∂μ = r * μ {x | f x = r}

Tactic:
rw [lintegral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
⊢ ∫⁻ (x : α) in {x | f x = r}, f x ∂μ = r * μ {x | f x = r}

Tactic:
have : ∀ᵐ x ∂μ, x ∈ { x | f x = r } → f x = r := ae_of_all μ fun _ hx => hx

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r
⊢ ∫⁻ (x : α) in {x | f x = r}, f x ∂μ = r * μ {x | f x = r}
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
@[simp] lemma log_one : log (1 : A) = 0

Proof state:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
⊢ log 1 = 0

Tactic:
simp [log]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma levyProkhorovDist_comm (μ ν : Measure Ω) :
    levyProkhorovDist μ ν = levyProkhorovDist ν μ

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
⊢ levyProkhorovDist μ ν = levyProkhorovDist ν μ

Tactic:
simp only [levyProkhorovDist, levyProkhorovEDist_comm]

Result:
no goals
-- Mathlib/Control/Fold.lean
theorem foldl_map (g : β → γ) (f : α → γ → α) (a : α) (l : t β) :
    foldl f a (g <$> l) = foldl (fun x y => f x (g y)) a l

Proof state:
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
g : β → γ
f : α → γ → α
a : α
l : t β
⊢ foldl f a (g <$> l) = foldl (fun x y => f x (g y)) a l

Tactic:
simp only [foldl, foldMap_map, Function.comp_def, Function.flip_def]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma tensor_id (X₁ X₂ : LocalizedMonoidal L W ε) : 𝟙 X₁ ⊗ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ : LocalizedMonoidal L W ε
⊢ 𝟙 X₁ ⊗ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)

Tactic:
simp [monoidalCategoryStruct]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_add_of_sub_right_le {a b c : Int} (h : a - c ≤ b) : a ≤ b + c

Proof state:
a b c : Int
h : a - c ≤ b
⊢ a ≤ b + c

Tactic:
have h := Int.add_le_add_right h c

Result:
a b c : Int
h✝ : a - c ≤ b
h : a - c + c ≤ b + c
⊢ a ≤ b + c

Proof state:
a b c : Int
h✝ : a - c ≤ b
h : a - c + c ≤ b + c
⊢ a ≤ b + c

Tactic:
rwa [Int.sub_add_cancel] at h

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem mem_sSup_of_directedOn {S : Set (Subring R)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S)
    {x : R} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Proof state:
R : Type u
inst✝ : Ring R
S : Set (Subring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
haveI : Nonempty S := Sne.to_subtype

Result:
R : Type u
inst✝ : Ring R
S : Set (Subring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Proof state:
R : Type u
inst✝ : Ring R
S : Set (Subring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk,
  exists_prop]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem re_eq_add_conj (z : K) : ↑(re z) = (z + conj z) / 2

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) = (z + (starRingEnd K) z) / 2

Tactic:
rw [add_conj, mul_div_cancel_left₀ (re z : K) two_ne_zero]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
lemma Iic_sup_erase (ha : a ∈ s) (has : ∀ b ∈ s, a ≤ b → b = a) : Iic a ⊔ s.erase a = s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, a ≤ b → b = a
⊢ Iic a ⊔ s.erase a = s

Tactic:
rw [sup_comm, erase_sup_Iic ha has]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean
theorem equalizer_ext (t : PullbackCone f g) {W : C} {k l : W ⟶ t.pt} (h₀ : k ≫ fst t = l ≫ fst t)
    (h₁ : k ≫ snd t = l ≫ snd t) : ∀ j : WalkingCospan, k ≫ t.π.app j = l ≫ t.π.app j
  | some WalkingPair.left => h₀
  | some WalkingPair.right => h₁
  | none => by rw [← t.w inl, reassoc_of% h₀]

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
W : C
k l : W ⟶ t.pt
h₀ : k ≫ t.fst = l ≫ t.fst
h₁ : k ≫ t.snd = l ≫ t.snd
⊢ k ≫ t.π.app none = l ≫ t.π.app none

Tactic:
rw [← t.w inl, reassoc_of% h₀]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem one_add (n : PosNum) : 1 + n = succ n

Proof state:
n : PosNum
⊢ 1 + n = n.succ

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_unit_singleton {v : E} (hv : ‖v‖ = 1) (w : E) :
    (orthogonalProjection (𝕜 ∙ v) w : E) = ⟪v, w⟫ • v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : E
hv : ‖v‖ = 1
w : E
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ↑(‖v‖ ^ 2) • ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w)

Tactic:
simp [hv]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : E
hv : ‖v‖ = 1
w : E
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ⟪v, w⟫_𝕜 • v

Tactic:
rw [← smul_orthogonalProjection_singleton 𝕜 w]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : E
hv : ‖v‖ = 1
w : E
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ↑(‖v‖ ^ 2) • ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w)
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_zero (f : R[X]) : expand R 0 f = C (eval 1 f)

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R[X]
⊢ (expand R 0) f = C (eval 1 f)

Tactic:
simp [expand]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem cancel_right {g₁ g₂ : α ≃*o β} {f : β ≃*o γ} (hf : Function.Injective f) :
    g₁.trans f = g₂.trans f ↔ g₁ = g₂ :=
  ⟨fun h => ext fun a => hf <| by rw [← trans_apply, h, trans_apply], by rintro rfl; rfl⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ g₂ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
⊢ g₁ = g₂ → g₁.trans f = g₂.trans f

Tactic:
rintro rfl

Result:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
⊢ g₁.trans f = g₁.trans f

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ g₂ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
h : g₁.trans f = g₂.trans f
a : α
⊢ f (g₁ a) = f (g₂ a)

Tactic:
rw [← trans_apply, h, trans_apply]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
⊢ g₁.trans f = g₁.trans f

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/CommRing.lean
theorem degreeOf_sub_le (i : σ) (p q : MvPolynomial σ R) :
    degreeOf i (p - q) ≤ max (degreeOf i p) (degreeOf i q)

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
i : σ
p q : MvPolynomial σ R
⊢ degreeOf i (p - q) ≤ degreeOf i p ⊔ degreeOf i q

Tactic:
simpa only [sub_eq_add_neg, degreeOf_neg] using degreeOf_add_le i p (-q)

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProd_of_not_isSFiniteKernel_right (κ : Kernel α β) (η : Kernel (α × β) γ)
    (h : ¬ IsSFiniteKernel η) :
    κ ⊗ₖ η = 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel η
⊢ κ ⊗ₖ η = 0

Tactic:
rw [compProd, dif_neg]

Result:
case hnc
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel η
⊢ ¬(IsSFiniteKernel κ ∧ IsSFiniteKernel η)

Proof state:
case hnc
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel η
⊢ ¬(IsSFiniteKernel κ ∧ IsSFiniteKernel η)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem tendsto_exp_nhds_zero_nhds_one : Tendsto exp (𝓝 0) (𝓝 1)

Proof state:
⊢ Tendsto rexp (𝓝 0) (𝓝 1)

Tactic:
convert continuous_exp.tendsto 0

Result:
case h.e'_5.h.e'_3

⊢ 1 = rexp 0

Proof state:
case h.e'_5.h.e'_3

⊢ 1 = rexp 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem coprod_inl_inr : coprod (inl R M M₂) (inr R M M₂) = LinearMap.id

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ (inl R M M₂).coprod (inr R M M₂) = id

Tactic:
ext <;>
  simp only [Prod.mk_add_mk, add_zero, id_apply, coprod_apply, inl_apply, inr_apply, zero_add]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem disjoint_map {m : α → β} (hm : Injective m) {f₁ f₂ : Filter α} :
    Disjoint (map m f₁) (map m f₂) ↔ Disjoint f₁ f₂

Proof state:
α : Type u_1
β : Type u_2
m : α → β
hm : Injective m
f₁ f₂ : Filter α
⊢ Disjoint (map m f₁) (map m f₂) ↔ Disjoint f₁ f₂

Tactic:
simp only [disjoint_iff, ← map_inf hm, map_eq_bot_iff]

Result:
no goals