harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem Scheme.Spec_map_presheaf_map_eqToHom {X : Scheme} {U V : X.Opens} (h : U = V) (W) :
    (Spec.map (X.presheaf.map (eqToHom h).op)).app W = eqToHom (by cases h; dsimp; simp)

Proof state:
case refl
X : Scheme
U : X.Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
W : (Spec Γ(X, U)).Opens
⊢ Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) W = eqToHom ⋯

Tactic:
refine (Scheme.congr_app this _).trans ?_

Result:
case refl
X : Scheme
U : X.Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
W : (Spec Γ(X, U)).Opens
⊢ Hom.app (𝟙 (Scheme.Spec.obj (op Γ(X, U)))) W ≫ (Scheme.Spec.obj (op Γ(X, U))).presheaf.map (eqToHom ⋯).op = eqToHom ⋯

Proof state:
case refl
X : Scheme
U : X.Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
W : (Spec Γ(X, U)).Opens
⊢ Hom.app (𝟙 (Scheme.Spec.obj (op Γ(X, U)))) W ≫ (Scheme.Spec.obj (op Γ(X, U))).presheaf.map (eqToHom ⋯).op = eqToHom ⋯

Tactic:
simp [eqToHom_map]

Result:
no goals

Proof state:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
⊢ Hom.app (Spec.map (X.presheaf.map (eqToHom h).op)) W = eqToHom ⋯

Tactic:
cases h

Result:
case refl
X : Scheme
U : X.Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
W : (Spec Γ(X, U)).Opens
⊢ Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) W = eqToHom ⋯

Proof state:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Hom.app (Spec.map (X.presheaf.map (eqToHom h).op)) W = eqToHom ⋯

Tactic:
have : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 _ := by
  rw [X.presheaf.map_id, op_id, Scheme.Spec.map_id]

Result:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
⊢ Hom.app (Spec.map (X.presheaf.map (eqToHom h).op)) W = eqToHom ⋯

Proof state:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))

Tactic:
rw [X.presheaf.map_id, op_id, Scheme.Spec.map_id]

Result:
no goals

Proof state:
case refl
X : Scheme
U : X.Opens
W : (Spec Γ(X, U)).Opens
⊢ Γ(Spec Γ(X, U), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (eqToHom ⋯).op) ⁻¹ᵁ W)

Tactic:
dsimp

Result:
case refl
X : Scheme
U : X.Opens
W : (Spec Γ(X, U)).Opens
⊢ Γ(Spec Γ(X, U), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (𝟙 (op U))) ⁻¹ᵁ W)

Proof state:
case refl
X : Scheme
U : X.Opens
W : (Spec Γ(X, U)).Opens
⊢ Γ(Spec Γ(X, U), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (𝟙 (op U))) ⁻¹ᵁ W)

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Γ(Spec Γ(X, V), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (eqToHom h).op) ⁻¹ᵁ W)

Tactic:
cases h

Result:
case refl
X : Scheme
U : X.Opens
W : (Spec Γ(X, U)).Opens
⊢ Γ(Spec Γ(X, U), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (eqToHom ⋯).op) ⁻¹ᵁ W)
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_iff_integrable_of_support_subset (h1s : support f ⊆ s) :
    IntegrableOn f s μ ↔ Integrable f μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s μ
x : α
hx : x ∉ s
⊢ f x = 0

Tactic:
contrapose! hx

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s μ
x : α
hx : f x ≠ 0
⊢ x ∈ s

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s μ
⊢ Integrable f μ

Tactic:
refine h.integrable_of_forall_not_mem_eq_zero fun x hx => ?_

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s μ
x : α
hx : x ∉ s
⊢ f x = 0

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s μ
x : α
hx : f x ≠ 0
⊢ x ∈ s

Tactic:
exact h1s (mem_support.2 hx)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
h1s : support f ⊆ s
⊢ IntegrableOn f s μ ↔ Integrable f μ

