harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Quiver/SingleObj.lean
theorem listToPath_pathToList {x : SingleObj α} (p : Path (star α) x) :
    listToPath (pathToList p) = p.cast rfl ext

Proof state:
case cons
α : Type u_1
x b✝ c✝ : SingleObj α
a✝¹ : Path (star α) b✝
a✝ : b✝ ⟶ c✝
ih : listToPath (pathToList a✝¹) = Path.cast ⋯ ⋯ a✝¹
⊢ listToPath (pathToList (a✝¹.cons a✝)) = Path.cast ⋯ ⋯ (a✝¹.cons a✝)

Tactic:
dsimp [pathToList] at *

Result:
case cons
α : Type u_1
x b✝ c✝ : SingleObj α
a✝¹ : Path (star α) b✝
a✝ : b✝ ⟶ c✝
ih : listToPath (pathToList a✝¹) = a✝¹
⊢ (listToPath (pathToList a✝¹)).cons a✝ = a✝¹.cons a✝

Proof state:
α : Type u_1
x : SingleObj α
p : Path (star α) x
⊢ listToPath (pathToList p) = Path.cast ⋯ ⋯ p

Tactic:
induction p with
| nil => rfl
| cons _ _ ih => dsimp [pathToList] at *; rw [ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
x : SingleObj α
⊢ listToPath (pathToList Path.nil) = Path.cast ⋯ ⋯ Path.nil

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
x b✝ c✝ : SingleObj α
a✝¹ : Path (star α) b✝
a✝ : b✝ ⟶ c✝
ih : listToPath (pathToList a✝¹) = a✝¹
⊢ (listToPath (pathToList a✝¹)).cons a✝ = a✝¹.cons a✝

Tactic:
rw [ih]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Commute.lean
lemma inverse_pow (r : M₀) : ∀ n : ℕ, Ring.inverse r ^ n = Ring.inverse (r ^ n)
  | 0 => by rw [pow_zero, pow_zero, Ring.inverse_one]
  | n + 1 => by
    rw [pow_succ', pow_succ, Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
      Ring.inverse_pow r n]

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
n : ℕ
⊢ inverse r ^ (n + 1) = inverse (r ^ (n + 1))

Tactic:
rw [pow_succ', pow_succ, Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
  Ring.inverse_pow r n]

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
⊢ inverse r ^ 0 = inverse (r ^ 0)

Tactic:
rw [pow_zero, pow_zero, Ring.inverse_one]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_two_mul : sin (2 * x) = 2 * sin x * cos x

Proof state:
x : ℂ
⊢ sin (2 * x) = 2 * sin x * cos x

Tactic:
rw [two_mul, sin_add, two_mul, add_mul, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem relabel_nil {r : α → β} : relabel r [] = []

Proof state:
α : Type u_1
β : Type u_2
r : α → β
⊢ relabel r [] = []

Tactic:
simp [relabel]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_im_symm (x y : F) : im ⟪x, y⟫ = -im ⟪y, x⟫

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ im ⟪x, y⟫_𝕜 = -im ⟪y, x⟫_𝕜

Tactic:
rw [← inner_conj_symm, conj_im]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem xor_cast {x y : BitVec w} (h : w = w') : x.cast h ^^^ y.cast h = (x ^^^ y).cast h

Proof state:
w w' : Nat
x y : BitVec w
h : w = w'
⊢ BitVec.cast h x ^^^ BitVec.cast h y = BitVec.cast h (x ^^^ y)

Tactic:
ext

Result:
case pred
w w' : Nat
x y : BitVec w
h : w = w'
i✝ : Nat
a✝ : i✝ < w'
⊢ (BitVec.cast h x ^^^ BitVec.cast h y).getLsbD i✝ = (BitVec.cast h (x ^^^ y)).getLsbD i✝

Proof state:
case pred
w w' : Nat
x y : BitVec w
h : w = w'
i✝ : Nat
a✝ : i✝ < w'
⊢ (BitVec.cast h x ^^^ BitVec.cast h y).getLsbD i✝ = (BitVec.cast h (x ^^^ y)).getLsbD i✝

Tactic:
simp_all [lt_of_getLsbD]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get?_modifyNth_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) :
    (modify f m l).get? n = l.get? n

Proof state:
α : Type u_1
f : α → α
m n : Nat
l : List α
h : m ≠ n
⊢ (modify f m l).get? n = l.get? n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/Identities.lean
theorem T_zpow_width_invariant (N : ℕ) (k n : ℤ) (f : SlashInvariantForm (Gamma N) k) (z : ℍ) :
    f (((ModularGroup.T ^ (N * n))) • z) = f z

Proof state:
N : ℕ
k n : ℤ
f : SlashInvariantForm Γ(N) k
z : ℍ
⊢ f (ModularGroup.T ^ (↑N * n) • z) = f z

Tactic:
rw [modular_T_zpow_smul z (N * n)]

Result:
N : ℕ
k n : ℤ
f : SlashInvariantForm Γ(N) k
z : ℍ
⊢ f (↑(↑N * n) +ᵥ z) = f z

Proof state:
N : ℕ
k n : ℤ
f : SlashInvariantForm Γ(N) k
z : ℍ
⊢ f (↑(↑N * n) +ᵥ z) = f z

Tactic:
simpa only [Int.cast_mul, Int.cast_natCast] using vAdd_width_periodic N k n f z

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
    a ∈ m.insert k v ↔ k == a ∨ a ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β k
⊢ a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m

Tactic:
simp [mem_iff_contains, contains_insert]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_bne_self : ∀ (x : Bool), ((!x) != x) = true

Proof state:
⊢ ∀ (x : Bool), ((!x) != x) = true

Tactic:
decide

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_zero' {ι : Type*} [Finite ι] [Nonempty ι] (b : Basis ι A M) :
    LinearMap.det (0 : M →ₗ[A] M) = 0

Proof state:
case intro
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι : Type u_7
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
val✝ : Fintype ι
⊢ LinearMap.det 0 = 0

Tactic:
rwa [← det_toMatrix b, LinearEquiv.map_zero, det_zero]

Result:
no goals

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι : Type u_7
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
⊢ LinearMap.det 0 = 0

Tactic:
cases nonempty_fintype ι

Result:
case intro
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι : Type u_7
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
val✝ : Fintype ι
⊢ LinearMap.det 0 = 0

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι : Type u_7
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
⊢ LinearMap.det 0 = 0

Tactic:
haveI := Classical.decEq ι

Result:
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι : Type u_7
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
⊢ LinearMap.det 0 = 0
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem sin_angle_mul_dist_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) :
    Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
  add_comm, sin_angle_add_mul_norm_of_inner_eq_zero h]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem inf_sup_symmDiff : a ⊓ b ⊔ a ∆ b = a ⊔ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊓ b ⊔ a ∆ b = a ⊔ b

