harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_add_of_degree_eq (h : degree p = degree q)
    (hlc : leadingCoeff p + leadingCoeff q ≠ 0) :
    leadingCoeff (p + q) = leadingCoeff p + leadingCoeff q

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
⊢ (p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff

Tactic:
have : natDegree (p + q) = natDegree p := by
  apply natDegree_eq_of_degree_eq
  rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
this : (p + q).natDegree = p.natDegree
⊢ (p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff

Proof state:
case h
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
⊢ (p + q).degree = p.degree

Tactic:
rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
this : (p + q).natDegree = p.natDegree
⊢ (p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff

Tactic:
simp only [leadingCoeff, this, natDegree_eq_of_degree_eq h, coeff_add]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
⊢ (p + q).natDegree = p.natDegree

Tactic:
apply natDegree_eq_of_degree_eq

Result:
case h
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
⊢ (p + q).degree = p.degree
-- Mathlib/Tactic/ComputeDegree.lean
theorem coeff_pow_of_natDegree_le_of_eq_ite' {m n o : ℕ} {a : R} {p : R[X]}
    (h_pow : natDegree p ≤ n) (h_exp : m * n ≤ o) (h_pow_bas : coeff p n = a) :
    coeff (p ^ m) o = if o = m * n then a ^ m else 0

Proof state:
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ m * n ≠ o

Tactic:
exact Iff.mp ne_comm h

Result:
no goals

Proof state:
case neg.h
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).natDegree < o

Tactic:
apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ‹_› ?_)

Result:
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).natDegree ≤ m * n

R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ m * n ≠ o

Proof state:
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
⊢ (p ^ m).coeff o = if o = m * n then a ^ m else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : o = m * n
⊢ (p ^ m).coeff o = a ^ m

case neg
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).coeff o = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).coeff o = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt

Result:
case neg.h
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).natDegree < o

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
m n : ℕ
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = p.coeff n ^ m

Tactic:
exact coeff_pow_of_natDegree_le ‹_›

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : o = m * n
⊢ (p ^ m).coeff o = a ^ m

Tactic:
subst h h_pow_bas

Result:
case pos
R : Type u_1
inst✝ : Semiring R
m n : ℕ
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = p.coeff n ^ m

Proof state:
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).natDegree ≤ m * n

Tactic:
exact natDegree_pow_le_of_le m ‹_›

Result:
no goals
-- Mathlib/Topology/Algebra/ClosedSubgroup.lean
lemma normalCore_isClosed (H : Subgroup G) (h : IsClosed (H : Set G)) :
    IsClosed (H.normalCore : Set G)

Proof state:
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
h : IsClosed ↑H
⊢ IsClosed (⋂ i, ↑(i • H))

Tactic:
apply isClosed_iInter

Result:
case h
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
h : IsClosed ↑H
⊢ ∀ (i : ConjAct G), IsClosed ↑(i • H)

Proof state:
case h.e'_3
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
h : IsClosed ↑H
g : ConjAct G
⊢ ↑(g • H) = (fun h => ConjAct.ofConjAct g⁻¹ * h * (ConjAct.ofConjAct g⁻¹)⁻¹) ⁻¹' ↑H

Tactic:
exact Set.ext (fun t ↦ Set.mem_smul_set_iff_inv_smul_mem)

Result:
no goals

Proof state:
case h
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
h : IsClosed ↑H
g : ConjAct G
⊢ IsClosed ↑(g • H)

Tactic:
convert IsClosed.preimage (IsTopologicalGroup.continuous_conj (ConjAct.ofConjAct g⁻¹)) h

Result:
case h.e'_3
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
h : IsClosed ↑H
g : ConjAct G
⊢ ↑(g • H) = (fun h => ConjAct.ofConjAct g⁻¹ * h * (ConjAct.ofConjAct g⁻¹)⁻¹) ⁻¹' ↑H

Proof state:
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
h : IsClosed ↑H
⊢ IsClosed ↑(⨅ g, g • H)

