harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/Submodule/Equiv.lean
theorem ofEq_rfl : ofEq p p rfl = LinearEquiv.refl R p

Proof state:
case h.a
R : Type u_1
M : Type u_5
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x✝ : ↥p
⊢ ↑((ofEq p p ⋯) x✝) = ↑((refl R ↥p) x✝)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
⊢ ofEq p p ⋯ = refl R ↥p

Tactic:
ext

Result:
case h.a
R : Type u_1
M : Type u_5
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x✝ : ↥p
⊢ ↑((ofEq p p ⋯) x✝) = ↑((refl R ↥p) x✝)
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.multiplicity_le_multiplicity_iff {c d : β} (hab : FiniteMultiplicity a b)
    (hcd : FiniteMultiplicity c d) :
    multiplicity a b ≤ multiplicity c d ↔ ∀ n : ℕ, a ^ n ∣ b → c ^ n ∣ d

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
hab : FiniteMultiplicity a b
hcd : FiniteMultiplicity c d
⊢ emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
apply emultiplicity_le_emultiplicity_iff

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
hab : FiniteMultiplicity a b
hcd : FiniteMultiplicity c d
⊢ multiplicity a b ≤ multiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
rw [← WithTop.coe_le_coe, ENat.some_eq_coe, ← hab.emultiplicity_eq_multiplicity,
  ← hcd.emultiplicity_eq_multiplicity]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
hab : FiniteMultiplicity a b
hcd : FiniteMultiplicity c d
⊢ emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
-- Mathlib/GroupTheory/Perm/Support.lean
theorem Disjoint.mono {x y : Perm α} (h : Disjoint f g) (hf : x.support ≤ f.support)
    (hg : y.support ≤ g.support) : Disjoint x y

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h : f.Disjoint g
hf : x.support ≤ f.support
hg : y.support ≤ g.support
⊢ x.Disjoint y

Tactic:
rw [disjoint_iff_disjoint_support] at h ⊢

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h : _root_.Disjoint f.support g.support
hf : x.support ≤ f.support
hg : y.support ≤ g.support
⊢ _root_.Disjoint x.support y.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h : _root_.Disjoint f.support g.support
hf : x.support ≤ f.support
hg : y.support ≤ g.support
⊢ _root_.Disjoint x.support y.support

Tactic:
exact h.mono hf hg

Result:
no goals
-- Mathlib/Topology/Sober.lean
theorem isGenericPoint_iff_forall_closed (hS : IsClosed S) (hxS : x ∈ S) :
    IsGenericPoint x S ↔ ∀ Z : Set α, IsClosed Z → x ∈ Z → S ⊆ Z

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z

Tactic:
have : closure {x} ⊆ S := closure_minimal (singleton_subset_iff.2 hxS) hS

Result:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z

Tactic:
simp_rw [IsGenericPoint, subset_antisymm_iff, this, true_and, closure, subset_sInter_iff,
  mem_setOf_eq, and_imp, singleton_subset_iff]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem mk_eq_add_mul_I (a b : ℝ) : Complex.mk a b = a + b * I :=
  Complex.ext_iff.2 <| by simp [ofReal]

Proof state:
a b : ℝ
⊢ { re := a, im := b }.re = (↑a + ↑b * I).re ∧ { re := a, im := b }.im = (↑a + ↑b * I).im

Tactic:
simp [ofReal]

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
theorem empty_mem_ssubsets {s : Finset α} (h : s.Nonempty) : ∅ ∈ s.ssubsets

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ⊆ s ∧ ∅ ≠ s

Tactic:
exact ⟨empty_subset s, h.ne_empty.symm⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ∈ s.ssubsets

Tactic:
rw [mem_ssubsets, ssubset_iff_subset_ne]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ⊆ s ∧ ∅ ≠ s
-- Mathlib/Algebra/Lie/TraceForm.lean
lemma traceForm_lieInvariant : (traceForm R L M).lieInvariant L

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y z : L
⊢ ((traceForm R L M) ⁅x, y⁆) z = -((traceForm R L M) y) ⁅x, z⁆

Tactic:
rw [← lie_skew, map_neg, LinearMap.neg_apply, LieModule.traceForm_apply_lie_apply R L M]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ LinearMap.BilinForm.lieInvariant L (traceForm R L M)

Tactic:
intro x y z

