harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Card.lean
theorem surj_on_of_inj_on_of_ncard_le {t : Set β} (f : ∀ a ∈ s, β) (hf : ∀ a ha, f a ha ∈ t)
    (hinj : ∀ a₁ a₂ ha₁ ha₂, f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂) (hst : t.ncard ≤ s.ncard)
    (ht : t.Finite

Proof state:
case convert_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : autoParam t.Finite _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h => f a ⋯
⊢ ∀ (a : α) (ha : a ∈ s.toFinset), f'' a ha ∈ t.toFinset

Tactic:
simp [f'', hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : autoParam t.Finite _auto✝
b : β
hb : b ∈ t
⊢ ∃ a, ∃ (ha : a ∈ s), b = f a ha

Tactic:
set f' : s → t := fun x ↦ ⟨f x.1 x.2, hf _ _⟩

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : autoParam t.Finite _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
⊢ ∃ a, ∃ (ha : a ∈ s), b = f a ha
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem integrable_coeFn {f : α →ₘ[μ] β} : MeasureTheory.Integrable f μ ↔ Integrable f

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α →ₘ[μ] β
⊢ MeasureTheory.Integrable (↑f) μ ↔ f.Integrable

Tactic:
rw [← integrable_mk, mk_coeFn]

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
theorem eraseNone_empty : eraseNone (∅ : Finset (Option α)) = ∅

Proof state:
α : Type u_1
⊢ eraseNone ∅ = ∅

Tactic:
ext

Result:
case h
α : Type u_1
a✝ : α
⊢ a✝ ∈ eraseNone ∅ ↔ a✝ ∈ ∅

Proof state:
case h
α : Type u_1
a✝ : α
⊢ a✝ ∈ eraseNone ∅ ↔ a✝ ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem lt_sup_iff : a < s.sup f ↔ ∃ b ∈ s, a < f b

Proof state:
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < s.sup f ↔ ∃ b ∈ s, a < f b

Tactic:
apply Iff.intro

Result:
case mp
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < s.sup f → ∃ b ∈ s, a < f b

case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (∃ b ∈ s, a < f b) → a < s.sup f

Proof state:
case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : c ∉ t
ih : a < t.sup f → ∃ b ∈ t, a < f b
⊢ a < (cons c t hc).sup f → ∃ b ∈ cons c t hc, a < f b

Tactic:
rw [sup_cons, lt_sup_iff]

Result:
case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : c ∉ t
ih : a < t.sup f → ∃ b ∈ t, a < f b
⊢ a < f c ∨ a < t.sup f → ∃ b ∈ cons c t hc, a < f b

Proof state:
case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (∃ b ∈ s, a < f b) → a < s.sup f

Tactic:
exact fun ⟨b, hb, hlt⟩ => lt_of_lt_of_le hlt (le_sup hb)

Result:
no goals

Proof state:
case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : c ∉ t
ih : a < t.sup f → ∃ b ∈ t, a < f b
⊢ a < f c ∨ a < t.sup f → ∃ b ∈ cons c t hc, a < f b

Tactic:
exact fun
| Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
| Or.inr h => let ⟨b, hb, hlt⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hlt⟩

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem isPiSystem_Ixx_mem {Ixx : α → α → Set α} {p : α → α → Prop}
    (Hne : ∀ {a b}, (Ixx a b).Nonempty → p a b)
    (Hi : ∀ {a₁ b₁ a₂ b₂}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)) (s t : Set α) :
    IsPiSystem { S | ∃ᵉ (l ∈ s) (u ∈ t), p l u ∧ Ixx l u = S }

Proof state:
α : Type u_1
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (a₁ ⊔ a₂) (b₁ ⊓ b₂)
s t : Set α
⊢ IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S}

