harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Harmonic/Bounds.lean
theorem log_add_one_le_harmonic (n : ℕ) :
    Real.log ↑(n+1) ≤ harmonic n

Proof state:
n : ℕ
⊢ ¬1 ≤ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case calc_3
n : ℕ
⊢ ∑ d ∈ Finset.Icc 1 n, (↑d)⁻¹ = ↑(harmonic n)

Tactic:
simp only [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast]

Result:
no goals

Proof state:
case calc_1
n : ℕ
⊢ Real.log ↑(n + 1) = ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹

Tactic:
rw [Nat.cast_one, integral_inv (by simp [(show ¬ (1 : ℝ) ≤ 0 by norm_num)]), div_one]

Result:
no goals

Proof state:
case calc_2
n : ℕ
⊢ ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹ ≤ ∑ d ∈ Finset.Icc 1 n, (↑d)⁻¹

Tactic:
exact (inv_antitoneOn_Icc_right <| by norm_num).integral_le_sum_Ico (Nat.le_add_left 1 n)

Result:
no goals

Proof state:
n : ℕ
⊢ 0 ∉ Set.uIcc 1 ↑(n + 1)

Tactic:
simp [(show ¬ (1 : ℝ) ≤ 0 by norm_num)]

Result:
no goals

Proof state:
n : ℕ
⊢ 0 < ↑1

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
⊢ Real.log ↑(n + 1) ≤ ↑(harmonic n)

Tactic:
calc _ = ∫ x in (1 : ℕ)..↑(n+1), x⁻¹ := ?_
     _ ≤ ∑ d ∈ Finset.Icc 1 n, (d : ℝ)⁻¹ := ?_
     _ = harmonic n := ?_

Result:
case calc_1
n : ℕ
⊢ Real.log ↑(n + 1) = ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹

case calc_2
n : ℕ
⊢ ∫ (x : ℝ) in ↑1 ..↑(n + 1), x⁻¹ ≤ ∑ d ∈ Finset.Icc 1 n, (↑d)⁻¹

case calc_3
n : ℕ
⊢ ∑ d ∈ Finset.Icc 1 n, (↑d)⁻¹ = ↑(harmonic n)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_swap_of_ne (a : Array α) {i j : Nat} {hi hj} (hp : p < a.size)
    (hi' : p ≠ i) (hj' : p ≠ j) : (a.swap i j hi hj)[p]'(a.size_swap .. |>.symm ▸ hp) = a[p]

Proof state:
α : Type u_1
p : Nat
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
hp : p < a.size
hi' : p ≠ i
hj' : p ≠ j
⊢ (a.swap i j hi hj)[p] = a[p]

Tactic:
simp [swap_def, getElem_set, hi'.symm, hj'.symm]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_add' (a b : α) : |a| ≤ |b| + |b + a|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ |a| ≤ |b| + |b + a|

Tactic:
simpa using abs_add (-b) (b + a)

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem summable_powerSeries_of_norm_lt_one {z : α}
    (h : CauchySeq fun n ↦ ∑ i ∈ range n, f i) (hz : ‖z‖ < 1) :
    Summable fun n ↦ f n * z ^ n :=
  summable_powerSeries_of_norm_lt (w := 1) (by simp [h]) (by simp [hz])

Proof state:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i
hz : ‖z‖ < 1
⊢ CauchySeq fun n => ∑ i ∈ Finset.range n, f i * 1 ^ i

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
z : α
h : CauchySeq fun n => ∑ i ∈ Finset.range n, f i
hz : ‖z‖ < 1
⊢ ‖z‖ < ‖1‖

Tactic:
simp [hz]

Result:
no goals
-- Mathlib/Analysis/Convex/Extreme.lean
lemma image_extremePoints (f : L) (s : Set E) :
    f '' extremePoints 𝕜 s = extremePoints 𝕜 (f '' s)

Proof state:
case h.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : EquivLike L E F
inst✝ : LinearEquivClass L 𝕜 E F
f : L
s : Set E
a : E
⊢ f a ∈ ⇑f '' extremePoints 𝕜 s ↔ f a ∈ extremePoints 𝕜 (⇑f '' s)

Tactic:
have : ∀ x y, f '' openSegment 𝕜 x y = openSegment 𝕜 (f x) (f y) :=
  image_openSegment _ (LinearMapClass.linearMap f).toAffineMap

