harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.insertList [BEq α] [PartialEquivBEq α] {l₁ l₂ : List ((a : α) × β a)}
    (h : DistinctKeys l₁) :
    DistinctKeys (insertList l₁ l₂)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih : ∀ {l₁ : List ((a : α) × β a)}, DistinctKeys l₁ → DistinctKeys (List.insertList l₁ t)
l₁ : List ((a : α) × β a)
h : DistinctKeys l₁
⊢ DistinctKeys
    (match ⟨k, v⟩ :: t with
    | [] => l₁
    | ⟨k, v⟩ :: toInsert => List.insertList (List.insertEntry k v l₁) toInsert)

Tactic:
exact ih h.insertEntry

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : ∀ {l₁ : List ((a : α) × β a)}, DistinctKeys l₁ → DistinctKeys (List.insertList l₁ tail✝)
l₁ : List ((a : α) × β a)
h : DistinctKeys l₁
⊢ DistinctKeys (List.insertList l₁ (⟨k✝, v✝⟩ :: tail✝))

Tactic:
rename_i k v t ih

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih : ∀ {l₁ : List ((a : α) × β a)}, DistinctKeys l₁ → DistinctKeys (List.insertList l₁ t)
l₁ : List ((a : α) × β a)
h : DistinctKeys l₁
⊢ DistinctKeys (List.insertList l₁ (⟨k, v⟩ :: t))

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih : ∀ {l₁ : List ((a : α) × β a)}, DistinctKeys l₁ → DistinctKeys (List.insertList l₁ t)
l₁ : List ((a : α) × β a)
h : DistinctKeys l₁
⊢ DistinctKeys (List.insertList l₁ (⟨k, v⟩ :: t))

Tactic:
rw [insertList.eq_def]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih : ∀ {l₁ : List ((a : α) × β a)}, DistinctKeys l₁ → DistinctKeys (List.insertList l₁ t)
l₁ : List ((a : α) × β a)
h : DistinctKeys l₁
⊢ DistinctKeys
    (match ⟨k, v⟩ :: t with
    | [] => l₁
    | ⟨k, v⟩ :: toInsert => List.insertList (List.insertEntry k v l₁) toInsert)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l₁ l₂ : List ((a : α) × β a)
h : DistinctKeys l₁
⊢ DistinctKeys (List.insertList l₁ l₂)

Tactic:
induction l₂ using assoc_induction generalizing l₁

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l₁ : List ((a : α) × β a)
h : DistinctKeys l₁
⊢ DistinctKeys (List.insertList l₁ [])

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : ∀ {l₁ : List ((a : α) × β a)}, DistinctKeys l₁ → DistinctKeys (List.insertList l₁ tail✝)
l₁ : List ((a : α) × β a)
h : DistinctKeys l₁
⊢ DistinctKeys (List.insertList l₁ (⟨k✝, v✝⟩ :: tail✝))

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l₁ : List ((a : α) × β a)
h : DistinctKeys l₁
⊢ DistinctKeys (List.insertList l₁ [])

Tactic:
simpa [insertList]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem isComplete_iff_ultrafilter {s : Set α} :
    IsComplete s ↔ ∀ l : Ultrafilter α, Cauchy (l : Filter α) → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x

Proof state:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x l

Tactic:
haveI := hl.1

Result:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
⊢ ∃ x ∈ s, ClusterPt x l

Proof state:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
⊢ ∃ x ∈ s, ClusterPt x l

Tactic:
rcases H (Ultrafilter.of l) hl.ultrafilter_of ((Ultrafilter.of_le l).trans hls) with ⟨x, hxs, hxl⟩

Result:
case intro.intro
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
x : α
hxs : x ∈ s
hxl : ↑(Ultrafilter.of l) ≤ 𝓝 x
⊢ ∃ x ∈ s, ClusterPt x l

Proof state:
case intro.intro
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
x : α
hxs : x ∈ s
hxl : ↑(Ultrafilter.of l) ≤ 𝓝 x
⊢ ∃ x ∈ s, ClusterPt x l

Tactic:
exact ⟨x, hxs, (ClusterPt.of_le_nhds hxl).mono (Ultrafilter.of_le l)⟩

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x

Tactic:
refine ⟨fun h l => h l, fun H => isComplete_iff_clusterPt.2 fun l hl hls => ?_⟩

Result:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x l
-- Mathlib/Geometry/Euclidean/Inversion/Basic.lean
theorem inversion_inversion (c : P) {R : ℝ} (hR : R ≠ 0) (x : P) :
    inversion c R (inversion c R x) = x

