harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_xor {x y : BitVec w} :
    (x ^^^ y).getMsbD i = (x.getMsbD i ^^ y.getMsbD i)

Proof state:
w i : Nat
x y : BitVec w
⊢ (decide (i < w) && (x ^^^ y).getLsbD (w - 1 - i)) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (i < w) && y.getLsbD (w - 1 - i))

Tactic:
by_cases h : i < w <;> simp [h]

Result:
no goals

Proof state:
w i : Nat
x y : BitVec w
⊢ (x ^^^ y).getMsbD i = (x.getMsbD i ^^ y.getMsbD i)

Tactic:
simp only [getMsbD]

Result:
w i : Nat
x y : BitVec w
⊢ (decide (i < w) && (x ^^^ y).getLsbD (w - 1 - i)) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (i < w) && y.getLsbD (w - 1 - i))
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem rank_range_of_surjective (f : M →ₗ[R] M') (h : Surjective f) :
    Module.rank R (LinearMap.range f) = Module.rank R M'

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ Module.rank R ↥(LinearMap.range f) = Module.rank R M'

Tactic:
rw [LinearMap.range_eq_top.2 h, rank_top]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem isRotated_nil_iff' : [] ~r l ↔ [] = l

Proof state:
α : Type u
l : List α
⊢ [] ~r l ↔ [] = l

Tactic:
rw [isRotated_comm, isRotated_nil_iff, eq_comm]

Result:
no goals
-- Mathlib/Logic/Nontrivial/Defs.lean
lemma not_subsingleton_iff_nontrivial : ¬ Subsingleton α ↔ Nontrivial α

Proof state:
α : Type u_1
⊢ ¬Subsingleton α ↔ Nontrivial α

Tactic:
rw [← not_nontrivial_iff_subsingleton, Classical.not_not]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem sup_lt {a b c : CauSeq α abs} (ha : a < c) (hb : b < c) : a ⊔ b < c

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a < c
hb : b < c
⊢ a ⊔ b < c

Tactic:
obtain ⟨⟨εa, εa0, ia, ha⟩, ⟨εb, εb0, ib, hb⟩⟩ := ha, hb

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ ↑(c - a) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(c - b) j
⊢ a ⊔ b < c

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ ↑(c - a) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(c - b) j
i : ℕ
hi : i ≥ ia ⊔ ib
⊢ εa ⊓ εb ≤ ↑(c - a ⊔ b) i

Tactic:
have := min_le_min (ha _ (sup_le_iff.mp hi).1) (hb _ (sup_le_iff.mp hi).2)

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ ↑(c - a) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(c - b) j
i : ℕ
hi : i ≥ ia ⊔ ib
this : εa ⊓ εb ≤ ↑(c - a) i ⊓ ↑(c - b) i
⊢ εa ⊓ εb ≤ ↑(c - a ⊔ b) i

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ ↑(c - a) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(c - b) j
i : ℕ
hi : i ≥ ia ⊔ ib
this : εa ⊓ εb ≤ ↑(c - a) i ⊓ ↑(c - b) i
⊢ εa ⊓ εb ≤ ↑(c - a ⊔ b) i

Tactic:
exact this.trans_eq (min_sub_sub_left _ _ _)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ ↑(c - a) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(c - b) j
⊢ a ⊔ b < c

Tactic:
refine ⟨εa ⊓ εb, lt_inf_iff.mpr ⟨εa0, εb0⟩, ia ⊔ ib, fun i hi => ?_⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ ↑(c - a) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(c - b) j
i : ℕ
hi : i ≥ ia ⊔ ib
⊢ εa ⊓ εb ≤ ↑(c - a ⊔ b) i
-- Mathlib/Probability/Kernel/Basic.lean
/-- See `swap_apply` for a partially applied version of this lemma. -/
lemma swap_apply' (ab : α × β) {s : Set (β × α)} (hs : MeasurableSet s) :
    swap α β ab s = s.indicator 1 ab.swap

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ab : α × β
s : Set (β × α)
hs : MeasurableSet s
⊢ ((swap α β) ab) s = s.indicator 1 ab.swap

Tactic:
rw [swap_apply, Measure.dirac_apply' _ hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (l : Vector γ n) (l' : Vector δ n) :
    map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l'

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
l : Array γ
l' : Array δ
h : l'.size = l.size
⊢ map f (zipWith g { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }) =
    zipWith (fun x y => f (g x y)) { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }

Tactic:
simp [Array.map_zipWith]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
δ : Type u_4
f : α → β
g : γ → δ → α
l : Vector γ n
l' : Vector δ n
⊢ map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l'

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
l : Array γ
l' : Vector δ l.size
⊢ map f (zipWith g { toArray := l, size_toArray := ⋯ } l') =
    zipWith (fun x y => f (g x y)) { toArray := l, size_toArray := ⋯ } l'

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
l : Array γ
l' : Vector δ l.size
⊢ map f (zipWith g { toArray := l, size_toArray := ⋯ } l') =
    zipWith (fun x y => f (g x y)) { toArray := l, size_toArray := ⋯ } l'

Tactic:
rcases l' with ⟨l', h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
l : Array γ
l' : Array δ
h : l'.size = l.size
⊢ map f (zipWith g { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }) =
    zipWith (fun x y => f (g x y)) { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
lemma of_isPullback {UX UY : Scheme.{u}} {iY : UY ⟶ Y} [IsOpenImmersion iY]
    {iX : UX ⟶ X} {f' : UX ⟶ UY} (h : IsPullback iX f' f iY) (H : P f) : P f'

Proof state:
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
UX UY : Scheme
iY : UY ⟶ Y
inst✝ : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
H : P f
⊢ P f'

Tactic:
rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_snd]

Result:
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
UX UY : Scheme
iY : UY ⟶ Y
inst✝ : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
H : P f
⊢ P (pullback.snd f iY)

Proof state:
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
UX UY : Scheme
iY : UY ⟶ Y
inst✝ : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
H : P f
⊢ P (pullback.snd f iY)

Tactic:
exact (iff_of_openCover' f (Y.affineCover.add iY)).mp H .none

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousAt_tsum {f : ι → α → ℝ≥0∞} (h : ∀ i, LowerSemicontinuousAt (f i) x) :
    LowerSemicontinuousAt (fun x' => ∑' i, f i x') x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun x' => ∑' (i : ι), f i x') x

Tactic:
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *

Result:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') univ x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
ι : Type u_3
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') univ x

Tactic:
exact lowerSemicontinuousWithinAt_tsum h

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infinite_of_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) (hi : Infinitesimal x⁻¹) :
    Infinite x

Proof state:
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
⊢ x.Infinite

Tactic:
rcases lt_or_gt_of_ne h0 with hn | hp

Result:
case inl
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hn : x < 0
⊢ x.Infinite

case inr
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hp : x > 0
⊢ x.Infinite

Proof state:
case inl
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hn : x < 0
⊢ x.Infinite

Tactic:
exact Or.inr (infiniteNeg_iff_infinitesimal_inv_neg.mpr ⟨hi, inv_lt_zero.mpr hn⟩)

Result:
no goals

Proof state:
case inr
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hp : x > 0
⊢ x.Infinite

Tactic:
exact Or.inl (infinitePos_iff_infinitesimal_inv_pos.mpr ⟨hi, inv_pos.mpr hp⟩)

Result:
no goals
-- Mathlib/Data/FunLike/Basic.lean
theorem coe_fn_eq {f g : F} : (f : ∀ a : α, β a) = (g : ∀ a : α, β a) ↔ f = g :=
  ⟨fun h ↦ DFunLike.coe_injective' h, fun h ↦ by cases h; rfl⟩

Proof state:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
h : f = g
⊢ ⇑f = ⇑g

Tactic:
cases h

Result:
case refl
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f : F
⊢ ⇑f = ⇑f

Proof state:
case refl
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f : F
⊢ ⇑f = ⇑f

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mlieBracketWithin_add_right
    (hW : MDifferentiableWithinAt I I.tangent (fun x ↦ (W x : TangentBundle I M)) s x)
    (hW₁ : MDifferentiableWithinAt I I.tangent (fun x ↦ (W₁ x : TangentBundle I M)) s x)
    (hs : UniqueMDiffWithinAt I s x) :
    mlieBracketWithin I V (W + W₁) s x =
      mlieBracketWithin I V W s x + mlieBracketWithin I V W₁ s x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) s x
hW₁ : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W₁ x }) s x
hs : UniqueMDiffWithinAt I s x
⊢ mlieBracketWithin I V (W + W₁) s x = mlieBracketWithin I V W s x + mlieBracketWithin I V W₁ s x

