harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem ContinuousLinearMap.curry_uncurryLeft
    (f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei i.succ) G) :
    f.uncurryLeft.curryLeft = f

Proof state:
case h.H
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G
m : Ei 0
x : (i : Fin n) → Ei i.succ
⊢ (f.uncurryLeft.curryLeft m) x = (f m) x

Tactic:
rw [ContinuousMultilinearMap.curryLeft_apply, ContinuousLinearMap.uncurryLeft_apply, tail_cons,
  cons_zero]

Result:
no goals

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G
⊢ f.uncurryLeft.curryLeft = f

Tactic:
ext m x

Result:
case h.H
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G
m : Ei 0
x : (i : Fin n) → Ei i.succ
⊢ (f.uncurryLeft.curryLeft m) x = (f m) x
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
theorem uncurry_eq (g : Y ⟶ A ⟶[C] X) : uncurry g = (A ◁ g) ≫ (ihom.ev A).app X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X Y : C
inst✝ : Closed A
g : Y ⟶ (ihom A).obj X
⊢ uncurry g = A ◁ g ≫ (ihom.ev A).app X

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem measure_union_add_inter₀ (s : Set α) (ht : NullMeasurableSet t μ) :
    μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Tactic:
rw [← measure_inter_add_diff₀ (s ∪ t) ht, union_inter_cancel_right, union_diff_right, ←
  measure_inter_add_diff₀ s ht, add_comm, ← add_assoc, add_right_comm]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem lift_of_comp (j : N →* P) : f.lift (f.isUnit_comp j) = j

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
j : N →* P
⊢ f.lift ⋯ = j

Tactic:
ext

Result:
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
j : N →* P
x✝ : N
⊢ (f.lift ⋯) x✝ = j x✝

Proof state:
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
j : N →* P
x✝ : N
⊢ (f.lift ⋯) x✝ = j x✝

Tactic:
simp_rw [lift_spec, MonoidHom.comp_apply, ← j.map_mul, sec_spec']

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma comp_assoc_of_second_is_zero_cochain {n₁ n₃ n₁₃ : ℤ}
    (z₁ : Cochain F G n₁) (z₂ : Cochain G K 0) (z₃ : Cochain K L n₃) (h₁₃ : n₁ + n₃ = n₁₃) :
    (z₁.comp z₂ (add_zero n₁)).comp z₃ h₁₃ = z₁.comp (z₂.comp z₃ (zero_add n₃)) h₁₃ :=
  comp_assoc _ _ _ _ _ (by omega)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₁ n₃ n₁₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K 0
z₃ : Cochain K L n₃
h₁₃ : n₁ + n₃ = n₁₃
⊢ n₁ + 0 + n₃ = n₁₃

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem det_eq_sum_mul_adjugate_col (A : Matrix n n α) (j : n) :
    det A = ∑ i : n, A i j * adjugate A j i

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
⊢ A.det = ∑ i : n, A i j * A.adjugate j i

Tactic:
simpa only [det_transpose, ← adjugate_transpose] using det_eq_sum_mul_adjugate_row Aᵀ j

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem prodMonoidal_rightUnitor_hom_snd (X : C₁ × C₂) :
    ((ρ_ X).hom : X ⊗ 𝟙_ _ ⟶ X).2 = (ρ_ X.2).hom

Proof state:
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (ρ_ X).hom.2 = (ρ_ X.2).hom

Tactic:
cases X

Result:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (ρ_ (fst✝, snd✝)).hom.2 = (ρ_ (fst✝, snd✝).2).hom

Proof state:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (ρ_ (fst✝, snd✝)).hom.2 = (ρ_ (fst✝, snd✝).2).hom

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem degree_of_c_ne_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) : P.toPoly.degree = 1

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ P.toPoly.degree = 1

Tactic:
rw [of_b_eq_zero ha hb, degree_linear hc]

Result:
no goals
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- `sSup` of `norm` is nonneg applied to the image of `f` on the vertical line `re z = x` -/
lemma sSupNormIm_nonneg (x : ℝ) : 0 ≤ sSupNormIm f x

Proof state:
case hs.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
x y : ℝ
z1 : ℂ
left✝ : z1 ∈ re ⁻¹' {x}
hz2 : (norm ∘ f) z1 = y
⊢ 0 ≤ y

Tactic:
simp only [← hz2, comp, norm_nonneg]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
x : ℝ
⊢ 0 ≤ sSupNormIm f x

Tactic:
apply Real.sSup_nonneg