Tactic:
push_cast

Result:
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
h : IsClosed ↑H
⊢ IsClosed (⋂ i, ↑(i • H))

Proof state:
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
h : IsClosed ↑H
⊢ IsClosed ↑H.normalCore

Tactic:
rw [normalCore_eq_iInf_conjAct]

Result:
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
h : IsClosed ↑H
⊢ IsClosed ↑(⨅ g, g • H)

Proof state:
case h
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
h : IsClosed ↑H
⊢ ∀ (i : ConjAct G), IsClosed ↑(i • H)

Tactic:
intro g

Result:
case h
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
h : IsClosed ↑H
g : ConjAct G
⊢ IsClosed ↑(g • H)
-- Mathlib/Order/WithBot.lean
/-- A version of `bot_lt_iff_ne_bot` for `WithBot` that only requires `LT α`, not
`PartialOrder α`. -/
protected lemma bot_lt_iff_ne_bot : ⊥ < x ↔ x ≠ ⊥

Proof state:
α : Type u_1
inst✝ : LT α
x : WithBot α
⊢ ⊥ < x ↔ x ≠ ⊥

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/Quantale.lean
theorem iSup_mul_distrib : (⨆ i, f i) * x = ⨆ i, f i * x

Proof state:
α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ (⨆ i, f i) * x = ⨆ i, f i * x

Tactic:
rw [iSup, sSup_mul_distrib, iSup_range]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem equiv_mul_right (g : G) (k : K) :
    hSK.equiv (g * k) = ((hSK.equiv g).fst, (hSK.equiv g).snd * k)

Proof state:
case fst.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ ↑(hSK.equiv (g * ↑k)).1 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).1

Tactic:
rw [this]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ hSK.equiv (g * ↑k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k)

Tactic:
ext

Result:
case fst.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ ↑(hSK.equiv (g * ↑k)).1 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).1

case snd.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ ↑(hSK.equiv (g * ↑k)).2 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).2

Proof state:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
⊢ LeftCosetEquivalence (↑K) (g * ↑k) g

Tactic:
simp [LeftCosetEquivalence, leftCoset_eq_iff]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
⊢ hSK.equiv (g * ↑k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k)

Tactic:
have : (hSK.equiv (g * k)).fst = (hSK.equiv g).fst :=
  hSK.equiv_fst_eq_iff_leftCosetEquivalence.2
    (by simp [LeftCosetEquivalence, leftCoset_eq_iff])

Result:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ hSK.equiv (g * ↑k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k)

Proof state:
case snd.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1
⊢ ↑(hSK.equiv (g * ↑k)).2 = ↑((hSK.equiv g).1, (hSK.equiv g).2 * k).2

Tactic:
rw [coe_mul, equiv_snd_eq_inv_mul, this, equiv_snd_eq_inv_mul, mul_assoc]

Result:
no goals
-- Mathlib/Order/InitialSeg.lean
theorem irrefl {r : α → α → Prop} [IsWellOrder α r] (f : r ≺i r) : False

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r f.top f.top
⊢ False

Tactic:
exact _root_.irrefl _ h

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
⊢ False

Tactic:
have h := f.lt_top f.top

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r (f.toRelEmbedding f.top) f.top
⊢ False

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r (f.toRelEmbedding f.top) f.top
⊢ False

Tactic:
rw [show f f.top = f.top from InitialSeg.eq f (InitialSeg.refl r) f.top] at h

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r f.top f.top
⊢ False
-- Mathlib/Data/Nat/Set.lean
theorem zero_union_range_succ : {0} ∪ range succ = univ

Proof state:
case h
n : ℕ
⊢ n ∈ {0} ∪ range succ ↔ n ∈ univ

Tactic:
cases n <;> simp

Result:
no goals

Proof state:
⊢ {0} ∪ range succ = univ

Tactic:
ext n