Tactic:
rw [mlieBracketWithin_swap, Pi.neg_apply, mlieBracketWithin_add_left hW hW₁ hs,
  mlieBracketWithin_swap (V := V), mlieBracketWithin_swap (V := V), Pi.neg_apply, Pi.neg_apply]

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) s x
hW₁ : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W₁ x }) s x
hs : UniqueMDiffWithinAt I s x
⊢ -(mlieBracketWithin I W V s x + mlieBracketWithin I W₁ V s x) =
    -mlieBracketWithin I W V s x + -mlieBracketWithin I W₁ V s x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) s x
hW₁ : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W₁ x }) s x
hs : UniqueMDiffWithinAt I s x
⊢ -(mlieBracketWithin I W V s x + mlieBracketWithin I W₁ V s x) =
    -mlieBracketWithin I W V s x + -mlieBracketWithin I W₁ V s x

Tactic:
abel

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem strictMonoOn_projIic : StrictMonoOn (projIic b) (Iic b) := fun x hx y hy hxy => by
  simpa only [projIic_of_mem, hx, hy]

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b x : α
hx : x ∈ Iic b
y : α
hy : y ∈ Iic b
hxy : x < y
⊢ projIic b x < projIic b y

Tactic:
simpa only [projIic_of_mem, hx, hy]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_of_isBounded {s : Set E} (h : Bornology.IsBounded s) :
    Bornology.IsVonNBounded 𝕜 s

