harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma fromSpec_app_of_le (V : X.Opens) (h : U ≤ V) :
    hU.fromSpec.app V = X.presheaf.map (homOfLE h).op ≫
      (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec _).presheaf.map (homOfLE le_top).op

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ ((Scheme.Hom.opensFunctor U.ι).map (eqToHom ⋯).op.unop).op ≫ (eqToHom ⋯).op) ≫
      (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
rfl

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map (homOfLE ⋯).op ≫
      (↑U).presheaf.map (eqToHom ⋯).op ≫
        (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
simp only [Scheme.Opens.toScheme_presheaf_map, Scheme.Opens.topIso_hom,
  Category.assoc, ← X.presheaf.map_comp_assoc]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ ((Scheme.Hom.opensFunctor U.ι).map (eqToHom ⋯).op.unop).op ≫ (eqToHom ⋯).op) ≫
      (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
⊢ Scheme.Hom.app hU.fromSpec V =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
have : U.ι ⁻¹ᵁ V = ⊤ := eq_top_iff.mpr fun x _ ↦ h x.2

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ Scheme.Hom.app hU.fromSpec V =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ Scheme.Hom.app hU.fromSpec V =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
rw [IsAffineOpen.fromSpec, Scheme.comp_app, Scheme.Opens.ι_app, Scheme.app_eq _ this,
  ← Scheme.Hom.appTop, IsAffineOpen.isoSpec_inv_appTop]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map (homOfLE ⋯).op ≫
      (↑U).presheaf.map (eqToHom ⋯).op ≫
        (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem map_ringChar {R : Type*} [CommRing R] [Nontrivial R] (χ : MulChar R R') :
    χ (ringChar R) = 0

Proof state:
R' : Type u_2
inst✝² : CommMonoidWithZero R'
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Nontrivial R
χ : MulChar R R'
⊢ χ ↑(ringChar R) = 0

Tactic:
rw [ringChar.Nat.cast_ringChar, χ.map_zero]

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

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

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem Multipliable.tendsto_cofinite_one (hf : Multipliable f) : Tendsto f cofinite (𝓝 1)

Proof state:
case intro
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
x : α
hx : x ∉ s
⊢ f x ∈ e

Tactic:
simpa using hs {x} (disjoint_singleton_left.2 hx)

Result:
no goals

Proof state:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ e ∈ Filter.map f cofinite

Tactic:
rw [Filter.mem_map]

Result:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ f ⁻¹' e ∈ cofinite

Proof state:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ f ⁻¹' e ∈ cofinite

Tactic:
rcases hf.vanishing he with ⟨s, hs⟩

Result:
case intro
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
⊢ f ⁻¹' e ∈ cofinite

Proof state:
case intro
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
⊢ f ⁻¹' e ∈ cofinite

Tactic:
refine s.eventually_cofinite_nmem.mono fun x hx ↦ ?_

Result:
case intro
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
x : α
hx : x ∉ s
⊢ f x ∈ e

Proof state:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
⊢ Tendsto f cofinite (𝓝 1)

Tactic:
intro e he

Result:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ e ∈ Filter.map f cofinite
-- Mathlib/Data/Seq/WSeq.lean
theorem dropn_think (s : WSeq α) (n) : drop (think s) n = (drop s n).think

Proof state:
α : Type u
s : WSeq α
n : ℕ
⊢ s.think.drop n = (s.drop n).think

Tactic:
induction n <;> simp [*, drop]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem comap_lift'_eq {m : γ → β} : comap m (f.lift' h) = f.lift' (preimage m ∘ h)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : γ → β
⊢ comap m (f.lift' h) = f.lift' (preimage m ∘ h)

Tactic:
simp only [Filter.lift', comap_lift_eq, comp_def, comap_principal]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.lean
theorem energy_nonneg : 0 ≤ P.energy G

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ 0 ≤ P.energy G

Tactic:
exact div_nonneg (Finset.sum_nonneg fun _ _ => sq_nonneg _) <| sq_nonneg _

Result:
no goals
-- Mathlib/CategoryTheory/WithTerminal.lean
theorem liftStar_lift_map {D : Type*} [Category D] {Z : D} (F : C ⥤ D) (M : ∀ x : C, Z ⟶ F.obj x)
    (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) (x : C) :
    (liftStar F M hM).hom ≫ (lift F M hM).map (starInitial.to (incl.obj x)) =
      M x ≫ (inclLift F M hM).hom.app x

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
x : C
⊢ (liftStar F M hM).hom ≫ (lift F M hM).map (starInitial.to (incl.obj x)) = M x ≫ (inclLift F M hM).hom.app x

Tactic:
erw [Category.id_comp, Category.comp_id]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
x : C
⊢ (lift F M hM).map (starInitial.to (incl.obj x)) = M x

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
x : C
⊢ (lift F M hM).map (starInitial.to (incl.obj x)) = M x

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma monotone_isoClosure : Monotone (isoClosure (C := C))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone isoClosure

Tactic:
intro P Q h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩

Result:
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
h : P ≤ Q
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ Q.isoClosure f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
h : P ≤ Q
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ Q.isoClosure f

Tactic:
exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem neLocus_self_add_right : neLocus f (f + g) = g.support

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f + g) = g.support

Tactic:
rw [← neLocus_zero_left, ← neLocus_add_left f 0 g, add_zero]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivWithinAt_of_mem_nhds (h : s ∈ 𝓝 x) :
    HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x

Tactic:
rw [HasFDerivAt, HasFDerivWithinAt, nhdsWithin_eq_nhds.mpr h]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
/-- When `C` has pullbacks, then `F.map f` is representable with respect to `F` for any
`f : a ⟶ b` in `C`. -/
lemma map [Full F] [HasPullbacks C] {a b : C} (f : a ⟶ b)
    [∀ c (g : c ⟶ b), PreservesLimit (cospan f g) F] :
    F.relativelyRepresentable (F.map f) := fun c g ↦ by
  obtain ⟨g, rfl⟩ := F.map_surjective g
  refine ⟨Limits.pullback f g, Limits.pullback.snd f g, F.map (Limits.pullback.fst f g), ?_⟩
  apply F.map_isPullback <| IsPullback.of_hasPullback f g

Proof state:
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : HasPullbacks C
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : c ⟶ b
⊢ ∃ b_1 snd fst, IsPullback fst (F.map snd) (F.map f) (F.map g)

Tactic:
refine ⟨Limits.pullback f g, Limits.pullback.snd f g, F.map (Limits.pullback.fst f g), ?_⟩

Result:
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : HasPullbacks C
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : c ⟶ b
⊢ IsPullback (F.map (pullback.fst f g)) (F.map (pullback.snd f g)) (F.map f) (F.map g)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : HasPullbacks C
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : F.obj c ⟶ F.obj b
⊢ ∃ b_1 snd fst, IsPullback fst (F.map snd) (F.map f) g

Tactic:
obtain ⟨g, rfl⟩ := F.map_surjective g

Result:
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : HasPullbacks C
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : c ⟶ b
⊢ ∃ b_1 snd fst, IsPullback fst (F.map snd) (F.map f) (F.map g)

Proof state:
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : HasPullbacks C
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : c ⟶ b
⊢ IsPullback (F.map (pullback.fst f g)) (F.map (pullback.snd f g)) (F.map f) (F.map g)

Tactic:
apply F.map_isPullback <| IsPullback.of_hasPullback f g

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Enum.lean
theorem enumOrd_surjective (hs : ¬ BddAbove s) {b : Ordinal} (hb : b ∈ s) :
    ∃ a, enumOrd s a = b

Proof state:
s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
hb : b ∈ s
⊢ ∃ a, enumOrd s a = b

Tactic:
rwa [← range_enumOrd hs] at hb

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem adjunction_counit_map_functor {X : TopCat} {U : Opens X} (V : Opens U) :
    U.isOpenEmbedding.isOpenMap.adjunction.counit.app (U.isOpenEmbedding.isOpenMap.functor.obj V) =
      eqToHom (by dsimp; rw [map_functor_eq V])

Proof state:
X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ ⋯.adjunction.counit.app (⋯.functor.obj V) = eqToHom ⋯

Tactic:
subsingleton

Result:
no goals

Proof state:
X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ ⋯.functor.obj ((map U.inclusion').obj (⋯.functor.obj V)) = ⋯.functor.obj V

Tactic:
rw [map_functor_eq V]

Result:
no goals

Proof state:
X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ (map U.inclusion' ⋙ ⋯.functor).obj (⋯.functor.obj V) = (𝟭 (Opens ↑X)).obj (⋯.functor.obj V)

Tactic:
dsimp

Result:
X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ ⋯.functor.obj ((map U.inclusion').obj (⋯.functor.obj V)) = ⋯.functor.obj V
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem Fin.circulant_mul_comm [CommSemigroup α] [AddCommMonoid α] :
    ∀ {n} (v w : Fin n → α), circulant v * circulant w = circulant w * circulant v
  | 0 => by simp [Injective]
  | _ + 1 => Matrix.circulant_mul_comm

Proof state:
α : Type u_1
inst✝¹ : CommSemigroup α
inst✝ : AddCommMonoid α
⊢ ∀ (v w : Fin 0 → α), circulant v * circulant w = circulant w * circulant v

Tactic:
simp [Injective]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem and_zero {x : BitVec w} : x &&& 0#w = 0#w

Proof state:
w : Nat
x : BitVec w
⊢ x &&& 0#w = 0#w

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (x &&& 0#w).getLsbD i = (0#w).getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (x &&& 0#w).getLsbD i = (0#w).getLsbD i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_zsmul_const [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b]
    (f : F) (n : ℤ) : f (n • a) = f 0 + n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℤ
⊢ f (n • a) = f 0 + n • b

Tactic:
simpa using map_add_zsmul f 0 n

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearMap.lean
@[simp]
lemma eq_restrictScalarsRange_iff (m : M') (n : N') (p : P') :
    p = restrictScalarsRange i j k hk B hB m n ↔ k p = B (i m) (j n)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : SMul S R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
inst✝¹² : Module S M
inst✝¹¹ : Module S N
inst✝¹⁰ : Module S P
inst✝⁹ : IsScalarTower S R M
inst✝⁸ : IsScalarTower S R N
inst✝⁷ : IsScalarTower S R P
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module S M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module S N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module S P'
inst✝ : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective ⇑k
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ range k
m : M'
n : N'
p : P'
⊢ p = ((i.restrictScalarsRange j k hk B hB) m) n ↔ k p = (B (i m)) (j n)

Tactic:
rw [← restrictScalarsRange_apply i j k hk B hB m n, hk.eq_iff]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem map_finset_prod {α F : Type*} [Fintype α] [EquivLike F M N] [MulEquivClass F M N] (f : F)
    (g : α → M) : f (∏ i : α, g i) = ∏ i : α, f (g i)

Proof state:
M : Type u_5
N : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
α : Type u_7
F : Type u_8
inst✝² : Fintype α
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
g : α → M
⊢ f (∏ i : α, g i) = ∏ i : α, f (g i)

Tactic:
simp [← finprod_eq_prod_of_fintype, MulEquivClass.map_finprod]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem mulVec_cramer (A : Matrix n n α) (b : n → α) : A *ᵥ cramer A b = A.det • b

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ A *ᵥ A.cramer b = A.det • b

Tactic:
rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec_assoc, one_mulVec]

Result:
no goals
-- Mathlib/Data/Multiset/Sym.lean
theorem sym2_map (f : α → β) (m : Multiset α) :
    (m.map f).sym2 = m.sym2.map (Sym2.map f) :=
  m.inductionOn fun xs => by simp [List.sym2_map]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
m : Multiset α
xs : List α
⊢ (map f ⟦xs⟧).sym2 = map (Sym2.map f) (Multiset.sym2 ⟦xs⟧)

Tactic:
simp [List.sym2_map]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem interior_sphere (x : E) {r : ℝ} (hr : r ≠ 0) : interior (sphere x r) = ∅

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (sphere x r) = ∅

Tactic:
rw [← frontier_closedBall x hr, interior_frontier isClosed_closedBall]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem toNat_add (hc : c < ℵ₀) (hd : d < ℵ₀) : toNat (c + d) = toNat c + toNat d

Proof state:
case intro.intro
c d : ℕ
⊢ toNat (↑c + ↑d) = toNat ↑c + toNat ↑d

Tactic:
norm_cast

Result:
no goals

Proof state:
case intro
d : Cardinal.{u}
hd : d < ℵ₀
c : ℕ
⊢ toNat (↑c + d) = toNat ↑c + toNat d

Tactic:
lift d to ℕ using hd

Result:
case intro.intro
c d : ℕ
⊢ toNat (↑c + ↑d) = toNat ↑c + toNat ↑d

Proof state:
c d : Cardinal.{u}
hc : c < ℵ₀
hd : d < ℵ₀
⊢ toNat (c + d) = toNat c + toNat d

Tactic:
lift c to ℕ using hc

Result:
case intro
d : Cardinal.{u}
hd : d < ℵ₀
c : ℕ
⊢ toNat (↑c + d) = toNat ↑c + toNat d
-- Mathlib/Algebra/Order/CauSeq/Completion.lean
theorem inv_mul_cancel {x : (Cauchy abv)} : x ≠ 0 → x⁻¹ * x = 1 :=
  Quotient.inductionOn x fun f hf => by
    simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf
    simp only [mk_eq_mk, hf, not_false_eq_true, inv_mk, mk_mul]
    exact Quotient.sound (CauSeq.inv_mul_cancel hf)

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ mk (f.inv ⋯ * f) = 1

Tactic:
exact Quotient.sound (CauSeq.inv_mul_cancel hf)

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ⟦f⟧ ≠ 0
⊢ (⟦f⟧)⁻¹ * ⟦f⟧ = 1

Tactic:
simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf

Result:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ (⟦f⟧)⁻¹ * ⟦f⟧ = 1

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ (⟦f⟧)⁻¹ * ⟦f⟧ = 1

Tactic:
simp only [mk_eq_mk, hf, not_false_eq_true, inv_mk, mk_mul]

Result:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ mk (f.inv ⋯ * f) = 1
-- Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean
theorem μ_forget_apply {G H : CommGrp.{u}} (p : G) (q : H) :
    Functor.LaxMonoidal.μ (forget CommGrp.{u}) G H (p, q) = (p, q)

Proof state:
case snd
G H : CommGrp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget CommGrp) G H (p, q)).2 = (p, q).2

Tactic:
exact congrFun (Functor.Monoidal.μ_snd (forget CommGrp.{u}) G H) (p, q)

Result:
no goals

Proof state:
case fst
G H : CommGrp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget CommGrp) G H (p, q)).1 = (p, q).1

Tactic:
exact congrFun (Functor.Monoidal.μ_fst (forget CommGrp.{u}) G H) (p, q)

Result:
no goals

Proof state:
G H : CommGrp
p : ↑G
q : ↑H
⊢ Functor.LaxMonoidal.μ (forget CommGrp) G H (p, q) = (p, q)

Tactic:
apply Prod.ext

Result:
case fst
G H : CommGrp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget CommGrp) G H (p, q)).1 = (p, q).1

case snd
G H : CommGrp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget CommGrp) G H (p, q)).2 = (p, q).2
-- Mathlib/Data/PNat/Xgcd.lean
theorem finish_isReduced : u.finish.IsReduced

Proof state:
u : XgcdType
⊢ u.finish.IsReduced

Tactic:
dsimp [IsReduced]

Result:
u : XgcdType
⊢ u.finish.ap = u.finish.bp

Proof state:
u : XgcdType
⊢ u.finish.ap = u.finish.bp

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn {f : α → ℝ} {s : Set α}
    (h : LocallyBoundedVariationOn f s) :
    ∃ p q : α → ℝ, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q

Proof state:
case inr.intro
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ ∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q

Tactic:
exact ⟨_, _, variationOnFromTo.monotoneOn h cs, variationOnFromTo.sub_self_monotoneOn h cs,
  (sub_sub_cancel _ _).symm⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
⊢ ∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨c, cs⟩)

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
h : LocallyBoundedVariationOn f ∅
⊢ ∃ p q, MonotoneOn p ∅ ∧ MonotoneOn q ∅ ∧ f = p - q

case inr.intro
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ ∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
h : LocallyBoundedVariationOn f ∅
⊢ ∃ p q, MonotoneOn p ∅ ∧ MonotoneOn q ∅ ∧ f = p - q

Tactic:
exact ⟨f, 0, subsingleton_empty.monotoneOn _, subsingleton_empty.monotoneOn _,
  (sub_zero f).symm⟩

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Ico (x y : ℝ) : Real.toEReal ⁻¹' Ico x y = Ico x y

Proof state:
x y : ℝ
⊢ Real.toEReal ⁻¹' Ico ↑x ↑y = Ico x y

Tactic:
simp_rw [← Ici_inter_Iio]

Result:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iio ↑y) = Ici x ∩ Iio y

