harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.abs_repr {α} (x : Cofix F α) : Quot.mk _ (Cofix.repr x) = x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
⊢ ∀ (x y : Cofix F α), R x y → LiftR' (α.RelLast' R) x.dest y.dest

Tactic:
clear x

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
⊢ ∀ (x y : Cofix F α), R x y → LiftR' (α.RelLast' R) x.dest y.dest

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
⊢ Quot.mk Mcongr x.repr = x

Tactic:
refine Cofix.bisim₂ R ?_ _ _ rfl

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
⊢ ∀ (x y : Cofix F α), R x y → LiftR' (α.RelLast' R) x.dest y.dest

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
x y : Cofix F α
h : R x y
⊢ LiftR' (α.RelLast' R) x.dest y.dest

Tactic:
subst h

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y => abs y.repr = x
y : Cofix F α
⊢ LiftR' (α.RelLast' R) (abs y.repr).dest y.dest
-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem zero_mem_lowerBounds_smoothingSeminormSeq_range (x : R) :
    0 ∈ lowerBounds (Set.range fun n : ℕ+ => μ (x ^ (n : ℕ)) ^ (1 / (n : ℝ)))

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
n : ℕ+
⊢ 0 ≤ (fun n => μ (x ^ ↑n) ^ (1 / ↑↑n)) n

Tactic:
exact rpow_nonneg (apply_nonneg μ _) _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
⊢ 0 ∈ lowerBounds (Set.range fun n => μ (x ^ ↑n) ^ (1 / ↑↑n))

Tactic:
rintro y ⟨n, rfl⟩

Result:
case intro
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
n : ℕ+
⊢ 0 ≤ (fun n => μ (x ^ ↑n) ^ (1 / ↑↑n)) n
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem _root_.Submodule.adjoint_subtypeL (U : Submodule 𝕜 E) [CompleteSpace U] :
    U.subtypeL† = orthogonalProjection U

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ ∀ (x : E) (y : ↥U), ⟪(orthogonalProjection U) x, y⟫_𝕜 = ⟪x, U.subtypeL y⟫_𝕜

Tactic:
intro x u

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
x : E
u : ↥U
⊢ ⟪(orthogonalProjection U) x, u⟫_𝕜 = ⟪x, U.subtypeL u⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ orthogonalProjection U = adjoint U.subtypeL

Tactic:
rw [eq_adjoint_iff]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ ∀ (x : E) (y : ↥U), ⟪(orthogonalProjection U) x, y⟫_𝕜 = ⟪x, U.subtypeL y⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
x : E
u : ↥U
⊢ ⟪(orthogonalProjection U) x, u⟫_𝕜 = ⟪x, U.subtypeL u⟫_𝕜

Tactic:
rw [U.coe_inner, inner_orthogonalProjection_left_eq_right,
  orthogonalProjection_mem_subspace_eq_self]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
x : E
u : ↥U
⊢ ⟪x, ↑u⟫_𝕜 = ⟪x, U.subtypeL u⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ adjoint U.subtypeL = orthogonalProjection U

Tactic:
symm

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ orthogonalProjection U = adjoint U.subtypeL

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
x : E
u : ↥U
⊢ ⟪x, ↑u⟫_𝕜 = ⟪x, U.subtypeL u⟫_𝕜

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem ofFinsupp_eq_one {a} : (⟨a⟩ : R[X]) = 1 ↔ a = 1

Proof state:
R : Type u
inst✝ : Semiring R
a : R[ℕ]
⊢ { toFinsupp := a } = 1 ↔ a = 1

Tactic:
rw [← ofFinsupp_one, ofFinsupp_inj]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem not_specializes_iff_exists_closed : ¬x ⤳ y ↔ ∃ S : Set X, IsClosed S ∧ x ∈ S ∧ y ∉ S

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (∃ s, IsClosed s ∧ x ∈ s ∧ y ∉ s) ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ y ∉ S

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬x ⤳ y ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ y ∉ S

Tactic:
rw [specializes_iff_forall_closed]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ y ∉ S

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ y ∉ S