Proof state:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ inversion c R (inversion c R x) = x

Tactic:
rw [inversion, dist_inversion_center, inversion_vsub_center, smul_smul, ← mul_pow,
  div_mul_div_comm, div_mul_cancel₀ _ (dist_ne_zero.2 hne), ← sq, div_self, one_pow, one_smul,
  vsub_vadd]

Result:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ R ^ 2 ≠ 0

Proof state:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ R ^ 2 ≠ 0

Tactic:
exact pow_ne_zero _ hR

Result:
no goals

Proof state:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
R : ℝ
hR : R ≠ 0
x : P
⊢ inversion x R (inversion x R x) = x

Tactic:
rw [inversion_self, inversion_self]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
⊢ inversion c R (inversion c R x) = x

Tactic:
rcases eq_or_ne x c with (rfl | hne)

Result:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
R : ℝ
hR : R ≠ 0
x : P
⊢ inversion x R (inversion x R x) = x

case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ inversion c R (inversion c R x) = x
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
lemma isMin_iff {x : PrimeSpectrum R} :
    IsMin x ↔ x.asIdeal ∈ minimalPrimes R

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃b : PrimeSpectrum R⦄, b ≤ x → x ≤ b) ↔ ∀ ⦃y : Ideal R⦄, y.IsPrime → y ≤ x.asIdeal → x.asIdeal ≤ y

Tactic:
exact ⟨fun H y hy e ↦ @H ⟨y, hy⟩ e, fun H y e ↦ H y.2 e⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsMin x ↔ Minimal (fun q => q.IsPrime ∧ ⊥ ≤ q) x.asIdeal

Tactic:
simp only [IsMin, Minimal, x.2, bot_le, and_self, and_true, true_and]

Result:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ ⦃b : PrimeSpectrum R⦄, b ≤ x → x ≤ b) ↔ ∀ ⦃y : Ideal R⦄, y.IsPrime → y ≤ x.asIdeal → x.asIdeal ≤ y

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsMin x ↔ x.asIdeal ∈ minimalPrimes R

Tactic:
show IsMin _ ↔ Minimal (fun q : Ideal R ↦ q.IsPrime ∧ ⊥ ≤ q) _

Result:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsMin x ↔ Minimal (fun q => q.IsPrime ∧ ⊥ ≤ q) x.asIdeal
-- Mathlib/Data/Finmap.lean
theorem extract_eq_lookup_erase (a : α) (s : Finmap β) : extract a s = (lookup a s, erase a s) :=
  induction_on s fun s => by simp [extract]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s✝ : Finmap β
s : AList β
⊢ extract a ⟦s⟧ = (lookup a ⟦s⟧, erase a ⟦s⟧)

Tactic:
simp [extract]

Result:
no goals
-- Mathlib/CategoryTheory/Enriched/Opposite.lean
/-- When composing a tensor product of morphisms with the `V`-composition morphism in `Cᵒᵖ`,
this re-writes the `V`-composition to be in `C` and moves the braiding to the left. -/
@[reassoc]
lemma tensorHom_eComp_op_eq {C : Type u} [EnrichedCategory V C] {x y z : Cᵒᵖ} {v w : V}
    (f : v ⟶ EnrichedCategory.Hom z y) (g : w ⟶ EnrichedCategory.Hom y x) :
    (f ⊗ g) ≫ eComp V z y x = (β_ v w).hom ≫ (g ⊗ f) ≫ eComp V x.unop y.unop z.unop

Proof state:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : Cᵒᵖ
v w : V
f : v ⟶ EnrichedCategory.Hom z y
g : w ⟶ EnrichedCategory.Hom y x
⊢ (f ⊗ g) ≫ eComp V z y x = (β_ v w).hom ≫ (g ⊗ f) ≫ eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)

Tactic:
rw [eComp_op_eq]

Result:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : Cᵒᵖ
v w : V
f : v ⟶ EnrichedCategory.Hom z y
g : w ⟶ EnrichedCategory.Hom y x
⊢ (f ⊗ g) ≫
      (β_ (EnrichedCategory.Hom (Opposite.unop y) (Opposite.unop z))
            (EnrichedCategory.Hom (Opposite.unop x) (Opposite.unop y))).hom ≫
        eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z) =
    (β_ v w).hom ≫ (g ⊗ f) ≫ eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)

Proof state:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : Cᵒᵖ
v w : V
f : v ⟶ EnrichedCategory.Hom z y
g : w ⟶ EnrichedCategory.Hom y x
⊢ (f ⊗ g) ≫
      (β_ (EnrichedCategory.Hom (Opposite.unop y) (Opposite.unop z))
            (EnrichedCategory.Hom (Opposite.unop x) (Opposite.unop y))).hom ≫
        eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z) =
    (β_ v w).hom ≫ (g ⊗ f) ≫ eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)

