harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem ker_eq_bot_of_injective {f : F} (hf : Injective f) : ker f = ⊥

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_11
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : Injective ⇑f
⊢ ker f = ⊥

Tactic:
rw [eq_bot_iff]

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_11
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : Injective ⇑f
⊢ ker f ≤ ⊥

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_11
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : Injective ⇑f
x : M
hx : x ∈ ker f
⊢ x ∈ ⊥

Tactic:
simpa only [mem_ker, mem_bot, ← map_zero f, hf.eq_iff] using hx

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_11
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : Injective ⇑f
⊢ ker f ≤ ⊥

Tactic:
intro x hx

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_11
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : Injective ⇑f
x : M
hx : x ∈ ker f
⊢ x ∈ ⊥
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem divInt_self (a : Rat) : a.num /. a.den = a

Proof state:
a : Rat
⊢ a.num /. ↑a.den = a

Tactic:
rw [divInt_ofNat, mkRat_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/HashSet/Lemmas.lean
theorem ext {m m' : HashSet α} : m.inner = m'.inner → m = m'

Proof state:
case mk.mk
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
inner✝¹ inner✝ : HashMap α Unit
⊢ { inner := inner✝¹ }.inner = { inner := inner✝ }.inner → { inner := inner✝¹ } = { inner := inner✝ }

Tactic:
rintro rfl

Result:
case mk.mk
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
inner✝ : HashMap α Unit
⊢ { inner := inner✝ } = { inner := { inner := inner✝ }.inner }

Proof state:
case mk
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m' : HashSet α
inner✝ : HashMap α Unit
⊢ { inner := inner✝ }.inner = m'.inner → { inner := inner✝ } = m'

Tactic:
cases m'

Result:
case mk.mk
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
inner✝¹ inner✝ : HashMap α Unit
⊢ { inner := inner✝¹ }.inner = { inner := inner✝ }.inner → { inner := inner✝¹ } = { inner := inner✝ }

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m m' : HashSet α
⊢ m.inner = m'.inner → m = m'

Tactic:
cases m

Result:
case mk
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m' : HashSet α
inner✝ : HashMap α Unit
⊢ { inner := inner✝ }.inner = m'.inner → { inner := inner✝ } = m'

Proof state:
case mk.mk
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
inner✝ : HashMap α Unit
⊢ { inner := inner✝ } = { inner := { inner := inner✝ }.inner }

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
lemma pairwiseDisjoint_piAntidiag_map_addRightEmbedding (hi : i ∉ s) (n : μ) :
    (antidiagonal n : Set (μ × μ)).PairwiseDisjoint fun p ↦
      map (addRightEmbedding fun j ↦ if j = i then p.1 else 0) (s.piAntidiag p.2)

Proof state:
case mk.mk
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a b : μ
hab : (a, b) ∈ ↑(antidiagonal n)
c d : μ
hcd : (c, d) ∈ ↑(antidiagonal n)
⊢ (a, b) ≠ (c, d) →
    (Disjoint on fun p => map (addRightEmbedding fun j => if j = i then p.1 else 0) (s.piAntidiag p.2)) (a, b) (c, d)

Tactic:
simp only [ne_eq, antidiagonal_congr' hab hcd, disjoint_left, mem_map, mem_piAntidiag,
  addRightEmbedding_apply, not_exists, not_and, and_imp, forall_exists_index]

Result:
case mk.mk
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a b : μ
hab : (a, b) ∈ ↑(antidiagonal n)
c d : μ
hcd : (c, d) ∈ ↑(antidiagonal n)
⊢ ¬b = d →
    ∀ ⦃a_2 : ι → μ⦄ (x : ι → μ),
      s.sum x = b →
        (∀ (i : ι), ¬x i = 0 → i ∈ s) →
          (x + fun j => if j = i then a else 0) = a_2 →
            ∀ (x : ι → μ), s.sum x = d → (∀ (i : ι), ¬x i = 0 → i ∈ s) → ¬(x + fun j => if j = i then c else 0) = a_2

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun p =>
    map (addRightEmbedding fun j => if j = i then p.1 else 0) (s.piAntidiag p.2)

Tactic:
rintro ⟨a, b⟩ hab ⟨c, d⟩ hcd

Result:
case mk.mk
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a b : μ
hab : (a, b) ∈ ↑(antidiagonal n)
c d : μ
hcd : (c, d) ∈ ↑(antidiagonal n)
⊢ (a, b) ≠ (c, d) →
    (Disjoint on fun p => map (addRightEmbedding fun j => if j = i then p.1 else 0) (s.piAntidiag p.2)) (a, b) (c, d)

Proof state:
case mk.mk
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a b : μ
hab : (a, b) ∈ ↑(antidiagonal n)
c d : μ
hcd : (c, d) ∈ ↑(antidiagonal n)
⊢ ¬b = d →
    ∀ ⦃a_2 : ι → μ⦄ (x : ι → μ),
      s.sum x = b →
        (∀ (i : ι), ¬x i = 0 → i ∈ s) →
          (x + fun j => if j = i then a else 0) = a_2 →
            ∀ (x : ι → μ), s.sum x = d → (∀ (i : ι), ¬x i = 0 → i ∈ s) → ¬(x + fun j => if j = i then c else 0) = a_2

Tactic:
rintro hfg _ f rfl - rfl g rfl - hgf

Result:
case mk.mk
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a c : μ
f : ι → μ
hab : (a, s.sum f) ∈ ↑(antidiagonal n)
g : ι → μ
hcd : (c, s.sum g) ∈ ↑(antidiagonal n)
hfg : ¬s.sum f = s.sum g
hgf : (g + fun j => if j = i then c else 0) = f + fun j => if j = i then a else 0
⊢ False
-- Mathlib/RingTheory/EssentialFiniteness.lean
lemma essFiniteType_iff_exists_subalgebra : EssFiniteType R S ↔
    ∃ (S₀ : Subalgebra R S) (M : Submonoid S₀), FiniteType R S₀ ∧ IsLocalization M S

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ EssFiniteType R S ↔ ∃ S₀ M, FiniteType R ↥S₀ ∧ IsLocalization M S

Tactic:
refine ⟨fun h ↦ ⟨subalgebra R S, submonoid R S, inferInstance, inferInstance⟩, ?_⟩

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∃ S₀ M, FiniteType R ↥S₀ ∧ IsLocalization M S) → EssFiniteType R S

Proof state:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
M : Submonoid ↥S₀
left✝ : FiniteType R ↥S₀
right✝ : IsLocalization M S
this : EssFiniteType (↥S₀) S := of_isLocalization S M
⊢ EssFiniteType R S

Tactic:
exact comp R S₀ S

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
M : Submonoid ↥S₀
left✝ : FiniteType R ↥S₀
right✝ : IsLocalization M S
⊢ EssFiniteType R S

Tactic:
letI := of_isLocalization S M

Result:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
M : Submonoid ↥S₀
left✝ : FiniteType R ↥S₀
right✝ : IsLocalization M S
this : EssFiniteType (↥S₀) S := of_isLocalization S M
⊢ EssFiniteType R S

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∃ S₀ M, FiniteType R ↥S₀ ∧ IsLocalization M S) → EssFiniteType R S

