harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem app_invApp (U : Opens Y) :
    f.c.app (op U) ≫ H.invApp _ ((Opens.map f.base).obj U) =
      Y.presheaf.map
        ((homOfLE (Set.image_preimage_subset f.base U.1)).op :
          op U ⟶ op (opensFunctor f |>.obj ((Opens.map f.base).obj U)))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
⊢ f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯) =
    f.c.app (op U) ≫ ((TopCat.Presheaf.pushforward C f.base).obj X.presheaf).map (homOfLE ⋯).op

Tactic:
congr

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
⊢ f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U) = Y.presheaf.map (homOfLE ⋯).op

Tactic:
erw [← Category.assoc]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
⊢ (f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj ((Opens.map f.base).obj U)))) =
    Y.presheaf.map (homOfLE ⋯).op

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
⊢ (f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj ((Opens.map f.base).obj U)))) =
    Y.presheaf.map (homOfLE ⋯).op

Tactic:
rw [IsIso.comp_inv_eq, f.c.naturality]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
⊢ f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯) =
    f.c.app (op U) ≫ ((TopCat.Presheaf.pushforward C f.base).obj X.presheaf).map (homOfLE ⋯).op
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem coe_essSup {f : α → ℝ≥0} (hf : IsBoundedUnder (· ≤ ·) (ae μ) f) :
    ((essSup f μ : ℝ≥0) : ℝ≥0∞) = essSup (fun x => (f x : ℝ≥0∞)) μ :=
  (ENNReal.coe_sInf <| hf).trans <|
    eq_of_forall_le_iff fun r => by
      simp [essSup, limsup, limsSup, eventually_map, ENNReal.forall_ennreal]; rfl

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f
r : ℝ≥0∞
⊢ (∀ i ∈ fun x => (map f (ae μ)).sets {x_1 | x_1 ≤ x}, r ≤ ↑i) ↔ ∀ (r_1 : ℝ≥0), (∀ᵐ (a : α) ∂μ, f a ≤ r_1) → r ≤ ↑r_1

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f
r : ℝ≥0∞
⊢ r ≤ ⨅ a ∈ fun x => (map f (ae μ)).sets {x_1 | (fun x_2 => (fun x1 x2 => x1 ≤ x2) x_2 x) x_1}, ↑a ↔
    r ≤ essSup (fun x => ↑(f x)) μ

Tactic:
simp [essSup, limsup, limsSup, eventually_map, ENNReal.forall_ennreal]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f
r : ℝ≥0∞
⊢ (∀ i ∈ fun x => (map f (ae μ)).sets {x_1 | x_1 ≤ x}, r ≤ ↑i) ↔ ∀ (r_1 : ℝ≥0), (∀ᵐ (a : α) ∂μ, f a ≤ r_1) → r ≤ ↑r_1
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem length_edges {u v : V} (p : G.Walk u v) : p.edges.length = p.length

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.edges.length = p.length

Tactic:
simp [edges]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem normalCore_eq_iInf_conjAct (H : Subgroup G) :
    H.normalCore = ⨅ (g : ConjAct G), g • H