Tactic:
push_neg

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (∃ s, IsClosed s ∧ x ∈ s ∧ y ∉ s) ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ y ∉ S
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem val_div_eq_divp (u₁ u₂ : αˣ) : ↑(u₁ / u₂) = ↑u₁ /ₚ u₂

Proof state:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑(u₁ / u₂) = ↑u₁ /ₚ u₂

Tactic:
rw [divp, division_def, Units.val_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem _root_.LinearMap.compQuadraticMap_polar [CommSemiring S] [Algebra S R] [Module S N]
    [Module S N'] [IsScalarTower S R N] [Module S M] [IsScalarTower S R M] (f : N →ₗ[S] N')
    (Q : QuadraticMap R M N) (x y : M) : polar (f.compQuadraticMap' Q) x y = f (polar Q x y)

Proof state:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R M
inst✝⁸ : Module R N
N' : Type u_8
inst✝⁷ : AddCommGroup N'
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra S R
inst✝⁴ : Module S N
inst✝³ : Module S N'
inst✝² : IsScalarTower S R N
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
f : N →ₗ[S] N'
Q : QuadraticMap R M N
x y : M
⊢ polar (⇑(f.compQuadraticMap' Q)) x y = f (polar (⇑Q) x y)

Tactic:
simp [polar]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma in₀₁_iff' :
    (graph t).Adj (in₀ a) (in₁ b) ↔ ∃ x : α × β × γ, x ∈ t ∧ x.1 = a ∧ x.2.1 = b where
  mp

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
⊢ (∃ x ∈ t, x.1 = a ∧ x.2.1 = b) → (graph t).Adj (in₀ a) (in₁ b)

Tactic:
rintro ⟨⟨a, b, c⟩, h, rfl, rfl⟩

Result:
case intro.mk.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₀ (a, b, c).1) (in₁ (a, b, c).2.1)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
⊢ (graph t).Adj (in₀ a) (in₁ b) → ∃ x ∈ t, x.1 = a ∧ x.2.1 = b

Tactic:
rintro ⟨⟩

Result:
case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ x ∈ t, x.1 = a ∧ x.2.1 = b

Proof state:
case intro.mk.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₀ (a, b, c).1) (in₁ (a, b, c).2.1)

Tactic:
constructor

Result:
case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ((a, b, c).1, (a, b, c).2.1, ?intro.mk.mk.intro.intro.c) ∈ t

case intro.mk.mk.intro.intro.c
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ γ

Proof state:
case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ((a, b, c).1, (a, b, c).2.1, ?intro.mk.mk.intro.intro.c) ∈ t

case intro.mk.mk.intro.intro.c
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ γ

Tactic:
assumption

Result:
no goals

Proof state:
case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ x ∈ t, x.1 = a ∧ x.2.1 = b

Tactic:
exact ⟨_, ‹_›, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ (a, b, c✝).1 = a ∧ (a, b, c✝).2.1 = b

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_eq_iff_eq_sin {x y : ℝ} (hy : y ∈ Ioo (-(π / 2)) (π / 2)) :
    arcsin x = y ↔ x = sin y

Proof state:
x y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
⊢ arcsin x = y ↔ x = sin y

Tactic:
simp only [le_antisymm_iff, arcsin_le_iff_le_sin' (mem_Ico_of_Ioo hy),
  le_arcsin_iff_sin_le' (mem_Ioc_of_Ioo hy)]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem FormalMultilinearSeries.continuousOn [CompleteSpace F] :
    ContinuousOn p.sum (EMetric.ball 0 p.radius)

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace F
h : 0 < p.radius
⊢ ContinuousOn p.sum (EMetric.ball 0 p.radius)

Tactic:
exact (p.hasFPowerSeriesOnBall h).continuousOn

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace F
h : 0 = p.radius
⊢ ContinuousOn p.sum (EMetric.ball 0 p.radius)

Tactic:
simp [← h, continuousOn_empty]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace F
⊢ ContinuousOn p.sum (EMetric.ball 0 p.radius)

Tactic:
rcases (zero_le p.radius).eq_or_lt with h | h

Result:
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace F
h : 0 = p.radius
⊢ ContinuousOn p.sum (EMetric.ball 0 p.radius)

case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace F
h : 0 < p.radius
⊢ ContinuousOn p.sum (EMetric.ball 0 p.radius)
-- Mathlib/LinearAlgebra/TensorProduct/Matrix.lean
theorem TensorProduct.toMatrix_assoc :
    toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP))
        (TensorProduct.assoc R M N P) =
      (1 : Matrix (ι × κ × τ) (ι × κ × τ) R).submatrix _root_.id (Equiv.prodAssoc _ _ _)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
ι : Type u_7
κ : Type u_8
τ : Type u_9
inst✝¹² : DecidableEq ι
inst✝¹¹ : DecidableEq κ
inst✝¹⁰ : DecidableEq τ
inst✝⁹ : Fintype ι
inst✝⁸ : Fintype κ
inst✝⁷ : Fintype τ
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
⊢ (toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP)))
      ↑(TensorProduct.assoc R M N P) =
    submatrix 1 _root_.id ⇑(Equiv.prodAssoc ι κ τ)