Tactic:
exact braiding_naturality_assoc f g _

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
theorem coe_mem_iff_mem {x : (CliffordAlgebra Q)ˣ} :
    ↑x ∈ (lipschitzGroup Q).toSubmonoid.map (Units.coeHom <| CliffordAlgebra Q) ↔
    x ∈ lipschitzGroup Q

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
⊢ (∃ x_1 ∈ lipschitzGroup Q, x_1 = x) ↔ x ∈ lipschitzGroup Q

Tactic:
exact exists_eq_right

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
⊢ ↑x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ↔ x ∈ lipschitzGroup Q

Tactic:
simp only [Submonoid.mem_map, Subgroup.mem_toSubmonoid, Units.coeHom_apply, exists_prop]

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
⊢ (∃ x_1 ∈ lipschitzGroup Q, ↑x_1 = ↑x) ↔ x ∈ lipschitzGroup Q

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
⊢ (∃ x_1 ∈ lipschitzGroup Q, ↑x_1 = ↑x) ↔ x ∈ lipschitzGroup Q

Tactic:
norm_cast

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
⊢ (∃ x_1 ∈ lipschitzGroup Q, x_1 = x) ↔ x ∈ lipschitzGroup Q
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem ideal_span_singleton_smul (r : R) (N : Submodule R M) :
    (Ideal.span {r} : Ideal R) • N = r • N

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
this : span R (⋃ t ∈ N, {r • t}) = r • N
⊢ Ideal.span {r} • N = r • N

Tactic:
conv_lhs => rw [← span_eq N, span_smul_span]

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
this : span R (⋃ t ∈ N, {r • t}) = r • N
⊢ span R (⋃ s ∈ {r}, ⋃ t ∈ ↑N, {s • t}) = r • N

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
this : span R (⋃ t ∈ N, {r • t}) = r • N
⊢ span R (⋃ s ∈ {r}, ⋃ t ∈ ↑N, {s • t}) = r • N

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
⊢ span R (⋃ t ∈ N, {r • t}) = r • N

Tactic:
convert span_eq (r • N)

Result:
case h.e'_2.h.e'_6
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
⊢ ⋃ t ∈ N, {r • t} = ↑(r • N)

Proof state:
case h.e'_2.h.e'_6
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
⊢ ⋃ t ∈ N, {r • t} = ↑(r • N)

Tactic:
exact (Set.image_eq_iUnion _ (N : Set M)).symm

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
⊢ Ideal.span {r} • N = r • N

Tactic:
have : span R (⋃ (t : M) (_ : t ∈ N), {r • t}) = r • N := by
  convert span_eq (r • N)
  exact (Set.image_eq_iUnion _ (N : Set M)).symm

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
this : span R (⋃ t ∈ N, {r • t}) = r • N
⊢ Ideal.span {r} • N = r • N
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.mul_right (H1 : IsCoprime x y) (H2 : IsCoprime x z) : IsCoprime x (y * z)

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime y x
H2 : IsCoprime z x
⊢ IsCoprime (y * z) x

Tactic:
exact H1.mul_left H2

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : IsCoprime x z
⊢ IsCoprime x (y * z)

Tactic:
rw [isCoprime_comm] at H1 H2 ⊢

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime y x
H2 : IsCoprime z x
⊢ IsCoprime (y * z) x
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem rank_bot : Module.rank F (⊥ : IntermediateField F E) = 1

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Module.rank F ↥⊥ = 1

Tactic:
rw [rank_eq_one_iff]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Polynomial.lean
lemma toContinuousMap_X_eq_id : X.toContinuousMap = .id R

Proof state:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ X.toContinuousMap = ContinuousMap.id R

Tactic:
ext

Result:
case h
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
a✝ : R
⊢ X.toContinuousMap a✝ = (ContinuousMap.id R) a✝

Proof state:
case h
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
a✝ : R
⊢ X.toContinuousMap a✝ = (ContinuousMap.id R) a✝

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem compl_gt [LinearOrder α] : (· > · : α → α → _)ᶜ = (· ≤ ·)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 => x1 > x2)ᶜ = fun x1 x2 => x1 ≤ x2

Tactic:
ext

Result:
case h.h.a
α : Type u_2
inst✝ : LinearOrder α
x✝¹ x✝ : α
⊢ (fun x1 x2 => x1 > x2)ᶜ x✝¹ x✝ ↔ x✝¹ ≤ x✝