Result:
case h.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : EquivLike L E F
inst✝ : LinearEquivClass L 𝕜 E F
f : L
s : Set E
a : E
this : ∀ (x y : E), ⇑f '' openSegment 𝕜 x y = openSegment 𝕜 (f x) (f y)
⊢ f a ∈ ⇑f '' extremePoints 𝕜 s ↔ f a ∈ extremePoints 𝕜 (⇑f '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : EquivLike L E F
inst✝ : LinearEquivClass L 𝕜 E F
f : L
s : Set E
⊢ ⇑f '' extremePoints 𝕜 s = extremePoints 𝕜 (⇑f '' s)

Tactic:
ext b

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : EquivLike L E F
inst✝ : LinearEquivClass L 𝕜 E F
f : L
s : Set E
b : F
⊢ b ∈ ⇑f '' extremePoints 𝕜 s ↔ b ∈ extremePoints 𝕜 (⇑f '' s)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : EquivLike L E F
inst✝ : LinearEquivClass L 𝕜 E F
f : L
s : Set E
b : F
⊢ b ∈ ⇑f '' extremePoints 𝕜 s ↔ b ∈ extremePoints 𝕜 (⇑f '' s)

Tactic:
obtain ⟨a, rfl⟩ := EquivLike.surjective f b

Result:
case h.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : EquivLike L E F
inst✝ : LinearEquivClass L 𝕜 E F
f : L
s : Set E
a : E
⊢ f a ∈ ⇑f '' extremePoints 𝕜 s ↔ f a ∈ extremePoints 𝕜 (⇑f '' s)

Proof state:
case h.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : EquivLike L E F
inst✝ : LinearEquivClass L 𝕜 E F
f : L
s : Set E
a : E
this : ∀ (x y : E), ⇑f '' openSegment 𝕜 x y = openSegment 𝕜 (f x) (f y)
⊢ f a ∈ ⇑f '' extremePoints 𝕜 s ↔ f a ∈ extremePoints 𝕜 (⇑f '' s)

Tactic:
simp only [mem_extremePoints, (EquivLike.surjective f).forall,
  (EquivLike.injective f).mem_set_image, (EquivLike.injective f).eq_iff, ← this]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem cyclotomic.isCoprime_rat {n m : ℕ} (h : n ≠ m) :
    IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Proof state:
n m : ℕ
h : n ≠ m
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Tactic:
rcases n.eq_zero_or_pos with (rfl | hnzero)

Result:
case inl
m : ℕ
h : 0 ≠ m
⊢ IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)

case inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Proof state:
case inr.inl
n : ℕ
hnzero : n > 0
h : n ≠ 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)

Tactic:
exact isCoprime_one_right

Result:
no goals

Proof state:
case inr.inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ ¬cyclotomic n ℚ ∣ cyclotomic m ℚ

Tactic:
exact fun hdiv => h <| cyclotomic_injective <|
  eq_of_monic_of_associated (cyclotomic.monic n ℚ) (cyclotomic.monic m ℚ) <|
    Irreducible.associated_of_dvd (cyclotomic.irreducible_rat hnzero)
      (cyclotomic.irreducible_rat hmzero) hdiv

Result:
no goals

Proof state:
case inl
m : ℕ
h : 0 ≠ m
⊢ IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)

Tactic:
exact isCoprime_one_left

Result:
no goals

Proof state:
case inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Tactic:
rcases m.eq_zero_or_pos with (rfl | hmzero)

Result:
case inr.inl
n : ℕ
hnzero : n > 0
h : n ≠ 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)

case inr.inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Proof state:
case inr.inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Tactic:
rw [Irreducible.coprime_iff_not_dvd <| cyclotomic.irreducible_rat <| hnzero]

Result:
case inr.inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ ¬cyclotomic n ℚ ∣ cyclotomic m ℚ
-- Mathlib/RingTheory/Localization/InvSubmonoid.lean
theorem toInvSubmonoid_eq_mk' (x : M) : (toInvSubmonoid M S x : S) = mk' S 1 x

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : ↥M
⊢ ↑((toInvSubmonoid M S) x) = mk' S 1 x

Tactic:
rw [← (IsLocalization.map_units S x).mul_left_inj]