Proof state:
case intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ (normSeminorm 𝕜 E).ball 0 r
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 ((normSeminorm 𝕜 E).ball 0 i) s

Tactic:
exact fun ε hε ↦ ((normSeminorm 𝕜 E).ball_zero_absorbs_ball_zero hε).mono_right hr

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Metric.ball 0 r
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
rw [Metric.nhds_basis_ball.isVonNBounded_iff]

Result:
case intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Metric.ball 0 r
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Metric.ball 0 i) s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
rcases h.subset_ball 0 with ⟨r, hr⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Metric.ball 0 r
⊢ Bornology.IsVonNBounded 𝕜 s

Proof state:
case intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Metric.ball 0 r
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Metric.ball 0 i) s

Tactic:
rw [← ball_normSeminorm 𝕜 E] at hr ⊢

Result:
case intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ (normSeminorm 𝕜 E).ball 0 r
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 ((normSeminorm 𝕜 E).ball 0 i) s
-- Mathlib/GroupTheory/Exponent.lean
theorem exponent_dvd_of_monoidHom (e : G →* H) (e_inj : Function.Injective e) :
    Monoid.exponent G ∣ Monoid.exponent H :=
  exponent_dvd_of_forall_pow_eq_one fun g => e_inj (by
    rw [map_pow, pow_exponent_eq_one, map_one])

Proof state:
G : Type u
inst✝¹ : Monoid G
H : Type u_1
inst✝ : Monoid H
e : G →* H
e_inj : Function.Injective ⇑e
g : G
⊢ e (g ^ exponent H) = e 1

Tactic:
rw [map_pow, pow_exponent_eq_one, map_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean
/-- If the coequalizer comparison map for `G` at `(f,g)` is an isomorphism, then `G` preserves the
coequalizer of `(f,g)`.
-/
lemma of_iso_comparison [i : IsIso (coequalizerComparison f g G)] :
    PreservesColimit (parallelPair f g) G

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
i : IsIso (coequalizerComparison f g G)
⊢ IsColimit (Cofork.ofπ (G.map (coequalizer.π f g)) ⋯)

Tactic:
exact
  @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (parallelPair (G.map f) (G.map g))) i

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
i : IsIso (coequalizerComparison f g G)
⊢ IsColimit (G.mapCocone (Cofork.ofπ (coequalizer.π f g) ⋯))

Tactic:
apply (isColimitMapCoconeCoforkEquiv _ _).symm _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
i : IsIso (coequalizerComparison f g G)
⊢ IsColimit (Cofork.ofπ (G.map (coequalizer.π f g)) ⋯)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
i : IsIso (coequalizerComparison f g G)
⊢ PreservesColimit (parallelPair f g) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (coequalizerIsCoequalizer f g)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
i : IsIso (coequalizerComparison f g G)
⊢ IsColimit (G.mapCocone (Cofork.ofπ (coequalizer.π f g) ⋯))
-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
/-- Rank-nullity theorem using `finrank` and subtraction. -/
lemma Submodule.finrank_quotient [Module.Finite R M] {S : Type*} [Ring S] [SMul R S] [Module S M]
    [IsScalarTower R S M] (N : Submodule S M) : finrank R (M ⧸ N) = finrank R M - finrank R N

Proof state:
R : Type u_2
M : Type u
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : HasRankNullity.{u, u_2} R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Module.Finite R M
S : Type u_1
inst✝³ : Ring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
N : Submodule S M
⊢ finrank R (M ⧸ N) = finrank R (M ⧸ restrictScalars R N) + finrank R ↥(restrictScalars R N) - finrank R ↥N

Tactic:
exact Nat.eq_sub_of_add_eq rfl

Result:
no goals