Result:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y z : L
⊢ ((traceForm R L M) ⁅x, y⁆) z = -((traceForm R L M) y) ⁅x, z⁆
-- Mathlib/GroupTheory/Complement.lean
@[to_additive (attr := simp)]
lemma not_isComplement_empty_left : ¬ IsComplement ∅ T :=
  fun h ↦ by simpa [eq_comm (a := ∅)] using h.mul_eq

Proof state:
G : Type u_1
inst✝ : Group G
T : Set G
h : IsComplement ∅ T
⊢ False

Tactic:
simpa [eq_comm (a := ∅)] using h.mul_eq

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem BalancedSz.symm {l r : ℕ} : BalancedSz l r → BalancedSz r l :=
  Or.imp (by rw [add_comm]; exact id) And.symm

Proof state:
l r : ℕ
⊢ r + l ≤ 1 → r + l ≤ 1

Tactic:
exact id

Result:
no goals

Proof state:
l r : ℕ
⊢ l + r ≤ 1 → r + l ≤ 1

Tactic:
rw [add_comm]

Result:
l r : ℕ
⊢ r + l ≤ 1 → r + l ≤ 1
-- Mathlib/LinearAlgebra/Prod.lean
theorem disjoint_inl_inr : Disjoint (range <| inl R M M₂) (range <| inr R M M₂)

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₂
⊢ Disjoint (range (inl R M M₂)) (range (inr R M M₂))

Tactic:
simp +contextual [disjoint_def, @eq_comm M 0, @eq_comm M₂ 0]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem UniformSpace.mem_closure_iff_symm_ball {s : Set α} {x} :
    x ∈ closure s ↔ ∀ {V}, V ∈ 𝓤 α → SymmetricRel V → (s ∩ ball x V).Nonempty

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set α
x : α
⊢ x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SymmetricRel V → (s ∩ ball x V).Nonempty

Tactic:
simp [mem_closure_iff_nhds_basis (hasBasis_nhds x), Set.Nonempty]

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
lemma none_mem_insertNone {s : Finset α} : none ∈ insertNone s

Proof state:
α : Type u_1
s : Finset α
⊢ none ∈ insertNone s

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem prim_iff₂ {f : ℕ → ℕ → ℕ} : (@Primrec' 2 fun v => f v.head v.tail.head) ↔ Primrec₂ f :=
  prim_iff.trans
    ⟨fun h => (h.comp <| Primrec.vector_cons.comp .fst <|
      Primrec.vector_cons.comp .snd (.const nil)).of_eq fun v => by simp,
    fun h => h.comp .vector_head (Primrec.vector_head.comp .vector_tail)⟩

Proof state:
f : ℕ → ℕ → ℕ
h : Primrec fun v => f v.head v.tail.head
v : ℕ × ℕ
⊢ f (v.1 ::ᵥ v.2 ::ᵥ nil).head (v.1 ::ᵥ v.2 ::ᵥ nil).tail.head = f v.1 v.2

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
theorem card_ConnectedComponent_eq_rank_ker_lapMatrix : Fintype.card G.ConnectedComponent =
    Module.finrank ℝ (LinearMap.ker (Matrix.toLin' (G.lapMatrix ℝ)))

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
⊢ Fintype.card G.ConnectedComponent = Module.finrank ℝ ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))

Tactic:
classical
rw [Module.finrank_eq_card_basis (lapMatrix_ker_basis G)]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
⊢ Fintype.card G.ConnectedComponent = Module.finrank ℝ ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))

Tactic:
rw [Module.finrank_eq_card_basis (lapMatrix_ker_basis G)]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
@[simp] lemma shatters_empty : 𝒜.Shatters ∅ ↔ 𝒜.Nonempty :=
  ⟨Shatters.nonempty, fun ⟨s, hs⟩ t ht ↦ ⟨s, hs, by rwa [empty_inter, eq_comm, ← subset_empty]⟩⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
x✝ : 𝒜.Nonempty
t : Finset α
ht : t ⊆ ∅
s : Finset α
hs : s ∈ 𝒜
⊢ ∅ ∩ s = t

Tactic:
rwa [empty_inter, eq_comm, ← subset_empty]

Result:
no goals
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem tsupport_subset_chartAt_source : tsupport f ⊆ (chartAt H c).source

Proof state:
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ tsupport ↑f ⊆ (chartAt H c).source

Tactic:
simpa only [extChartAt_source] using f.tsupport_subset_extChartAt_source