Result:
case h
n : ℕ
⊢ n ∈ {0} ∪ range succ ↔ n ∈ univ
-- Mathlib/Probability/Moments/Basic.lean
lemma mgf_id_map (hX : AEMeasurable X μ) : mgf id (μ.map X) = mgf X μ

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ AEStronglyMeasurable (fun ω => rexp (t * id ω)) (Measure.map X μ)

Tactic:
exact (measurable_const_mul _).exp.aestronglyMeasurable

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
⊢ mgf id (Measure.map X μ) = mgf X μ

Tactic:
ext t

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ mgf id (Measure.map X μ) t = mgf X μ t

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ mgf id (Measure.map X μ) t = mgf X μ t

Tactic:
rw [mgf, integral_map hX]

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ ∫ (x : Ω), rexp (t * id (X x)) ∂μ = mgf X μ t

case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ AEStronglyMeasurable (fun ω => rexp (t * id ω)) (Measure.map X μ)

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ ∫ (x : Ω), rexp (t * id (X x)) ∂μ = mgf X μ t

Tactic:
simp [mgf]

Result:
no goals
-- Mathlib/Data/Nat/Count.lean
theorem count_injective {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) : m = n

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
⊢ m = n

Tactic:
by_contra! h : m ≠ n

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
⊢ False

Proof state:
case inr
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
this : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ}, p m → p n → count p m = count p n → m ≠ n → m < n → False
hmn : ¬m < n
⊢ False

Tactic:
exact this hn hm heq.symm h.symm (h.lt_or_lt.resolve_left hmn)

Result:
no goals

Proof state:
p✝ : ℕ → Prop
inst✝¹ : DecidablePred p✝
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
hmn : m < n
⊢ False

Tactic:
simpa [heq] using count_strict_mono hm hmn

Result:
no goals

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
⊢ False

Tactic:
wlog hmn : m < n

Result:
case inr
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
this : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ}, p m → p n → count p m = count p n → m ≠ n → m < n → False
hmn : ¬m < n
⊢ False

p✝ : ℕ → Prop
inst✝¹ : DecidablePred p✝
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
hmn : m < n
⊢ False
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inv_inl (r : R) :
    (inl r)⁻¹ = (inl (r⁻¹ : R) : tsze R M)

Proof state:
case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ (inl r)⁻¹.snd = (inl r⁻¹).snd

Tactic:
rw [snd_inv, fst_inl, snd_inl, snd_inl, smul_zero, smul_zero, neg_zero]

Result:
no goals

Proof state:
case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ (inl r)⁻¹.fst = (inl r⁻¹).fst

Tactic:
rw [fst_inv, fst_inl, fst_inl]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ (inl r)⁻¹ = inl r⁻¹

Tactic:
ext

Result:
case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ (inl r)⁻¹.fst = (inl r⁻¹).fst

case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ (inl r)⁻¹.snd = (inl r⁻¹).snd
-- Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
@[reassoc (attr := simp)]
lemma homEquiv_apply_π (τ : F₁ ⟶ F₂) (j : J) :
    homEquiv V τ ≫ enrichedHomπ V _ _ j = eHomEquiv V (τ.app j)

Proof state:
V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₂
τ : F₁ ⟶ F₂
j : J
⊢ (homEquiv V) τ ≫ enrichedHomπ V F₁ F₂ j = (eHomEquiv V) (τ.app j)

Tactic:
simp [homEquiv]

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Final.lean
theorem Functor.final_of_isFiltered_of_pUnit [IsFiltered C] (F : C ⥤ Discrete PUnit) :
    Final F

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ ∃ t, x✝¹ ≫ F.map t = x✝ ≫ F.map t

Tactic:
use 𝟙 c

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ x✝¹ ≫ F.map (𝟙 c) = x✝ ≫ F.map (𝟙 c)

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ Nonempty (x✝ ⟶ F.obj (Classical.choice ⋯))

Tactic:
exact ⟨Discrete.eqToHom (by simp)⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
⊢ F.Final

