harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Support.lean
theorem nodup_of_pairwise_disjoint {l : List (Perm α)} (h1 : (1 : Perm α) ∉ l)
    (h2 : l.Pairwise Disjoint) : l.Nodup

Proof state:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
⊢ l.Nodup

Tactic:
refine List.Pairwise.imp_of_mem ?_ h2

Result:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
⊢ ∀ {a b : Perm α}, a ∈ l → b ∈ l → a.Disjoint b → a ≠ b

Proof state:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
τ σ : Perm α
h_mem : τ ∈ l
a✝¹ : σ ∈ l
h_disjoint : τ.Disjoint σ
a✝ : τ = σ
⊢ False

Tactic:
subst τ

Result:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : σ.Disjoint σ
⊢ False

Proof state:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : σ.Disjoint σ
⊢ σ = 1

Tactic:
exact ext fun a => or_self_iff.mp (h_disjoint a)

Result:
no goals

Proof state:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ : σ ∈ l
h_mem : 1 ∈ l
h_disjoint : σ.Disjoint σ
this : σ = 1
⊢ False

Tactic:
exact h1 h_mem

Result:
no goals

Proof state:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : σ.Disjoint σ
⊢ False

Tactic:
suffices (σ : Perm α) = 1 by
  rw [this] at h_mem
  exact h1 h_mem

Result:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : σ.Disjoint σ
⊢ σ = 1

Proof state:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
⊢ ∀ {a b : Perm α}, a ∈ l → b ∈ l → a.Disjoint b → a ≠ b

Tactic:
intro τ σ h_mem _ h_disjoint _

Result:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
τ σ : Perm α
h_mem : τ ∈ l
a✝¹ : σ ∈ l
h_disjoint : τ.Disjoint σ
a✝ : τ = σ
⊢ False

Proof state:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : σ.Disjoint σ
this : σ = 1
⊢ False

Tactic:
rw [this] at h_mem

Result:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ : σ ∈ l
h_mem : 1 ∈ l
h_disjoint : σ.Disjoint σ
this : σ = 1
⊢ False
-- Mathlib/Algebra/Regular/Basic.lean
theorem isRightRegular_of_mul_eq_one (h : a * b = 1) : IsRightRegular a :=
  IsRightRegular.of_mul (a := b) (by rw [h]; exact isRegular_one.right)

Proof state:
R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular 1

Tactic:
exact isRegular_one.right

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular (a * b)

Tactic:
rw [h]

Result:
R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular 1
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem UniformSpace.Core.nhds_toTopologicalSpace {α : Type u} (u : Core α) (x : α) :
    @nhds α u.toTopologicalSpace x = comap (Prod.mk x) u.uniformity

Proof state:
case hopen.intro.intro
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
⊢ ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity

Tactic:
filter_upwards [preimage_mem_comap hV] with b hb

Result:
case h
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
b : α
hb : b ∈ Prod.mk a ⁻¹' V
⊢ Prod.mk a ⁻¹' id U ∈ comap (Prod.mk b) u.uniformity

Proof state:
case hopen
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
⊢ ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity

Tactic:
rcases u.comp_mem_uniformity_sets hU with ⟨V, hV, hVU⟩

Result:
case hopen.intro.intro
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
⊢ ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity

Proof state:
case h
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
b : α
hb : b ∈ Prod.mk a ⁻¹' V
c : α
hc : c ∈ Prod.mk b ⁻¹' V
⊢ c ∈ Prod.mk a ⁻¹' id U

Tactic:
exact hVU ⟨b, hb, hc⟩

Result:
no goals

Proof state:
case hopen
α : Type u
u : Core α
x : α
⊢ ∀ (a : α),
    ∀ i ∈ u.uniformity,
      ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id i ∈ comap (Prod.mk x) u.uniformity

Tactic:
intro a U hU

Result:
case hopen
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
⊢ ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity

Proof state:
case h
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
b : α
hb : b ∈ Prod.mk a ⁻¹' V
⊢ Prod.mk a ⁻¹' id U ∈ comap (Prod.mk b) u.uniformity

Tactic:
filter_upwards [preimage_mem_comap hV] with c hc

