harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
lemma shiftIso_add (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') :
    F.shiftIso (m + n) a a'' (by rw [add_assoc, ha', ha'']) =
      isoWhiskerRight (shiftFunctorAdd C m n) _ ≪≫ Functor.associator _ _ _ ≪≫
        isoWhiskerLeft _ (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha'' :=
  ShiftSequence.shiftIso_add _ _ _ _ _ _ _

Proof state:
C : Type u_1
A : Type u_2
inst✝⁶ : Category.{?u.41035, u_1} C
inst✝⁵ : Category.{?u.41039, u_2} A
F : C ⥤ A
M : Type u_3
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
G : Type u_4
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ m + n + a = a''

Tactic:
rw [add_assoc, ha', ha'']

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isClosed_singleton_iff_isMaximal (x : PrimeSpectrum R) :
    IsClosed ({x} : Set (PrimeSpectrum R)) ↔ x.asIdeal.IsMaximal

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : zeroLocus ↑x.asIdeal ⊆ {x}
⊢ x.asIdeal.IsMaximal

Tactic:
rcases x.asIdeal.exists_le_maximal x.2.1 with ⟨m, hm, hxm⟩

Result:
case mp.intro.intro
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : zeroLocus ↑x.asIdeal ⊆ {x}
m : Ideal R
hm : m.IsMaximal
hxm : x.asIdeal ≤ m
⊢ x.asIdeal.IsMaximal

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : x.asIdeal.IsMaximal
⊢ zeroLocus ↑x.asIdeal ⊆ {x}

Tactic:
exact fun p hp ↦ PrimeSpectrum.ext (H.eq_of_le p.2.1 hp).symm

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsClosed {x} ↔ x.asIdeal.IsMaximal

Tactic:
rw [← closure_subset_iff_isClosed, ← zeroLocus_vanishingIdeal_eq_closure,
    vanishingIdeal_singleton]

Result:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ zeroLocus ↑x.asIdeal ⊆ {x} ↔ x.asIdeal.IsMaximal

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ zeroLocus ↑x.asIdeal ⊆ {x} ↔ x.asIdeal.IsMaximal

Tactic:
constructor <;> intro H

Result:
case mp
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : zeroLocus ↑x.asIdeal ⊆ {x}
⊢ x.asIdeal.IsMaximal

case mpr
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : x.asIdeal.IsMaximal
⊢ zeroLocus ↑x.asIdeal ⊆ {x}

Proof state:
case mp.intro.intro
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : zeroLocus ↑x.asIdeal ⊆ {x}
m : Ideal R
hm : m.IsMaximal
hxm : x.asIdeal ≤ m
⊢ x.asIdeal.IsMaximal

Tactic:
exact (congr_arg asIdeal (@H ⟨m, hm.isPrime⟩ hxm)) ▸ hm

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

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

Tactic:
rwa [Int.neg_neg] at h

Result:
no goals

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

Tactic:
have h := Int.neg_le_neg h

Result:
a b : Int
h✝ : a ≤ -b
h : - -b ≤ -a
⊢ b ≤ -a
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
theorem riemannZeta_one_sub {s : ℂ} (hs : ∀ n : ℕ, s ≠ -n) (hs' : s ≠ 1) :
    riemannZeta (1 - s) = 2 * (2 * π) ^ (-s) * Gamma s * cos (π * s / 2) * riemannZeta s

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : s ≠ 1
⊢ riemannZeta (1 - s) = 2 * (2 * ↑π) ^ (-s) * Gamma s * cos (↑π * s / 2) * riemannZeta s

Tactic:
rw [riemannZeta, hurwitzZetaEven_one_sub 0 hs (Or.inr hs'), cosZeta_zero, hurwitzZetaEven_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_true : (countP fun (_ : α) => true) = length

Proof state:
α : Type u_1
⊢ (countP fun x => true) = length

Tactic:
funext l

Result:
case h
α : Type u_1
l : List α
⊢ countP (fun x => true) l = l.length

Proof state:
case h
α : Type u_1
l : List α
⊢ countP (fun x => true) l = l.length

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Ultra.lean
lemma nnnorm_intCast_le_one (z : ℤ) :
    ‖(z : R)‖₊ ≤ 1

Proof state:
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
z : ℤ
⊢ ‖↑z‖₊ ≤ 1

Tactic:
cases z <;>
simpa only [Int.ofNat_eq_coe, Int.cast_natCast, Int.cast_negSucc, Nat.cast_one, nnnorm_neg]
  using nnnorm_natCast_le_one _ _

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Alternating/Basic.lean
theorem toAlternatingMap_injective :
    Injective (toAlternatingMap : (M [⋀^ι]→L[R] N) → (M [⋀^ι]→ₗ[R] N)) := fun f g h =>
  DFunLike.ext' <| by convert DFunLike.ext'_iff.1 h

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
f g : M [⋀^ι]→L[R] N
h : f.toAlternatingMap = g.toAlternatingMap
⊢ ⇑f = ⇑g

Tactic:
convert DFunLike.ext'_iff.1 h

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Chain.lean
@[simp] lemma chainTop_zero : chainTop 0 β = β

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
β : Weight R L M
⊢ chainTop 0 β = β

Tactic:
ext

Result:
case h
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
β : Weight R L M
x✝ : L
⊢ (chainTop 0 β) x✝ = β x✝

Proof state:
case h
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
β : Weight R L M
x✝ : L
⊢ (chainTop 0 β) x✝ = β x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem col_vecMul [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :
    Matrix.col ι (v ᵥ* M) = (Matrix.row ι v * M)ᵀ

Proof state:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
⊢ col ι (v ᵥ* M) = (row ι v * M)ᵀ

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
i✝ : n
j✝ : ι
⊢ col ι (v ᵥ* M) i✝ j✝ = (row ι v * M)ᵀ i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
i✝ : n
j✝ : ι
⊢ col ι (v ᵥ* M) i✝ j✝ = (row ι v * M)ᵀ i✝ j✝

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem IsFiniteMeasureOnCompacts.map (μ : Measure α) [IsFiniteMeasureOnCompacts μ]
    (f : α ≃ₜ β) : IsFiniteMeasureOnCompacts (Measure.map f μ)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : TopologicalSpace β
mβ : MeasurableSpace β
inst✝¹ : BorelSpace β
μ : Measure α
inst✝ : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ (Measure.map (⇑f) μ) K < ⊤

Tactic:
rw [← Homeomorph.toMeasurableEquiv_coe, MeasurableEquiv.map_apply]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : TopologicalSpace β
mβ : MeasurableSpace β
inst✝¹ : BorelSpace β
μ : Measure α
inst✝ : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ μ (⇑f.toMeasurableEquiv ⁻¹' K) < ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : TopologicalSpace β
mβ : MeasurableSpace β
inst✝¹ : BorelSpace β
μ : Measure α
inst✝ : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
⊢ IsFiniteMeasureOnCompacts (Measure.map (⇑f) μ)

Tactic:
refine ⟨fun K hK ↦ ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : TopologicalSpace β
mβ : MeasurableSpace β
inst✝¹ : BorelSpace β
μ : Measure α
inst✝ : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ (Measure.map (⇑f) μ) K < ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : TopologicalSpace β
mβ : MeasurableSpace β
inst✝¹ : BorelSpace β
μ : Measure α
inst✝ : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ μ (⇑f.toMeasurableEquiv ⁻¹' K) < ⊤

Tactic:
exact IsCompact.measure_lt_top (f.isCompact_preimage.2 hK)

Result:
no goals
-- Mathlib/RingTheory/Ideal/IsPrimary.lean
theorem isPrime_radical {I : Ideal R} (hi : I.IsPrimary) : IsPrime (radical I) :=
  ⟨mt radical_eq_top.1 hi.1,
   fun {x y} ⟨m, hxy⟩ => by
    rw [mul_pow] at hxy; rcases (isPrimary_iff.mp hi).2 hxy with h | h
    · exact Or.inl ⟨m, h⟩
    · exact Or.inr (mem_radical_of_pow_mem h)⟩

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.IsPrimary
x y : R
x✝ : x * y ∈ I.radical
m : ℕ
hxy : (x * y) ^ m ∈ I
⊢ x ∈ I.radical ∨ y ∈ I.radical

Tactic:
rw [mul_pow] at hxy

Result:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.IsPrimary
x y : R
x✝ : x * y ∈ I.radical
m : ℕ
hxy : x ^ m * y ^ m ∈ I
⊢ x ∈ I.radical ∨ y ∈ I.radical

Proof state:
case inl
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.IsPrimary
x y : R
x✝ : x * y ∈ I.radical
m : ℕ
hxy : x ^ m * y ^ m ∈ I
h : x ^ m ∈ I
⊢ x ∈ I.radical ∨ y ∈ I.radical

Tactic:
exact Or.inl ⟨m, h⟩

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.IsPrimary
x y : R
x✝ : x * y ∈ I.radical
m : ℕ
hxy : x ^ m * y ^ m ∈ I
h : y ^ m ∈ I.radical
⊢ x ∈ I.radical ∨ y ∈ I.radical

Tactic:
exact Or.inr (mem_radical_of_pow_mem h)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.IsPrimary
x y : R
x✝ : x * y ∈ I.radical
m : ℕ
hxy : x ^ m * y ^ m ∈ I
⊢ x ∈ I.radical ∨ y ∈ I.radical

Tactic:
rcases (isPrimary_iff.mp hi).2 hxy with h | h

Result:
case inl
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.IsPrimary
x y : R
x✝ : x * y ∈ I.radical
m : ℕ
hxy : x ^ m * y ^ m ∈ I
h : x ^ m ∈ I
⊢ x ∈ I.radical ∨ y ∈ I.radical

case inr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.IsPrimary
x y : R
x✝ : x * y ∈ I.radical
m : ℕ
hxy : x ^ m * y ^ m ∈ I
h : y ^ m ∈ I.radical
⊢ x ∈ I.radical ∨ y ∈ I.radical
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma div_zero {a : EReal} : a / 0 = 0

Proof state:
a : EReal
⊢ a * 0⁻¹ = 0

Tactic:
rw [inv_zero, mul_zero a]

Result:
no goals

Proof state:
a : EReal
⊢ a / 0 = 0

Tactic:
change a * 0⁻¹ = 0

Result:
a : EReal
⊢ a * 0⁻¹ = 0
-- Mathlib/Topology/Connected/PathConnected.lean
theorem IsPathConnected.isConnected (hF : IsPathConnected F) : IsConnected F

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
hF : IsPathConnected F
⊢ IsConnected F

Tactic:
rw [isConnected_iff_connectedSpace]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
hF : IsPathConnected F
⊢ ConnectedSpace ↑F

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
hF : PathConnectedSpace ↑F
⊢ ConnectedSpace ↑F

Tactic:
exact @PathConnectedSpace.connectedSpace _ _ hF

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
hF : IsPathConnected F
⊢ ConnectedSpace ↑F

Tactic:
rw [isPathConnected_iff_pathConnectedSpace] at hF

Result:
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
hF : PathConnectedSpace ↑F
⊢ ConnectedSpace ↑F
-- Mathlib/AlgebraicTopology/SimplicialNerve.lean
@[ext]
lemma hom_ext {J : Type*} [LinearOrder J]
    (i j : SimplicialThickening J) (x y : i ⟶ j) (h : ∀ t, t ∈ x.I ↔ t ∈ y.I) : x = y

Proof state:
case I
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : SimplicialThickening J), t ∈ x.I ↔ t ∈ y.I
⊢ x.I = y.I

Tactic:
ext

Result:
case I.h
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : SimplicialThickening J), t ∈ x.I ↔ t ∈ y.I
x✝ : SimplicialThickening J
⊢ x✝ ∈ x.I ↔ x✝ ∈ y.I

Proof state:
case I.h
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : SimplicialThickening J), t ∈ x.I ↔ t ∈ y.I
x✝ : SimplicialThickening J
⊢ x✝ ∈ x.I ↔ x✝ ∈ y.I

Tactic:
apply h

Result:
no goals

Proof state:
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : SimplicialThickening J), t ∈ x.I ↔ t ∈ y.I
⊢ x = y

Tactic:
apply Path.ext

Result:
case I
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : SimplicialThickening J), t ∈ x.I ↔ t ∈ y.I
⊢ x.I = y.I
-- Mathlib/Data/Set/NAry.lean
theorem image2_right (h : s.Nonempty) : image2 (fun _ y => y) s t = t

Proof state:
α : Type u_1
β : Type u_3
s : Set α
t : Set β
h : s.Nonempty
⊢ image2 (fun x y => y) s t = t

Tactic:
simp [nonempty_def.mp h, Set.ext_iff]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
/-- The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero. -/
lemma NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded {ι 𝕜 𝔸 : Type*}
    [NormedDivisionRing 𝕜] [NormedAddCommGroup 𝔸] [Module 𝕜 𝔸] [BoundedSMul 𝕜 𝔸] {l : Filter ι}
    {ε : ι → 𝕜} {f : ι → 𝔸} (hε : Tendsto ε l (𝓝 0)) (hf : IsBoundedUnder (· ≤ ·) l (norm ∘ f)) :
    Tendsto (ε • f) l (𝓝 0)

Proof state:
ι : Type u_1
𝕜 : Type u_2
𝔸 : Type u_3
inst✝³ : NormedDivisionRing 𝕜
inst✝² : NormedAddCommGroup 𝔸
inst✝¹ : Module 𝕜 𝔸
inst✝ : BoundedSMul 𝕜 𝔸
l : Filter ι
ε : ι → 𝕜
f : ι → 𝔸
hε : ε =o[l] fun _x => 1
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
⊢ (ε • f) =o[l] fun _x => 1

Tactic:
simpa using IsLittleO.smul_isBigO hε (hf.isBigO_const (one_ne_zero : (1 : 𝕜) ≠ 0))

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
𝔸 : Type u_3
inst✝³ : NormedDivisionRing 𝕜
inst✝² : NormedAddCommGroup 𝔸
inst✝¹ : Module 𝕜 𝔸
inst✝ : BoundedSMul 𝕜 𝔸
l : Filter ι
ε : ι → 𝕜
f : ι → 𝔸
hε : Tendsto ε l (𝓝 0)
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
⊢ Tendsto (ε • f) l (𝓝 0)

Tactic:
rw [← isLittleO_one_iff 𝕜] at hε ⊢

Result:
ι : Type u_1
𝕜 : Type u_2
𝔸 : Type u_3
inst✝³ : NormedDivisionRing 𝕜
inst✝² : NormedAddCommGroup 𝔸
inst✝¹ : Module 𝕜 𝔸
inst✝ : BoundedSMul 𝕜 𝔸
l : Filter ι
ε : ι → 𝕜
f : ι → 𝔸
hε : ε =o[l] fun _x => 1
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
⊢ (ε • f) =o[l] fun _x => 1
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem sub_comp {X Y Z : C} (f g : X ⟶ Y) (h : Y ⟶ Z) : (f - g) ≫ h = f ≫ h - g ≫ h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ (f - g) ≫ h = f ≫ h - g ≫ h

Tactic:
rw [sub_def, Category.assoc, σ_comp, ← Category.assoc, prod.lift_map, sub_def]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
theorem isUniformEmbedding_restrictScalars :
    IsUniformEmbedding (restrictScalars 𝕜' : E [⋀^ι]→L[𝕜] F → E [⋀^ι]→L[𝕜'] F)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜 F
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup F
𝕜' : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜'
inst✝⁵ : NormedAlgebra 𝕜' 𝕜
inst✝⁴ : Module 𝕜' E
inst✝³ : IsScalarTower 𝕜' 𝕜 E
inst✝² : Module 𝕜' F
inst✝¹ : IsScalarTower 𝕜' 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
⊢ IsUniformEmbedding (restrictScalars 𝕜')

Tactic:
rw [← isUniformEmbedding_toContinuousMultilinearMap.of_comp_iff]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜 F
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup F
𝕜' : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜'
inst✝⁵ : NormedAlgebra 𝕜' 𝕜
inst✝⁴ : Module 𝕜' E
inst✝³ : IsScalarTower 𝕜' 𝕜 E
inst✝² : Module 𝕜' F
inst✝¹ : IsScalarTower 𝕜' 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
⊢ IsUniformEmbedding (toContinuousMultilinearMap ∘ restrictScalars 𝕜')

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜 F
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup F
𝕜' : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜'
inst✝⁵ : NormedAlgebra 𝕜' 𝕜
inst✝⁴ : Module 𝕜' E
inst✝³ : IsScalarTower 𝕜' 𝕜 E
inst✝² : Module 𝕜' F
inst✝¹ : IsScalarTower 𝕜' 𝕜 F
inst✝ : ContinuousSMul 𝕜 E
⊢ IsUniformEmbedding (toContinuousMultilinearMap ∘ restrictScalars 𝕜')

Tactic:
exact (ContinuousMultilinearMap.isUniformEmbedding_restrictScalars 𝕜').comp
  isUniformEmbedding_toContinuousMultilinearMap

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem Filter.coclosedCompact_eq_cocompact : coclosedCompact X = cocompact X

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ coclosedCompact X ≤ cocompact X

Tactic:
rw [hasBasis_coclosedCompact.le_basis_iff hasBasis_cocompact]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ ∀ (i' : Set X), IsCompact i' → ∃ i, (IsClosed i ∧ IsCompact i) ∧ iᶜ ⊆ i'ᶜ

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ ∀ (i' : Set X), IsCompact i' → ∃ i, (IsClosed i ∧ IsCompact i) ∧ iᶜ ⊆ i'ᶜ

Tactic:
exact fun K hK ↦ ⟨closure K, ⟨isClosed_closure, hK.closure⟩, compl_subset_compl.2 subset_closure⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ coclosedCompact X = cocompact X

Tactic:
refine le_antisymm ?_ cocompact_le_coclosedCompact

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ coclosedCompact X ≤ cocompact X
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_add (μ ν : Measure α) {f : α → β} (hf : Measurable f) :
    (μ + ν).map f = μ.map f + ν.map f

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
f : α → β
hf : Measurable f
⊢ map f (μ + ν) = map f μ + map f ν

Tactic:
simp [← mapₗ_apply_of_measurable hf]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_le_of_neg (ha : a < 0) (hb : b < 0) : 1 / a ≤ b ↔ 1 / b ≤ a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
ha : a < 0
hb : b < 0
⊢ 1 / a ≤ b ↔ 1 / b ≤ a

Tactic:
simpa using inv_le_of_neg ha hb

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem prod_comap_inl : (prod p q).comap (inl R M M₂) = p

Proof state:
case h
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₂
p : Submodule R M
q : Submodule R M₂
x✝ : M
⊢ x✝ ∈ comap (inl R M M₂) (p.prod q) ↔ x✝ ∈ p

Tactic:
simp

Result:
no goals

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₂
p : Submodule R M
q : Submodule R M₂
⊢ comap (inl R M M₂) (p.prod q) = p

Tactic:
ext

Result:
case h
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₂
p : Submodule R M
q : Submodule R M₂
x✝ : M
⊢ x✝ ∈ comap (inl R M M₂) (p.prod q) ↔ x✝ ∈ p
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem Int.alternating_sum_range_choose_of_ne {n : ℕ} (h0 : n ≠ 0) :
    (∑ m ∈ range (n + 1), ((-1) ^ m * n.choose m : ℤ)) = 0

Proof state:
n : ℕ
h0 : n ≠ 0
⊢ ∑ m ∈ range (n + 1), (-1) ^ m * ↑(n.choose m) = 0

Tactic:
rw [Int.alternating_sum_range_choose, if_neg h0]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_map (f : β → α) (s : Multiset β) : filter p (map f s) = map f (filter (p ∘ f) s) :=
  Quot.inductionOn s fun l => by simp [List.filter_map]; rfl

Proof state:
α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ filter p (map f (Quot.mk (⇑(isSetoid β)) l)) = map f (filter (p ∘ f) (Quot.mk (⇑(isSetoid β)) l))

Tactic:
simp [List.filter_map]

Result:
α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ List.map f (List.filter ((fun b => decide (p b)) ∘ f) l) ~
    List.map (fun x => f x) (List.filter (fun b => decide (p (f b))) l)

Proof state:
α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ List.map f (List.filter ((fun b => decide (p b)) ∘ f) l) ~
    List.map (fun x => f x) (List.filter (fun b => decide (p (f b))) l)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
theorem Ideal.toCharacterSpace_apply_eq_zero_of_mem {a : A} (ha : a ∈ I) :
    I.toCharacterSpace a = 0

Proof state:
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : I.IsMaximal
a : A
ha : a ∈ I
⊢ I.toCharacterSpace a = 0

Tactic:
unfold Ideal.toCharacterSpace

Result:
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : I.IsMaximal
a : A
ha : a ∈ I
⊢ (CharacterSpace.equivAlgHom.symm ((↑(NormedRing.algEquivComplexOfComplete ⋯).symm).comp (Quotient.mkₐ ℂ I))) a = 0

Proof state:
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : I.IsMaximal
a : A
ha : a ∈ I
⊢ (CharacterSpace.equivAlgHom.symm ((↑(NormedRing.algEquivComplexOfComplete ⋯).symm).comp (Quotient.mkₐ ℂ I))) a = 0

Tactic:
simp only [CharacterSpace.equivAlgHom_symm_coe, AlgHom.coe_comp, AlgHom.coe_coe,
  Quotient.mkₐ_eq_mk, Function.comp_apply, NormedRing.algEquivComplexOfComplete_symm_apply]

Result:
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : I.IsMaximal
a : A
ha : a ∈ I
⊢ ⋯.some = 0

Proof state:
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : I.IsMaximal
a : A
ha : a ∈ I
⊢ ⋯.some = 0

Tactic:
exact Set.eq_of_mem_singleton (Set.singleton_nonempty (0 : ℂ)).some_mem

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem map_permutations (f : α → β) (ts : List α) :
    map (map f) (permutations ts) = permutations (map f ts)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) ts.permutations = (map f ts).permutations

Tactic:
rw [permutations, permutations, map, map_permutationsAux, map]

Result:
no goals