harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem linearEquiv_det_reflection : (reflection K).det = (-1) ^ finrank 𝕜 Kᗮ

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
⊢ LinearMap.det ↑(reflection K).toLinearEquiv = ↑(-1) ^ finrank 𝕜 ↥Kᗮ

Tactic:
exact det_reflection K

Result:
no goals

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
⊢ ↑(LinearEquiv.det (reflection K).toLinearEquiv) = ↑((-1) ^ finrank 𝕜 ↥Kᗮ)

Tactic:
rw [LinearEquiv.coe_det, Units.val_pow_eq_pow_val]

Result:
case a
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
⊢ LinearMap.det ↑(reflection K).toLinearEquiv = ↑(-1) ^ finrank 𝕜 ↥Kᗮ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
⊢ LinearEquiv.det (reflection K).toLinearEquiv = (-1) ^ finrank 𝕜 ↥Kᗮ

Tactic:
ext

Result:
case a
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
⊢ ↑(LinearEquiv.det (reflection K).toLinearEquiv) = ↑((-1) ^ finrank 𝕜 ↥Kᗮ)
-- Mathlib/MeasureTheory/Measure/AEDisjoint.lean
theorem symm (h : AEDisjoint μ s t) : AEDisjoint μ t s

Proof state:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ AEDisjoint μ t s

