harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem ae_eq_empty : s =ᵐ[μ] (∅ : Set α) ↔ μ s = 0 :=
  eventuallyEq_empty.trans <| by simp only [ae_iff, Classical.not_not, setOf_mem_eq]

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : Set α
⊢ (∀ᵐ (x : α) ∂μ, x ∉ s) ↔ μ s = 0

Tactic:
simp only [ae_iff, Classical.not_not, setOf_mem_eq]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma Nonempty.pow (hs : s.Nonempty) : ∀ {n}, (s ^ n).Nonempty
  | 0 => by simp
  | n + 1 => by rw [pow_succ]; exact hs.pow.mul hs

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
hs : s.Nonempty
⊢ (s ^ 0).Nonempty

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ (s ^ n * s).Nonempty

Tactic:
exact hs.pow.mul hs

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ (s ^ (n + 1)).Nonempty

Tactic:
rw [pow_succ]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ (s ^ n * s).Nonempty
-- Mathlib/Topology/Instances/Matrix.lean
theorem Continuous.matrix_det [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R]
    {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun x => (A x).det

Proof state:
X : Type u_1
n : Type u_5
R : Type u_8
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
l : Equiv.Perm n
x✝ : l ∈ Finset.univ
⊢ Continuous fun x => ∏ i : n, A x (l i) i

Tactic:
exact continuous_finset_prod _ fun l _ => hA.matrix_elem _ _

Result:
no goals

Proof state:
X : Type u_1
n : Type u_5
R : Type u_8
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous fun x => (A x).det

Tactic:
simp_rw [Matrix.det_apply]

Result:
X : Type u_1
n : Type u_5
R : Type u_8
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous fun x => ∑ σ : Equiv.Perm n, Equiv.Perm.sign σ • ∏ i : n, A x (σ i) i

Proof state:
X : Type u_1
n : Type u_5
R : Type u_8
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous fun x => ∑ σ : Equiv.Perm n, Equiv.Perm.sign σ • ∏ i : n, A x (σ i) i

Tactic:
refine continuous_finset_sum _ fun l _ => Continuous.const_smul ?_ _

Result:
X : Type u_1
n : Type u_5
R : Type u_8
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
l : Equiv.Perm n
x✝ : l ∈ Finset.univ
⊢ Continuous fun x => ∏ i : n, A x (l i) i
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma ofNat_lt_cast : ofNat(n) < (p : K) ↔ OfNat.ofNat n < p

Proof state:
K : Type u_5
inst✝¹ : LinearOrderedSemifield K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ OfNat.ofNat n < ↑p ↔ OfNat.ofNat n < p

Tactic:
simp [← cast_lt (K := K)]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_nadd_le₃' {a' b' c' : Ordinal} (ha : a' ≤ a) (hb : b' ≤ b) (hc : c' ≤ c) :
    a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') ≤
      a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')

Proof state:
a b c a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' ≤ b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a

Tactic:
convert nmul_nadd_le₃ hb hc ha using 1 <;>
  (simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]; abel_nf)

Result:
no goals

Proof state:
case h.e'_4
a b c a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a = b ⨳ c ⨳ a ♯ b' ⨳ c' ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a'

Tactic:
simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]