Tactic:
ext ⟨i, j, k⟩ ⟨⟨i', j'⟩, k'⟩

Result:
case a.mk.mk.mk.mk
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
ι : Type u_7
κ : Type u_8
τ : Type u_9
inst✝¹² : DecidableEq ι
inst✝¹¹ : DecidableEq κ
inst✝¹⁰ : DecidableEq τ
inst✝⁹ : Fintype ι
inst✝⁸ : Fintype κ
inst✝⁷ : Fintype τ
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
⊢ (toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP)))
      ↑(TensorProduct.assoc R M N P) (i, j, k) ((i', j'), k') =
    submatrix 1 _root_.id ⇑(Equiv.prodAssoc ι κ τ) (i, j, k) ((i', j'), k')

Proof state:
case a.mk.mk.mk.mk
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
ι : Type u_7
κ : Type u_8
τ : Type u_9
inst✝¹² : DecidableEq ι
inst✝¹¹ : DecidableEq κ
inst✝¹⁰ : DecidableEq τ
inst✝⁹ : Fintype ι
inst✝⁸ : Fintype κ
inst✝⁷ : Fintype τ
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
i : ι
j : κ
k k' : τ
i' : ι
j' : κ
⊢ (toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP)))
      ↑(TensorProduct.assoc R M N P) (i, j, k) ((i', j'), k') =
    submatrix 1 _root_.id ⇑(Equiv.prodAssoc ι κ τ) (i, j, k) ((i', j'), k')

Tactic:
simp only [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, assoc_tmul,
  Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply, @eq_comm _ k',
  @eq_comm _ j', smul_eq_mul, mul_ite, mul_one, mul_zero, ← ite_and, @eq_comm _ i',
  submatrix_apply, Matrix.one_apply, id_eq, Equiv.prodAssoc_apply, Prod.mk.injEq]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CoverLifting.lean
lemma sheafAdjunctionCocontinuous_homEquiv_apply_val {F : Sheaf K A} {H : Sheaf J A}
    (f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H) :
    ((G.sheafAdjunctionCocontinuous A J K).homEquiv F H f).val =
      (G.op.ranAdjunction A).homEquiv F.val H.val f.val :=
  ((sheafToPresheaf K A).congr_map
    (((G.op.ranAdjunction A).restrictFullyFaithful_homEquiv_apply
      (fullyFaithfulSheafToPresheaf K A) (fullyFaithfulSheafToPresheaf J A)
      (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm
      (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm f))).trans (by
        dsimp
        erw [Functor.map_id, Category.comp_id, Category.id_comp,
          Adjunction.homEquiv_unit])

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
H : Sheaf J A
f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H
⊢ (sheafToPresheaf K A).map
      ((fullyFaithfulSheafToPresheaf K A).preimage
        ((G.op.ranAdjunction A).unit.app ((sheafToPresheaf K A).obj F) ≫
          G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm.hom.app F) ≫
            G.op.ran.map ((sheafToPresheaf J A).map f) ≫
              (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm.hom.app H)) =
    ((G.op.ranAdjunction A).homEquiv F.val H.val) f.val

Tactic:
dsimp

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
H : Sheaf J A
f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H
⊢ (G.op.ranAdjunction A).unit.app F.val ≫
      G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).inv.app F) ≫
        G.op.ran.map f.val ≫ 𝟙 ((G.sheafPushforwardCocontinuous A J K).obj H).val =
    ((G.op.ranAdjunction A).homEquiv F.val H.val) f.val

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
H : Sheaf J A
f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H
⊢ (G.op.ranAdjunction A).unit.app F.val ≫
      G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).inv.app F) ≫
        G.op.ran.map f.val ≫ 𝟙 ((G.sheafPushforwardCocontinuous A J K).obj H).val =
    ((G.op.ranAdjunction A).homEquiv F.val H.val) f.val