Tactic:
rintro ⟨S₀, M, _, _⟩

Result:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
M : Submonoid ↥S₀
left✝ : FiniteType R ↥S₀
right✝ : IsLocalization M S
⊢ EssFiniteType R S
-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.ext {α : TypeVec n} (x y : Cofix F α) (h : x.dest = y.dest) : x = y

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : Cofix F α
h : x.dest = y.dest
⊢ x = y

Tactic:
rw [← Cofix.mk_dest x, h, Cofix.mk_dest]

Result:
no goals
-- Mathlib/Logic/Unique.lean
theorem nonempty_unique (α : Sort u) [Subsingleton α] [Nonempty α] : Nonempty (Unique α)

Proof state:
α : Sort u
inst✝¹ : Subsingleton α
inst✝ : Nonempty α
⊢ Nonempty (Unique α)

Tactic:
inhabit α

Result:
α : Sort u
inst✝¹ : Subsingleton α
inst✝ : Nonempty α
inhabited_h : Inhabited α
⊢ Nonempty (Unique α)

Proof state:
α : Sort u
inst✝¹ : Subsingleton α
inst✝ : Nonempty α
inhabited_h : Inhabited α
⊢ Nonempty (Unique α)

Tactic:
exact ⟨Unique.mk' α⟩

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
lemma contravariant_sequence_exact₃ {n₁ : ℕ} (x₃ : Ext S.X₃ Y n₁)
    (hx₃ : (mk₀ S.g).comp x₃ (zero_add n₁) = 0) {n₀ : ℕ} (hn₀ : 1 + n₀ = n₁) :
    ∃ (x₁ : Ext S.X₁ Y n₀), hS.extClass.comp x₁ hn₀ = x₃

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₁ : ℕ
x₃ : Ext S.X₃ Y n₁
hx₃ : (mk₀ S.g).comp x₃ ⋯ = 0
n₀ : ℕ
hn₀ : 1 + n₀ = n₁
this :
  (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y hn₀)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) ⋯).Exact