Proof state:
case h.h.a
α : Type u_2
inst✝ : LinearOrder α
x✝¹ x✝ : α
⊢ (fun x1 x2 => x1 > x2)ᶜ x✝¹ x✝ ↔ x✝¹ ≤ x✝

Tactic:
simp [compl]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
lemma range_toUniformOnFun [DecidableEq ι] [TopologicalSpace F] :
    range toUniformOnFun =
      {f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F |
        Continuous (toFun _ f) ∧
        (∀ (m : Π i, E i) i x y,
          toFun _ f (update m i (x + y)) = toFun _ f (update m i x) + toFun _ f (update m i y)) ∧
        (∀ (m : Π i, E i) i (c : 𝕜) x,
          toFun _ f (update m i (c • x)) = c • toFun _ f (update m i x))}

Proof state:
case h.mpr
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → TopologicalSpace (E i)
inst✝⁵ : (i : ι) → AddCommGroup (E i)
inst✝⁴ : (i : ι) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : DecidableEq ι
inst✝ : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F
⊢ f ∈
      {f |
        Continuous ((toFun {s | IsVonNBounded 𝕜 s}) f) ∧
          (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
              (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (x + y)) =
                (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x) + (toFun {s | IsVonNBounded 𝕜 s}) f (update m i y)) ∧
            ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
              (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (c • x)) =
                c • (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x)} →
    f ∈ range toUniformOnFun

Tactic:
rintro ⟨hcont, hadd, hsmul⟩

