harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/Embedding/TruncLEHomology.lean
lemma quasiIso_truncLEMap_iff :
    QuasiIso (truncLEMap φ e) ↔ ∀ (i : ι) (i' : ι') (_ : e.f i = i'), QuasiIsoAt φ i'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncLE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso (truncLEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Tactic:
rw [← quasiIso_opFunctor_map_iff]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncLE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso ((opFunctor C c').map (truncLEMap φ e).op) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncLE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso ((opFunctor C c').map (truncLEMap φ e).op) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Tactic:
simp only [← quasiIsoAt_opFunctor_map_iff φ]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncLE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso ((opFunctor C c').map (truncLEMap φ e).op) ↔
    ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt ((opFunctor C c').map φ.op) i'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncLE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso ((opFunctor C c').map (truncLEMap φ e).op) ↔
    ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt ((opFunctor C c').map φ.op) i'

Tactic:
apply quasiIso_truncGEMap_iff

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finite_mulSupport_coe {I : Ideal R} (hI : I ≠ 0) :
    (mulSupport fun v : HeightOneSpectrum R => (v.asIdeal : FractionalIdeal R⁰ K) ^
      ((Associates.mk v.asIdeal).count (Associates.mk I).factors : ℤ)).Finite

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {x | ¬x.asIdeal ^ (Associates.mk x.asIdeal).count (Associates.mk I).factors = 1}.Finite

Tactic:
exact finite_mulSupport hI

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {x | ↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors) ≠ 1}.Finite

Tactic:
simp_rw [Ne, zpow_natCast, ← FractionalIdeal.coeIdeal_pow, FractionalIdeal.coeIdeal_eq_one]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {x | ¬x.asIdeal ^ (Associates.mk x.asIdeal).count (Associates.mk I).factors = 1}.Finite

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ (mulSupport fun v => ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors)).Finite

Tactic:
rw [mulSupport]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {x | ↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors) ≠ 1}.Finite
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_eq_zero {p : ℝ} : ENNReal.ofReal p = 0 ↔ p ≤ 0

Proof state:
p : ℝ
⊢ ENNReal.ofReal p = 0 ↔ p ≤ 0

Tactic:
simp [ENNReal.ofReal]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem lift_restrict : lift (restrict h) = F

Proof state:
case h.refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ F
⊢ x ∈ lift (restrict h)

Tactic:
let y : E := ⟨x, h hx⟩

Result:
case h.refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ F
y : ↥E := ⟨x, ⋯⟩
⊢ x ∈ lift (restrict h)

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
⊢ x ∈ lift (restrict h) ↔ x ∈ F

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

Result:
case h.refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ lift (restrict h)
⊢ x ∈ F

case h.refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ F
⊢ x ∈ lift (restrict h)

Proof state:
case h.refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ F
y : ↥E := ⟨x, ⋯⟩
⊢ x ∈ lift (restrict h)

Tactic:
exact (mem_lift y).2 ((mem_restrict h y).2 hx)

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
⊢ lift (restrict h) = F

Tactic:
ext x

Result:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
⊢ x ∈ lift (restrict h) ↔ x ∈ F

Proof state:
case h.refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ lift (restrict h)
y : ↥E := ⟨x, ⋯⟩
⊢ x ∈ F

Tactic:
exact (mem_restrict h y).1 ((mem_lift y).1 hx)

Result:
no goals

Proof state:
case h.refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ lift (restrict h)
⊢ x ∈ F

Tactic:
let y : E := ⟨x, lift_le (restrict h) hx⟩

Result:
case h.refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ lift (restrict h)
y : ↥E := ⟨x, ⋯⟩
⊢ x ∈ F
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_pow_of_pow_leadingCoeff_ne_zero {f : MvPolynomial σ R} {n : ℕ}
    (hf : m.leadingCoeff f ^ n ≠ 0) :
    m.degree (f ^ n) = n • m.degree f

Proof state:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.toSyn (n • m.degree f) ≤ m.toSyn (m.degree (f ^ n))

Tactic:
apply le_degree

Result:
case a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ n • m.degree f ∈ (f ^ n).support

Proof state:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.toSyn (m.degree (f ^ n)) = m.toSyn (n • m.degree f)

Tactic:
apply le_antisymm (m.degree_pow_le n)

Result:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.toSyn (n • m.degree f) ≤ m.toSyn (m.degree (f ^ n))

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.degree (f ^ n) = n • m.degree f

Tactic:
apply m.toSyn.injective

Result:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.toSyn (m.degree (f ^ n)) = m.toSyn (n • m.degree f)

Proof state:
case a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ n • m.degree f ∈ (f ^ n).support

Tactic:
rw [mem_support_iff, coeff_pow_nsmul_degree]

Result:
case a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.leadingCoeff f ^ n ≠ 0

Proof state:
case a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.leadingCoeff f ^ n ≠ 0
⊢ m.leadingCoeff f ^ n ≠ 0

Tactic:
exact hf

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
theorem compactSpace_iff_quasiCompact (X : Scheme) :
    CompactSpace X ↔ QuasiCompact (terminal.from X)

Proof state:
X : Scheme
⊢ CompactSpace ↑↑X.toPresheafedSpace ↔ QuasiCompact (terminal.from X)

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @QuasiCompact)]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem borel_eq_borel_of_le {t t' : TopologicalSpace γ}
    (ht : PolishSpace (h := t)) (ht' : PolishSpace (h := t')) (hle : t ≤ t') :
    @borel _ t = @borel _ t'

Proof state:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
⊢ borel γ ≤ borel γ

Tactic:
intro s hs

Result:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet s

Proof state:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
e : MeasurableEmbedding id
⊢ MeasurableSet s

Tactic:
convert e.measurableSet_image.2 hs

Result:
case h.e'_3
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
e : MeasurableEmbedding id
⊢ s = id '' s

Proof state:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
have e := @Continuous.measurableEmbedding
  _ _ (@borel _ t') t' _ _ (@BorelSpace.mk _ _ (borel γ) rfl)
  t _ (@borel _ t) (@BorelSpace.mk _ t (@borel _ t) rfl) (continuous_id_of_le hle) injective_id

Result:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
e : MeasurableEmbedding id
⊢ MeasurableSet s

Proof state:
case h.e'_3
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
e : MeasurableEmbedding id
⊢ s = id '' s

Tactic:
simp only [id_eq, image_id']

Result:
no goals

Proof state:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
⊢ borel γ = borel γ

Tactic:
refine le_antisymm ?_ (borel_anti hle)

Result:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
⊢ borel γ ≤ borel γ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_iff_le_and_ne {a b : Int} : a < b ↔ a ≤ b ∧ a ≠ b

Proof state:
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
this : n ≠ 0
⊢ a < b

Tactic:
apply lt.intro

Result:
case h
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
this : n ≠ 0
⊢ a + ↑(succ ?n) = b

case n
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
this : n ≠ 0
⊢ Nat

Proof state:
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
⊢ a < b

Tactic:
have : n ≠ 0 := aneb.imp fun eq => by rw [← hn, eq, ofNat_zero, Int.add_zero]

Result:
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
this : n ≠ 0
⊢ a < b

Proof state:
a b : Int
⊢ a < b ↔ a ≤ b ∧ a ≠ b

Tactic:
refine ⟨fun h => ⟨Int.le_of_lt h, Int.ne_of_lt h⟩, fun ⟨aleb, aneb⟩ => ?_⟩

Result:
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
⊢ a < b

Proof state:
case h
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
this : n ≠ 0
⊢ a + ↑(succ ?n) = b

case n
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
this : n ≠ 0
⊢ Nat

Tactic:
rwa [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero this)] at hn

Result:
no goals

Proof state:
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
eq : n = 0
⊢ a = b

Tactic:
rw [← hn, eq, ofNat_zero, Int.add_zero]

Result:
no goals

Proof state:
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
⊢ a < b

Tactic:
let ⟨n, hn⟩ := le.dest aleb

Result:
a b : Int
x✝ : a ≤ b ∧ a ≠ b
aleb : a ≤ b
aneb : a ≠ b
n : Nat
hn : a + ↑n = b
⊢ a < b
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Lemmas.lean
theorem HeapNode.WF.realSize_eq :
    ∀ {n} {s : HeapNode α}, s.WF le a n → s.realSize + 1 = 2 ^ n
  | _, .nil, rfl => rfl
  | _, .node .., ⟨_, rfl, _, c, s⟩ => by
    rw [realSize, realSize_eq c, Nat.pow_succ, Nat.mul_succ]
    simp [Nat.add_assoc, realSize_eq s]

Proof state:
α : Type u_1
le : α → α → Bool
a a✝² : α
a✝¹ a✝ : HeapNode α
w✝ : Nat
left✝ : ∀ [inst : TotalBLE le], le a a✝² = true
c : WF le a✝² a✝¹ w✝
s : WF le a a✝ w✝
⊢ 2 ^ w✝ + a✝.realSize + 1 = 2 ^ w✝ * 1 + 2 ^ w✝

Tactic:
simp [Nat.add_assoc, realSize_eq s]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
a a✝² : α
a✝¹ a✝ : HeapNode α
w✝ : Nat
left✝ : ∀ [inst : TotalBLE le], le a a✝² = true
c : WF le a✝² a✝¹ w✝
s : WF le a a✝ w✝
⊢ (node a✝² a✝¹ a✝).realSize + 1 = 2 ^ (w✝ + 1)

Tactic:
rw [realSize, realSize_eq c, Nat.pow_succ, Nat.mul_succ]

Result:
α : Type u_1
le : α → α → Bool
a a✝² : α
a✝¹ a✝ : HeapNode α
w✝ : Nat
left✝ : ∀ [inst : TotalBLE le], le a a✝² = true
c : WF le a✝² a✝¹ w✝
s : WF le a a✝ w✝
⊢ 2 ^ w✝ + a✝.realSize + 1 = 2 ^ w✝ * 1 + 2 ^ w✝
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem add_omega0 {a : Ordinal} (h : a < ω) : a + ω = ω

Proof state:
case intro
n : ℕ
h : ↑n < ω
⊢ ↑n + ω = ω

Tactic:
exact natCast_add_omega0 n

Result:
no goals

Proof state:
a : Ordinal.{u_1}
h : a < ω
⊢ a + ω = ω

Tactic:
obtain ⟨n, rfl⟩ := lt_omega0.1 h

Result:
case intro
n : ℕ
h : ↑n < ω
⊢ ↑n + ω = ω
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_lsub_iff {ι : Type u} {f : ι → Ordinal.{max u v}} {a} :
    a < lsub.{_, v} f ↔ ∃ i, a ≤ f i

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
a : Ordinal.{max v u}
⊢ a < lsub f ↔ ∃ i, a ≤ f i

Tactic:
simpa only [not_forall, not_lt, not_le] using not_congr (@lsub_le_iff.{_, v} _ f a)

Result:
no goals
-- Mathlib/Algebra/Ring/Hom/Defs.lean
theorem coe_addMonoidHom_mkRingHomOfMulSelfOfTwoNeZero (h h_two h_one) :
    (f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one : β →+ α) = f

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x✝ : β
⊢ ↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) x✝ = f x✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
⊢ ↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) = f

Tactic:
ext

Result:
case h
α : Type u_2
β : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x✝ : β
⊢ ↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) x✝ = f x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_filterMap (f : α → Option β) (g : β → γ) (l : List α) :
    map g (filterMap f l) = filterMap (fun x => (f x).map g) l

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ
l : List α
⊢ map g (filterMap f l) = filterMap (fun x => Option.map g (f x)) l

Tactic:
simp only [← filterMap_eq_map, filterMap_filterMap, Option.map_eq_bind]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem not_lt_of_cons_le_cons [DecidableEq α] [LT α] [DecidableLT α]
    [i₀ : Std.Irrefl (· < · : α → α → Prop)]
    [i₁ : Std.Asymm (· < · : α → α → Prop)]
    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
    {a b : α} {l₁ l₂ : List α} (h : a :: l₁ ≤ b :: l₂) : ¬ b < a

Proof state:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
h : a < b
⊢ ¬b < a

Tactic:
exact i₁.asymm _ _ h

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
h : a :: l₁ ≤ b :: l₂
⊢ ¬b < a

Tactic:
rw [cons_le_cons_iff] at h

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
h : a < b ∨ a = b ∧ l₁ ≤ l₂
⊢ ¬b < a

Proof state:
case inr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a : α
l₁ l₂ : List α
h : l₁ ≤ l₂
⊢ ¬a < a

Tactic:
exact i₀.irrefl _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
h : a < b ∨ a = b ∧ l₁ ≤ l₂
⊢ ¬b < a

Tactic:
rcases h with h | ⟨rfl, h⟩

Result:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a b : α
l₁ l₂ : List α
h : a < b
⊢ ¬b < a

case inr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
a : α
l₁ l₂ : List α
h : l₁ ≤ l₂
⊢ ¬a < a
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem map_id_obj_unop (U : (Opens X)ᵒᵖ) : (map (𝟙 X)).obj (unop U) = unop U

Proof state:
X : TopCat
U : (Opens ↑X)ᵒᵖ
⊢ (map (𝟙 X)).obj (unop U) = unop U

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem colimitObjIsoColimitCompEvaluation_ι_app_hom [HasColimitsOfShape J C] (F : J ⥤ K ⥤ C)
    (j : J) (k : K) :
    (colimit.ι F j).app k ≫ (colimitObjIsoColimitCompEvaluation F k).hom =
      colimit.ι (F ⋙ (evaluation K C).obj k) j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (colimit.ι F j).app k ≫ (colimitObjIsoColimitCompEvaluation F k).hom = colimit.ι (F ⋙ (evaluation K C).obj k) j

Tactic:
dsimp [colimitObjIsoColimitCompEvaluation]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (colimit.ι F j).app k ≫ (preservesColimitIso ((evaluation K C).obj k) F).hom =
    colimit.ι (F ⋙ (evaluation K C).obj k) j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (colimit.ι F j).app k =
    colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (preservesColimitIso ((evaluation K C).obj k) F).inv

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (colimit.ι F j).app k ≫ (preservesColimitIso ((evaluation K C).obj k) F).hom =
    colimit.ι (F ⋙ (evaluation K C).obj k) j

Tactic:
rw [← Iso.eq_comp_inv]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (colimit.ι F j).app k =
    colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (preservesColimitIso ((evaluation K C).obj k) F).inv
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.length_eq {l₁ l₂ : List α} (p : l₁ ~ l₂) : length l₁ = length l₂

Proof state:
case cons
α : Type u_1
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
ih : l₁✝.length = l₂✝.length
⊢ (x✝ :: l₁✝).length = (x✝ :: l₂✝).length

Tactic:
simp only [length_cons, ih]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ l₁.length = l₂.length

Tactic:
induction p with
| nil => rfl
| cons _ _ ih => simp only [length_cons, ih]
| swap => rfl
| trans _ _ ih₁ ih₂ => simp only [ih₁, ih₂]

Result:
no goals

Proof state:
case nil
α : Type u_1
l₁ l₂ : List α
⊢ [].length = [].length

Tactic:
rfl

Result:
no goals

Proof state:
case trans
α : Type u_1
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : l₁✝.length = l₂✝.length
ih₂ : l₂✝.length = l₃✝.length
⊢ l₁✝.length = l₃✝.length

Tactic:
simp only [ih₁, ih₂]

Result:
no goals

Proof state:
case swap
α : Type u_1
l₁ l₂ : List α
x✝ y✝ : α
l✝ : List α
⊢ (y✝ :: x✝ :: l✝).length = (x✝ :: y✝ :: l✝).length

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean
theorem limitCompWhiskeringRightIsoLimitComp_inv_π {C : Type*} [Category C] {D : Type*}
    [Category D] {E : Type*} [Category E] {J : Type*} [Category J]
    [HasLimitsOfShape J D] (F : D ⥤ E) [PreservesLimitsOfShape J F] (G : J ⥤ C ⥤ D) (j : J) :
    (limitCompWhiskeringRightIsoLimitComp F G).inv ≫
      limit.π (G ⋙ (whiskeringRight _ _ _).obj F) j = whiskerRight (limit.π G j) F

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{u_7, u_3} E
J : Type u_4
inst✝² : Category.{u_8, u_4} J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
G : J ⥤ C ⥤ D
j : J
⊢ (limitCompWhiskeringRightIsoLimitComp F G).inv ≫ limit.π (G ⋙ (whiskeringRight C D E).obj F) j =
    whiskerRight (limit.π G j) F

Tactic:
simp [limitCompWhiskeringRightIsoLimitComp]

Result:
no goals