Result:
case h
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
b : α
hb : b ∈ Prod.mk a ⁻¹' V
c : α
hc : c ∈ Prod.mk b ⁻¹' V
⊢ c ∈ Prod.mk a ⁻¹' id U

Proof state:
α : Type u
u : Core α
x : α
⊢ 𝓝 x = comap (Prod.mk x) u.uniformity

Tactic:
apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun _ ↦ (basis_sets _).comap _)

Result:
case hpure
α : Type u
u : Core α
x : α
⊢ ∀ (a : α), ∀ i ∈ u.uniformity, a ∈ Prod.mk a ⁻¹' id i

case hopen
α : Type u
u : Core α
x : α
⊢ ∀ (a : α),
    ∀ i ∈ u.uniformity,
      ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id i ∈ comap (Prod.mk x) u.uniformity

Proof state:
case hpure
α : Type u
u : Core α
x : α
⊢ ∀ (a : α), ∀ i ∈ u.uniformity, a ∈ Prod.mk a ⁻¹' id i

Tactic:
exact fun a U hU ↦ u.refl hU rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem subNatNat_add (m n k : Nat) : subNatNat (m + n) k = m + subNatNat n k

Proof state:
m n k : Nat
⊢ subNatNat (m + n) k = ↑m + subNatNat n k