Result:
case h.e'_4
a b c a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ toOrdinal
      (toNatOrdinal (b ⨳ c ⨳ a) + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a') +
        toNatOrdinal (b' ⨳ c' ⨳ a)) =
    toOrdinal
      (toNatOrdinal (b ⨳ c ⨳ a) + toNatOrdinal (b' ⨳ c' ⨳ a) + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a'))

Proof state:
a b c a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') ≤
    a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')

Tactic:
simp only [nmul_comm _ (_ ⨳ _)]

Result:
a b c a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' ≤ b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a

Proof state:
case h.e'_4
a b c a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ toOrdinal
      (toNatOrdinal (b ⨳ c ⨳ a) + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a') +
        toNatOrdinal (b' ⨳ c' ⨳ a)) =
    toOrdinal
      (toNatOrdinal (b ⨳ c ⨳ a) + toNatOrdinal (b' ⨳ c' ⨳ a) + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a'))

Tactic:
abel_nf

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem lift_injective [CharZero R] {d : ℤ} (r : { r : R // r * r = ↑d })
    (hd : ∀ n : ℤ, d ≠ n * n) : Function.Injective (lift r) :=
  (injective_iff_map_eq_zero (lift r)).mpr fun a ha => by
    have h_inj : Function.Injective ((↑) : ℤ → R) := Int.cast_injective
    suffices lift r a.norm = 0 by
      simp only [intCast_re, add_zero, lift_apply_apply, intCast_im, Int.cast_zero,
        zero_mul] at this
      rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this
    rw [norm_eq_mul_conj, RingHom.map_mul, ha, zero_mul]

Proof state:
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
this : ↑a.norm = 0
⊢ a = 0

Tactic:
rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this

Result:
no goals

Proof state:
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
⊢ a = 0

Tactic:
have h_inj : Function.Injective ((↑) : ℤ → R) := Int.cast_injective

Result:
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ a = 0

Proof state:
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
this : (lift r) ↑a.norm = 0
⊢ a = 0

Tactic:
simp only [intCast_re, add_zero, lift_apply_apply, intCast_im, Int.cast_zero,
  zero_mul] at this

Result:
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
this : ↑a.norm = 0
⊢ a = 0

Proof state:
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ (lift r) ↑a.norm = 0

Tactic:
rw [norm_eq_mul_conj, RingHom.map_mul, ha, zero_mul]

Result:
no goals

Proof state:
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ a = 0

Tactic:
suffices lift r a.norm = 0 by
  simp only [intCast_re, add_zero, lift_apply_apply, intCast_im, Int.cast_zero,
    zero_mul] at this
  rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this

Result:
R : Type
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ (lift r) ↑a.norm = 0
-- Mathlib/Data/Matroid/Constructions.lean
theorem freeOn_isBasis_iff : (freeOn E).IsBasis I X ↔ I = X ∧ X ⊆ E

Proof state:
case mpr
α : Type u_1
E I X : Set α
⊢ I = X ∧ X ⊆ E → (freeOn E).IsBasis I X

Tactic:
rintro ⟨rfl, hIE⟩

Result:
case mpr.intro
α : Type u_1
E I : Set α
hIE : I ⊆ E
⊢ (freeOn E).IsBasis I I

Proof state:
α : Type u_1
E I X : Set α
⊢ (freeOn E).IsBasis I X ↔ I = X ∧ X ⊆ E

Tactic:
use fun h ↦ ⟨(freeOn_indep h.subset_ground).eq_of_isBasis h ,h.subset_ground⟩

Result:
case mpr
α : Type u_1
E I X : Set α
⊢ I = X ∧ X ⊆ E → (freeOn E).IsBasis I X

Proof state:
case mpr.intro
α : Type u_1
E I : Set α
hIE : I ⊆ E
⊢ (freeOn E).IsBasis I I

Tactic:
exact (freeOn_indep hIE).isBasis_self

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsBasis.isBasis_restrict_of_subset (hI : M.IsBasis I X) (hXY : X ⊆ Y) :
    (M ↾ Y).IsBasis I X

Proof state:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
⊢ (M ↾ Y).IsBasis I X

Tactic:
rwa [← isBase_restrict_iff, M.restrict_restrict_eq hXY, isBase_restrict_iff]

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem Rel.add_right {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r b c) : Rel r (a + b) (a + c)

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (a + b) (a + c)

Tactic:
rw [add_comm a b, add_comm a c]

Result:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (b + a) (c + a)

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (b + a) (c + a)

Tactic:
exact Rel.add_left h

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem image_mk_openSegment_right (x : E) (y₁ y₂ : F) :
    (fun y => (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun x_1 => (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p => p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}

Tactic:
refine EqOn.image_eq fun a ha ↦ ?_

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
a : 𝕜 × 𝕜
ha : a ∈ {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
⊢ (x, a.1 • y₁ + a.2 • y₂) = a.1 • (x, y₁) + a.2 • (x, y₂)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun y => (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)

Tactic:
rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun x_1 => (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p => p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
a : 𝕜 × 𝕜
ha : a ∈ {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
⊢ (x, a.1 • y₁ + a.2 • y₂) = a.1 • (x, y₁) + a.2 • (x, y₂)

Tactic:
simp [Convex.combo_self ha.2.2]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem type_fin (n : ℕ) : typeLT (Fin n) = n

Proof state:
n : ℕ
⊢ (type fun x1 x2 => x1 < x2) = ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem div_neg_self {a : K} (h : a ≠ 0) : a / -a = -1

Proof state:
K : Type u_1
inst✝ : DivisionRing K
a : K
h : a ≠ 0
⊢ a / -a = -1

Tactic:
rw [div_neg_eq_neg_div, div_self h]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_le_coe_iff {k : ℕ} : s.encard ≤ k ↔ s.Finite ∧ ∃ (n₀ : ℕ), s.encard = n₀ ∧ n₀ ≤ k :=
  ⟨fun h ↦ ⟨finite_of_encard_le_coe h, by rwa [ENat.le_coe_iff] at h⟩,
    fun ⟨_,⟨n₀,hs, hle⟩⟩ ↦ by rwa [hs, Nat.cast_le]⟩

Proof state:
α : Type u_1
s : Set α
k : ℕ
x✝ : s.Finite ∧ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
left✝ : s.Finite
n₀ : ℕ
hs : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ s.encard ≤ ↑k

Tactic:
rwa [hs, Nat.cast_le]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k

Tactic:
rwa [ENat.le_coe_iff] at h

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem dTo_eq {i j : ι} (r : c.Rel i j) : C.dTo j = (C.xPrevIso r).hom ≫ C.d i j

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : c.Rel i j
⊢ C.dTo j = (C.xPrevIso r).hom ≫ C.d i j

Tactic:
obtain rfl := c.prev_eq' r

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
r : c.Rel (c.prev j) j
⊢ C.dTo j = (C.xPrevIso r).hom ≫ C.d (c.prev j) j

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
r : c.Rel (c.prev j) j
⊢ C.dTo j = (C.xPrevIso r).hom ≫ C.d (c.prev j) j

Tactic:
exact (Category.id_comp _).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem reverse_push (as : Array α) (a : α) : (as.push a).reverse = #[a] ++ as.reverse

Proof state:
α : Type u_1
as : Array α
a : α
⊢ (as.push a).reverse = #[a] ++ as.reverse

Tactic:
cases as

Result:
case mk
α : Type u_1
a : α
toList✝ : List α
⊢ ({ toList := toList✝ }.push a).reverse = #[a] ++ { toList := toList✝ }.reverse

Proof state:
case mk
α : Type u_1
a : α
toList✝ : List α
⊢ ({ toList := toList✝ }.push a).reverse = #[a] ++ { toList := toList✝ }.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem exists_mem_closure_infDist_eq_dist [ProperSpace α] (hne : s.Nonempty) (x : α) :
    ∃ y ∈ closure s, infDist x s = dist x y

Proof state:
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
hne : s.Nonempty
x : α
⊢ ∃ y ∈ closure s, infDist x s = dist x y

Tactic:
simpa only [infDist_closure] using isClosed_closure.exists_infDist_eq_dist hne.closure x

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/LinearMap.lean
lemma restrict_commute {f g : M →ₗ[R] M} (h : Commute f g) {p : Submodule R M}
    (hf : MapsTo f p p) (hg : MapsTo g p p) :
    Commute (f.restrict hf) (g.restrict hg)

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
⊢ f.restrict hf * g.restrict hg = g.restrict hg * f.restrict hf

Tactic:
conv_lhs => rw [mul_eq_comp, ← restrict_comp]; congr; rw [← mul_eq_comp, h.eq]

Result:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
⊢ (g * f).restrict ⋯ = g.restrict hg * f.restrict hf

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
⊢ (g * f).restrict ⋯ = g.restrict hg * f.restrict hf

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
⊢ Commute (f.restrict hf) (g.restrict hg)

Tactic:
change _ * _ = _ * _

Result:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
⊢ f.restrict hf * g.restrict hg = g.restrict hg * f.restrict hf
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem contains_mk [BEq α] {data : Array α} {size : data.size = n} {a : α} :
    (Vector.mk data size).contains a = data.contains a

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
data : Array α
size : data.size = n
a : α
⊢ { toArray := data, size_toArray := size }.contains a = data.contains a

Tactic:
simp [contains]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_reinsertAux [BEq α] [Hashable α] [PartialEquivBEq α]
    (data : {d : Array (AssocList α β) // 0 < d.size}) (a : α) (b : β a) :
    Perm (toListModel (reinsertAux hash data a b).1) (⟨a, b⟩ :: toListModel data.1)

Proof state:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
data : { d // 0 < d.size }
a : α
b : β a
l : List ((a : α) × β a)
h₁ : toListModel data.val ~ (bucket data.val ⋯ a).toList ++ l
h₂ :
  toListModel (updateBucket data.val ⋯ a fun l => AssocList.cons a b l) ~
    (AssocList.cons a b (bucket data.val ⋯ a)).toList ++ l
⊢ toListModel (updateBucket data.val ⋯ a fun l => AssocList.cons a b l) ~ ⟨a, b⟩ :: toListModel data.val

Tactic:
exact h₂.trans (Perm.cons _ (Perm.symm h₁))

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
data : { d // 0 < d.size }
a : α
b : β a
⊢ toListModel (reinsertAux hash data a b).val ~ ⟨a, b⟩ :: toListModel data.val

Tactic:
rw [reinsertAux_eq]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
data : { d // 0 < d.size }
a : α
b : β a
⊢ toListModel (updateBucket data.val ⋯ a fun l => AssocList.cons a b l) ~ ⟨a, b⟩ :: toListModel data.val

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
data : { d // 0 < d.size }
a : α
b : β a
⊢ toListModel (updateBucket data.val ⋯ a fun l => AssocList.cons a b l) ~ ⟨a, b⟩ :: toListModel data.val

Tactic:
obtain ⟨l, h₁, h₂, -⟩ := exists_bucket_of_update data.1 data.2 a (fun l => l.cons a b)

Result:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
data : { d // 0 < d.size }
a : α
b : β a
l : List ((a : α) × β a)
h₁ : toListModel data.val ~ (bucket data.val ⋯ a).toList ++ l
h₂ :
  toListModel (updateBucket data.val ⋯ a fun l => AssocList.cons a b l) ~
    (AssocList.cons a b (bucket data.val ⋯ a)).toList ++ l
⊢ toListModel (updateBucket data.val ⋯ a fun l => AssocList.cons a b l) ~ ⟨a, b⟩ :: toListModel data.val
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l₁.length = l₂.length :=
  match l₁, l₂ with
  | [], [] => rfl
  | [], _ :: _ => by simp [beq_nil_iff] at h
  | _ :: _, [] => by simp [nil_beq_iff] at h
  | a :: l₁, b :: l₂ => by
    simp at h
    simpa [Nat.add_one_inj] using length_eq_of_beq h.2

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
head✝ : α
tail✝ : List α
h : ([] == head✝ :: tail✝) = true
⊢ [].length = (head✝ :: tail✝).length

Tactic:
simp [beq_nil_iff] at h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝ == []) = true
⊢ (head✝ :: tail✝).length = [].length

Tactic:
simp [nil_beq_iff] at h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l₁✝ l₂✝ : List α
a : α
l₁ : List α
b : α
l₂ : List α
h : (a == b) = true ∧ (l₁ == l₂) = true
⊢ (a :: l₁).length = (b :: l₂).length

Tactic:
simpa [Nat.add_one_inj] using length_eq_of_beq h.2

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l₁✝ l₂✝ : List α
a : α
l₁ : List α
b : α
l₂ : List α
h : (a :: l₁ == b :: l₂) = true
⊢ (a :: l₁).length = (b :: l₂).length

Tactic:
simp at h

Result:
α : Type u_1
inst✝ : BEq α
l₁✝ l₂✝ : List α
a : α
l₁ : List α
b : α
l₂ : List α
h : (a == b) = true ∧ (l₁ == l₂) = true
⊢ (a :: l₁).length = (b :: l₂).length
-- Mathlib/Data/List/Map2.lean
theorem map₂Left_eq_map₂Left' : ∀ as bs, map₂Left f as bs = (map₂Left' f as bs).fst
  | [], _ => by simp
  | a :: as, [] => by simp
  | a :: as, b :: bs => by simp [map₂Left_eq_map₂Left']

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
⊢ map₂Left f (a :: as) [] = (map₂Left' f (a :: as) []).fst

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
x✝ : List β
⊢ map₂Left f [] x✝ = (map₂Left' f [] x✝).fst

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
b : β
bs : List β
⊢ map₂Left f (a :: as) (b :: bs) = (map₂Left' f (a :: as) (b :: bs)).fst

Tactic:
simp [map₂Left_eq_map₂Left']

Result:
no goals
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingDist_self (x : ∀ i, β i) : hammingDist x x = 0

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ hammingDist x x = 0

Tactic:
rw [hammingDist, card_eq_zero, filter_eq_empty_iff]

Result:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ ∀ ⦃x_1 : ι⦄, x_1 ∈ univ → ¬x x_1 ≠ x x_1

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ ∀ ⦃x_1 : ι⦄, x_1 ∈ univ → ¬x x_1 ≠ x x_1

Tactic:
exact fun _ _ H => H rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_nonneg_of_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) : 0 ≤ ∫ a, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
⊢ 0 ≤ ∫ (a : α), f a ∂μ

Tactic:
have A : CompleteSpace ℝ := by infer_instance

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
A : CompleteSpace ℝ
⊢ 0 ≤ ∫ (a : α), f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
A : CompleteSpace ℝ
⊢ 0 ≤ if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0

Tactic:
exact setToFun_nonneg (dominatedFinMeasAdditive_weightedSMul μ)
  (fun s _ _ => weightedSMul_nonneg s) hf

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
A : CompleteSpace ℝ
⊢ 0 ≤ ∫ (a : α), f a ∂μ

Tactic:
simp only [integral_def, A, L1.integral_def, dite_true]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
A : CompleteSpace ℝ
⊢ 0 ≤ if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
⊢ CompleteSpace ℝ

Tactic:
infer_instance

Result:
no goals