⊢ ∃ x₁, hS.extClass.comp x₁ hn₀ = x₃

Tactic:
rw [ShortComplex.ab_exact_iff] at this

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₁ : ℕ
x₃ : Ext S.X₃ Y n₁
hx₃ : (mk₀ S.g).comp x₃ ⋯ = 0
n₀ : ℕ
hn₀ : 1 + n₀ = n₁
this :
  ∀
    (x₂ :
      ↑(ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y hn₀)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯))
            ⋯).X₂),
    (ConcreteCategory.hom
            (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y hn₀)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯))
                ⋯).g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y hn₀)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯))
                  ⋯).f)
            x₁ =
          x₂
⊢ ∃ x₁, hS.extClass.comp x₁ hn₀ = x₃

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₁ : ℕ
x₃ : Ext S.X₃ Y n₁
hx₃ : (mk₀ S.g).comp x₃ ⋯ = 0
n₀ : ℕ
hn₀ : 1 + n₀ = n₁
⊢ ∃ x₁, hS.extClass.comp x₁ hn₀ = x₃

Tactic:
have := contravariant_sequence_exact₃' hS Y n₀ n₁ hn₀

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₁ : ℕ
x₃ : Ext S.X₃ Y n₁
hx₃ : (mk₀ S.g).comp x₃ ⋯ = 0
n₀ : ℕ
hn₀ : 1 + n₀ = n₁
this :
  (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y hn₀)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) ⋯).Exact
⊢ ∃ x₁, hS.extClass.comp x₁ hn₀ = x₃

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₁ : ℕ
x₃ : Ext S.X₃ Y n₁
hx₃ : (mk₀ S.g).comp x₃ ⋯ = 0
n₀ : ℕ
hn₀ : 1 + n₀ = n₁
this :
  ∀
    (x₂ :
      ↑(ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y hn₀)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯))
            ⋯).X₂),
    (ConcreteCategory.hom
            (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y hn₀)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯))
                ⋯).g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y hn₀)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯))
                  ⋯).f)
            x₁ =
          x₂
⊢ ∃ x₁, hS.extClass.comp x₁ hn₀ = x₃

Tactic:
exact this x₃ hx₃

Result:
no goals
-- Mathlib/NumberTheory/ZetaValues.lean
theorem hasSum_zeta_two : HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 2) (π ^ 2 / 6)

Proof state:
case h.e'_6

⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 * 1 - 1) * π ^ (2 * 1) * ↑(bernoulli (2 * 1)) / ↑(2 * 1)!

Tactic:
rw [mul_one]

Result:
case h.e'_6

⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(bernoulli 2) / ↑2!

Proof state:
case h.e'_6

⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(bernoulli 2) / ↑2!

Tactic:
rw [bernoulli_eq_bernoulli'_of_ne_one (by decide : 2 ≠ 1), bernoulli'_two]

Result:
case h.e'_6

⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(1 / 6) / ↑2!

Proof state:
⊢ HasSum (fun n => 1 / ↑n ^ 2) (π ^ 2 / 6)

Tactic:
convert hasSum_zeta_nat one_ne_zero using 1

Result:
case h.e'_6

⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 * 1 - 1) * π ^ (2 * 1) * ↑(bernoulli (2 * 1)) / ↑(2 * 1)!

Proof state:
case h.e'_6

⊢ π ^ 2 * (6 * 2) = 2 * π ^ 2 * 6

Tactic:
ring

Result:
no goals

Proof state:
⊢ 2 ≠ 1

Tactic:
decide

Result:
no goals

Proof state:
case h.e'_6

⊢ π ^ 2 / 6 = 2 * π ^ 2 * (1 / 6) / 2

Tactic:
field_simp

Result:
case h.e'_6

⊢ π ^ 2 * (6 * 2) = 2 * π ^ 2 * 6

Proof state:
case h.e'_6

⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(1 / 6) / ↑2!

Tactic:
norm_num [Nat.factorial]

Result:
case h.e'_6

⊢ π ^ 2 / 6 = 2 * π ^ 2 * (1 / 6) / 2
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem ne_infty_iff_exists {x : OnePoint X} : x ≠ ∞ ↔ ∃ y : X, (y : OnePoint X) = x

Proof state:
X : Type u_1
x : OnePoint X
⊢ x ≠ ∞ ↔ ∃ y, ↑y = x

