harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mfderiv_congr_point {x' : M} (h : x = x') :
    @Eq (E →L[𝕜] E') (mfderiv I I' f x) (mfderiv I I' f x')

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x x' : M
h : x = x'
⊢ mfderiv I I' f x = mfderiv I I' f x'

Tactic:
subst h

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
⊢ mfderiv I I' f x = mfderiv I I' f x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
⊢ mfderiv I I' f x = mfderiv I I' f x

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
lemma span_smul_eq
    (s : Set R) (N : Submodule R M) :
    Ideal.span s • N = s • N

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

Tactic:
rw [← coe_set_smul, coe_span_smul]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem map_nhdsWithin_eq (h : e.IsImage s t) (hx : x ∈ e.source) : map e (𝓝[s] x) = 𝓝[t] e x

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
t : Set Y
x : X
h : e.IsImage s t
hx : x ∈ e.source
⊢ map (↑e) (𝓝[s] x) = 𝓝[t] ↑e x

Tactic:
rw [e.map_nhdsWithin_eq hx, h.image_eq, e.nhdsWithin_target_inter (e.map_source hx)]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem leadingCoeff_monomial (a : R) (n : ℕ) : leadingCoeff (monomial n a) = a

Proof state:
case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ ((monomial n) a).leadingCoeff = a

Tactic:
rw [leadingCoeff, natDegree_monomial, if_neg ha, coeff_monomial]

Result:
case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ (if n = n then a else 0) = a

Proof state:
case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ (if n = n then a else 0) = a

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ ((monomial n) a).leadingCoeff = a

Tactic:
by_cases ha : a = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : a = 0
⊢ ((monomial n) a).leadingCoeff = a

case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ ((monomial n) a).leadingCoeff = a

Proof state:
case pos
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : a = 0
⊢ ((monomial n) a).leadingCoeff = a