Tactic:
refine final_of_exists_of_isFiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)

Result:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∃ c, Nonempty (x✝ ⟶ F.obj c)

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ ∃ c' t, x✝¹ ≫ F.map t = x✝ ≫ F.map t

Proof state:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∃ c, Nonempty (x✝ ⟶ F.obj c)

Tactic:
use Classical.choice IsFiltered.nonempty

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ Nonempty (x✝ ⟶ F.obj (Classical.choice ⋯))

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ ∃ c' t, x✝¹ ≫ F.map t = x✝ ≫ F.map t

Tactic:
use c

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ ∃ t, x✝¹ ≫ F.map t = x✝ ≫ F.map t

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ x✝.as = (F.obj (Classical.choice ⋯)).as

Tactic:
simp

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ x✝¹ ≫ F.map (𝟙 c) = x✝ ≫ F.map (𝟙 c)

Tactic:
apply Subsingleton.elim

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem goldConj_irrational : Irrational ψ

Proof state:
this✝ : Irrational √↑5
this : Irrational (↑1 - √↑5)
⊢ Irrational ψ

Tactic:
convert this.rat_mul (show (0.5 : ℚ) ≠ 0 by norm_num)

Result:
case h.e'_1
this✝ : Irrational √↑5
this : Irrational (↑1 - √↑5)
⊢ ψ = ↑0.5 * (↑1 - √↑5)

Proof state:
⊢ Nat.Prime 5

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_1
this✝ : Irrational √↑5
this : Irrational (↑1 - √↑5)
⊢ ψ = 1 / 2 * (1 - √5)

Tactic:
field_simp

Result:
no goals

Proof state:
⊢ Irrational ψ

Tactic:
have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)

Result:
this : Irrational √↑5
⊢ Irrational ψ

Proof state:
this : Irrational √↑5
⊢ Irrational ψ

Tactic:
have := this.rat_sub 1

Result:
this✝ : Irrational √↑5
this : Irrational (↑1 - √↑5)
⊢ Irrational ψ

Proof state:
this✝ : Irrational √↑5
this : Irrational (↑1 - √↑5)
⊢ 0.5 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_1
this✝ : Irrational √↑5
this : Irrational (↑1 - √↑5)
⊢ ψ = ↑0.5 * (↑1 - √↑5)

Tactic:
norm_num

Result:
case h.e'_1
this✝ : Irrational √↑5
this : Irrational (↑1 - √↑5)
⊢ ψ = 1 / 2 * (1 - √5)
-- Mathlib/.lake/packages/lean4/src/lean/Init/System/Platform.lean
theorem numBits_pos : 0 < numBits

Proof state:
h : numBits = 64
⊢ 0 < numBits

Tactic:
simp [h]

Result:
no goals

Proof state:
⊢ 0 < numBits

Tactic:
cases numBits_eq <;> next h => simp [h]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.conj : IsCycle f → IsCycle (g * f * g⁻¹)

Proof state:
case intro.intro
α : Type u_2
f g : Perm α
x : α
hx : f x ≠ x
h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ (g * f * g⁻¹).IsCycle

Tactic:
refine ⟨g x, by simp [coe_mul, inv_apply_self, hx], fun y hy => ?_⟩

Result:
case intro.intro
α : Type u_2
f g : Perm α
x : α
hx : f x ≠ x
h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
y : α
hy : (g * f * g⁻¹) y ≠ y
⊢ (g * f * g⁻¹).SameCycle (g x) y

Proof state:
α : Type u_2
f g : Perm α
x : α
hx : f x ≠ x
h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ (g * f * g⁻¹) (g x) ≠ g x

Tactic:
simp [coe_mul, inv_apply_self, hx]

Result:
no goals

Proof state:
α : Type u_2
f g : Perm α
⊢ f.IsCycle → (g * f * g⁻¹).IsCycle

Tactic:
rintro ⟨x, hx, h⟩