Tactic:
induction x using OnePoint.rec <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Enrichment.lean
lemma enrichedOrdinaryCategorySelf_eHomWhiskerLeft (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :
    eHomWhiskerLeft C X g = (ihom X).map g

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ (ρ_ ((ihom X).obj Y₁)).inv ≫ (ihom X).obj Y₁ ◁ curry' g ≫ comp X Y₁ Y₂ = (ihom X).map g

Tactic:
rw [whiskerLeft_curry'_comp, Iso.inv_hom_id_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ eHomWhiskerLeft C X g = (ihom X).map g

Tactic:
change (ρ_ _).inv ≫ _ ◁ curry' g ≫ comp X Y₁ Y₂ = _

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ (ρ_ ((ihom X).obj Y₁)).inv ≫ (ihom X).obj Y₁ ◁ curry' g ≫ comp X Y₁ Y₂ = (ihom X).map g
-- Mathlib/Data/Num/Lemmas.lean
theorem one_le_cast [LinearOrderedSemiring α] (n : PosNum) : (1 : α) ≤ n

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemiring α
n : PosNum
⊢ 1 ≤ ↑n

Tactic:
apply to_nat_pos

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
lemma pairingIn_neg_two_neg_two_iff :
    P.pairingIn S i j = -2 ∧ P.pairingIn S j i = -2 ↔ P.root i = -P.root j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst✝⁶ : Finite ι
inst✝⁵ : CharZero R
inst✝⁴ : NoZeroSMulDivisors R M
inst✝³ : LinearOrderedCommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
⊢ P.pairingIn S i j = -2 ∧ P.pairingIn S j i = -2 ↔ P.root i = -P.root j

Tactic:
simp only [← P.pairing_neg_two_neg_two_iff, ← P.algebraMap_pairingIn S,
  ← map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff, ← map_neg]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp]
lemma tail_cons {t u v} (p : G.Walk u v) (h : G.Adj t u) :
    (p.cons h).tail = p.copy (getVert_zero p).symm rfl

Proof state:
V : Type u
G : SimpleGraph V
t u v : V
p : G.Walk u v
h : G.Adj t u
⊢ (cons h p).tail = p.copy ⋯ ⋯

Tactic:
match p with
| .nil => rfl
| .cons h q => rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
t u v : V
p : G.Walk u v
h : G.Adj t u
⊢ (cons h nil).tail = nil.copy ⋯ ⋯

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
t u v✝¹ : V
p : G.Walk u v✝¹
h✝ : G.Adj t u
v v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
⊢ (cons h✝ (cons h q)).tail = (cons h q).copy ⋯ ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/FieldTheory/Differential/Basic.lean
@[simp]
lemma logDeriv_zero : logDeriv (0 : R) = 0

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
⊢ logDeriv 0 = 0

Tactic:
simp [logDeriv]

Result:
no goals
-- Mathlib/Algebra/Module/Equiv/Basic.lean
theorem ofSubsingleton_self : ofSubsingleton M M = refl R M

Proof state:
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
⊢ ofSubsingleton M M = refl R M

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x✝ : M
⊢ (ofSubsingleton M M) x✝ = (refl R M) x✝

Proof state:
case h
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x✝ : M
⊢ (ofSubsingleton M M) x✝ = (refl R M) x✝

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Topology/PartitionOfUnity.lean
theorem exists_finset_nhd' {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) :
    ∃ I : Finset ι, (∀ᶠ x in 𝓝[s] x₀, ∑ i ∈ I, ρ i x = 1) ∧
      ∀ᶠ x in 𝓝 x₀, support (ρ · x) ⊆ I

Proof state:
case intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI : ∀ᶠ (x : X) in 𝓝 x₀, (support fun i => (ρ i) x) ⊆ ↑I
⊢ ∃ I, (∀ᶠ (x : X) in 𝓝[s] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 => (ρ x_1) x) ⊆ ↑I

Tactic:
refine ⟨I, eventually_nhdsWithin_iff.mpr (hI.mono fun x hx x_in ↦ ?_), hI⟩

Result:
case intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI : ∀ᶠ (x : X) in 𝓝 x₀, (support fun i => (ρ i) x) ⊆ ↑I
x : X
hx : (support fun i => (ρ i) x) ⊆ ↑I
x_in : x ∈ s
⊢ ∑ i ∈ I, (ρ i) x = 1

Proof state:
case intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI : ∀ᶠ (x : X) in 𝓝 x₀, (support fun i => (ρ i) x) ⊆ ↑I
x : X
hx : (support fun i => (ρ i) x) ⊆ ↑I
x_in : x ∈ s
⊢ ∑ i ∈ I, (ρ i) x = 1

Tactic:
have : ∑ᶠ i : ι, ρ i x = ∑ i ∈ I, ρ i x := finsum_eq_sum_of_support_subset _ hx

Result:
case intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI : ∀ᶠ (x : X) in 𝓝 x₀, (support fun i => (ρ i) x) ⊆ ↑I
x : X
hx : (support fun i => (ρ i) x) ⊆ ↑I
x_in : x ∈ s
this : ∑ᶠ (i : ι), (ρ i) x = ∑ i ∈ I, (ρ i) x
⊢ ∑ i ∈ I, (ρ i) x = 1

Proof state:
case intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI : ∀ᶠ (x : X) in 𝓝 x₀, (support fun i => (ρ i) x) ⊆ ↑I
x : X
hx : (support fun i => (ρ i) x) ⊆ ↑I
x_in : x ∈ s
this : ∑ᶠ (i : ι), (ρ i) x = ∑ i ∈ I, (ρ i) x
⊢ ∑ i ∈ I, (ρ i) x = 1

Tactic:
rwa [eq_comm, ρ.sum_eq_one x_in] at this

Result:
no goals

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ∃ I, (∀ᶠ (x : X) in 𝓝[s] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 => (ρ x_1) x) ⊆ ↑I

Tactic:
rcases ρ.locallyFinite.exists_finset_support x₀ with ⟨I, hI⟩

Result:
case intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
I : Finset ι
hI : ∀ᶠ (x : X) in 𝓝 x₀, (support fun i => (ρ i) x) ⊆ ↑I
⊢ ∃ I, (∀ᶠ (x : X) in 𝓝[s] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 => (ρ x_1) x) ⊆ ↑I
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem mk_coordChange (e₁ e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet)
    (h₂ : b ∈ e₂.baseSet) (x : F) :
    (b, e₁.coordChange e₂ b x) = e₂ (e₁.toPartialHomeomorph.symm (b, x))

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x).1 = (↑e₂ (↑e₁.symm (b, x))).1