Tactic:
simp only [ha, (monomial n).map_zero, leadingCoeff_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
/-- A morphism of modules is surjective if and only the morphism of exterior algebras that it
induces is surjective. -/
@[simp]
lemma map_surjective_iff {f : M →ₗ[R] N} :
    Function.Surjective (map f) ↔ Function.Surjective f

Proof state:
case intro
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑(map f)
y : N
x : ExteriorAlgebra R M
hx : (map f) x = (ι R) y
⊢ ∃ a, f a = y

Tactic:
existsi ιInv x

Result:
case intro
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑(map f)
y : N
x : ExteriorAlgebra R M
hx : (map f) x = (ι R) y
⊢ f (ιInv x) = y

Proof state:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑(map f)
y : N
⊢ ∃ a, f a = y

Tactic:
obtain ⟨x, hx⟩ := h (ι R y)

Result:
case intro
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑(map f)
y : N
x : ExteriorAlgebra R M
hx : (map f) x = (ι R) y
⊢ ∃ a, f a = y

Proof state:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ Function.Surjective ⇑(map f) ↔ Function.Surjective ⇑f

Tactic:
refine ⟨fun h y ↦ ?_, fun h ↦ CliffordAlgebra.map_surjective _ h⟩

Result:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑(map f)
y : N
⊢ ∃ a, f a = y

Proof state:
case intro
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑(map f)
y : N
x : ExteriorAlgebra R M
hx : (map f) x = (ι R) y
⊢ f (ιInv x) = y

Tactic:
rw [← LinearMap.comp_apply, ← ιInv_comp_map, LinearMap.comp_apply]

Result:
case intro
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑(map f)
y : N
x : ExteriorAlgebra R M
hx : (map f) x = (ι R) y
⊢ ιInv ((map f).toLinearMap x) = y

Proof state:
case intro
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑(map f)
y : N
x : ExteriorAlgebra R M
hx : (map f) x = (ι R) y
⊢ ιInv ((map f).toLinearMap x) = y

Tactic:
erw [hx, ExteriorAlgebra.ι_leftInverse]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem measure_le_lintegral_thickenedIndicator (μ : Measure X) {E : Set X}
    (E_mble : MeasurableSet E) {δ : ℝ} (δ_pos : 0 < δ) :
    μ E ≤ ∫⁻ x, (thickenedIndicator δ_pos E x : ℝ≥0∞) ∂μ

Proof state:
case h.e'_4.h.e'_4.h
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
x✝ : X
⊢ ↑((thickenedIndicator δ_pos E) x✝) = thickenedIndicatorAux δ E x✝

Tactic:
dsimp

Result:
case h.e'_4.h.e'_4.h
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
x✝ : X
⊢ ↑(thickenedIndicatorAux δ E x✝).toNNReal = thickenedIndicatorAux δ E x✝

Proof state:
case h.e'_4.h.e'_4.h
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
x✝ : X
⊢ ↑(thickenedIndicatorAux δ E x✝).toNNReal = thickenedIndicatorAux δ E x✝

Tactic:
simp only [thickenedIndicatorAux_lt_top.ne, ENNReal.coe_toNNReal, Ne, not_false_iff]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
⊢ μ E ≤ ∫⁻ (x : X), ↑((thickenedIndicator δ_pos E) x) ∂μ

Tactic:
convert measure_le_lintegral_thickenedIndicatorAux μ E_mble δ

Result:
case h.e'_4.h.e'_4.h
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
x✝ : X
⊢ ↑((thickenedIndicator δ_pos E) x✝) = thickenedIndicatorAux δ E x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_congr {xs ys : Array α} (w : xs = ys)
    (f : (i : Nat) → α → (h : i < xs.size) → β) :
    mapFinIdx xs f = mapFinIdx ys (fun i a h => f i a (by simp [w]; omega))

Proof state:
α : Type u_1
β : Type u_2
xs : Array α
f : (i : Nat) → α → i < xs.size → β
⊢ xs.mapFinIdx f = xs.mapFinIdx fun i a h => f i a ⋯

Tactic:
rfl

Result:
no goals

Proof state:
α : Type ?u.50064
β : Type ?u.50093
xs ys : Array α
w : xs = ys
f : (i : Nat) → α → i < xs.size → β
i : Nat
a : α
h : i < ys.size
⊢ i < ys.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.50064
β : Type ?u.50093
xs ys : Array α
w : xs = ys
f : (i : Nat) → α → i < xs.size → β
i : Nat
a : α
h : i < ys.size
⊢ i < xs.size

Tactic:
simp [w]

Result:
α : Type ?u.50064
β : Type ?u.50093
xs ys : Array α
w : xs = ys
f : (i : Nat) → α → i < xs.size → β
i : Nat
a : α
h : i < ys.size
⊢ i < ys.size

Proof state:
α : Type u_1
β : Type u_2
xs ys : Array α
w : xs = ys
f : (i : Nat) → α → i < xs.size → β
⊢ xs.mapFinIdx f = ys.mapFinIdx fun i a h => f i a ⋯

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
xs : Array α
f : (i : Nat) → α → i < xs.size → β
⊢ xs.mapFinIdx f = xs.mapFinIdx fun i a h => f i a ⋯
-- Mathlib/Analysis/Normed/Operator/Compact.lean
theorem IsCompactOperator.continuous_comp {f : M₁ → M₂} (hf : IsCompactOperator f) {g : M₂ → M₃}
    (hg : Continuous g) : IsCompactOperator (g ∘ f)

Proof state:
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝³ : TopologicalSpace M₁
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : AddCommMonoid M₁
f : M₁ → M₂
hf : IsCompactOperator f
g : M₂ → M₃
hg : Continuous g
⊢ IsCompactOperator (g ∘ f)

Tactic:
rcases hf with ⟨K, hK, hKf⟩

Result:
case intro.intro
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝³ : TopologicalSpace M₁
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : AddCommMonoid M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ IsCompactOperator (g ∘ f)

Proof state:
case intro.intro
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝³ : TopologicalSpace M₁
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : AddCommMonoid M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ f ⁻¹' K ⊆ f ⁻¹' (g ⁻¹' (g '' K))

Tactic:
exact preimage_mono (subset_preimage_image _ _)

Result:
no goals

Proof state:
case intro.intro
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝³ : TopologicalSpace M₁
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : AddCommMonoid M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ f ⁻¹' K ⊆ g ∘ f ⁻¹' (g '' K)

Tactic:
rw [preimage_comp]

Result:
case intro.intro
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝³ : TopologicalSpace M₁
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : AddCommMonoid M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ f ⁻¹' K ⊆ f ⁻¹' (g ⁻¹' (g '' K))

Proof state:
case intro.intro
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝³ : TopologicalSpace M₁
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : AddCommMonoid M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ IsCompactOperator (g ∘ f)

Tactic:
refine ⟨g '' K, hK.image hg, mem_of_superset hKf ?_⟩

Result:
case intro.intro
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝³ : TopologicalSpace M₁
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : AddCommMonoid M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ f ⁻¹' K ⊆ g ∘ f ⁻¹' (g '' K)
-- Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean
@[to_additive]
lemma csInf_div (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
    sInf (s / t) = sInf s / sSup t

Proof state:
M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sInf (s / t) = sInf s / sSup t

Tactic:
rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualBasis_repr (l : Dual R M) (i : ι) : b.dualBasis.repr l i = l (b i)

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
l : Dual R M
i : ι
⊢ (b.dualBasis.repr l) i = l (b i)

Tactic:
rw [← linearCombination_dualBasis b, Basis.linearCombination_repr b.dualBasis l]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem PartialOrder.toPreorder_injective :
    Function.Injective (@PartialOrder.toPreorder α) := fun A B h ↦ by
  cases A
  cases B
  cases h
  congr

Proof state:
case mk.mk.refl
α : Type u_2
toPreorder✝ : Preorder α
le_antisymm✝¹ le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
⊢ mk le_antisymm✝¹ = mk le_antisymm✝

Tactic:
congr

Result:
no goals

Proof state:
α : Type u_2
A B : PartialOrder α
h : toPreorder = toPreorder
⊢ A = B

Tactic:
cases A

Result:
case mk
α : Type u_2
B : PartialOrder α
toPreorder✝ : Preorder α
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
h : toPreorder = toPreorder
⊢ mk le_antisymm✝ = B

Proof state:
case mk
α : Type u_2
B : PartialOrder α
toPreorder✝ : Preorder α
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
h : toPreorder = toPreorder
⊢ mk le_antisymm✝ = B

Tactic:
cases B

Result:
case mk.mk
α : Type u_2
toPreorder✝¹ : Preorder α
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
toPreorder✝ : Preorder α
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
h : toPreorder = toPreorder
⊢ mk le_antisymm✝¹ = mk le_antisymm✝

Proof state:
case mk.mk
α : Type u_2
toPreorder✝¹ : Preorder α
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
toPreorder✝ : Preorder α
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
h : toPreorder = toPreorder
⊢ mk le_antisymm✝¹ = mk le_antisymm✝

Tactic:
cases h

Result:
case mk.mk.refl
α : Type u_2
toPreorder✝ : Preorder α
le_antisymm✝¹ le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
⊢ mk le_antisymm✝¹ = mk le_antisymm✝
-- Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean
lemma sheafCondition_iff_bijective_toPullbackObj (P : Cᵒᵖ ⥤ Type v') :
    S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
⊢ S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)

Tactic:
have := (S.toSquare.op.map P).pullbackCone.isLimitEquivBijective

Result:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
this : IsLimit (S.op.map P).pullbackCone ≃ Function.Bijective (S.op.map P).pullbackCone.toPullbackObj
⊢ S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
this : IsLimit (S.op.map P).pullbackCone ≃ Function.Bijective (S.op.map P).pullbackCone.toPullbackObj
⊢ S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P)

Tactic:
exact ⟨fun h ↦ this h.isLimit, fun h ↦ Square.IsPullback.mk _ (this.symm h)⟩

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCodetector_def (G : C) :
    IsCodetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : X ⟶ G, ∃! h', f ≫ h' = h) → IsIso f :=
  ⟨fun hG X Y f hf =>
    hG _ fun H hH h => by
      obtain rfl := Set.mem_singleton_iff.1 hH
      exact hf h,
    fun hG _ _ _ hf => hG _ fun _ => hf _ (Set.mem_singleton _) _⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCodetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
H : C
hH : H ∈ {G}
h : X ⟶ H
⊢ ∃! h', f ≫ h' = h

Tactic:
obtain rfl := Set.mem_singleton_iff.1 hH

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
H : C
h : X ⟶ H
hG : IsCodetector H
hf : ∀ (h : X ⟶ H), ∃! h', f ≫ h' = h
hH : H ∈ {H}
⊢ ∃! h', f ≫ h' = h

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
H : C
h : X ⟶ H
hG : IsCodetector H
hf : ∀ (h : X ⟶ H), ∃! h', f ≫ h' = h
hH : H ∈ {H}
⊢ ∃! h', f ≫ h' = h

Tactic:
exact hf h

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem inits_core_eq (l : List α) (s : Stream' α) :
    initsCore l s = l::initsCore (l ++ [head s]) (tail s)

Proof state:
α : Type u
l : List α
s : Stream' α
⊢ corec
      (fun x =>
        match x with
        | (a, snd) => a)
      (fun p =>
        match p with
        | (l', s') => (l' ++ [s'.head], s'.tail))
      (l, s) =
    l ::
      corec
        (fun x =>
          match x with
          | (a, snd) => a)
        (fun p =>
          match p with
          | (l', s') => (l' ++ [s'.head], s'.tail))
        (l ++ [s.head], s.tail)

Tactic:
rw [corec_eq]

Result:
no goals

Proof state:
α : Type u
l : List α
s : Stream' α
⊢ initsCore l s = l :: initsCore (l ++ [s.head]) s.tail

Tactic:
unfold initsCore corecOn

Result:
α : Type u
l : List α
s : Stream' α
⊢ corec
      (fun x =>
        match x with
        | (a, snd) => a)
      (fun p =>
        match p with
        | (l', s') => (l' ++ [s'.head], s'.tail))
      (l, s) =
    l ::
      corec
        (fun x =>
          match x with
          | (a, snd) => a)
        (fun p =>
          match p with
          | (l', s') => (l' ++ [s'.head], s'.tail))
        (l ++ [s.head], s.tail)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_mkArray_self [LawfulBEq α] {a : α} :
    (mkArray n a).erase a = mkArray (n - 1) a

Proof state:
α : Type u_1
inst✝¹ : BEq α
n : Nat
inst✝ : LawfulBEq α
a : α
⊢ ((List.replicate n a).erase a).toArray = (List.replicate (n - 1) a).toArray

Tactic:
simp [List.erase_replicate]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
n : Nat
inst✝ : LawfulBEq α
a : α
⊢ (mkArray n a).erase a = mkArray (n - 1) a

Tactic:
simp only [← List.toArray_replicate, List.erase_toArray]

Result:
α : Type u_1
inst✝¹ : BEq α
n : Nat
inst✝ : LawfulBEq α
a : α
⊢ ((List.replicate n a).erase a).toArray = (List.replicate (n - 1) a).toArray
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem le_weightedOrder {n : ℕ∞} (h : ∀ d : σ →₀ ℕ, weight w d < n → coeff R d f = 0) :
    n ≤ f.weightedOrder w

Proof state:
case top.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff R d) f = 0
d : σ →₀ ℕ
⊢ (coeff R d) f = (coeff R d) 0

Tactic:
exact h d (ENat.coe_lt_top _)

Result:
no goals

Proof state:
case top
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff R d) f = 0
⊢ f = 0

Tactic:
ext d

Result:
case top.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff R d) f = 0
d : σ →₀ ℕ
⊢ (coeff R d) f = (coeff R d) 0

Proof state:
case coe
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff R d) f = 0
⊢ ↑a✝ ≤ weightedOrder w f

Tactic:
apply nat_le_weightedOrder

Result:
case coe.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff R d) f = 0
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < a✝ → (coeff R d) f = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < n → (coeff R d) f = 0
⊢ n ≤ weightedOrder w f

Tactic:
cases n

Result:
case top
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff R d) f = 0
⊢ ⊤ ≤ weightedOrder w f

case coe
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff R d) f = 0
⊢ ↑a✝ ≤ weightedOrder w f