Proof state:
case h
G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ g ∈ { carrier := {a | ∀ (b : G), b * a * b⁻¹ ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ } ↔
    ∀ (i : ConjAct G), i⁻¹ • g ∈ H

Tactic:
refine ⟨fun h x ↦ h x⁻¹, fun h x ↦ ?_⟩

Result:
case h
G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
h : ∀ (i : ConjAct G), i⁻¹ • g ∈ H
x : G
⊢ x * g * x⁻¹ ∈ H

Proof state:
case h
G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
h : ∀ (i : ConjAct G), i⁻¹ • g ∈ H
x : G
⊢ x * g * x⁻¹ ∈ H

Tactic:
simpa only [ConjAct.toConjAct_inv, inv_inv] using h x⁻¹

Result:
no goals

Proof state:
case h
G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ g ∈ H.normalCore ↔ g ∈ ⨅ g, g • H

Tactic:
simp only [Subgroup.normalCore, Subgroup.mem_iInf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem]

Result:
case h
G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ g ∈ { carrier := {a | ∀ (b : G), b * a * b⁻¹ ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ } ↔
    ∀ (i : ConjAct G), i⁻¹ • g ∈ H

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore = ⨅ g, g • H

Tactic:
ext g

Result:
case h
G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ g ∈ H.normalCore ↔ g ∈ ⨅ g, g • H
-- Mathlib/FieldTheory/Differential/Basic.lean
lemma logDeriv_prod_of_eq_zero (ι : Type*) (s : Finset ι) (f : ι → R) (h : ∀ x ∈ s, f x = 0) :
    logDeriv (∏ x ∈ s, f x) = ∑ x ∈ s, logDeriv (f x)

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
s : Finset ι
f : ι → R
h : ∀ x ∈ s, f x = 0
⊢ logDeriv (∏ x ∈ s, f x) = ∑ x ∈ s, logDeriv (f x)

Tactic:
unfold logDeriv

Result:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
s : Finset ι
f : ι → R
h : ∀ x ∈ s, f x = 0
⊢ (∏ x ∈ s, f x)′ / ∏ x ∈ s, f x = ∑ x ∈ s, (f x)′ / f x

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
s : Finset ι
f : ι → R
h : ∀ x ∈ s, f x = 0
⊢ (∏ x ∈ s, f x)′ / ∏ x ∈ s, f x = ∑ x ∈ s, (f x)′ / f x

Tactic:
simp_all

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean
theorem norm_toSpanSingleton (x : E) : ‖toSpanSingleton 𝕜 x‖ = ‖x‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
N : ℝ
x✝ : N ≥ 0
h : ‖x‖ * ‖1‖ ≤ N * ‖1‖
⊢ 0 < ‖1‖

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x_1 : 𝕜), ‖(toSpanSingleton 𝕜 x) x_1‖ ≤ N * ‖x_1‖
⊢ ‖x‖ ≤ N

Tactic:
specialize h 1

Result:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
N : ℝ
x✝ : N ≥ 0
h : ‖(toSpanSingleton 𝕜 x) 1‖ ≤ N * ‖1‖
⊢ ‖x‖ ≤ N

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ‖toSpanSingleton 𝕜 x‖ = ‖x‖

Tactic:
refine opNorm_eq_of_bounds (norm_nonneg _) (fun x => ?_) fun N _ h => ?_

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : E
x : 𝕜
⊢ ‖(toSpanSingleton 𝕜 x✝) x‖ ≤ ‖x✝‖ * ‖x‖

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x_1 : 𝕜), ‖(toSpanSingleton 𝕜 x) x_1‖ ≤ N * ‖x_1‖
⊢ ‖x‖ ≤ N

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
N : ℝ
x✝ : N ≥ 0
h : ‖x‖ * ‖1‖ ≤ N * ‖1‖
⊢ ‖x‖ ≤ N

Tactic:
exact (mul_le_mul_right (by simp)).mp h

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
N : ℝ
x✝ : N ≥ 0
h : ‖(toSpanSingleton 𝕜 x) 1‖ ≤ N * ‖1‖
⊢ ‖x‖ ≤ N

Tactic:
rw [toSpanSingleton_apply, norm_smul, mul_comm] at h

Result:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
N : ℝ
x✝ : N ≥ 0
h : ‖x‖ * ‖1‖ ≤ N * ‖1‖
⊢ ‖x‖ ≤ N

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : E
x : 𝕜
⊢ ‖(toSpanSingleton 𝕜 x✝) x‖ ≤ ‖x✝‖ * ‖x‖