Result:
case h.mpr.intro.intro
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → TopologicalSpace (E i)
inst✝⁵ : (i : ι) → AddCommGroup (E i)
inst✝⁴ : (i : ι) → Module 𝕜 (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : DecidableEq ι
inst✝ : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F
hcont : Continuous ((toFun {s | IsVonNBounded 𝕜 s}) f)
hadd :
  ∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
    (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (x + y)) =
      (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x) + (toFun {s | IsVonNBounded 𝕜 s}) f (update m i y)
hsmul :
  ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
    (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (c • x)) = c • (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x)
⊢ f ∈ range toUniformOnFun
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma map_id (i : Fin (n + 1 + 1)) : map F f i i (by simp) = 𝟙 _

Proof state:
C : Type u_1
inst✝ : Category.{?u.90683, u_1} C
n m : ℕ
F G : ComposableArrows C n
X : C
f : X ⟶ F.left
i : Fin (n + 1 + 1)
⊢ i ≤ i

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
i : Fin (n + 1 + 1)
⊢ map F f i i ⋯ = 𝟙 (obj F X i)

Tactic:
obtain ⟨_|_, hi⟩ := i <;> simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degrees_prod_le {ι : Type*} {s : Finset ι} {f : ι → MvPolynomial σ R} :
    (∏ i ∈ s, f i).degrees ≤ ∑ i ∈ s, (f i).degrees

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (∏ i ∈ s, f i).degrees ≤ ∑ i ∈ s, (f i).degrees

Tactic:
exact supDegree_prod_le (map_zero _) (map_add _)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (∏ i ∈ s, f i).degrees ≤ ∑ i ∈ s, (f i).degrees

Tactic:
classical exact supDegree_prod_le (map_zero _) (map_add _)

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem mul_inl_eq_op_smul [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
    (x : tsze R M) (r : R) :
    x * inl r = x <• r :=
  ext rfl (by dsimp; rw [smul_zero, zero_add])

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x : tsze R M
r : R
⊢ (x * inl r).snd = (x <• r).snd

Tactic:
dsimp

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x : tsze R M
r : R
⊢ x.fst •> 0 + x.snd <• r = x.snd <• r

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x : tsze R M
r : R
⊢ x.fst •> 0 + x.snd <• r = x.snd <• r

Tactic:
rw [smul_zero, zero_add]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma restrictSubtype_indep_iff_of_subset (hIX : I ⊆ X) :
    (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep I

Proof state:
α : Type u_1
X I : Set α
M : Matroid α
hIX : I ⊆ X
⊢ (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep I

Tactic:
rw [restrictSubtype_indep_iff, image_preimage_eq_iff.2]

Result:
α : Type u_1
X I : Set α
M : Matroid α
hIX : I ⊆ X
⊢ I ⊆ range Subtype.val

Proof state:
α : Type u_1
X I : Set α
M : Matroid α
hIX : I ⊆ X
⊢ I ⊆ range Subtype.val

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_top : expGrowthSup ⊤ = ⊤

Proof state:
⊢ expGrowthInf ⊤ ≤ expGrowthSup ⊤

Tactic:
exact expGrowthInf_le_expGrowthSup

Result:
no goals

Proof state:
⊢ ⊤ ≤ expGrowthSup ⊤

Tactic:
rw [← expGrowthInf_top]

Result:
⊢ expGrowthInf ⊤ ≤ expGrowthSup ⊤

Proof state:
⊢ expGrowthSup ⊤ = ⊤

Tactic:
apply top_le_iff.1

Result:
⊢ ⊤ ≤ expGrowthSup ⊤
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem hasFiniteIntegral_restrict_of_bounded [NormedAddCommGroup E] {f : α → E} {s : Set α}
    {μ : Measure α} {C} (hs : μ s < ∞) (hf : ∀ᵐ x ∂μ.restrict s, ‖f x‖ ≤ C) :
    HasFiniteIntegral f (μ.restrict s) :=
  haveI : IsFiniteMeasure (μ.restrict s) := ⟨by rwa [Measure.restrict_apply_univ]⟩
  hasFiniteIntegral_of_bounded hf

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
C : ℝ
hs : μ s < ⊤
hf : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ (μ.restrict s) univ < ⊤

Tactic:
rwa [Measure.restrict_apply_univ]

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwise_insert_of_symmetric_of_not_mem (hr : Symmetric r) (ha : a ∉ s) :
    (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
hr : Symmetric r
ha : a ∉ s
⊢ (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b

Tactic:
simp only [pairwise_insert_of_not_mem ha, hr.iff a, and_self_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem coeff_mul_of_natDegree_le (pm : p.natDegree ≤ m) (qn : q.natDegree ≤ n) :
    (p * q).coeff (m + n) = p.coeff m * q.coeff n

Proof state:
R : Type u
m n : ℕ
inst✝ : Semiring R
p q : R[X]
pm : p.natDegree ≤ m
qn : q.natDegree ≤ n
⊢ (p * q).coeff (m + n) = p.coeff m * q.coeff n

Tactic:
simp_rw [← Polynomial.toFinsupp_apply, toFinsupp_mul]

Result:
R : Type u
m n : ℕ
inst✝ : Semiring R
p q : R[X]
pm : p.natDegree ≤ m
qn : q.natDegree ≤ n
⊢ (p.toFinsupp * q.toFinsupp) (m + n) = p.toFinsupp m * q.toFinsupp n

Proof state:
case refine_1
R : Type u
m n : ℕ
inst✝ : Semiring R
p q : R[X]
pm : p.natDegree ≤ m
qn : q.natDegree ≤ n
⊢ ∀ (a1 a2 : ℕ), id (a1 + a2) = id a1 + id a2

Tactic:
simp

Result:
no goals

Proof state:
case refine_3
R : Type u
m n : ℕ
inst✝ : Semiring R
p q : R[X]
pm : p.natDegree ≤ m
qn : q.natDegree ≤ n
⊢ AddMonoidAlgebra.supDegree id q.toFinsupp ≤ id n

Tactic:
rwa [supDegree_eq_natDegree, id_eq]

Result:
no goals

Proof state:
R : Type u
m n : ℕ
inst✝ : Semiring R
p q : R[X]
pm : p.natDegree ≤ m
qn : q.natDegree ≤ n
⊢ (p.toFinsupp * q.toFinsupp) (m + n) = p.toFinsupp m * q.toFinsupp n

Tactic:
refine AddMonoidAlgebra.apply_add_of_supDegree_le ?_ Function.injective_id ?_ ?_

Result:
case refine_1
R : Type u
m n : ℕ
inst✝ : Semiring R
p q : R[X]
pm : p.natDegree ≤ m
qn : q.natDegree ≤ n
⊢ ∀ (a1 a2 : ℕ), id (a1 + a2) = id a1 + id a2

case refine_2
R : Type u
m n : ℕ
inst✝ : Semiring R
p q : R[X]
pm : p.natDegree ≤ m
qn : q.natDegree ≤ n
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp ≤ id m

case refine_3
R : Type u
m n : ℕ
inst✝ : Semiring R
p q : R[X]
pm : p.natDegree ≤ m
qn : q.natDegree ≤ n
⊢ AddMonoidAlgebra.supDegree id q.toFinsupp ≤ id n

Proof state:
case refine_2
R : Type u
m n : ℕ
inst✝ : Semiring R
p q : R[X]
pm : p.natDegree ≤ m
qn : q.natDegree ≤ n
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp ≤ id m

Tactic:
rwa [supDegree_eq_natDegree, id_eq]

Result:
no goals