Proof state:
R : Type u_2
M : Type u
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : HasRankNullity.{u, u_2} R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Module.Finite R M
S : Type u_1
inst✝³ : Ring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
N : Submodule S M
⊢ finrank R (M ⧸ N) = finrank R M - finrank R ↥N

Tactic:
rw [← (N.restrictScalars R).finrank_quotient_add_finrank]

Result:
R : Type u_2
M : Type u
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : HasRankNullity.{u, u_2} R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Module.Finite R M
S : Type u_1
inst✝³ : Ring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
N : Submodule S M
⊢ finrank R (M ⧸ N) = finrank R (M ⧸ restrictScalars R N) + finrank R ↥(restrictScalars R N) - finrank R ↥N
-- Mathlib/RingTheory/EssentialFiniteness.lean
lemma EssFiniteType.of_isLocalization (M : Submonoid R) [IsLocalization M S] :
    EssFiniteType R S

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : S
⊢ ∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a

Tactic:
obtain ⟨⟨x, t⟩, e⟩ := IsLocalization.surj M s

Result:
case h.intro.mk
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : S
x : R
t : ↥M
e : s * (algebraMap R S) ↑(x, t).2 = (algebraMap R S) (x, t).1
⊢ ∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a

Proof state:
case h.intro.mk
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : S
x : R
t : ↥M
e : s * (algebraMap R S) ↑(x, t).2 = (algebraMap R S) (x, t).1
⊢ ∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a

Tactic:
exact ⟨_, IsLocalization.map_units S t, x, e.symm⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ ∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
use ∅

Result:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ ∀ (s : S), ∃ t ∈ adjoin R ↑∅, IsUnit t ∧ s * t ∈ adjoin R ↑∅

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ ∀ (s : S), ∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a

Tactic:
intro s

Result:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : S
⊢ ∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ ∀ (s : S), ∃ t ∈ adjoin R ↑∅, IsUnit t ∧ s * t ∈ adjoin R ↑∅

Tactic:
simp only [Finset.coe_empty, Algebra.adjoin_empty, exists_and_left, Algebra.mem_bot,
  Set.mem_range, exists_exists_eq_and]

Result:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ ∀ (s : S), ∃ a, IsUnit ((algebraMap R S) a) ∧ ∃ y, (algebraMap R S) y = s * (algebraMap R S) a

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ EssFiniteType R S

Tactic:
rw [essFiniteType_iff]

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ ∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
-- Mathlib/Combinatorics/SimpleGraph/LineGraph.lean
@[simp] lemma lineGraph_bot : (⊥ : SimpleGraph V).lineGraph = ⊥

Proof state:
V : Type u_1
⊢ ⊥.lineGraph = ⊥

Tactic:
aesop (add simp lineGraph)

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem refl_trans : (PartialEquiv.refl α).trans e = e :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [trans_source, preimage_id])

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ ((PartialEquiv.refl α).trans e).source = e.source

Tactic:
simp [trans_source, preimage_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_append {x y : List α} : (x ++ y).all f = (x.all f && y.all f)

Proof state:
case nil
α : Type u_1
f : α → Bool
y : List α
⊢ ([] ++ y).all f = ([].all f && y.all f)

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → Bool
y : List α
h : α
t : List α
ih : (t ++ y).all f = (t.all f && y.all f)
⊢ (h :: t ++ y).all f = ((h :: t).all f && y.all f)

Tactic:
simp_all [Bool.and_assoc]

Result:
no goals

Proof state:
α : Type u_1
f : α → Bool
x y : List α
⊢ (x ++ y).all f = (x.all f && y.all f)

Tactic:
induction x with
| nil => rfl
| cons h t ih => simp_all [Bool.and_assoc]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem HasFDerivAt.hasFDerivAt_norm_smul_pos
    (ht : 0 < t) (h : HasFDerivAt (‖·‖) f x) :
    HasFDerivAt (‖·‖) f (t • x)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : 0 < t
h : HasFDerivAt (fun x => ‖x‖) f x
⊢ HasFDerivAt (fun x => ‖x‖) f (t • x)

Tactic:
simpa [ht] using h.hasFDerivAt_norm_smul ht.ne'

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem coeff_homogeneousComponent (d : σ →₀ ℕ) :
    coeff d (homogeneousComponent n φ) = if d.degree = n then coeff d φ else 0

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d ((homogeneousComponent n) φ) = if d.degree = n then coeff d φ else 0

Tactic:
rw [degree_eq_weight_one]

Result:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d ((homogeneousComponent n) φ) = if (weight fun x => 1) d = n then coeff d φ else 0

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d ((homogeneousComponent n) φ) = if (weight fun x => 1) d = n then coeff d φ else 0

Tactic:
convert coeff_weightedHomogeneousComponent n φ d

Result:
no goals