Proof state:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iio ↑y) = Ici x ∩ Iio y

Tactic:
simp

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem csSup_image [Nonempty β] {s : Set β} (hs : s.Nonempty) {f : β → α}
    (hf : BddAbove (Set.range fun i : s ↦ f i)) (hf' : sSup ∅ ≤ ⨆ i : s, f i) :
    sSup (f '' s) = ⨆ a ∈ s, f a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty β
s : Set β
hs : s.Nonempty
f : β → α
hf : BddAbove (range fun i => f ↑i)
hf' : sSup ∅ ≤ ⨆ i, f ↑i
⊢ sSup (f '' s) = ⨆ a ∈ s, f a

Tactic:
rw [← ciSup_subtype'' hs hf hf', iSup, Set.image_eq_range]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
@[reassoc (attr := simp)]
lemma symmetry_fst [Full F] [Faithful F] : hf'.symmetry hg ≫ hg.fst' f' = hf'.snd g

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ hf'.symmetry hg ≫ hg.fst' f' = hf'.snd g

Tactic:
simp [symmetry]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem forall_eq_apply_imp_iff {f : α → β} {p : β → Prop} :
    (∀ b a, b = f a → p b) ↔ ∀ a, p (f a)

Proof state:
α : Sort ?u.16346
β : Sort u_1
f : α → β
p : β → Prop
⊢ (∀ (b : β) (a : α), b = f a → p b) ↔ ∀ (a : α), p (f a)

Tactic:
simp [forall_comm]

Result:
no goals