Tactic:
rwa [AEDisjoint, inter_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftUnshift_add {n' a : ℤ} (γ₁ γ₂ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') :
    (γ₁ + γ₂).leftUnshift n hn = γ₁.leftUnshift n hn + γ₂.leftUnshift n hn

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ₁ γ₂ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = γ₁.leftUnshift n hn + γ₂.leftUnshift n hn

Tactic:
apply _root_.map_add

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ₁ γ₂ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
⊢ (γ₁ + γ₂).leftUnshift n hn = γ₁.leftUnshift n hn + γ₂.leftUnshift n hn

Tactic:
change (leftShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = _

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ₁ γ₂ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = γ₁.leftUnshift n hn + γ₂.leftUnshift n hn
-- Mathlib/Order/SuccPred/Limit.lean
theorem not_isSuccPrelimit_iff_exists_covBy (a : α) : ¬IsSuccPrelimit a ↔ ∃ b, b ⋖ a

Proof state:
α : Type u_1
inst✝ : LT α
a : α
⊢ ¬IsSuccPrelimit a ↔ ∃ b, b ⋖ a

Tactic:
simp [IsSuccPrelimit]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem coe_preimage_self (s : Set α) : ((↑) : s → α) ⁻¹' s = univ

Proof state:
α : Type u_1
s : Set α
⊢ val ⁻¹' s = univ

Tactic:
rw [← preimage_range, range_coe]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
lemma comp_map {a : M} (f : ShiftedHom X Y a) (F : C ⥤ D) [F.CommShift M]
    (G : D ⥤ E) [G.CommShift M] : f.map (F ⋙ G) = (f.map F).map G

Proof state:
C : Type u_1
inst✝⁸ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁷ : Category.{u_6, u_2} D
E : Type u_3
inst✝⁶ : Category.{u_7, u_3} E
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
inst✝² : HasShift E M
X Y : C
a : M
f : ShiftedHom X Y a
F : C ⥤ D
inst✝¹ : F.CommShift M
G : D ⥤ E
inst✝ : G.CommShift M
⊢ f.map (F ⋙ G) = (f.map F).map G

Tactic:
simp [map, Functor.commShiftIso_comp_hom_app]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma j_eq_zero_of_char_two (h : W.a₁ = 0) : W.j = 0

Proof state:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 2
h : W.a₁ = 0
⊢ W.j = 0

Tactic:
rw [j_eq_zero_iff_of_char_two', h, zero_pow (Nat.succ_ne_zero _)]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem sub_rat_iff : LiouvilleWith p (x - r) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
r : ℚ
⊢ LiouvilleWith p (x - ↑r) ↔ LiouvilleWith p x

Tactic:
rw [sub_eq_add_neg, ← Rat.cast_neg, add_rat_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
theorem Quot.desc_colimitCocone (F : J ⥤ Type u) [Small.{u} (Quot F)] :
    Quot.desc (colimitCocone F) = equivShrink.{u} (Quot F)

Proof state:
case h.mk.mk
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : Small.{u, max u v} (Quot F)
x✝ : Quot F
j : J
x : F.obj j
⊢ desc (colimitCocone F) (Quot.mk (Rel F) ⟨j, x⟩) = (equivShrink (Quot F)) (Quot.mk (Rel F) ⟨j, x⟩)

Tactic:
rfl

Result:
no goals

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : Small.{u, max u v} (Quot F)
⊢ desc (colimitCocone F) = ⇑(equivShrink (Quot F))

Tactic:
ext ⟨j, x⟩

Result:
case h.mk.mk
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : Small.{u, max u v} (Quot F)
x✝ : Quot F
j : J
x : F.obj j
⊢ desc (colimitCocone F) (Quot.mk (Rel F) ⟨j, x⟩) = (equivShrink (Quot F)) (Quot.mk (Rel F) ⟨j, x⟩)
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem vanishingIdeal_singleton (x : PrimeSpectrum R) :
    vanishingIdeal ({x} : Set (PrimeSpectrum R)) = x.asIdeal

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ vanishingIdeal {x} = x.asIdeal

Tactic:
simp [vanishingIdeal]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem beqEqOfEqEq {a b c d : Nat} (p : (a = b) = (c = d)) : (a == b) = (c == d)

Proof state:
a b c d : Nat
p : (a = b) = (c = d)
⊢ (a == b) = (c == d)

Tactic:
simp only [Bool.beq_eq_decide_eq, p]

Result:
no goals
-- Mathlib/Data/List/Destutter.lean
theorem destutter'_sublist (a) : l.destutter' R a <+ a :: l

Proof state:
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : R a b
⊢ a :: destutter' R b l <+ a :: b :: l

Tactic:
exact Sublist.cons₂ a (hl b)

Result:
no goals

Proof state:
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
⊢ (if R a b then a :: destutter' R b l else destutter' R a l) <+ a :: b :: l

Tactic:
split_ifs

Result:
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : R a b
⊢ a :: destutter' R b l <+ a :: b :: l

case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : ¬R a b
⊢ destutter' R a l <+ a :: b :: l

Proof state:
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ destutter' R a [] <+ [a]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ destutter' R a l <+ a :: l

Tactic:
induction' l with b l hl generalizing a

Result:
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ destutter' R a [] <+ [a]

case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
⊢ destutter' R a (b :: l) <+ a :: b :: l

Proof state:
case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : ¬R a b
⊢ destutter' R a l <+ a :: b :: l

Tactic:
exact (hl a).trans ((l.sublist_cons_self b).cons_cons a)

Result:
no goals

Proof state:
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
⊢ destutter' R a (b :: l) <+ a :: b :: l

Tactic:
rw [destutter']

Result:
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
⊢ (if R a b then a :: destutter' R b l else destutter' R a l) <+ a :: b :: l
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem HasFPowerSeriesWithinAt.sub
    (hf : HasFPowerSeriesWithinAt f pf s x) (hg : HasFPowerSeriesWithinAt g pg s x) :
    HasFPowerSeriesWithinAt (f - g) (pf - pg) s x

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f pf s x
hg : HasFPowerSeriesWithinAt g pg s x
⊢ HasFPowerSeriesWithinAt (f - g) (pf - pg) s x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/Analysis/Oscillation.lean
theorem eq_zero_iff_continuousWithinAt [TopologicalSpace E] (f : E → F) {D : Set E}
    {x : E} (xD : x ∈ D) : oscillationWithin f D x = 0 ↔ ContinuousWithinAt f D x

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
ε0 : ∃ i, ∃ (_ : i ∈ Filter.map f (𝓝[D] x)), diam i < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε

Tactic:
obtain ⟨S, hS, Sε⟩ := ε0

Result:
case intro.intro
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
S : Set F
hS : S ∈ Filter.map f (𝓝[D] x)
Sε : diam S < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε

Tactic:
simp_rw [← hf, oscillationWithin, iInf_lt_iff] at ε0

Result:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
ε0 : ∃ i, ∃ (_ : i ∈ Filter.map f (𝓝[D] x)), diam i < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε

Proof state:
case intro.intro
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
S : Set F
hS : S ∈ Filter.map f (𝓝[D] x)
Sε : diam S < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε

Tactic:
refine Filter.mem_of_superset hS (fun y hy ↦ lt_of_le_of_lt ?_ Sε)

Result:
case intro.intro
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
S : Set F
hS : S ∈ Filter.map f (𝓝[D] x)
Sε : diam S < ε
y : E
hy : y ∈ f ⁻¹' S
⊢ edist (f y) (f x) ≤ diam S

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
⊢ oscillationWithin f D x = 0 ↔ ContinuousWithinAt f D x

Tactic:
refine ⟨fun hf ↦ EMetric.tendsto_nhds.mpr (fun ε ε0 ↦ ?_), fun hf ↦ hf.oscillationWithin_eq_zero⟩

Result:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε

Proof state:
case intro.intro
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
xD : x ∈ D
hf : oscillationWithin f D x = 0
ε : ℝ≥0∞
S : Set F
hS : S ∈ Filter.map f (𝓝[D] x)
Sε : diam S < ε
y : E
hy : y ∈ f ⁻¹' S
⊢ edist (f y) (f x) ≤ diam S

Tactic:
exact edist_le_diam_of_mem (mem_preimage.1 hy) <| mem_preimage.1 (mem_of_mem_nhdsWithin xD hS)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_ne_nil_of_left_ne_nil {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ []

Proof state:
α : Type u_1
s : List α
h : s ≠ []
t : List α
⊢ s ++ t ≠ []

Tactic:
simp_all

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem mul_nat_iff (hn : n ≠ 0) : LiouvilleWith p (x * n) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
n : ℕ
hn : n ≠ 0
⊢ LiouvilleWith p (x * ↑n) ↔ LiouvilleWith p x

Tactic:
rw [← Rat.cast_natCast, mul_rat_iff (Nat.cast_ne_zero.2 hn)]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Ici : (some : α → WithBot α) '' Ici a = Ici (a : WithBot α)

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Ici a = Ici ↑a

Tactic:
rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Ici_subset_Ioi.2 <| bot_lt_coe a)]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem find?_eq [BEq α] (a : α) (l : AssocList α β) :
    find? a l = (l.toList.find? (·.1 == a)).map (·.2)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : BEq α
a : α
l : AssocList α β
⊢ find? a l = Option.map (fun x => x.snd) (List.find? (fun x => x.fst == a) l.toList)

Tactic:
simp [find?_eq_findEntry?]

Result:
no goals
-- Mathlib/LinearAlgebra/Semisimple.lean
lemma IsSemisimple.restrict {p : Submodule R M} (hp : p ∈ f.invtSubmodule) (hf : f.IsSemisimple) :
    IsSemisimple (f.restrict hp)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : IsSemisimpleModule R[X] (AEval' f)
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ IsSemisimpleModule R[X] (AEval' (LinearMap.restrict f hp))

Tactic:
exact e.complementedLattice_iff.mpr inferInstance

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : IsSemisimpleModule R[X] (AEval' f)
⊢ IsSemisimpleModule R[X] (AEval' (LinearMap.restrict f hp))

Tactic:
let e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o
    Iic (AEval.mapSubmodule R M f ⟨p, hp⟩) :=
  (Submodule.orderIsoMapComap <| AEval.restrict_equiv_mapSubmodule f p hp).trans <|
    Submodule.mapIic _

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : IsSemisimpleModule R[X] (AEval' f)
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ IsSemisimpleModule R[X] (AEval' (LinearMap.restrict f hp))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsSemisimple
⊢ IsSemisimple (LinearMap.restrict f hp)

Tactic:
rw [IsSemisimple] at hf ⊢

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : IsSemisimpleModule R[X] (AEval' f)
⊢ IsSemisimpleModule R[X] (AEval' (LinearMap.restrict f hp))
-- Mathlib/RingTheory/FiniteType.lean
theorem freeAlgebra (ι : Type*) [Finite ι] : FiniteType R (FreeAlgebra R ι)

Proof state:
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
⊢ FiniteType R (FreeAlgebra R ι)

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ FiniteType R (FreeAlgebra R ι)

Proof state:
case intro
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ FiniteType R (FreeAlgebra R ι)

Tactic:
classical
exact
  ⟨⟨Finset.univ.image (FreeAlgebra.ι R), by
      rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
      exact FreeAlgebra.adjoin_range_ι R ι⟩⟩

Result:
no goals

Proof state:
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ adjoin R (Set.range (FreeAlgebra.ι R)) = ⊤

Tactic:
exact FreeAlgebra.adjoin_range_ι R ι

Result:
no goals

Proof state:
case intro
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ FiniteType R (FreeAlgebra R ι)

Tactic:
exact
  ⟨⟨Finset.univ.image (FreeAlgebra.ι R), by
      rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
      exact FreeAlgebra.adjoin_range_ι R ι⟩⟩

Result:
no goals

Proof state:
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ adjoin R ↑(Finset.image (FreeAlgebra.ι R) Finset.univ) = ⊤

Tactic:
rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]

Result:
R : Type uR
inst✝¹ : CommSemiring R
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ adjoin R (Set.range (FreeAlgebra.ι R)) = ⊤
-- Mathlib/Algebra/Homology/Embedding/IsSupported.lean
lemma IsStrictlySupportedOutside.isSupportedOutside (h : K.IsStrictlySupportedOutside e) :
    K.IsSupportedOutside e where
  exactAt i

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h : K.IsStrictlySupportedOutside e
i : ι
⊢ K.ExactAt (e.f i)

Tactic:
rw [exactAt_iff]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h : K.IsStrictlySupportedOutside e
i : ι
⊢ (K.sc (e.f i)).Exact

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h : K.IsStrictlySupportedOutside e
i : ι
⊢ (K.sc (e.f i)).Exact

Tactic:
exact ShortComplex.exact_of_isZero_X₂ _ (h.isZero i)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a

Proof state:
α : Type u_1
β : Type u_2
n✝ : Nat
l : Vector α n✝
f g : α → β
⊢ map f l = map g l ↔ ∀ (a : α), a ∈ l → f a = g a

Tactic:
cases l <;> simp_all

Result:
no goals
-- Mathlib/Data/Nat/Cast/Basic.lean
theorem NeZero.nat_of_neZero {R S} [Semiring R] [Semiring S]
    {F} [FunLike F R S] [RingHomClass F R S] (f : F)
    {n : ℕ} [hn : NeZero (n : S)] : NeZero (n : R) :=
  .of_map (f := f) (neZero

Proof state:
R : Type u_6
S : Type u_7
inst✝³ : Semiring R
inst✝² : Semiring S
F : Type u_8
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
n : ℕ
hn : NeZero ↑n
⊢ NeZero (f ↑n)

Tactic:
simp only [map_natCast, hn]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_neg_one : U R (-1) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ U R (-1) = 0

Tactic:
simpa using U_sub_one R 0

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_add_cancel (x y : BitVec w) : x - y + y = x

Proof state:
w : Nat
x y : BitVec w
⊢ x - y + y = x

Tactic:
rw [sub_toAdd, BitVec.add_assoc, BitVec.add_comm _ y,
    ← BitVec.add_assoc, ← sub_toAdd, add_sub_cancel]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
theorem toSphere_apply_univ' : μ.toSphere univ = dim E * μ (ball 0 1 \ {0})

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ μ.toSphere univ = ↑(dim E) * μ (ball 0 1 \ {0})

Tactic:
rw [μ.toSphere_apply' .univ, image_univ, Subtype.range_coe, Ioo_smul_sphere_zero] <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Subspace.lean
theorem sup_span {S : Set (ℙ K V)} {W : Subspace K V} : W ⊔ span S = span (W ∪ S)

Proof state:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ W ⊔ span S = span (↑W ∪ S)

Tactic:
rw [span_union, span_coe]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.mul_toMatrix₂_mul (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix n' n R)
    (N : Matrix m m' R) :
    M * LinearMap.toMatrix₂ b₁ b₂ B * N =
      LinearMap.toMatrix₂ b₁' b₂' (B.compl₁₂ (toLin b₁' b₁ Mᵀ) (toLin b₂' b₂ N))

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix n' n R
N : Matrix m m' R
⊢ M * (toMatrix₂ b₁ b₂) B * N = (toMatrix₂ b₁' b₂') (B.compl₁₂ ((toLin b₁' b₁) Mᵀ) ((toLin b₂' b₂) N))

Tactic:
simp_rw [LinearMap.toMatrix₂_compl₁₂ b₁ b₂, toMatrix_toLin, transpose_transpose]

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem sub_eq_add : a - b = a + b

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a - b = a + b

Tactic:
rw [sub_eq_add_neg, add_right_inj, neg_eq]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem disjoint_pi : Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i)

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i)

Tactic:
simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff']

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma isIso_iff_isIso_coyoneda_map {X Y : C} (f : X ⟶ Y) :
    IsIso f ↔ ∀ c : C, IsIso ((coyoneda.map f.op).app c)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (∀ (T : C), Function.Bijective fun x => f ≫ x) ↔ ∀ (c : C), IsIso ((coyoneda.map f.op).app c)

Tactic:
exact forall_congr' fun _ ↦ (isIso_iff_bijective _).symm

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (c : C), IsIso ((coyoneda.map f.op).app c)

Tactic:
rw [isIso_iff_coyoneda_map_bijective]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (∀ (T : C), Function.Bijective fun x => f ≫ x) ↔ ∀ (c : C), IsIso ((coyoneda.map f.op).app c)
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
theorem eval_one_cyclotomic_prime_pow {R : Type*} [CommRing R] {p : ℕ} (k : ℕ)
    [hn : Fact p.Prime] : eval 1 (cyclotomic (p ^ (k + 1)) R) = p

Proof state:
R : Type u_1
inst✝ : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ eval 1 (cyclotomic (p ^ (k + 1)) R) = ↑p

Tactic:
simp only [cyclotomic_prime_pow_eq_geom_sum hn.out, eval_X, one_pow, Finset.sum_const, eval_pow,
  eval_finset_sum, Finset.card_range, smul_one_eq_cast]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem exists_lintegral_le (hint : ∫⁻ a, f a ∂μ ≠ ∞) : ∃ x, ∫⁻ a, f a ∂μ ≤ f x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst✝ : IsProbabilityMeasure μ
hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤
⊢ ∃ x, ∫⁻ (a : α), f a ∂μ ≤ f x

Tactic:
simpa only [laverage_eq_lintegral] using
  exists_laverage_le (IsProbabilityMeasure.ne_zero μ) hint

Result:
no goals