Tactic:
refine ⟨fun h => ?_, fun h => h.integrableOn⟩

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s μ
⊢ Integrable f μ
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem exists_rat_eq_of_terminates (terminates : (of v).Terminates) : ∃ q : ℚ, v = ↑q

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
terminates : (of v).Terminates
n : ℕ
v_eq_conv : v = (of v).convs n
q : ℚ
conv_eq_q : (of v).convs n = ↑q
⊢ ∃ q, v = ↑q

Tactic:
have : v = (↑q : K) := Eq.trans v_eq_conv conv_eq_q

Result:
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
terminates : (of v).Terminates
n : ℕ
v_eq_conv : v = (of v).convs n
q : ℚ
conv_eq_q : (of v).convs n = ↑q
this : v = ↑q
⊢ ∃ q, v = ↑q

Proof state:
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
terminates : (of v).Terminates
n : ℕ
v_eq_conv : v = (of v).convs n
⊢ ∃ q, v = ↑q

Tactic:
obtain ⟨q, conv_eq_q⟩ : ∃ q : ℚ, (of v).convs n = (↑q : K) := exists_rat_eq_nth_conv v n

Result:
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
terminates : (of v).Terminates
n : ℕ
v_eq_conv : v = (of v).convs n
q : ℚ
conv_eq_q : (of v).convs n = ↑q
⊢ ∃ q, v = ↑q

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
terminates : (of v).Terminates
⊢ ∃ q, v = ↑q

Tactic:
obtain ⟨n, v_eq_conv⟩ : ∃ n, v = (of v).convs n := of_correctness_of_terminates terminates

Result:
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
terminates : (of v).Terminates
n : ℕ
v_eq_conv : v = (of v).convs n
⊢ ∃ q, v = ↑q

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
terminates : (of v).Terminates
n : ℕ
v_eq_conv : v = (of v).convs n
q : ℚ
conv_eq_q : (of v).convs n = ↑q
this : v = ↑q
⊢ ∃ q, v = ↑q

Tactic:
use q, this

Result:
no goals
-- Mathlib/RingTheory/Flat/EquationalCriterion.lean
theorem exists_factorization_of_isFinitelyPresented [Flat R M] {P : Type*} [AddCommGroup P]
    [Module R P] [FinitePresentation R P] (h₁ : P →ₗ[R] M) :
      ∃ (k : ℕ) (h₂ : P →ₗ[R] (Fin k →₀ R)) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