Result:
no goals
-- Mathlib/Data/List/Enum.lean
theorem forall_mem_zipIdx' {l : List α} {p : α × ℕ → Prop} :
    (∀ x ∈ l.zipIdx, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (l[i], i) :=
  forall_mem_zipIdx.trans <| by simp

Proof state:
α : Type u_1
l : List α
p : α × ℕ → Prop
⊢ (∀ (i : ℕ) (x : i < l.length), p (l[i], 0 + i)) ↔ ∀ (i : ℕ) (x : i < l.length), p (l[i], i)

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Nimber/Field.lean
theorem invAux_mem_invSet_of_lt (ha : a ≠ 0) (hb : a < b) : invAux a ∈ invSet b

Proof state:
a b : Nimber
ha : a ≠ 0
hb : a < b
H : a.invAux * (1 + (b + a) * 0) ∈ b.invSet
⊢ a.invAux ∈ b.invSet

Tactic:
rwa [mul_zero, add_zero, mul_one] at H

Result:
no goals

Proof state:
a b : Nimber
ha : a ≠ 0
hb : a < b
⊢ a.invAux ∈ b.invSet

Tactic:
have H := cons_mem_invSet ha hb (zero_mem_invSet b)

Result:
a b : Nimber
ha : a ≠ 0
hb : a < b
H : a.invAux * (1 + (b + a) * 0) ∈ b.invSet
⊢ a.invAux ∈ b.invSet
-- Mathlib/Algebra/Algebra/Tower.lean
theorem smul_mem_span_smul {s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S} {x : A}
    (hx : x ∈ span R t) : k • x ∈ span R (s • t)

Proof state:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ span R t
⊢ k • x ∈ span R (s • t)

Tactic:
rw [span_smul_of_span_eq_top hs]

Result:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ span R t
⊢ k • x ∈ restrictScalars R (span S t)

Proof state:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ span R t
⊢ k • x ∈ restrictScalars R (span S t)

Tactic:
exact (span S t).smul_mem k (span_le_restrictScalars R S t hx)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem mem_prehaar_empty {K₀ : Set G} {f : Compacts G → ℝ} :
    f ∈ haarProduct K₀ ↔ ∀ K : Compacts G, f K ∈ Icc (0 : ℝ) (index (K : Set G) K₀)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
K₀ : Set G
f : Compacts G → ℝ
⊢ f ∈ haarProduct K₀ ↔ ∀ (K : Compacts G), f K ∈ Icc 0 ↑(index (↑K) K₀)

Tactic:
simp only [haarProduct, Set.pi, forall_prop_of_true, mem_univ, mem_setOf_eq]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@[to_additive]
lemma prod_eq_one_iff_of_le_one (hf : f ≤ 1) : ∏ i, f i = 1 ↔ f = 1 :=
  (Finset.prod_eq_one_iff_of_le_one' fun i _ ↦ hf i).trans <| by simp [funext_iff]

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : Fintype ι
inst✝ : OrderedCommMonoid M
f : ι → M
hf : f ≤ 1
⊢ (∀ i ∈ Finset.univ, f i = 1) ↔ f = 1

Tactic:
simp [funext_iff]

Result:
no goals
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_add_compl_eq (u t : Set Ω) (hs : s.Finite) :
    uniformOn (s ∩ u) t * uniformOn s u + uniformOn (s ∩ uᶜ) t * uniformOn s uᶜ =
      uniformOn s t

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
⊢ (uniformOn (s ∩ u)) t * (uniformOn s) u + (uniformOn (s ∩ uᶜ)) t * (uniformOn s) uᶜ = (uniformOn s) t

Tactic:
have : uniformOn s t = (uniformOn (s ∩ u) t * uniformOn (s ∩ u ∪ s ∩ uᶜ) (s ∩ u) +
    uniformOn (s ∩ uᶜ) t * uniformOn (s ∩ u ∪ s ∩ uᶜ) (s ∩ uᶜ)) := by
  rw [uniformOn_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
    (disjoint_compl_right.mono inf_le_right inf_le_right), Set.inter_union_compl]

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
this :
  (uniformOn s) t =
    (uniformOn (s ∩ u)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      (uniformOn (s ∩ uᶜ)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
⊢ (uniformOn (s ∩ u)) t * (uniformOn s) u + (uniformOn (s ∩ uᶜ)) t * (uniformOn s) uᶜ = (uniformOn s) t

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
this :
  (uniformOn s) t =
    (uniformOn (s ∩ u)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      (uniformOn (s ∩ uᶜ)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
⊢ (uniformOn (s ∩ u)) t * (uniformOn s) u + (uniformOn (s ∩ uᶜ)) t * (uniformOn s) uᶜ =
    (uniformOn (s ∩ u)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      (uniformOn (s ∩ uᶜ)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)

Tactic:
simp [uniformOn_inter_self hs]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
⊢ (uniformOn s) t =
    (uniformOn (s ∩ u)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      (uniformOn (s ∩ uᶜ)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)

Tactic:
rw [uniformOn_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
  (disjoint_compl_right.mono inf_le_right inf_le_right), Set.inter_union_compl]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
this :
  (uniformOn s) t =
    (uniformOn (s ∩ u)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      (uniformOn (s ∩ uᶜ)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
⊢ (uniformOn (s ∩ u)) t * (uniformOn s) u + (uniformOn (s ∩ uᶜ)) t * (uniformOn s) uᶜ = (uniformOn s) t

Tactic:
rw [this]

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
this :
  (uniformOn s) t =
    (uniformOn (s ∩ u)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      (uniformOn (s ∩ uᶜ)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
⊢ (uniformOn (s ∩ u)) t * (uniformOn s) u + (uniformOn (s ∩ uᶜ)) t * (uniformOn s) uᶜ =
    (uniformOn (s ∩ u)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      (uniformOn (s ∩ uᶜ)) t * (uniformOn (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_nadd_lt {a' b' : Ordinal} (ha : a' < a) (hb : b' < b) :
    a' ⨳ b ♯ a ⨳ b' < a ⨳ b ♯ a' ⨳ b'

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

Tactic:
conv_rhs => rw [nmul]

Result:
a b a' b' : Ordinal.{u}
ha : a' < a
hb : b' < b
⊢ a' ⨳ b ♯ a ⨳ b' < sInf {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} ♯ a' ⨳ b'

Proof state:
a b a' b' : Ordinal.{u}
ha : a' < a
hb : b' < b
⊢ a' ⨳ b ♯ a ⨳ b' < sInf {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} ♯ a' ⨳ b'

Tactic:
exact csInf_mem (nmul_nonempty a b) a' ha b' hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_eq_cons_iff' {f : α → β} {l : List α} :
    map f l = b :: l₂ ↔ l.head?.map f = some b ∧ l.tail?.map (map f) = some l₂

Proof state:
α : Type u_1
β : Type u_2
b : β
l₂ : List β
f : α → β
l : List α
⊢ map f l = b :: l₂ ↔ Option.map f l.head? = some b ∧ Option.map (map f) l.tail? = some l₂

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformContinuous₂.tendstoUniformly [UniformSpace α] [UniformSpace γ] {f : α → β → γ}
    (h : UniformContinuous₂ f) {x : α} : TendstoUniformly f (f x) (𝓝 x) :=
  UniformContinuousOn.tendstoUniformly univ_mem <| by rwa [univ_prod_univ, uniformContinuousOn_univ]

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
f : α → β → γ
h : UniformContinuous₂ f
x : α
⊢ UniformContinuousOn (↿f) (univ ×ˢ univ)

Tactic:
rwa [univ_prod_univ, uniformContinuousOn_univ]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
/-- A closed ball in a product space is a product of closed balls. See also `closedBall_pi'`
for a version assuming `Nonempty β` instead of `0 ≤ r`. -/
lemma closedBall_pi (x : ∀ b, π b) {r : ℝ} (hr : 0 ≤ r) :
    closedBall x r = Set.pi univ fun b => closedBall (x b) r

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Set.univ.pi fun b => closedBall (x b) r

Tactic:
ext p

Result:
case h
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
hr : 0 ≤ r
p : (b : β) → π b
⊢ p ∈ closedBall x r ↔ p ∈ Set.univ.pi fun b => closedBall (x b) r

Proof state:
case h
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
x : (b : β) → π b
r : ℝ
hr : 0 ≤ r
p : (b : β) → π b
⊢ p ∈ closedBall x r ↔ p ∈ Set.univ.pi fun b => closedBall (x b) r

Tactic:
simp [dist_pi_le_iff hr]

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem nhds_eq' (l : Filter α) : 𝓝 l = l.lift' fun s => { l' | s ∈ l' }

Proof state:
α : Type u_2
l : Filter α
⊢ 𝓝 l = l.lift' fun s => {l' | s ∈ l'}

Tactic:
simpa only [Function.comp_def, Iic_principal] using nhds_eq l

Result:
no goals
-- Mathlib/Algebra/Order/Group/MinMax.lean
theorem abs_min_sub_min_le_max (a b c d : α) : |min a b - min c d| ≤ max |a - c| |b - d|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ |a - c| ⊔ |b - d|

Tactic:
simpa only [max_neg_neg, neg_sub_neg, abs_sub_comm] using
  abs_max_sub_max_le_max (-a) (-b) (-c) (-d)

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem ennrealToMeasure_toENNRealVectorMeasure (μ : Measure α) :
    ennrealToMeasure (toENNRealVectorMeasure μ) = μ := Measure.ext fun s hs => by
  rw [ennrealToMeasure_apply hs, toENNRealVectorMeasure_apply_measurable hs]

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ μ.toENNRealVectorMeasure.ennrealToMeasure s = μ s

Tactic:
rw [ennrealToMeasure_apply hs, toENNRealVectorMeasure_apply_measurable hs]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ico_add_one_left_eq_Ioo (a b : α) : Ico (a + 1) b = Ioo a b

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
⊢ Ico (a + 1) b = Ioo a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_left_eq_Ioo a b

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma div_two_mul_two_add_one_of_odd (h : Odd n) : n / 2 * 2 + 1 = n

Proof state:
n : ℕ
h : Odd n
⊢ n / 2 * 2 + 1 = n

Tactic:
rw [← odd_iff.mp h, div_add_mod']

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem think_equiv (s : WSeq α) : think s ~ʷ s

Proof state:
α : Type u
s : WSeq α
⊢ LiftRel (fun x1 x2 => x1 = x2) s.think s

Tactic:
simpa using Equiv.refl _

Result:
no goals

Proof state:
α : Type u
s : WSeq α
⊢ s.think ~ʷ s

Tactic:
unfold Equiv

Result:
α : Type u
s : WSeq α
⊢ LiftRel (fun x1 x2 => x1 = x2) s.think s
-- Mathlib/Data/ZMod/Basic.lean
theorem natCast_zmod_eq_zero_iff_dvd (a b : ℕ) : (a : ZMod b) = 0 ↔ b ∣ a

Proof state:
a b : ℕ
⊢ ↑a = 0 ↔ b ∣ a

Tactic:
rw [← Nat.cast_zero, ZMod.natCast_eq_natCast_iff, Nat.modEq_zero_iff_dvd]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma swapRight_eq (κ : Kernel α (β × γ)) : swapRight κ = map κ Prod.swap

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
⊢ κ.swapRight = κ.map Prod.swap

Tactic:
simp [swapRight]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_indicatorConstLp [CompleteSpace E]
    {p : ℝ≥0∞} (ht : MeasurableSet t) (hμt : μ t ≠ ∞) (e : E) :
    ∫ x, indicatorConstLp p ht hμt e x ∂μ = (μ t).toReal • e :=
  calc
    ∫ x, indicatorConstLp p ht hμt e x ∂μ = ∫ x in univ, indicatorConstLp p ht hμt e x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
t : Set X
μ : Measure X
inst✝ : CompleteSpace E
p : ℝ≥0∞
ht : MeasurableSet t
hμt : μ t ≠ ⊤
e : E
⊢ (μ (t ∩ univ)).toReal • e = (μ t).toReal • e

Tactic:
rw [inter_univ]

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
t : Set X
μ : Measure X
inst✝ : CompleteSpace E
p : ℝ≥0∞
ht : MeasurableSet t
hμt : μ t ≠ ⊤
e : E
⊢ ∫ (x : X), ↑↑(indicatorConstLp p ht hμt e) x ∂μ = ∫ (x : X) in univ, ↑↑(indicatorConstLp p ht hμt e) x ∂μ

Tactic:
rw [setIntegral_univ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_neg [CommRing S] [IsDomain S] [Algebra T S] (p : T[X]) :
    (-p).aroots S = p.aroots S

Proof state:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
⊢ (-p).aroots S = p.aroots S

Tactic:
rw [aroots, Polynomial.map_neg, roots_neg]

Result:
no goals