Tactic:
rintro _ ⟨l₁, hls₁, u₁, hut₁, _, rfl⟩ _ ⟨l₂, hls₂, u₂, hut₂, _, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (a₁ ⊔ a₂) (b₁ ⊓ b₂)
s t : Set α
l₁ : α
hls₁ : l₁ ∈ s
u₁ : α
hut₁ : u₁ ∈ t
left✝¹ : p l₁ u₁
l₂ : α
hls₂ : l₂ ∈ s
u₂ : α
hut₂ : u₂ ∈ t
left✝ : p l₂ u₂
⊢ (Ixx l₁ u₁ ∩ Ixx l₂ u₂).Nonempty → Ixx l₁ u₁ ∩ Ixx l₂ u₂ ∈ {S | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S}

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (a₁ ⊔ a₂) (b₁ ⊓ b₂)
s t : Set α
l₁ : α
hls₁ : l₁ ∈ s
u₁ : α
hut₁ : u₁ ∈ t
left✝¹ : p l₁ u₁
l₂ : α
hls₂ : l₂ ∈ s
u₂ : α
hut₂ : u₂ ∈ t
left✝ : p l₂ u₂
⊢ (Ixx l₁ u₁ ∩ Ixx l₂ u₂).Nonempty → Ixx l₁ u₁ ∩ Ixx l₂ u₂ ∈ {S | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S}

Tactic:
simp only [Hi]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (a₁ ⊔ a₂) (b₁ ⊓ b₂)
s t : Set α
l₁ : α
hls₁ : l₁ ∈ s
u₁ : α
hut₁ : u₁ ∈ t
left✝¹ : p l₁ u₁
l₂ : α
hls₂ : l₂ ∈ s
u₂ : α
hut₂ : u₂ ∈ t
left✝ : p l₂ u₂
⊢ (Ixx (l₁ ⊔ l₂) (u₁ ⊓ u₂)).Nonempty → Ixx (l₁ ⊔ l₂) (u₁ ⊓ u₂) ∈ {S | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S}

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (a₁ ⊔ a₂) (b₁ ⊓ b₂)
s t : Set α
l₁ : α
hls₁ : l₁ ∈ s
u₁ : α
hut₁ : u₁ ∈ t
left✝¹ : p l₁ u₁
l₂ : α
hls₂ : l₂ ∈ s
u₂ : α
hut₂ : u₂ ∈ t
left✝ : p l₂ u₂
⊢ (Ixx (l₁ ⊔ l₂) (u₁ ⊓ u₂)).Nonempty → Ixx (l₁ ⊔ l₂) (u₁ ⊓ u₂) ∈ {S | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S}

Tactic:
exact fun H => ⟨l₁ ⊔ l₂, sup_ind l₁ l₂ hls₁ hls₂, u₁ ⊓ u₂, inf_ind u₁ u₂ hut₁ hut₂, Hne H, rfl⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem isTrail_copy {u v u' v'} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
    (p.copy hu hv).IsTrail ↔ p.IsTrail

Proof state:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).IsTrail ↔ p.IsTrail

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).IsTrail ↔ p.IsTrail

Proof state:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).IsTrail ↔ p.IsTrail

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem factors_prod_eq_basis (x : π C (· ∈ s)) :
    (factors C s x).prod = spanFinBasis C s x

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x : ↑(π C fun x => x ∈ s)
⊢ (factors C s x).prod = spanFinBasis C s x

Tactic:
ext y

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
⊢ (factors C s x).prod y = (spanFinBasis C s x) y

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
⊢ (factors C s x).prod y = (spanFinBasis C s x) y

Tactic:
dsimp [spanFinBasis]

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
⊢ (factors C s x).prod y = if y = x then 1 else 0

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
⊢ (factors C s x).prod y = if y = x then 1 else 0

Tactic:
split_ifs with h <;> [exact factors_prod_eq_basis_of_eq _ _ h;
  exact factors_prod_eq_basis_of_ne _ _ h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
/--
`P` is local at the target if
1. `P` respects isomorphisms.
2. If `P` holds for `f : X ⟶ Y`, then `P` holds for `f ∣_ U` for any `U`.
3. If `P` holds for `f ∣_ U` for an open cover `U` of `Y`, then `P` holds for `f`.
-/
protected lemma mk' {P : MorphismProperty Scheme} [P.RespectsIso]
    (restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U))
    (of_sSup_eq_top :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ →
        (∀ i, P (f ∣_ U i)) → P f) :
    IsLocalAtTarget P

Proof state:
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f
⊢ IsLocalAtTarget P

Tactic:
refine ⟨inferInstance, fun {X Y} f 𝒰 ↦ ⟨?_, fun H ↦ of_sSup_eq_top f _ 𝒰.iSup_opensRange ?_⟩⟩