Proof state:
case top
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff R d) f = 0
⊢ ⊤ ≤ weightedOrder w f

Tactic:
rw [top_le_iff, weightedOrder_eq_top_iff]

Result:
case top
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff R d) f = 0
⊢ f = 0

Proof state:
case coe.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff R d) f = 0
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < a✝ → (coeff R d) f = 0

Tactic:
simpa only [ENat.some_eq_coe, Nat.cast_lt] using h

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem frobenius_nnnorm_one [DecidableEq n] [SeminormedAddCommGroup α] [One α] :
    ‖(1 : Matrix n n α)‖₊ = .sqrt (Fintype.card n) * ‖(1 : α)‖₊

Proof state:
n : Type u_4
α : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ↑(Fintype.card n) ^ (1 / OfNat.ofNat 2).toReal * ‖1‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊

Tactic:
simp [NNReal.sqrt_eq_rpow]

Result:
no goals

Proof state:
n : Type u_4
α : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ‖(WithLp.equiv 2 (n → α)).symm (Function.const n 1)‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊

Tactic:
rw [PiLp.nnnorm_equiv_symm_const (ENNReal.ofNat_ne_top (n := 2))]

Result:
n : Type u_4
α : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ↑(Fintype.card n) ^ (1 / OfNat.ofNat 2).toReal * ‖1‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊

Proof state:
n : Type u_4
α : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ‖1‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊

Tactic:
calc
  ‖(diagonal 1 : Matrix n n α)‖₊
  _ = ‖(WithLp.equiv 2 (n → α)).symm (Function.const _ 1)‖₊ := frobenius_nnnorm_diagonal _
  _ = .sqrt (Fintype.card n) * ‖(1 : α)‖₊ := by
    rw [PiLp.nnnorm_equiv_symm_const (ENNReal.ofNat_ne_top (n := 2))]
    simp [NNReal.sqrt_eq_rpow]

Result:
no goals