Tactic:
rw [sup_comm, symmDiff_sup_inf]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem apply_mem_span_image_of_mem_span [RingHomSurjective σ₁₂] (f : F) {x : M}
    {s : Set M} (h : x ∈ Submodule.span R s) : f x ∈ Submodule.span R₂ (f '' s)

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
F : Type u_8
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
x : M
s : Set M
h : x ∈ span R s
⊢ f x ∈ span R₂ (⇑f '' s)

Tactic:
rw [Submodule.span_image]

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
F : Type u_8
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
x : M
s : Set M
h : x ∈ span R s
⊢ f x ∈ map f (span R s)

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
F : Type u_8
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
x : M
s : Set M
h : x ∈ span R s
⊢ f x ∈ map f (span R s)

Tactic:
exact Submodule.mem_map_of_mem h

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem isPell_norm : ∀ {b : ℤ√d}, IsPell b ↔ b * star b = 1
  | ⟨x, y⟩ => by simp [Zsqrtd.ext_iff, IsPell, mul_comm]; ring_nf

Proof state:
d x y : ℤ
⊢ IsPell { re := x, im := y } ↔ { re := x, im := y } * star { re := x, im := y } = 1

Tactic:
simp [Zsqrtd.ext_iff, IsPell, mul_comm]

Result:
d x y : ℤ
⊢ x * x - y * (d * y) = 1 ↔ x * x + -(y * (d * y)) = 1

Proof state:
d x y : ℤ
⊢ x * x - y * (d * y) = 1 ↔ x * x + -(y * (d * y)) = 1

Tactic:
ring_nf

Result:
no goals
-- Mathlib/CategoryTheory/HomCongr.lean
theorem map_homCongr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y) :
    F.map (Iso.homCongr α β f) = Iso.homCongr (F.mapIso α) (F.mapIso β) (F.map f)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ F.map ((α.homCongr β) f) = ((F.mapIso α).homCongr (F.mapIso β)) (F.map f)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/AbstractCompletion.lean