Tactic:
rw [e₂.coe_fst', ← e₁.coe_fst', e₁.apply_symm_apply' h₁]

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑e₁.symm (b, x)) ∈ e₁.baseSet

B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑e₁.symm (b, x)) ∈ e₂.baseSet

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑e₁.symm (b, x)) ∈ e₂.baseSet

Tactic:
rwa [e₁.proj_symm_apply' h₁]

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x) = ↑e₂ (↑e₁.symm (b, x))

Tactic:
refine Prod.ext ?_ rfl

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x).1 = (↑e₂ (↑e₁.symm (b, x))).1

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑e₁.symm (b, x)) ∈ e₁.baseSet

Tactic:
rwa [e₁.proj_symm_apply' h₁]

Result:
no goals
-- Mathlib/Computability/Reduce.lean
theorem le_antisymm {d₁ d₂ : ManyOneDegree} : d₁ ≤ d₂ → d₂ ≤ d₁ → d₁ = d₂

Proof state:
d₁ d₂ : ManyOneDegree
⊢ d₁ ≤ d₂ → d₂ ≤ d₁ → d₁ = d₂

Tactic:
induction d₁ using ManyOneDegree.ind_on

Result:
case h
d₂ : ManyOneDegree
p✝ : Set ℕ
⊢ of p✝ ≤ d₂ → d₂ ≤ of p✝ → of p✝ = d₂

Proof state:
case h.h
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ ≤ of p✝ → of p✝ ≤ of p✝¹ → of p✝¹ = of p✝

Tactic:
intro hp hq

Result:
case h.h
p✝¹ p✝ : Set ℕ
hp : of p✝¹ ≤ of p✝
hq : of p✝ ≤ of p✝¹
⊢ of p✝¹ = of p✝

Proof state:
case h.h
p✝¹ p✝ : Set ℕ
hp : of p✝¹ ≤ of p✝
hq : of p✝ ≤ of p✝¹
⊢ of p✝¹ = of p✝

Tactic:
simp_all only [ManyOneEquiv, of_le_of, of_eq_of, true_and]

Result:
no goals

Proof state:
case h
d₂ : ManyOneDegree
p✝ : Set ℕ
⊢ of p✝ ≤ d₂ → d₂ ≤ of p✝ → of p✝ = d₂

Tactic:
induction d₂ using ManyOneDegree.ind_on

Result:
case h.h
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ ≤ of p✝ → of p✝ ≤ of p✝¹ → of p✝¹ = of p✝
-- Mathlib/Logic/Encodable/Basic.lean
theorem rel_sequence {r : β → β → Prop} {f : α → β} (hf : Directed r f) (a : α) :
    r (f a) (f (hf.sequence f (encode a + 1)))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a) (f (Directed.sequence f hf (encode a + 1)))

Tactic:
simp only [Directed.sequence, add_eq, Nat.add_zero, encodek, and_self]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a) (f (Classical.choose ⋯))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a) (f (Classical.choose ⋯))

Tactic:
exact (Classical.choose_spec (hf _ a)).2

Result:
no goals