Tactic:
erw [Functor.map_id, Category.comp_id, Category.id_comp,
  Adjunction.homEquiv_unit]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
theorem edgeFinset_replaceVertex_of_not_adj (hn : ¬G.Adj s t) : (G.replaceVertex s t).edgeFinset =
    G.edgeFinset \ G.incidenceFinset t ∪ (G.neighborFinset s).image (s(·, t))

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
⊢ (G.replaceVertex s t).edgeFinset = (G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s).toFinset

Tactic:
exact Set.toFinset_congr (G.edgeSet_replaceVertex_of_not_adj hn)

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
⊢ (G.replaceVertex s t).edgeFinset = G.edgeFinset \ G.incidenceFinset t ∪ image (fun x => s(x, t)) (G.neighborFinset s)

Tactic:
simp only [incidenceFinset, neighborFinset, ← Set.toFinset_diff, ← Set.toFinset_image,
  ← Set.toFinset_union]

Result:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
⊢ (G.replaceVertex s t).edgeFinset = (G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s).toFinset
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleRange_of_gt {n : ℕ} {i j : Fin n} (h : i < j) : cycleRange i j = j

Proof state:
case h
n : ℕ
i j : Fin n
h : i < j
⊢ j ∉ Set.range ⇑(castLEEmb ⋯)

Tactic:
simpa

Result:
no goals

Proof state:
n : ℕ
i j : Fin n
h : i < j
⊢ i.cycleRange j = j

Tactic:
rw [cycleRange, ofLeftInverse'_eq_ofInjective,
  ← Function.Embedding.toEquivRange_eq_ofInjective, ← viaFintypeEmbedding,
  viaFintypeEmbedding_apply_not_mem_range]