P : Type u_3
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R P
h₁ : P →ₗ[R] M
w✝ : ℕ
K : Submodule R (Fin w✝ → R)
ϕ : P ≃ₗ[R] (Fin w✝ → R) ⧸ K
hK : K.FG
this✝ : Module.Finite R ↥K
this : (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w✝ → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
⊢ h₁ ∘ₗ ↑ϕ.symm = (y ∘ₗ K.liftQ a ⋯ ∘ₗ ↑ϕ) ∘ₗ ↑ϕ.symm

Tactic:
apply (cancel_right K.mkQ_surjective).mp

Result:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
P : Type u_3
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R P
h₁ : P →ₗ[R] M
w✝ : ℕ
K : Submodule R (Fin w✝ → R)
ϕ : P ≃ₗ[R] (Fin w✝ → R) ⧸ K
hK : K.FG
this✝ : Module.Finite R ↥K
this : (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w✝ → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
⊢ (h₁ ∘ₗ ↑ϕ.symm) ∘ₗ K.mkQ = ((y ∘ₗ K.liftQ a ⋯ ∘ₗ ↑ϕ) ∘ₗ ↑ϕ.symm) ∘ₗ K.mkQ

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
P : Type u_3
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R P
h₁ : P →ₗ[R] M
w✝ : ℕ
K : Submodule R (Fin w✝ → R)
ϕ : P ≃ₗ[R] (Fin w✝ → R) ⧸ K
hK : K.FG
this : Module.Finite R ↥K
⊢ (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0

Tactic:
simp_rw [comp_assoc, (LinearMap.exact_subtype_mkQ K).linearMap_comp_eq_zero, comp_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Range/Lemmas.lean
theorem mem_of_mem_range' {r : Range} (h : x ∈ List.range' r.start r.size r.step) : x ∈ r

Proof state:
x : Nat
r : Range
h : x ∈ List.range' r.start ((r.stop - r.start + r.step - 1) / r.step) r.step
⊢ (r.start - r.start) % r.step = 0

Tactic:
simp

Result:
no goals

Proof state:
x : Nat
r : Range
h : x ∈ List.range' r.start ((r.stop - r.start + r.step - 1) / r.step) r.step
⊢ r.start ≤ r.start

Tactic:
simp

Result:
no goals

Proof state:
x : Nat
r : Range
h : x ∈ List.range' r.start ((r.stop - r.start + r.step - 1) / r.step) r.step
⊢ x ∈ r

Tactic:
apply mem_of_mem_range'_aux (by simp) (by simp) h

Result:
no goals

Proof state:
x : Nat
r : Range
h : x ∈ List.range' r.start r.size r.step
⊢ x ∈ r

Tactic:
unfold size at h

Result:
x : Nat
r : Range
h : x ∈ List.range' r.start ((r.stop - r.start + r.step - 1) / r.step) r.step
⊢ x ∈ r
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem exists_of_mem_mapFinIdx {b : β} {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β}
    (h : b ∈ l.mapFinIdx f) : ∃ (i : Nat) (h : i < n), f i l[i] h = b

Proof state:
β : Type u_1
α : Type u_2
n : Nat
b : β
l : Vector α n
f : (i : Nat) → α → i < n → β
h : b ∈ l.mapFinIdx f
⊢ ∃ i h, f i l[i] h = b

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
β : Type u_1
α : Type u_2
b : β
l : Array α
f : (i : Nat) → α → i < l.size → β
h : b ∈ { toArray := l, size_toArray := ⋯ }.mapFinIdx f
⊢ ∃ i h, f i { toArray := l, size_toArray := ⋯ }[i] h = b

Proof state:
β : Type u_1
α : Type u_2
b : β
l : Array α
f : (i : Nat) → α → i < l.size → β
h : b ∈ { toArray := l, size_toArray := ⋯ }.mapFinIdx f
⊢ b ∈ l.toList.mapFinIdx f

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
β : Type u_1
α : Type u_2
b : β
l : Array α
f : (i : Nat) → α → i < l.size → β
h : b ∈ { toArray := l, size_toArray := ⋯ }.mapFinIdx f
⊢ ∃ i h, f i { toArray := l, size_toArray := ⋯ }[i] h = b

Tactic:
exact List.exists_of_mem_mapFinIdx (by simpa using h)

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem isCaratheodory_iUnion_lt {s : ℕ → Set α} :
    ∀ {n : ℕ}, (∀ i < n, IsCaratheodory m (s i)) → IsCaratheodory m (⋃ i < n, s i)
  | 0, _ => by simp [Nat.not_lt_zero]
  | n + 1, h => by
    rw [biUnion_lt_succ]
    exact isCaratheodory_union m
            (isCaratheodory_iUnion_lt fun i hi => h i <| lt_of_lt_of_le hi <| Nat.le_succ _)
            (h n (le_refl (n + 1)))

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
x✝ : ∀ i < 0, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i, ⋃ (_ : i < 0), s i)

Tactic:
simp [Nat.not_lt_zero]

Result:
no goals

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
n : ℕ
h : ∀ i < n + 1, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i, ⋃ (_ : i < n + 1), s i)

Tactic:
rw [biUnion_lt_succ]

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
n : ℕ
h : ∀ i < n + 1, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory ((⋃ k, ⋃ (_ : k < n), s k) ∪ s n)

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
n : ℕ
h : ∀ i < n + 1, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory ((⋃ k, ⋃ (_ : k < n), s k) ∪ s n)

Tactic:
exact isCaratheodory_union m
        (isCaratheodory_iUnion_lt fun i hi => h i <| lt_of_lt_of_le hi <| Nat.le_succ _)
        (h n (le_refl (n + 1)))

Result:
no goals
-- Mathlib/RingTheory/RingHom/FiniteType.lean
theorem finiteType_holdsForLocalizationAway : HoldsForLocalizationAway @FiniteType

Proof state:
case h.e'_5.h
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
r✝ : R
x✝ : S
⊢ (let_fun I := (algebraMap R S).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝

Tactic:
rw [Algebra.smul_def]

Result:
case h.e'_5.h
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
r✝ : R
x✝ : S
⊢ (let_fun I := (algebraMap R S).toAlgebra;
    r✝ • x✝) =
    (algebraMap R S) r✝ * x✝

Proof state:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Algebra.FiniteType R S

Tactic:
exact IsLocalization.finiteType_of_monoid_fg (Submonoid.powers r) S

Result:
no goals

Proof state:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (algebraMap R S).FiniteType

Tactic:
suffices Algebra.FiniteType R S by
  rw [RingHom.FiniteType]
  convert this; ext
  rw [Algebra.smul_def]; rfl

Result:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Algebra.FiniteType R S

Proof state:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
⊢ Algebra.FiniteType R S

Tactic:
convert this

Result:
case h.e'_5
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
⊢ (algebraMap R S).toAlgebra = inst✝¹

Proof state:
case h.e'_5
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
⊢ (algebraMap R S).toAlgebra = inst✝¹

Tactic:
ext

Result:
case h.e'_5.h
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
r✝ : R
x✝ : S
⊢ (let_fun I := (algebraMap R S).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝

Proof state:
⊢ HoldsForLocalizationAway @FiniteType

Tactic:
introv R _

Result:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (algebraMap R S).FiniteType

Proof state:
case h.e'_5.h
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
r✝ : R
x✝ : S
⊢ (let_fun I := (algebraMap R S).toAlgebra;
    r✝ • x✝) =
    (algebraMap R S) r✝ * x✝

Tactic:
rfl

Result:
no goals

Proof state:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
⊢ (algebraMap R S).FiniteType

Tactic:
rw [RingHom.FiniteType]

Result:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
⊢ Algebra.FiniteType R S
-- Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
/-- Transfer reflection of colimits along a natural isomorphism in the diagram. -/
lemma reflectsColimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂)
    [ReflectsColimit K₁ F] :
    ReflectsColimit K₂ F where
  reflects {c} t := ⟨by
    apply IsColimit.precomposeHomEquiv h c (isColimitOfReflects F _)
    apply ((IsColimit.precomposeHomEquiv (isoWhiskerRight h F :) _).symm t).ofIsoColimit _
    exact Cocones.ext (Iso.refl _)⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ (Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c) ≅ F.mapCocone ((Cocones.precompose h.hom).obj c)

Tactic:
exact Cocones.ext (Iso.refl _)

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ IsColimit c

Tactic:
apply IsColimit.precomposeHomEquiv h c (isColimitOfReflects F _)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ IsColimit (F.mapCocone ((Cocones.precompose h.hom).obj c))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ IsColimit (F.mapCocone ((Cocones.precompose h.hom).obj c))

Tactic:
apply ((IsColimit.precomposeHomEquiv (isoWhiskerRight h F :) _).symm t).ofIsoColimit _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ (Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c) ≅ F.mapCocone ((Cocones.precompose h.hom).obj c)
-- Mathlib/Topology/Maps/Basic.lean
theorem comp (hg : IsQuotientMap g) (hf : IsQuotientMap f) : IsQuotientMap (g ∘ f) :=
  ⟨hg.surjective.comp hf.surjective, by rw [hg.eq_coinduced, hf.eq_coinduced, coinduced_compose]⟩

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsQuotientMap g
hf : IsQuotientMap f
⊢ inst✝ = coinduced (g ∘ f) inst✝²

Tactic:
rw [hg.eq_coinduced, hf.eq_coinduced, coinduced_compose]

Result:
no goals
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem lift_comp_apply (x : K) : lift i j p (i x) = j x

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : CommRing K
inst✝⁶ : CommRing L
inst✝⁵ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x : K
⊢ (RingEquiv.refl M).symm (j x) = j x

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : CommRing K
inst✝⁶ : CommRing L
inst✝⁵ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x : K
⊢ (lift i j p) (i x) = j x

Tactic:
rw [lift_apply i j p _ 0 x (by rw [pow_zero, pow_one]), iterateFrobeniusEquiv_zero]

Result:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : CommRing K
inst✝⁶ : CommRing L
inst✝⁵ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x : K
⊢ (RingEquiv.refl M).symm (j x) = j x

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : CommRing K
inst✝⁶ : CommRing L
inst✝⁵ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x : K
⊢ i x = i x ^ p ^ 0

Tactic:
rw [pow_zero, pow_one]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem rightLim_eq (f : StieltjesFunction) (x : ℝ) : Function.rightLim f x = f x

Proof state:
f : StieltjesFunction
x : ℝ
⊢ rightLim (↑f) x = ↑f x

Tactic:
rw [← f.mono.continuousWithinAt_Ioi_iff_rightLim_eq, continuousWithinAt_Ioi_iff_Ici]

Result:
f : StieltjesFunction
x : ℝ
⊢ ContinuousWithinAt (↑f) (Ici x) x

Proof state:
f : StieltjesFunction
x : ℝ
⊢ ContinuousWithinAt (↑f) (Ici x) x

Tactic:
exact f.right_continuous' x

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_neg (x : Game) : (-x).birthday = x.birthday

Proof state:
x : Game
⊢ x.birthday ≤ (-x).birthday

Tactic:
conv_lhs => rw [← neg_neg x]

Result:
x : Game
⊢ (- -x).birthday ≤ (-x).birthday

Proof state:
x : Game
⊢ (- -x).birthday ≤ (-x).birthday

Tactic:
exact birthday_neg' _

Result:
no goals

Proof state:
x : Game
⊢ (-x).birthday = x.birthday

Tactic:
apply le_antisymm (birthday_neg' x)

Result:
x : Game
⊢ x.birthday ≤ (-x).birthday
-- Mathlib/FieldTheory/PurelyInseparable/Tower.lean
/-- The same-universe version of `Field.lift_rank_mul_lift_sepDegree_of_isSeparable`. -/
lemma rank_mul_sepDegree_of_isSeparable (K : Type v) [Field K] [Algebra F K]
    [Algebra E K] [IsScalarTower F E K] [Algebra.IsSeparable F E] :
    Module.rank F E * sepDegree E K = sepDegree F K

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
⊢ Module.rank F E * sepDegree E K = sepDegree F K

Tactic:
simpa only [Cardinal.lift_id] using lift_rank_mul_lift_sepDegree_of_isSeparable F E K

Result:
no goals
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem map_mem_separableClosure_iff (i : E →ₐ[F] K) {x : E} :
    i x ∈ separableClosure F K ↔ x ∈ separableClosure F E

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ i x ∈ separableClosure F K ↔ x ∈ separableClosure F E

Tactic:
simp_rw [mem_separableClosure_iff, IsSeparable, minpoly.algHom_eq i i.injective]

Result:
no goals
-- Mathlib/LinearAlgebra/SModEq.lean
theorem _root_.sub_smodEq_zero : x - y ≡ 0 [SMOD U] ↔ x ≡ y [SMOD U]

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
⊢ x - y ≡ 0 [SMOD U] ↔ x ≡ y [SMOD U]

Tactic:
simp only [SModEq.sub_mem, sub_zero]

Result:
no goals