Result:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : ↥M
⊢ ↑((toInvSubmonoid M S) x) * (algebraMap R S) ↑x = mk' S 1 x * (algebraMap R S) ↑x

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : ↥M
⊢ ↑((toInvSubmonoid M S) x) * (algebraMap R S) ↑x = mk' S 1 x * (algebraMap R S) ↑x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
    ⟦aig.mkGate input, assign⟧
      =
    ((⟦aig, input.lhs.ref, assign⟧ ^^ input.lhs.inv) && (⟦aig, input.rhs.ref, assign⟧ ^^ input.rhs.inv))

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
⊢ (match elem : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs (aig.mkGate input).aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs (aig.mkGate input).aig.decls assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Tactic:
split

Result:
case h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
b✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.const b✝
⊢ b✝ =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

case h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

case h_3
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    (lval ^^ linv✝) && (rval ^^ rinv✝)) =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))
-- Mathlib/Algebra/Lie/Submodule.lean
theorem mem_map_of_surjective {y : L'} (h₁ : Function.Surjective f) (h₂ : y ∈ I.map f) :
    ∃ x : I, f x = y

Proof state:
case h
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : Function.Surjective ⇑f
x : L
hx : x ∈ ↑I
⊢ f ↑⟨x, hx⟩ = ↑f x

Tactic:
rw [LieHom.coe_toLinearMap]

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
y : L'
h₁ : Function.Surjective ⇑f
h₂ : ∃ y_1 ∈ ↑I, ↑f y_1 = y
⊢ ∃ x, f ↑x = y

Tactic:
obtain ⟨x, hx, rfl⟩ := h₂

Result:
case intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : Function.Surjective ⇑f
x : L
hx : x ∈ ↑I
⊢ ∃ x_1, f ↑x_1 = ↑f x

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
y : L'
h₁ : Function.Surjective ⇑f
h₂ : y ∈ map f I
⊢ ∃ x, f ↑x = y

Tactic:
rw [← LieSubmodule.mem_toSubmodule, coe_map_of_surjective h₁, Submodule.mem_map] at h₂

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
y : L'
h₁ : Function.Surjective ⇑f
h₂ : ∃ y_1 ∈ ↑I, ↑f y_1 = y
⊢ ∃ x, f ↑x = y

Proof state:
case intro.intro
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : Function.Surjective ⇑f
x : L
hx : x ∈ ↑I
⊢ ∃ x_1, f ↑x_1 = ↑f x

Tactic:
use ⟨x, hx⟩

Result:
case h
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : Function.Surjective ⇑f
x : L
hx : x ∈ ↑I
⊢ f ↑⟨x, hx⟩ = ↑f x
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem cycleType_kerParam_apply_apply :
    cycleType (kerParam g ⟨k, v⟩) = cycleType k + ∑ c, (v c).val.cycleType

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
hU : U.Pairwise fun i j => (↑(v i)).Disjoint ↑(v j)
⊢ ((kerParam g) (k, v)).cycleType = k.cycleType + ∑ c : { x // x ∈ g.cycleFactorsFinset }, (↑(v c)).cycleType

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_apply, ← Prod.fst_mul_snd ⟨k, v⟩, Prod.mk_mul_mk, mul_one,
  one_mul, Finset.univ_eq_attach, Disjoint.cycleType (disjoint_ofSubtype_noncommPiCoprod g k v),
  Subgroup.noncommPiCoprod_apply, Disjoint.cycleType_noncommProd hU, Finset.univ_eq_attach]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
U : Set { x // x ∈ g.cycleFactorsFinset } := ↑Finset.univ
hU : U.Pairwise fun i j => (↑(v i)).Disjoint ↑(v j)
⊢ (ofSubtype k).cycleType + ∑ i ∈ g.cycleFactorsFinset.attach, (↑(v i)).cycleType =
    k.cycleType + ∑ c ∈ g.cycleFactorsFinset.attach, (↑(v c)).cycleType
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem compositionAsSet_card (n : ℕ) : Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)

Proof state:
n : ℕ
⊢ Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)

Tactic:
have : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1) := by simp

Result:
n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)
⊢ Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)

Proof state:
n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)
⊢ Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)

Tactic:
rw [← this]

Result:
n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)
⊢ Fintype.card (CompositionAsSet n) = Fintype.card (Finset (Fin (n - 1)))

Proof state:
n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)
⊢ Fintype.card (CompositionAsSet n) = Fintype.card (Finset (Fin (n - 1)))

Tactic:
exact Fintype.card_congr (compositionAsSetEquiv n)

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Refinements.lean
lemma epi_iff_surjective_up_to_refinements (f : X ⟶ Y) :
    Epi f ↔ ∀ ⦃A : C⦄ (y : A ⟶ Y),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f

Proof state:
case mp
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
a✝ : Epi f
A : C
a : A ⟶ Y
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ a = x ≫ f

Tactic:
exact ⟨pullback a f, pullback.fst a f, inferInstance, pullback.snd a f, pullback.condition⟩

Result:
no goals

Proof state:
case mpr
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f
⊢ Epi f

Tactic:
obtain ⟨A, π, hπ, a', fac⟩ := hf (𝟙 Y)

Result:
case mpr.intro.intro.intro.intro
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f
A : C
π : A ⟶ Y
hπ : Epi π
a' : A ⟶ X
fac : π ≫ 𝟙 Y = a' ≫ f
⊢ Epi f

Proof state:
case mpr.intro.intro.intro.intro
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f
A : C
π : A ⟶ Y
hπ : Epi π
a' : A ⟶ X
fac : π = a' ≫ f
⊢ Epi f

Tactic:
exact epi_of_epi_fac fac.symm

Result:
no goals

Proof state:
case mp
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Epi f → ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
intro _ A a

Result:
case mp
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
a✝ : Epi f
A : C
a : A ⟶ Y
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ a = x ≫ f