Result:
case h
n : ℕ
i j : Fin n
h : i < j
⊢ j ∉ Set.range ⇑(castLEEmb ⋯)
-- Mathlib/Topology/LocallyFinite.lean
theorem LocallyFinite.eventually_subset {s : ι → Set X}
    (hs : LocallyFinite s) (hs' : ∀ i, IsClosed (s i)) (x : X) :
    ∀ᶠ y in 𝓝 x, {i | y ∈ s i} ⊆ {i | x ∈ s i}

Proof state:
case h
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed (s i)
x y : X
i : ι
hi : i ∈ {i | y ∈ s i}
hy : ∀ (i : ι), x ∉ s i → y ∉ s i
⊢ i ∈ {i | x ∈ s i}

Tactic:
exact not_imp_not.mp (hy i) hi

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed (s i)
x : X
⊢ ∀ᶠ (y : X) in 𝓝 x, {i | y ∈ s i} ⊆ {i | x ∈ s i}

Tactic:
filter_upwards [hs.iInter_compl_mem_nhds hs' x] with y hy i hi

Result:
case h
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed (s i)
x y : X
hy : y ∈ ⋂ i, ⋂ (_ : x ∉ s i), (s i)ᶜ
i : ι
hi : i ∈ {i | y ∈ s i}
⊢ i ∈ {i | x ∈ s i}

Proof state:
case h
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed (s i)
x y : X
hy : y ∈ ⋂ i, ⋂ (_ : x ∉ s i), (s i)ᶜ
i : ι
hi : i ∈ {i | y ∈ s i}
⊢ i ∈ {i | x ∈ s i}

Tactic:
simp only [mem_iInter, mem_compl_iff] at hy

Result:
case h
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed (s i)
x y : X
i : ι
hi : i ∈ {i | y ∈ s i}
hy : ∀ (i : ι), x ∉ s i → y ∉ s i
⊢ i ∈ {i | x ∈ s i}
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem norm_setToSimpleFunc_le_sum_opNorm {m : MeasurableSpace α} (T : Set α → F' →L[ℝ] F)
    (f : α →ₛ F') : ‖f.setToSimpleFunc T‖ ≤ ∑ x ∈ f.range, ‖T (f ⁻¹' {x})‖ * ‖x‖ :=
  calc
    ‖∑ x ∈ f.range, T (f ⁻¹' {x}) x‖ ≤ ∑ x ∈ f.range, ‖T (f ⁻¹' {x}) x‖ := norm_sum_le _ _
    _ ≤ ∑ x ∈ f.range, ‖T (f ⁻¹' {x})‖ * ‖x‖

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T : Set α → F' →L[ℝ] F
f : α →ₛ F'
⊢ ∑ x ∈ f.range, ‖(T (⇑f ⁻¹' {x})) x‖ ≤ ∑ x ∈ f.range, ‖T (⇑f ⁻¹' {x})‖ * ‖x‖

Tactic:
refine Finset.sum_le_sum fun b _ => ?_

Result:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T : Set α → F' →L[ℝ] F
f : α →ₛ F'
b : F'
x✝ : b ∈ f.range
⊢ ‖(T (⇑f ⁻¹' {b})) b‖ ≤ ‖T (⇑f ⁻¹' {b})‖ * ‖b‖

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T : Set α → F' →L[ℝ] F
f : α →ₛ F'
b : F'
x✝ : b ∈ f.range
⊢ ‖(T (⇑f ⁻¹' {b})) b‖ ≤ ‖T (⇑f ⁻¹' {b})‖ * ‖b‖

Tactic:
simp_rw [ContinuousLinearMap.le_opNorm]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
lemma sup_toAddSubgroup (p p' : Submodule R M) :
    (p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ (p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ x ∈ (p ⊔ p').toAddSubgroup ↔ x ∈ p.toAddSubgroup ⊔ p'.toAddSubgroup

Proof state:
case h
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubgroup, ∃ z ∈ p'.toAddSubgroup, y + z = x

Tactic:
rfl

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ x ∈ (p ⊔ p').toAddSubgroup ↔ x ∈ p.toAddSubgroup ⊔ p'.toAddSubgroup

Tactic:
rw [mem_toAddSubgroup, mem_sup, AddSubgroup.mem_sup]

Result:
case h
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubgroup, ∃ z ∈ p'.toAddSubgroup, y + z = x
-- Mathlib/Topology/Compactness/LocallyCompact.lean
theorem exists_compact_subset [LocallyCompactSpace X] {x : X} {U : Set X} (hU : IsOpen U)
    (hx : x ∈ U) : ∃ K : Set X, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
x : X
U : Set X
hU : IsOpen U
hx : x ∈ U
⊢ ∃ K, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U

Tactic:
rcases LocallyCompactSpace.local_compact_nhds x U (hU.mem_nhds hx) with ⟨K, h1K, h2K, h3K⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
x : X
U : Set X
hU : IsOpen U
hx : x ∈ U
K : Set X
h1K : K ∈ 𝓝 x
h2K : K ⊆ U
h3K : IsCompact K
⊢ ∃ K, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
x : X
U : Set X
hU : IsOpen U
hx : x ∈ U
K : Set X
h1K : K ∈ 𝓝 x
h2K : K ⊆ U
h3K : IsCompact K
⊢ ∃ K, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U

Tactic:
exact ⟨K, h3K, mem_interior_iff_mem_nhds.2 h1K, h2K⟩

Result:
no goals