Tactic:
rw [toSpanSingleton_apply, norm_smul, mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
/-- Given a cartesian morphism `φ : a ⟶ b` lying over `f : R ⟶ S` in `𝒳`, and two morphisms
`ψ ψ' : a' ⟶ a` such that `ψ ≫ φ = ψ' ≫ φ`. Then we must have `ψ = ψ'`. -/
protected lemma ext (φ : a ⟶ b) [IsCartesian p f φ] {a' : 𝒳} (ψ ψ' : a' ⟶ a)
    [IsHomLift p (𝟙 R) ψ] [IsHomLift p (𝟙 R) ψ'] (h : ψ ≫ φ = ψ' ≫ φ) : ψ = ψ'

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsCartesian f φ
a' : 𝒳
ψ ψ' : a' ⟶ a
inst✝¹ : p.IsHomLift (𝟙 R) ψ
inst✝ : p.IsHomLift (𝟙 R) ψ'
h : ψ ≫ φ = ψ' ≫ φ
⊢ ψ = ψ'

Tactic:
rw [map_uniq p f φ (ψ ≫ φ) ψ rfl, map_uniq p f φ (ψ ≫ φ) ψ' h.symm]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma yonedaEquiv_symm_naturality_left {X X' : C} (f : X' ⟶ X) (F : Cᵒᵖ ⥤ Type v₁)
    (x : F.obj ⟨X⟩) : yoneda.map f ≫ yonedaEquiv.symm x = yonedaEquiv.symm ((F.map f.op) x)

Proof state:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' : C
f : X' ⟶ X
F : Cᵒᵖ ⥤ Type v₁
x : F.obj (op X)
⊢ F.map (yonedaEquiv (yoneda.map f)).op x = F.map f.op x

Tactic:
erw [yonedaEquiv_yoneda_map]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' : C
f : X' ⟶ X
F : Cᵒᵖ ⥤ Type v₁
x : F.obj (op X)
⊢ yoneda.map f ≫ yonedaEquiv.symm x = yonedaEquiv.symm (F.map f.op x)

Tactic:
apply yonedaEquiv.injective

Result:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' : C
f : X' ⟶ X
F : Cᵒᵖ ⥤ Type v₁
x : F.obj (op X)
⊢ yonedaEquiv (yoneda.map f ≫ yonedaEquiv.symm x) = yonedaEquiv (yonedaEquiv.symm (F.map f.op x))

Proof state:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' : C
f : X' ⟶ X
F : Cᵒᵖ ⥤ Type v₁
x : F.obj (op X)
⊢ yonedaEquiv (yoneda.map f ≫ yonedaEquiv.symm x) = yonedaEquiv (yonedaEquiv.symm (F.map f.op x))

Tactic:
simp only [yonedaEquiv_comp, yoneda_obj_obj, yonedaEquiv_symm_app_apply, Equiv.apply_symm_apply]

Result:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' : C
f : X' ⟶ X
F : Cᵒᵖ ⥤ Type v₁
x : F.obj (op X)
⊢ F.map (yonedaEquiv (yoneda.map f)).op x = F.map f.op x
-- Mathlib/Topology/NhdsSet.lean
theorem nhdsSet_union (s t : Set X) : 𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ 𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t

Tactic:
simp only [nhdsSet, image_union, sSup_union]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem coe_image_subset (s : Set α) (t : Set s) : ((↑) : s → α) '' t ⊆ s :=
  fun x ⟨y, _, yvaleq⟩ => by
  rw [← yvaleq]; exact y.property

Proof state:
α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ ↑y ∈ s

Tactic:
exact y.property

Result:
no goals

Proof state:
α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ x ∈ s

Tactic:
rw [← yvaleq]

Result:
α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ ↑y ∈ s
-- Mathlib/Control/Traversable/Lemmas.lean
theorem traverse_eq_map_id' (f : β → γ) :
    traverse (m := Id) (pure ∘ f) = pure ∘ (map f : t β → t γ)

Proof state:
case h
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
β γ : Type u
f : β → γ
x✝ : t β
⊢ traverse (pure ∘ f) x✝ = (pure ∘ map f) x✝

Tactic:
exact traverse_eq_map_id _ _

Result:
no goals

Proof state:
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
β γ : Type u
f : β → γ
⊢ traverse (pure ∘ f) = pure ∘ map f

Tactic:
ext

Result:
case h
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
β γ : Type u
f : β → γ
x✝ : t β
⊢ traverse (pure ∘ f) x✝ = (pure ∘ map f) x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem utf8PrevAux_lt_of_pos : ∀ (cs : List Char) (i p : Pos), p ≠ 0 →
    (utf8PrevAux cs i p).1 < p.1
  | [], _, _, h =>
    Nat.lt_of_le_of_lt (Nat.zero_le _)
      (Nat.zero_lt_of_ne_zero (mt (congrArg Pos.mk) h))
  | c::cs, i, p, h => by
    simp [utf8PrevAux]
    apply iteInduction (motive := (Pos.byteIdx · < _)) <;> intro h'
    next => exact h' ▸ Nat.add_lt_add_left (Char.utf8Size_pos _) _
    next => exact utf8PrevAux_lt_of_pos _ _ _ h

Proof state:
case hpos
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
h' : i + c = p
⊢ i.byteIdx < p.byteIdx

case hneg
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
h' : ¬i + c = p
⊢ (utf8PrevAux cs (i + c) p).byteIdx < p.byteIdx

Tactic:
next => exact h' ▸ Nat.add_lt_add_left (Char.utf8Size_pos _) _

Result:
case hneg
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
h' : ¬i + c = p
⊢ (utf8PrevAux cs (i + c) p).byteIdx < p.byteIdx

Proof state:
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
h' : i + c = p
⊢ i.byteIdx < p.byteIdx

Tactic:
exact h' ▸ Nat.add_lt_add_left (Char.utf8Size_pos _) _

Result:
no goals

Proof state:
case hneg
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
h' : ¬i + c = p
⊢ (utf8PrevAux cs (i + c) p).byteIdx < p.byteIdx

Tactic:
next => exact utf8PrevAux_lt_of_pos _ _ _ h

Result:
no goals

Proof state:
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
h' : ¬i + c = p
⊢ (utf8PrevAux cs (i + c) p).byteIdx < p.byteIdx

Tactic:
exact utf8PrevAux_lt_of_pos _ _ _ h

Result:
no goals

Proof state:
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
⊢ (utf8PrevAux (c :: cs) i p).byteIdx < p.byteIdx

Tactic:
simp [utf8PrevAux]

Result:
c : Char
cs : List Char
i p : Pos
h : p ≠ 0
⊢ (ite (i + c = p) i (utf8PrevAux cs (i + c) p)).byteIdx < p.byteIdx
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformInducing.mk' {f : α → β}
    (h : ∀ s, s ∈ 𝓤 α ↔ ∃ t ∈ 𝓤 β, ∀ x y : α, (f x, f y) ∈ t → (x, y) ∈ s) : IsUniformInducing f :=
  ⟨by simp [eq_comm, Filter.ext_iff, subset_def, h]⟩

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ ∃ t ∈ 𝓤 β, ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s
⊢ comap (fun x => (f x.1, f x.2)) (𝓤 β) = 𝓤 α

Tactic:
simp [eq_comm, Filter.ext_iff, subset_def, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem cast_setWidth (h : v = v') (x : BitVec w) :
    (x.setWidth v).cast h = x.setWidth v'

Proof state:
v w : Nat
x : BitVec w
⊢ BitVec.cast ⋯ (setWidth v x) = setWidth v x

Tactic:
ext

Result:
case pred
v w : Nat
x : BitVec w
i✝ : Nat
a✝ : i✝ < v
⊢ (BitVec.cast ⋯ (setWidth v x)).getLsbD i✝ = (setWidth v x).getLsbD i✝

Proof state:
case pred
v w : Nat
x : BitVec w
i✝ : Nat
a✝ : i✝ < v
⊢ (BitVec.cast ⋯ (setWidth v x)).getLsbD i✝ = (setWidth v x).getLsbD i✝

Tactic:
simp

Result:
no goals

Proof state:
v v' w : Nat
h : v = v'
x : BitVec w
⊢ BitVec.cast h (setWidth v x) = setWidth v' x

Tactic:
subst h

Result:
v w : Nat
x : BitVec w
⊢ BitVec.cast ⋯ (setWidth v x) = setWidth v x
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
@[simp]
lemma support_subgraphOfAdj {u v : V} (h : G.Adj u v) :
    (G.subgraphOfAdj h).support = {u , v}

Proof state:
case h
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ (∃ w, (G.subgraphOfAdj h).Adj x✝ w) ↔ x✝ ∈ {u, v}

Tactic:
simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]

Result:
case h
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ (∃ w, u = x✝ ∧ v = w ∨ u = w ∧ v = x✝) ↔ x✝ ∈ {u, v}

Proof state:
case h
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ (∃ w, u = x✝ ∧ v = w ∨ u = w ∧ v = x✝) ↔ x✝ ∈ {u, v}

Tactic:
refine ⟨?_, fun h ↦ h.elim (fun hl ↦ ⟨v, .inl ⟨hl.symm, rfl⟩⟩) fun hr ↦ ⟨u, .inr ⟨rfl, hr.symm⟩⟩⟩

Result:
case h
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ (∃ w, u = x✝ ∧ v = w ∨ u = w ∧ v = x✝) → x✝ ∈ {u, v}

Proof state:
case h.intro
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ w✝ : V
hw : u = x✝ ∧ v = w✝ ∨ u = w✝ ∧ v = x✝
⊢ x✝ ∈ {u, v}

Tactic:
exact hw.elim (fun h1 ↦ .inl h1.1.symm) fun hr ↦ .inr hr.2.symm

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (G.subgraphOfAdj h).support = {u, v}

Tactic:
ext

Result:
case h
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj h).support ↔ x✝ ∈ {u, v}

Proof state:
case h
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj h).support ↔ x✝ ∈ {u, v}

Tactic:
rw [Subgraph.mem_support]

Result:
case h
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ (∃ w, (G.subgraphOfAdj h).Adj x✝ w) ↔ x✝ ∈ {u, v}

Proof state:
case h
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ (∃ w, u = x✝ ∧ v = w ∨ u = w ∧ v = x✝) → x✝ ∈ {u, v}

Tactic:
rintro ⟨_, hw⟩

Result:
case h.intro
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ w✝ : V
hw : u = x✝ ∧ v = w✝ ∨ u = w✝ ∧ v = x✝
⊢ x✝ ∈ {u, v}
-- Mathlib/Data/PFun.lean
theorem coe_preimage (f : α → β) (s : Set β) : (f : α →. β).preimage s = f ⁻¹' s

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set β
x✝ : α
⊢ x✝ ∈ (↑f).preimage s ↔ x✝ ∈ f ⁻¹' s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (↑f).preimage s = f ⁻¹' s

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set β
x✝ : α
⊢ x✝ ∈ (↑f).preimage s ↔ x✝ ∈ f ⁻¹' s
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffWithinAt.fderivWithin_right (hf : ContDiffWithinAt 𝕜 n f s x₀)
    (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 ≤ n) (hx₀s : x₀ ∈ s) :
    ContDiffWithinAt 𝕜 m (fderivWithin 𝕜 f s) s x₀ :=
  ContDiffWithinAt.fderivWithin
    (ContDiffWithinAt.comp (x₀, x₀) hf contDiffWithinAt_snd <| prod_subset_preimage_snd s s)
    contDiffWithinAt_id hs hmn hx₀s (by rw [preimage_id'])

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x₀ : E
m n : WithTop ℕ∞
hf : ContDiffWithinAt 𝕜 n f s x₀
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx₀s : x₀ ∈ s
⊢ s ⊆ (fun x => x) ⁻¹' s

Tactic:
rw [preimage_id']

Result:
no goals
-- Mathlib/Algebra/CharP/Two.lean
theorem two_zsmul (x : R) : (2 : ℤ) • x = 0

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x : R
⊢ 2 • x = 0

Tactic:
rw [two_zsmul, add_self_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Lie/Free.lean
theorem Rel.smulOfTower {S : Type*} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (t : S)
    (a b : lib R X) (h : Rel R X a b) : Rel R X (t • a) (t • b)

Proof state:
R : Type u
X : Type v
inst✝³ : CommRing R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
t : S
a b : lib R X
h : Rel R X a b
⊢ Rel R X (t • a) (t • b)

Tactic:
rw [← smul_one_smul R t a, ← smul_one_smul R t b]

Result:
R : Type u
X : Type v
inst✝³ : CommRing R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
t : S
a b : lib R X
h : Rel R X a b
⊢ Rel R X ((t • 1) • a) ((t • 1) • b)

Proof state:
R : Type u
X : Type v
inst✝³ : CommRing R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
t : S
a b : lib R X
h : Rel R X a b
⊢ Rel R X ((t • 1) • a) ((t • 1) • b)

Tactic:
exact h.smul _

Result:
no goals
-- Mathlib/RingTheory/WittVector/Frobenius.lean
theorem coeff_frobeniusFun (x : 𝕎 R) (n : ℕ) :
    coeff (frobeniusFun x) n = MvPolynomial.aeval x.coeff (frobeniusPoly p n)

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ x.frobeniusFun.coeff n = (aeval x.coeff) (frobeniusPoly p n)

Tactic:
rw [frobeniusFun, coeff_mk]

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem HasDerivAt.hasGradientAt (h : HasDerivAt g g' u) :
    HasGradientAt g (starRingEnd 𝕜 g') u

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g g' u
⊢ HasDerivAt g (((toDual 𝕜 𝕜) ((starRingEnd 𝕜) g')) 1) u

Tactic:
simpa

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g g' u
⊢ HasGradientAt g ((starRingEnd 𝕜) g') u

Tactic:
rw [hasGradientAt_iff_hasFDerivAt, hasFDerivAt_iff_hasDerivAt]

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g g' u
⊢ HasDerivAt g (((toDual 𝕜 𝕜) ((starRingEnd 𝕜) g')) 1) u
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_mul_cos_sq :
    ∫ x in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3

Proof state:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3

Tactic:
exact this

Result:
no goals

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3

Tactic:
have := @integral_sin_pow_odd_mul_cos_pow a b 0 2

Result:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ (2 * 0 + 1) * cos x ^ 2 = ∫ (u : ℝ) in cos b..cos a, u ^ 2 * (1 - u ^ 2) ^ 0
⊢ ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3

Proof state:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ (2 * 0 + 1) * cos x ^ 2 = ∫ (u : ℝ) in cos b..cos a, u ^ 2 * (1 - u ^ 2) ^ 0
⊢ ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3

Tactic:
norm_num at this

Result:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x * cos x ^ 2 = (cos a ^ 3 - cos b ^ 3) / 3
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma measurable_density_right (κ : Kernel α (γ × β)) (ν : Kernel α γ)
    {s : Set β} (hs : MeasurableSet s) (a : α) :
    Measurable (fun x ↦ density κ ν a x s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
s : Set β
hs : MeasurableSet s
a : α
⊢ Measurable ((fun p => κ.density ν p.1 p.2 s) ∘ fun x => (a, x))

Tactic:
exact (measurable_density κ ν hs).comp measurable_prod_mk_left

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
s : Set β
hs : MeasurableSet s
a : α
⊢ Measurable fun x => κ.density ν a x s

Tactic:
change Measurable ((fun (p : α × γ) ↦ density κ ν p.1 p.2 s) ∘ (fun x ↦ (a, x)))

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
s : Set β
hs : MeasurableSet s
a : α
⊢ Measurable ((fun p => κ.density ν p.1 p.2 s) ∘ fun x => (a, x))
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_eq_one_iff {a b : ℝ≥0∞} (hb₀ : b ≠ 0) (hb₁ : b ≠ ∞) : a / b = 1 ↔ a = b :=
  ⟨fun h => by rw [← (eq_div_iff hb₀ hb₁).mp h.symm, mul_one], fun h =>
    h.symm ▸ ENNReal.div_self hb₀ hb₁⟩

Proof state:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb₁ : b ≠ ⊤
h : a / b = 1
⊢ a = b

Tactic:
rw [← (eq_div_iff hb₀ hb₁).mp h.symm, mul_one]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Construction.lean
theorem app_eq (X : C) : (app τ) (W.Q.obj X) = τ.app X

Proof state:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
X : C
⊢ τ.app ((objEquiv W).invFun (W.Q.obj X)) = τ.app X

Tactic:
rfl

Result:
no goals

Proof state:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
X : C
⊢ app τ (W.Q.obj X) = τ.app X

Tactic:
simp only [app, eqToHom_refl, comp_id, id_comp]

Result:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
X : C
⊢ τ.app ((objEquiv W).invFun (W.Q.obj X)) = τ.app X