Tactic:
cases n.lt_or_ge k with
| inl h' =>
  simp [subNatNat_of_lt h', sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h')]
  conv => lhs; rw [← Nat.sub_add_cancel (Nat.le_of_lt h')]
  apply subNatNat_add_add
| inr h' => simp [subNatNat_of_le h',
    subNatNat_of_le (Nat.le_trans h' (le_add_left ..)), Nat.add_sub_assoc h']

Result:
no goals

Proof state:
case inr
m n k : Nat
h' : n ≥ k
⊢ subNatNat (m + n) k = ↑m + subNatNat n k

Tactic:
simp [subNatNat_of_le h',
subNatNat_of_le (Nat.le_trans h' (le_add_left ..)), Nat.add_sub_assoc h']

Result:
no goals

Proof state:
case inl
m n k : Nat
h' : n < k
⊢ subNatNat (m + n) k = subNatNat m (k - n)

Tactic:
conv => lhs; rw [← Nat.sub_add_cancel (Nat.le_of_lt h')]

Result:
case inl
m n k : Nat
h' : n < k
⊢ subNatNat (m + n) (k - n + n) = subNatNat m (k - n)

Proof state:
case inl
m n k : Nat
h' : n < k
⊢ subNatNat (m + n) k = ↑m + subNatNat n k

Tactic:
simp [subNatNat_of_lt h', sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h')]

Result:
case inl
m n k : Nat
h' : n < k
⊢ subNatNat (m + n) k = subNatNat m (k - n)

Proof state:
case inl
m n k : Nat
h' : n < k
⊢ subNatNat (m + n) (k - n + n) = subNatNat m (k - n)

Tactic:
apply subNatNat_add_add

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivWithinAt_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
    HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x :=
  calc
    HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' (s \ {y}) x :=
      (hasFDerivWithinAt_diff_singleton _).symm
    _ ↔ HasFDerivWithinAt f f' (t \ {y}) 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 t : Set E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' (t \ {y}) x

Tactic:
suffices 𝓝[s \ {y}] x = 𝓝[t \ {y}] x by simp only [HasFDerivWithinAt, this]

Result:
𝕜 : 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 t : Set E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ 𝓝[s \ {y}] x = 𝓝[t \ {y}] 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 t : Set E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : 𝓝[s \ {y}] x = 𝓝[t \ {y}] x
⊢ HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' (t \ {y}) x

Tactic:
simp only [HasFDerivWithinAt, this]

Result:
no goals

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 t : Set E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ 𝓝[s \ {y}] x = 𝓝[t \ {y}] x

Tactic:
simpa only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_inter', diff_eq,
  inter_comm] using h

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
@[simp, norm_cast]
lemma inr_nonneg_iff {a : A} : 0 ≤ (a : A⁺¹) ↔ 0 ≤ a

Proof state:
case neg.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
⊢ 0 ≤ a → 0 ≤ ↑a

Tactic:
refine fun h ↦ (ha ?_).elim

Result:
case neg.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
h : 0 ≤ a
⊢ IsSelfAdjoint a

Proof state:
case neg.refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
h : 0 ≤ ↑a
⊢ IsSelfAdjoint a

Tactic:
exact isSelfAdjoint_inr (R := ℂ) |>.mp <| .of_nonneg h

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ 0 ≤ ↑a ↔ 0 ≤ a

Tactic:
by_cases ha : IsSelfAdjoint a

Result:
case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ 0 ≤ ↑a ↔ 0 ≤ a

case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
⊢ 0 ≤ ↑a ↔ 0 ≤ a

Proof state:
case neg.refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
⊢ 0 ≤ ↑a → 0 ≤ a

case neg.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
⊢ 0 ≤ a → 0 ≤ ↑a

Tactic:
all_goals refine fun h ↦ (ha ?_).elim

Result:
case neg.refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
h : 0 ≤ ↑a
⊢ IsSelfAdjoint a

case neg.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
h : 0 ≤ a
⊢ IsSelfAdjoint a

Proof state:
case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
⊢ 0 ≤ ↑a ↔ 0 ≤ a

Tactic:
refine ⟨?_, ?_⟩

Result:
case neg.refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
⊢ 0 ≤ ↑a → 0 ≤ a

case neg.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
⊢ 0 ≤ a → 0 ≤ ↑a

Proof state:
case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ 0 ≤ ↑a ↔ 0 ≤ a

Tactic:
exact inr_zero ℂ (A := A) ▸ inr_le_iff 0 a

Result:
no goals

Proof state:
case neg.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
h : 0 ≤ a
⊢ IsSelfAdjoint a

Tactic:
exact .of_nonneg h

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
/-- For a prime ideal `p` of `R`, `p` extended to `S` and
restricted back to `R` is `p` if and only if `p` is the restriction of a prime in `S`. -/
lemma comap_map_eq_self_iff_of_isPrime {S : Type*} [CommSemiring S] {f : R →+* S}
    (p : Ideal R) [p.IsPrime] :
    (p.map f).comap f = p ↔ (∃ (q : Ideal S), q.IsPrime ∧ q.comap f = p)

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ comap f (map f p) = p ↔ ∃ q, q.IsPrime ∧ comap f q = p

Tactic:
refine ⟨fun hp ↦ ?_, ?_⟩

Result:
case refine_1
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
hp : comap f (map f p) = p
⊢ ∃ q, q.IsPrime ∧ comap f q = p

case refine_2
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ (∃ q, q.IsPrime ∧ comap f q = p) → comap f (map f p) = p

Proof state:
case refine_2
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
⊢ (∃ q, q.IsPrime ∧ comap f q = p) → comap f (map f p) = p

Tactic:
rintro ⟨q, hq, rfl⟩

Result:
case refine_2.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
q : Ideal S
hq : q.IsPrime
inst✝ : (comap f q).IsPrime
⊢ comap f (map f (comap f q)) = comap f q

Proof state:
case refine_1
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
hp : comap f (map f p) = p
⊢ ∃ q, q.IsPrime ∧ comap f q = p

Tactic:
obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_le_prime_disjoint _ _
  (disjoint_map_primeCompl_iff_comap_le.mpr hp.le)

Result:
case refine_1.intro.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
hp : comap f (map f p) = p
q : Ideal S
hq₁ : q.IsPrime
hq₂ : map f p ≤ q
hq₃ : Disjoint ↑q ↑(Submonoid.map f p.primeCompl)
⊢ ∃ q, q.IsPrime ∧ comap f q = p

Proof state:
case refine_1.intro.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
p : Ideal R
inst✝ : p.IsPrime
hp : comap f (map f p) = p
q : Ideal S
hq₁ : q.IsPrime
hq₂ : map f p ≤ q
hq₃ : Disjoint ↑q ↑(Submonoid.map f p.primeCompl)
⊢ ∃ q, q.IsPrime ∧ comap f q = p

Tactic:
exact ⟨q, hq₁, le_antisymm (disjoint_map_primeCompl_iff_comap_le.mp hq₃)
  (map_le_iff_le_comap.mp hq₂)⟩

Result:
no goals

Proof state:
case refine_2.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
f : R →+* S
q : Ideal S
hq : q.IsPrime
inst✝ : (comap f q).IsPrime
⊢ comap f (map f (comap f q)) = comap f q

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Grothendieck.lean
theorem map_id_eq : map (𝟙 F) = 𝟙 (Cat.of <| Grothendieck <| F)

Proof state:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ ∀ (X : Grothendieck F), (map (𝟙 F)).obj X = (𝟙 (Cat.of (Grothendieck F))).obj X

Tactic:
intro X

Result:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (map (𝟙 F)).obj X = (𝟙 (Cat.of (Grothendieck F))).obj X

Proof state:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ autoParam
    (∀ (X Y : Grothendieck F) (f : X ⟶ Y),
      (map (𝟙 F)).map f = eqToHom ⋯ ≫ (𝟙 (Cat.of (Grothendieck F))).map f ≫ eqToHom ⋯)
    _auto✝

Tactic:
intro X Y f

Result:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ (map (𝟙 F)).map f = eqToHom ⋯ ≫ (𝟙 (Cat.of (Grothendieck F))).map f ≫ eqToHom ⋯

Proof state:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (map (𝟙 F)).obj X = (𝟙 (Cat.of (Grothendieck F))).obj X

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ map (𝟙 F) = 𝟙 (Cat.of (Grothendieck F))

Tactic:
fapply Functor.ext

Result:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ ∀ (X : Grothendieck F), (map (𝟙 F)).obj X = (𝟙 (Cat.of (Grothendieck F))).obj X

case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ autoParam
    (∀ (X Y : Grothendieck F) (f : X ⟶ Y),
      (map (𝟙 F)).map f = eqToHom ⋯ ≫ (𝟙 (Cat.of (Grothendieck F))).map f ≫ eqToHom ⋯)
    _auto✝

Proof state:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ (map (𝟙 F)).map f = eqToHom ⋯ ≫ (𝟙 (Cat.of (Grothendieck F))).map f ≫ eqToHom ⋯

Tactic:
simp [map_map]

Result:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ { base := f.base, fiber := f.fiber } = f

Proof state:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ { base := f.base, fiber := f.fiber } = f

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
lemma NullMeasurable.measure_preimage_eq_measure_restrict_preimage_of_ae_compl_eq_const
    {β : Type*} [MeasurableSpace β] {b : β} {f : α → β} {s : Set α}
    (f_mble : NullMeasurable f (μ.restrict s)) (hs : f =ᵐ[Measure.restrict μ sᶜ] (fun _ ↦ b))
    {t : Set β} (t_mble : MeasurableSet t) (ht : b ∉ t) :
    μ (f ⁻¹' t) = μ.restrict s (f ⁻¹' t)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : f =ᶠ[ae (μ.restrict sᶜ)] fun x => b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)

Tactic:
rw [EventuallyEq, ae_iff, Measure.restrict_apply₀] at hs

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)

α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : (μ.restrict sᶜ) {a | ¬f a = b} = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ NullMeasurableSet {a | ¬f a = b} (μ.restrict sᶜ)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : (μ.restrict sᶜ) {a | ¬f a = b} = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ NullMeasurableSet {a | ¬f a = b} (μ.restrict sᶜ)

Tactic:
exact NullMeasurableSet.of_null hs

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FinallySmall.lean
theorem InitiallySmall.exists_small_weakly_initial_set [InitiallySmall.{w} J] :
    ∃ (s : Set J) (_ : Small.{w} s), ∀ i, ∃ j ∈ s, Nonempty (j ⟶ i)

Proof state:
case intro
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : InitiallySmall J
i : J
f : CostructuredArrow (fromInitialModel J) i
⊢ ∃ j ∈ Set.range (fromInitialModel J).obj, Nonempty (j ⟶ i)

Tactic:
exact ⟨(fromInitialModel J).obj f.left, Set.mem_range_self _, ⟨f.hom⟩⟩

Result:
no goals

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : InitiallySmall J
⊢ ∃ s, ∃ (_ : Small.{w, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)

Tactic:
refine ⟨Set.range (fromInitialModel J).obj, inferInstance, fun i => ?_⟩

Result:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : InitiallySmall J
i : J
⊢ ∃ j ∈ Set.range (fromInitialModel J).obj, Nonempty (j ⟶ i)

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : InitiallySmall J
i : J
⊢ ∃ j ∈ Set.range (fromInitialModel J).obj, Nonempty (j ⟶ i)

Tactic:
obtain ⟨f⟩ : Nonempty (CostructuredArrow (fromInitialModel J) i) := IsConnected.is_nonempty

Result:
case intro
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : InitiallySmall J
i : J
f : CostructuredArrow (fromInitialModel J) i
⊢ ∃ j ∈ Set.range (fromInitialModel J).obj, Nonempty (j ⟶ i)
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem length_tail_add_one (l : List α) (h : 0 < length l) : (length (tail l)) + 1 = length l

Proof state:
α : Type u_1
l : List α
h : 0 < l.length
⊢ l.tail.length + 1 = l.length

Tactic:
simp [Nat.sub_add_cancel h]

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
private lemma logC_zero {b : ℕ} :
    logC b 0 = 0

Proof state:
b : ℕ
hb : 1 < b
x✝ : ℕ × ℕ
q e : ℕ
heq : (0, 0) = (q, e)
⊢ e = 0

Tactic:
rw [(Prod.mk.inj heq).2]

Result:
no goals

Proof state:
b : ℕ
hb : 1 < b
x✝ : ℕ × ℕ
q e : ℕ
heq : logC.step 0 b hb = (q, e)
⊢ e = 0

Tactic:
rw [logC.step, dif_pos (zero_lt_of_lt hb)] at heq

Result:
b : ℕ
hb : 1 < b
x✝ : ℕ × ℕ
q e : ℕ
heq : (0, 0) = (q, e)
⊢ e = 0

Proof state:
b : ℕ
hb : 1 < b
x✝ : ℕ × ℕ
q✝ e✝ : ℕ
heq✝ : logC.step 0 b hb = (q✝, e✝)
⊢ e✝ = 0

Tactic:
next q e heq =>
rw [logC.step, dif_pos (zero_lt_of_lt hb)] at heq
rw [(Prod.mk.inj heq).2]

Result:
no goals

Proof state:
case inr
b : ℕ
hb : 1 < b
⊢ logC b 0 = 0

Tactic:
case inr =>
  rw [logC, dif_pos hb]
  split
  next q e heq =>
  rw [logC.step, dif_pos (zero_lt_of_lt hb)] at heq
  rw [(Prod.mk.inj heq).2]

Result:
no goals

Proof state:
b : ℕ
hb : b ≤ 1
⊢ logC b 0 = 0

Tactic:
exact logC_of_left_le_one hb

Result:
no goals

Proof state:
b : ℕ
⊢ logC b 0 = 0

Tactic:
rcases le_or_lt b 1 with hb | hb

Result:
case inl
b : ℕ
hb : b ≤ 1
⊢ logC b 0 = 0

case inr
b : ℕ
hb : 1 < b
⊢ logC b 0 = 0

Proof state:
b : ℕ
hb : 1 < b
⊢ (match logC.step 0 b hb with
    | (fst, e) => e) =
    0

Tactic:
split

Result:
b : ℕ
hb : 1 < b
x✝ : ℕ × ℕ
q✝ e✝ : ℕ
heq✝ : logC.step 0 b hb = (q✝, e✝)
⊢ e✝ = 0

Proof state:
b : ℕ
hb : 1 < b
⊢ logC b 0 = 0

Tactic:
rw [logC, dif_pos hb]

Result:
b : ℕ
hb : 1 < b
⊢ (match logC.step 0 b hb with
    | (fst, e) => e) =
    0

Proof state:
case inl
b : ℕ
hb : b ≤ 1
⊢ logC b 0 = 0

case inr
b : ℕ
hb : 1 < b
⊢ logC b 0 = 0

Tactic:
case inl => exact logC_of_left_le_one hb

Result:
case inr
b : ℕ
hb : 1 < b
⊢ logC b 0 = 0