Proof state:
case mpr
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f) → Epi f

Tactic:
intro hf

Result:
case mpr
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f
⊢ Epi f

Proof state:
case mpr.intro.intro.intro.intro
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f
A : C
π : A ⟶ Y
hπ : Epi π
a' : A ⟶ X
fac : π ≫ 𝟙 Y = a' ≫ f
⊢ Epi f

Tactic:
rw [comp_id] at fac

Result:
case mpr.intro.intro.intro.intro
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f
A : C
π : A ⟶ Y
hπ : Epi π
a' : A ⟶ X
fac : π = a' ≫ f
⊢ Epi f

Proof state:
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔ ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
constructor

Result:
case mp
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Epi f → ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

case mpr
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f) → Epi f
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem sub_equiv_sub {f1 f2 g1 g2 : CauSeq β abv} (hf : f1 ≈ f2) (hg : g1 ≈ g2) :
    f1 - g1 ≈ f2 - g2

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f1 f2 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 - g1 ≈ f2 - g2

Tactic:
simpa only [sub_eq_add_neg] using add_equiv_add hf (neg_equiv_neg hg)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_filterMap (f : α → Option β) (p : β → Bool) (l : List α) :
    filter p (filterMap f l) = filterMap (fun x => (f x).filter p) l

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
l : List α
⊢ filter p (filterMap f l) = filterMap (fun x => Option.filter p (f x)) l

Tactic:
rw [← filterMap_eq_filter, filterMap_filterMap]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
l : List α
⊢ filterMap (fun x => (f x).bind (Option.guard fun x => p x = true)) l = filterMap (fun x => Option.filter p (f x)) l

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
l : List α
x : α
⊢ (f x).bind (Option.guard fun x => p x = true) = Option.filter p (f x)

Tactic:
cases f x <;> simp [Option.filter, Option.guard]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
l : List α
⊢ filterMap (fun x => (f x).bind (Option.guard fun x => p x = true)) l = filterMap (fun x => Option.filter p (f x)) l

Tactic:
congr

Result:
case e_f
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
l : List α
⊢ (fun x => (f x).bind (Option.guard fun x => p x = true)) = fun x => Option.filter p (f x)

Proof state:
case e_f
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
l : List α
⊢ (fun x => (f x).bind (Option.guard fun x => p x = true)) = fun x => Option.filter p (f x)

Tactic:
funext x

Result:
case e_f.h
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
l : List α
x : α
⊢ (f x).bind (Option.guard fun x => p x = true) = Option.filter p (f x)
-- Mathlib/Combinatorics/Colex.lean
@[simp] lemma cons_le_cons (ha hb) : toColex (s.cons a ha) ≤ toColex (s.cons b hb) ↔ a ≤ b

Proof state:
case inr
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b

Tactic:
rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
  singleton_le_singleton]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b

Tactic:
classical
rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
  singleton_le_singleton]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b

Tactic:
obtain rfl | hab := eq_or_ne a b

Result:
case inl
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
ha hb : a ∉ s
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons a s hb } ↔ a ≤ a

case inr
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b

Proof state:
case inl
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
ha hb : a ∉ s
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons a s hb } ↔ a ≤ a

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_bot : a \ ⊥ = a :=
  eq_of_forall_ge_iff fun b => by rw [sdiff_le_iff, bot_sup_eq]

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ ⊥ ≤ b ↔ a ≤ b

Tactic:
rw [sdiff_le_iff, bot_sup_eq]

Result:
no goals
-- Mathlib/Topology/Separation/CompletelyRegular.lean
lemma separatesPoints_continuous_of_t35Space [T35Space X] :
    SeparatesPoints (Continuous : Set (X → ℝ))

Proof state:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
⊢ ∃ f ∈ Continuous, f x ≠ f y

Tactic:
obtain ⟨f, f_cont, f_zero, f_one⟩ :=
  CompletelyRegularSpace.completely_regular x {y} isClosed_singleton x_ne_y

Result:
case intro.intro.intro
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → ↑I
f_cont : Continuous f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ ∃ f ∈ Continuous, f x ≠ f y

Proof state:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
⊢ SeparatesPoints Continuous

Tactic:
intro x y x_ne_y

Result:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
⊢ ∃ f ∈ Continuous, f x ≠ f y

Proof state:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → ↑I
f_cont : Continuous f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ (fun x => ↑(f x)) x ≠ (fun x => ↑(f x)) y

Tactic:
aesop

Result:
no goals

Proof state:
case intro.intro.intro
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → ↑I
f_cont : Continuous f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ ∃ f ∈ Continuous, f x ≠ f y

Tactic:
exact ⟨fun x ↦ f x, continuous_subtype_val.comp f_cont, by aesop⟩

Result:
no goals