Result:
case refine_1
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
⊢ P f → ∀ (i : 𝒰.1), P (Scheme.Cover.pullbackHom 𝒰 f i)

case refine_2
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.1), P (Scheme.Cover.pullbackHom 𝒰 f i)
⊢ ∀ (i : 𝒰.J), P (f ∣_ Scheme.Hom.opensRange (𝒰.map i))

Proof state:
case refine_1
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
⊢ P f → ∀ (i : 𝒰.1), P (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
exact fun H i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mp (restrict _ _ H)

Result:
no goals

Proof state:
case refine_2
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.1), P (Scheme.Cover.pullbackHom 𝒰 f i)
⊢ ∀ (i : 𝒰.J), P (f ∣_ Scheme.Hom.opensRange (𝒰.map i))

Tactic:
exact fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (H i)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem takeWhile_replicate_eq_filter (p : α → Bool) :
    (replicate n a).takeWhile p = (replicate n a).filter p

Proof state:
α : Type u_1
n : Nat
a : α
p : α → Bool
⊢ takeWhile p (replicate n a) = filter p (replicate n a)

Tactic:
induction n with
| zero => simp
| succ n ih =>
  simp only [replicate_succ, takeWhile_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case succ
α : Type u_1
a : α
p : α → Bool
n : Nat
ih : takeWhile p (replicate n a) = filter p (replicate n a)
⊢ takeWhile p (replicate (n + 1) a) = filter p (replicate (n + 1) a)

Tactic:
simp only [replicate_succ, takeWhile_cons]

Result:
case succ
α : Type u_1
a : α
p : α → Bool
n : Nat
ih : takeWhile p (replicate n a) = filter p (replicate n a)
⊢ (if p a = true then a :: takeWhile p (replicate n a) else []) = filter p (a :: replicate n a)

Proof state:
case zero
α : Type u_1
a : α
p : α → Bool
⊢ takeWhile p (replicate 0 a) = filter p (replicate 0 a)

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
a : α
p : α → Bool
n : Nat
ih : takeWhile p (replicate n a) = filter p (replicate n a)
⊢ (if p a = true then a :: takeWhile p (replicate n a) else []) = filter p (a :: replicate n a)

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
    preserves finite coproducts. -/
lemma preservesCoproduct_of_preservesBiproduct {f : J → C} [PreservesBiproduct f F] :
    PreservesColimit (Discrete.functor f) F where
  preserves {c} hc :=
    ⟨IsColimit.ofIsoColimit
        ((IsColimit.precomposeHomEquiv (Discrete.compNatIsoDiscrete _ _) _).symm
          (isBilimitOfPreserves F (biconeIsBilimitOfColimitCoconeOfIsColimit hc)).isColimit) <|
      Cocones.ext (Iso.refl _) (by rintro ⟨⟩; simp)⟩

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : PreservesBiproduct f F
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ ∀ (j : Discrete J),
    ((Cocones.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
                (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).ι.app
          j ≫
        (Iso.refl
            ((Cocones.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
                (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).pt).hom =
      (F.mapCocone c).ι.app j

Tactic:
rintro ⟨⟩

Result:
case mk
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : PreservesBiproduct f F
c : Cocone (Discrete.functor f)
hc : IsColimit c
as✝ : J
⊢ ((Cocones.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
              (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).ι.app
        { as := as✝ } ≫
      (Iso.refl
          ((Cocones.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
              (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).pt).hom =
    (F.mapCocone c).ι.app { as := as✝ }

Proof state:
case mk
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : PreservesBiproduct f F
c : Cocone (Discrete.functor f)
hc : IsColimit c
as✝ : J
⊢ ((Cocones.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
              (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).ι.app
        { as := as✝ } ≫
      (Iso.refl
          ((Cocones.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
              (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).pt).hom =
    (F.mapCocone c).ι.app { as := as✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem balancedCore_mem_nhds_zero (hU : U ∈ 𝓝 (0 : E)) : balancedCore 𝕜 U ∈ 𝓝 (0 : E)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : y • V ∈ 𝓝 0
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
⊢ ‖a * y‖ < r

Tactic:
rw [norm_mul, ← one_mul r]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : y • V ∈ 𝓝 0
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
⊢ ‖a‖ * ‖y‖ < 1 * r

Proof state:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : y • V ∈ 𝓝 0
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ (a * y) • V ⊆ U

Tactic:
rintro _ ⟨z, hz, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : y • V ∈ 𝓝 0
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
⊢ (fun x => (a * y) • x) z ∈ U

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.1 • x.2) (𝓝 (0, 0)) (𝓝 0)
⊢ ∃ r V, 0 < r ∧ V ∈ 𝓝 0 ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U

Tactic:
simpa only [← Prod.exists', ← Prod.forall', ← and_imp, ← and_assoc, exists_prop] using
  h.basis_left (NormedAddCommGroup.nhds_zero_basis_norm_lt.prod_nhds (𝓝 _).basis_sets) U hU

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem bneEqOfEqEq {a b c d : Nat} (p : (a = b) = (c = d)) : (a != b) = (c != d)

Proof state:
a b c d : Nat
p : (a = b) = (c = d)
⊢ (a != b) = (c != d)

Tactic:
simp only [bne, beqEqOfEqEq p]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem equiv_block_det (M : Matrix m m R) {p q : m → Prop} [DecidablePred p] [DecidablePred q]
    (e : ∀ x, q x ↔ p x) : (toSquareBlockProp M p).det = (toSquareBlockProp M q).det

Proof state:
m : Type u_3
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
M : Matrix m m R
p q : m → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : ∀ (x : m), q x ↔ p x
⊢ (M.toSquareBlockProp p).det = (M.toSquareBlockProp q).det

Tactic:
convert Matrix.det_reindex_self (Equiv.subtypeEquivRight e) (toSquareBlockProp M q)

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Torsion/Finite.lean
theorem Module.finrank_eq_zero_iff_isTorsion [StrongRankCondition R] [Module.Finite R M] :
    finrank R M = 0 ↔ Module.IsTorsion R M

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ IsTorsion R M

Tactic:
rw [← rank_eq_zero_iff_isTorsion (R := R), ← finrank_eq_rank]

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ ↑(finrank R M) = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ ↑(finrank R M) = 0

Tactic:
norm_cast

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma triangle (X Y : LocalizedMonoidal L W ε) :
    (α_ X (𝟙_ _) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Proof state:
case h.e'_3.h
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
        L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y =
    ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (L'.obj X' ⊗ L'.obj (𝟙_ C)) ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y
this :
  ((e₁.symm.hom ⊗ ε.symm.hom) ⊗ e₂.symm.hom) ≫
      (α_ (L'.obj X') (L.obj (𝟙_ C)) (L'.obj Y')).hom ≫ (e₁.symm.inv ⊗ ε.symm.inv ⊗ e₂.symm.inv) =
    (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom
e_1✝ : ((X ⊗ 𝟙_ (LocalizedMonoidal L W ε)) ⊗ Y ⟶ X ⊗ Y) = ((X ⊗ unit) ⊗ Y ⟶ X ⊗ Y)
⊢ (ρ_ X).hom ▷ Y =
    ((e₁.inv ⊗ ε.inv) ⊗ e₂.inv) ≫
      (L'.obj X' ⊗ L'.obj (𝟙_ C)) ◁ e₂.hom ≫ ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ Y ≫ e₁.hom ▷ Y

Tactic:
exact triangle_aux₃ _ _ _ e₁ e₂

Result:
no goals

Proof state:
case intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
obtain ⟨Y', ⟨e₂⟩⟩ : ∃ X₂, Nonempty ((L').obj X₂ ≅ Y) := ⟨_, ⟨(L').objObjPreimageIso Y⟩⟩

Result:
case intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y
-- Mathlib/Algebra/Polynomial/Div.lean
/-- See `Polynomial.mul_self_modByMonic` for the other multiplication order. That version, unlike
this one, requires commutativity. -/
@[simp]
lemma self_mul_modByMonic (hq : q.Monic) : (q * p) %ₘ q = 0

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ q * p %ₘ q = 0

Tactic:
rw [modByMonic_eq_zero_iff_dvd hq]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ q ∣ q * p

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ q ∣ q * p

Tactic:
exact dvd_mul_right q p

Result:
no goals