Result:
case hs
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
x : ℝ
⊢ ∀ x_1 ∈ norm ∘ f '' (re ⁻¹' {x}), 0 ≤ x_1

Proof state:
case hs
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
x : ℝ
⊢ ∀ x_1 ∈ norm ∘ f '' (re ⁻¹' {x}), 0 ≤ x_1

Tactic:
rintro y ⟨z1, _, hz2⟩

Result:
case hs.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
x y : ℝ
z1 : ℂ
left✝ : z1 ∈ re ⁻¹' {x}
hz2 : (norm ∘ f) z1 = y
⊢ 0 ≤ y
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.ext (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s')
    (h : ∀ i, p i → ∃ i', p' i' ∧ s' i' ⊆ s i) (h' : ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i') :
    l = l'

Proof state:
case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι), p i' → ∃ i, p' i ∧ s' i ⊆ s i'

Tactic:
simpa using h

Result:
no goals

Proof state:
case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'

Tactic:
simpa using h'

Result:
no goals

Proof state:
case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ l' ≤ l

Tactic:
rw [hl'.le_basis_iff hl]

Result:
case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι), p i' → ∃ i, p' i ∧ s' i ⊆ s i'

Proof state:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ l = l'

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ l ≤ l'

case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ l' ≤ l

Proof state:
case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ l ≤ l'

Tactic:
rw [hl.le_basis_iff hl']

Result:
case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range
    {f : M → M'} {x : M} (hc : ContinuousWithinAt f s x) :
    𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x x) =
      𝓝[(extChartAt I x).target ∩
        (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)] (extChartAt I x x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
⊢ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x =
    𝓝[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)] ↑(extChartAt I x) x

Tactic:
rw [← (extChartAt I x).image_source_inter_eq', ← map_extChartAt_nhdsWithin_eq_image,
  ← map_extChartAt_nhdsWithin, nhdsWithin_inter_of_mem']

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
⊢ f ⁻¹' (extChartAt I' (f x)).source ∈ 𝓝[s] x

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
⊢ f ⁻¹' (extChartAt I' (f x)).source ∈ 𝓝[s] x

Tactic:
exact hc (extChartAt_source_mem_nhds _)

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_incl_top : (⊤ : LieSubmodule R L N).map N.incl = N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ map N.incl ⊤ = N

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem continuous_negPart [Fact (1 ≤ p)] : Continuous fun f : Lp ℝ p μ => negPart f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
⊢ Continuous fun f => posPart (-f)

Tactic:
exact continuous_posPart.comp continuous_neg

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
⊢ Continuous fun f => negPart f

Tactic:
unfold negPart

Result:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
⊢ Continuous fun f => posPart (-f)
-- Mathlib/Data/Finmap.lean
theorem dlookup_list_toFinmap (a : α) (s : List (Sigma β)) : lookup a s.toFinmap = s.dlookup a

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup a s.toFinmap = dlookup a s

Tactic:
rw [List.toFinmap, lookup_toFinmap, lookup_to_alist]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem BinaryInput.each_cast {aig1 aig2 : AIG α} (lhs rhs : Ref aig1)
    (h1 h2 : aig1.decls.size ≤ aig2.decls.size) :
    BinaryInput.mk (lhs.cast h1) (rhs.cast h2) = (BinaryInput.mk lhs rhs).cast h2

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
lhs rhs : aig1.Ref
h1 h2 : aig1.decls.size ≤ aig2.decls.size
⊢ { lhs := lhs.cast h1, rhs := rhs.cast h2 } = { lhs := lhs, rhs := rhs }.cast h2

Tactic:
simp [BinaryInput.cast]

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp, norm_cast] lemma coe_lt_coe : (a : WithTop α) < b ↔ a < b

Proof state:
α : Type u_1
a b : α
inst✝ : LT α
⊢ ↑a < ↑b ↔ a < b

Tactic:
simp [lt_def]

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
theorem skewAdjoint.I_smul_neg_I (a : skewAdjoint A) : I • (skewAdjoint.negISMul a : A) = a

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : ↥(skewAdjoint A)
⊢ I • ↑(negISMul a) = ↑a

Tactic:
simp only [smul_smul, skewAdjoint.negISMul_apply_coe, neg_smul, smul_neg, I_mul_I, one_smul,
  neg_neg]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Slope.lean
@[simp] lemma slope_neg_fun (f : k → E) : slope (-f) = -slope f

Proof state:
k : Type u_1
E : Type u_2
inst✝² : Field k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
f : k → E
⊢ slope (-f) = -slope f

Tactic:
ext x y

Result:
case h.h
k : Type u_1
E : Type u_2
inst✝² : Field k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
f : k → E
x y : k
⊢ slope (-f) x y = (-slope f) x y

Proof state:
case h.h
k : Type u_1
E : Type u_2
inst✝² : Field k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
f : k → E
x y : k
⊢ slope (-f) x y = (-slope f) x y

Tactic:
exact slope_neg f x y

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem sum_single (f : SkewMonoidAlgebra k G) : f.sum single = f

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
f : SkewMonoidAlgebra k G
⊢ f.sum single = f

Tactic:
apply toFinsupp_injective

Result:
case a
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
f : SkewMonoidAlgebra k G
⊢ (f.sum single).toFinsupp = f.toFinsupp

Proof state:
case a
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
f : SkewMonoidAlgebra k G
⊢ (f.sum single).toFinsupp = f.toFinsupp

Tactic:
simp only [toFinsupp_sum', toFinsupp_single, Finsupp.sum_single]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem pow_eq_aeval_mod_charpoly (M : Matrix n n R) (k : ℕ) :
    M ^ k = aeval M (X ^ k %ₘ M.charpoly)

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
⊢ M ^ k = (aeval M) (X ^ k %ₘ M.charpoly)

Tactic:
rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]

Result:
no goals
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem ramificationIdx_eq_factors_count [DecidableEq (Ideal S)]
    (hp0 : map f p ≠ ⊥) (hP : P.IsPrime) (hP0 : P ≠ ⊥) :
    ramificationIdx f p P = (factors (map f p)).count P

Proof state:
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : DecidableEq (Ideal S)
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
⊢ ramificationIdx f p P = Multiset.count P (factors (map f p))

Tactic:
rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp0 hP hP0,
  factors_eq_normalizedFactors]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem whiskerRight_comp_symm {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) :
    η ▷ g ▷ h = (α_ f g h).hom ≫ η ▷ (g ≫ h) ≫ (α_ f' g h).inv

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ g ▷ h = (α_ f g h).hom ≫ η ▷ (g ≫ h) ≫ (α_ f' g h).inv

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem norm_eq_zero_iff' {x : mixedSpace K} (hx : x ∈ Set.range (mixedEmbedding K)) :
    mixedEmbedding.norm x = 0 ↔ x = 0

Proof state:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
⊢ mixedEmbedding.norm ((mixedEmbedding K) a) = 0 ↔ (mixedEmbedding K) a = 0

Tactic:
rw [norm_eq_norm, Rat.cast_abs, abs_eq_zero, Rat.cast_eq_zero, Algebra.norm_eq_zero_iff,
  map_eq_zero]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ Set.range ⇑(mixedEmbedding K)
⊢ mixedEmbedding.norm x = 0 ↔ x = 0

Tactic:
obtain ⟨a, rfl⟩ := hx

Result:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
⊢ mixedEmbedding.norm ((mixedEmbedding K) a) = 0 ↔ (mixedEmbedding K) a = 0
-- Mathlib/RingTheory/Localization/Away/Basic.lean
theorem mul_invSelf : algebraMap R S x * invSelf x = 1

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ (algebraMap R S) x * invSelf x = 1

Tactic:
convert IsLocalization.mk'_mul_mk'_eq_one (M := Submonoid.powers x) (S := S) _ 1

Result:
case h.e'_2.h.e'_5
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ (algebraMap R S) x = mk' S (↑⟨x, ⋯⟩) 1

Proof state:
case h.e'_2.h.e'_5
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ mk' S (↑⟨x, ⋯⟩) 1 = (algebraMap R S) x

Tactic:
apply IsLocalization.mk'_one

Result:
no goals

Proof state:
case h.e'_2.h.e'_5
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ (algebraMap R S) x = mk' S (↑⟨x, ⋯⟩) 1

Tactic:
symm

Result:
case h.e'_2.h.e'_5
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ mk' S (↑⟨x, ⋯⟩) 1 = (algebraMap R S) x
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem toAddMonoidHom_injective {f g : A →ₑ+[φ] B} (h : (f : A →+ B) = (g : A →+ B)) : f = g

Proof state:
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : DistribMulAction M A
B : Type u_5
inst✝¹ : AddMonoid B
inst✝ : DistribMulAction N B
f g : A →ₑ+[φ] B
h : ↑f = ↑g
⊢ f = g

Tactic:
ext a

Result:
case a
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : DistribMulAction M A
B : Type u_5
inst✝¹ : AddMonoid B
inst✝ : DistribMulAction N B
f g : A →ₑ+[φ] B
h : ↑f = ↑g
a : A
⊢ f a = g a

Proof state:
case a
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : DistribMulAction M A
B : Type u_5
inst✝¹ : AddMonoid B
inst✝ : DistribMulAction N B
f g : A →ₑ+[φ] B
h : ↑f = ↑g
a : A
⊢ f a = g a

Tactic:
exact DFunLike.congr_fun h a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findFinIdx?_toArray (p : α → Bool) (v : Vector α n) :
    v.toArray.findFinIdx? p = (v.findFinIdx? p).map (Fin.cast v.size_toArray.symm)

Proof state:
case mk
α : Type u_1
p : α → Bool
v : Array α
⊢ Array.findFinIdx? p { toArray := v, size_toArray := ⋯ }.toArray =
    Option.map (Fin.cast ⋯) (findFinIdx? p { toArray := v, size_toArray := ⋯ })

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Bool
v : Vector α n
⊢ Array.findFinIdx? p v.toArray = Option.map (Fin.cast ⋯) (findFinIdx? p v)

Tactic:
rcases v with ⟨v, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
v : Array α
⊢ Array.findFinIdx? p { toArray := v, size_toArray := ⋯ }.toArray =
    Option.map (Fin.cast ⋯) (findFinIdx? p { toArray := v, size_toArray := ⋯ })
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem image_Iio (e : α ≃o β) (a : α) : e '' Iio a = Iio (e a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ ⇑e '' Iio a = Iio (e a)

Tactic:
rw [e.image_eq_preimage, e.symm.preimage_Iio, e.symm_symm]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem lift_spec_mul (z w v) : f.lift hg z * w = v ↔ g (f.sec z).1 * w = g (f.sec z).2 * v

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
w v : P
⊢ (f.lift hg) z * w = v ↔ g (f.sec z).1 * w = g ↑(f.sec z).2 * v

Tactic:
erw [mul_comm, ← mul_assoc, mul_inv_left hg, mul_comm]

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma rnDeriv_toReal_pos [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (h : κ a ≪ η a) :
    ∀ᵐ x ∂(κ a), 0 < (rnDeriv κ η a x).toReal

Proof state:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : κ a ≪ η a
x : γ
h0 : 0 < κ.rnDeriv η a x
htop : κ.rnDeriv η a x ≠ ⊤
⊢ 0 < (κ.rnDeriv η a x).toReal

Tactic:
simp_all only [pos_iff_ne_zero, ne_eq, ENNReal.toReal_pos, not_false_eq_true, and_self]

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : κ a ≪ η a
⊢ ∀ᵐ (x : γ) ∂κ a, 0 < (κ.rnDeriv η a x).toReal

Tactic:
filter_upwards [rnDeriv_pos h, h.ae_le (rnDeriv_ne_top κ _)] with x h0 htop

Result:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : κ a ≪ η a
x : γ
h0 : 0 < κ.rnDeriv η a x
htop : κ.rnDeriv η a x ≠ ⊤
⊢ 0 < (κ.rnDeriv η a x).toReal
-- Mathlib/Computability/Primrec.lean
theorem comp₂ (f : ℕ → ℕ → ℕ) (hf : @Primrec' 2 fun v => f v.head v.tail.head) {n g h}
    (hg : @Primrec' n g) (hh : @Primrec' n h) : Primrec' fun v => f (g v) (h v)

Proof state:
f : ℕ → ℕ → ℕ
hf : Primrec' fun v => f v.head v.tail.head
n : ℕ
g h : List.Vector ℕ n → ℕ
hg : Primrec' g
hh : Primrec' h
⊢ Primrec' fun v => f (g v) (h v)

Tactic:
simpa using hf.comp' (hg.cons <| hh.cons Primrec'.nil)

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_sub_one (a : α) : ⌈a - 1⌉ = ⌈a⌉ - 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ⌈a - 1⌉ = ⌈a⌉ - 1

Tactic:
rw [eq_sub_iff_add_eq, ← ceil_add_one, sub_add_cancel]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Ico {a b : α} : (Nat.cast : ℕ → α) ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉₊ ⌈b⌉₊

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ico a b ↔ x✝ ∈ Ico ⌈a⌉₊ ⌈b⌉₊

Tactic:
simp [ceil_le, lt_ceil]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
⊢ Nat.cast ⁻¹' Ico a b = Ico ⌈a⌉₊ ⌈b⌉₊

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ico a b ↔ x✝ ∈ Ico ⌈a⌉₊ ⌈b⌉₊