Result:
case intro.intro
α : Type u_2
f g : Perm α
x : α
hx : f x ≠ x
h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ (g * f * g⁻¹).IsCycle

Proof state:
case intro.intro
α : Type u_2
f g : Perm α
x : α
hx : f x ≠ x
h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
y : α
hy : (g * f * g⁻¹) y ≠ y
⊢ (g * f * g⁻¹).SameCycle (g x) (g (g⁻¹ y))

Tactic:
exact (h <| eq_inv_iff_eq.not.2 hy).conj

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
f g : Perm α
x : α
hx : f x ≠ x
h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
y : α
hy : (g * f * g⁻¹) y ≠ y
⊢ (g * f * g⁻¹).SameCycle (g x) y

Tactic:
rw [← apply_inv_self g y]

Result:
case intro.intro
α : Type u_2
f g : Perm α
x : α
hx : f x ≠ x
h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
y : α
hy : (g * f * g⁻¹) y ≠ y
⊢ (g * f * g⁻¹).SameCycle (g x) (g (g⁻¹ y))
-- Mathlib/Topology/Sheaves/Limits.lean
theorem isSheaf_of_isLimit [HasLimits C] {X : TopCat} (F : J ⥤ Presheaf.{v} C X)
    (H : ∀ j, (F.obj j).IsSheaf) {c : Cone F} (hc : IsLimit c) : c.pt.IsSheaf

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimits C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), (F.obj j).IsSheaf
c : Cone F
hc : IsLimit c
⊢ c.pt.IsSheaf

Tactic:
let F' : J ⥤ Sheaf C X :=
  { obj := fun j => ⟨F.obj j, H j⟩
    map := fun f => ⟨F.map f⟩ }

Result:
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimits C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), (F.obj j).IsSheaf
c : Cone F
hc : IsLimit c
F' : J ⥤ Sheaf C X :=
  { obj := fun j => { val := F.obj j, cond := ⋯ }, map := fun {X_1 Y} f => { val := F.map f }, map_id := ⋯,
    map_comp := ⋯ }
⊢ c.pt.IsSheaf

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimits C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), (F.obj j).IsSheaf
c : Cone F
hc : IsLimit c
F' : J ⥤ Sheaf C X :=
  { obj := fun j => { val := F.obj j, cond := ⋯ }, map := fun {X_1 Y} f => { val := F.map f }, map_id := ⋯,
    map_comp := ⋯ }
⊢ c.pt.IsSheaf

Tactic:
let e : F' ⋙ Sheaf.forget C X ≅ F := NatIso.ofComponents fun _ => Iso.refl _

Result:
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimits C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), (F.obj j).IsSheaf
c : Cone F
hc : IsLimit c
F' : J ⥤ Sheaf C X :=
  { obj := fun j => { val := F.obj j, cond := ⋯ }, map := fun {X_1 Y} f => { val := F.map f }, map_id := ⋯,
    map_comp := ⋯ }
e : F' ⋙ Sheaf.forget C X ≅ F := NatIso.ofComponents (fun x => Iso.refl ((F' ⋙ Sheaf.forget C X).obj x)) ⋯
⊢ c.pt.IsSheaf

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimits C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), (F.obj j).IsSheaf
c : Cone F
hc : IsLimit c
F' : J ⥤ Sheaf C X :=
  { obj := fun j => { val := F.obj j, cond := ⋯ }, map := fun {X_1 Y} f => { val := F.map f }, map_id := ⋯,
    map_comp := ⋯ }
e : F' ⋙ Sheaf.forget C X ≅ F := NatIso.ofComponents (fun x => Iso.refl ((F' ⋙ Sheaf.forget C X).obj x)) ⋯
⊢ c.pt.IsSheaf

Tactic:
exact Presheaf.isSheaf_of_iso
  ((isLimitOfPreserves (Sheaf.forget C X) (limit.isLimit F')).conePointsIsoOfNatIso hc e)
  (limit F').2

Result:
no goals