theorem map_unique {f : α → β} {g : hatα → hatβ} (hg : UniformContinuous g)
    (h : ∀ a, ι' (f a) = g (ι a)) : map f = g :=
  pkg.funext (pkg.continuous_map _ _) hg.continuous <| by
    intro a
    change pkg.extend (ι' ∘ f) _ = _
    simp_rw [Function.comp_def, h, ← comp_apply (f := g)]
    rw [pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)]

Proof state:
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.map pkg' f (pkg.coe a) = g (pkg.coe a)

Tactic:
change pkg.extend (ι' ∘ f) _ = _

Result:
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (pkg'.coe ∘ f) (pkg.coe a) = g (pkg.coe a)

Proof state:
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
⊢ ∀ (a : α), pkg.map pkg' f (pkg.coe a) = g (pkg.coe a)

Tactic:
intro a

Result:
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.map pkg' f (pkg.coe a) = g (pkg.coe a)

Proof state:
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (fun x => (g ∘ pkg.coe) x) (pkg.coe a) = (g ∘ pkg.coe) a

Tactic:
rw [pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (pkg'.coe ∘ f) (pkg.coe a) = g (pkg.coe a)

Tactic:
simp_rw [Function.comp_def, h, ← comp_apply (f := g)]

Result:
α : Type u_1
inst✝¹ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝ : UniformSpace β
pkg' : AbstractCompletion β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (fun x => (g ∘ pkg.coe) x) (pkg.coe a) = (g ∘ pkg.coe) a
-- Mathlib/Topology/Basic.lean
theorem frontier_eq_closure_inter_closure : frontier s = closure s ∩ closure sᶜ

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ frontier s = closure s ∩ closure sᶜ

Tactic:
rw [closure_compl, frontier, diff_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDense.lean
theorem edist_approxOn_mono {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s)
    [SeparableSpace s] (x : β) {m n : ℕ} (h : m ≤ n) :
    edist (approxOn f hf s y₀ h₀ n x) (f x) ≤ edist (approxOn f hf s y₀ h₀ m x) (f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
m n : ℕ
h : m ≤ n
⊢ edist ((approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist ((approxOn f hf s y₀ h₀ m) x) (f x)

Tactic:
dsimp only [approxOn, coe_comp, Function.comp_def]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
m n : ℕ
h : m ≤ n
⊢ edist ((nearestPt (fun k => Nat.rec y₀ (fun n n_ih => ↑(denseSeq (↑s) n)) k) n) (f x)) (f x) ≤
    edist ((nearestPt (fun k => Nat.rec y₀ (fun n n_ih => ↑(denseSeq (↑s) n)) k) m) (f x)) (f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
m n : ℕ
h : m ≤ n
⊢ edist ((nearestPt (fun k => Nat.rec y₀ (fun n n_ih => ↑(denseSeq (↑s) n)) k) n) (f x)) (f x) ≤
    edist ((nearestPt (fun k => Nat.rec y₀ (fun n n_ih => ↑(denseSeq (↑s) n)) k) m) (f x)) (f x)

Tactic:
exact edist_nearestPt_le _ _ ((nearestPtInd_le _ _ _).trans h)

Result:
no goals
-- Mathlib/Algebra/Tropical/Basic.lean
theorem add_eq_left ⦃x y : Tropical R⦄ (h : x ≤ y) : x + y = x :=
  untrop_injective (by simpa using h)

Proof state:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : x ≤ y
⊢ untrop (x + y) = untrop x

Tactic:
simpa using h

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean
theorem preregular_isSheaf_iff (e : C ≌ D) (F : Cᵒᵖ ⥤ A) : haveI := e.preregular
    IsSheaf (regularTopology C) F ↔ IsSheaf (regularTopology D) (e.inverse.op ⋙ F)

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F

Tactic:
exact isoWhiskerRight e.op.unitIso F

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (regularTopology C) F

Tactic:
rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (regularTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)

C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
⊢ IsSheaf (regularTopology C) F ↔ IsSheaf (regularTopology D) (e.inverse.op ⋙ F)

Tactic:
refine ⟨fun hF ↦ ((e.sheafCongrPreregular A).functor.obj ⟨F, hF⟩).cond, fun hF ↦ ?_⟩

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (regularTopology C) F

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{u_6, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (regularTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)

Tactic:
exact (e.sheafCongrPreregular A).inverse.obj ⟨e.inverse.op ⋙ F, hF⟩ |>.cond

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem Raw₀.buckets_empty {c} {i : Nat} {h} :
    (empty c : Raw₀ α β).1.buckets[i]'h = AssocList.nil

Proof state:
α : Type u
β : α → Type v
c i : Nat
h : i < (empty c).val.buckets.size
⊢ (empty c).val.buckets[i] = AssocList.nil

Tactic:
simp [empty]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Reflective.lean
theorem unitCompPartialBijective_symm_apply [Reflective i] (A : C) {B : C} (hB : i.essImage B)
    (f) : (unitCompPartialBijective A hB).symm f = (reflectorAdjunction i).unit.app A ≫ f

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
A B : C
hB : i.essImage B
f : i.obj ((reflector i).obj A) ⟶ B
⊢ (unitCompPartialBijective A hB).symm f = (reflectorAdjunction i).unit.app A ≫ f

Tactic:
simp [unitCompPartialBijective, unitCompPartialBijectiveAux_symm_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then
the push-forward of finite measures `f* : FiniteMeasure X → FiniteMeasure Y` is continuous
(in the topologies of weak convergence of measures). -/
lemma continuous_map {f : Ω → Ω'} (f_cont : Continuous f) :
    Continuous (fun ν ↦ FiniteMeasure.map ν f)

Proof state:
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous f
⊢ Continuous fun ν => ν.map f

Tactic:
rw [continuous_iff_continuousAt]

Result:
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous f
⊢ ∀ (x : FiniteMeasure Ω), ContinuousAt (fun ν => ν.map f) x

Proof state:
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous f
⊢ ∀ (x : FiniteMeasure Ω), ContinuousAt (fun ν => ν.map f) x

Tactic:
exact fun _ ↦ tendsto_map_of_tendsto_of_continuous _ _ continuous_id.continuousAt f_cont

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem injOn_of_ncard_image_eq (h : (f '' s).ncard = s.ncard) (hs : s.Finite

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).encard = s.encard
hs : autoParam s.Finite _auto✝
⊢ InjOn f s

Tactic:
exact hs.injOn_of_encard_image_eq h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).ncard = s.ncard
hs : autoParam s.Finite _auto✝
⊢ InjOn f s

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, (hs.image _).cast_ncard_eq] at h

Result:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).encard = s.encard
hs : autoParam s.Finite _auto✝
⊢ InjOn f s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofFin_ofNat (n : Nat) :
    ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n

Proof state:
w n : Nat
⊢ { toFin := OfNat.ofNat n } = OfNat.ofNat n

Tactic:
simp only [OfNat.ofNat, Fin.ofNat', BitVec.ofNat, Nat.and_pow_two_sub_one_eq_mod]

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_Ioc (f : ∀ i, α i) (i : ι) (a b : α i) :
    update f i '' Ioc a b = Ioc (update f i a) (update f i b)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ioc a b = Ioc (update f i a) (update f i b)

Tactic:
rw [← Icc_diff_left, ← Icc_diff_left, image_diff (update_injective _ _), image_singleton,
  image_update_Icc]

Result:
no goals
-- Mathlib/Order/Chain.lean
theorem subset_succChain : s ⊆ SuccChain r s :=
  if h : ∃ t, IsChain r s ∧ SuperChain r s t then (succChain_spec h).2.1
  else by
    rw [exists_and_left] at h
    simp [SuccChain, dif_neg, h, Subset.rfl]

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ s ⊆ SuccChain r s

Tactic:
rw [exists_and_left] at h

Result:
α : Type u_1
r : α → α → Prop
s : Set α
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ s ⊆ SuccChain r s

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ s ⊆ SuccChain r s

Tactic:
simp [SuccChain, dif_neg, h, Subset.rfl]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
@[stacks 00EC]
lemma zeroLocus_eq_basicOpen_of_isIdempotentElem
    (e : R) (he : IsIdempotentElem e) :
    zeroLocus {e} = basicOpen (1 - e)

Proof state:
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ zeroLocus {e} = ↑(basicOpen (1 - e))

Tactic:
rw [basicOpen_eq_zeroLocus_of_isIdempotentElem _ he.one_sub, sub_sub_cancel]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem NormedCommGroup.nhds_one_basis_norm_lt :
    (𝓝 (1 : E)).HasBasis (fun ε : ℝ => 0 < ε) fun ε => { y | ‖y‖ < ε }

Proof state:
case h.e'_5.h.h.e'_2.h.h.e'_3.h.e'_3
E : Type u_5
inst✝ : SeminormedGroup E
x✝¹ : ℝ
x✝ : E
⊢ x✝ = x✝ / 1

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ (𝓝 1).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y‖ < ε}

Tactic:
convert NormedCommGroup.nhds_basis_norm_lt (1 : E)

Result:
case h.e'_5.h.h.e'_2.h.h.e'_3.h.e'_3
E : Type u_5
inst✝ : SeminormedGroup E
x✝¹ : ℝ
x✝ : E
⊢ x✝ = x✝ / 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_le_sub_left_of_le_add {a b c : Int} (h : c ≤ a + b) : -a ≤ b - c

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

Tactic:
have h := Int.le_neg_add_of_add_le (Int.sub_left_le_of_le_add h)

Result:
a b c : Int
h✝ : c ≤ a + b
h : -a ≤ -c + b
⊢ -a ≤ b - c

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

Tactic:
rwa [Int.add_comm] at h

Result:
no goals