harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem HasDerivAt.rpow (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) (h : 0 < f x) :
    HasDerivAt (fun x => f x ^ g x)
      (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x

Proof state:
f g : ℝ → ℝ
f' g' x : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hg : HasDerivWithinAt g g' Set.univ x
h : 0 < f x
⊢ HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) Set.univ x

Tactic:
exact hf.rpow hg h

Result:
no goals

Proof state:
f g : ℝ → ℝ
f' g' x : ℝ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h : 0 < f x
⊢ HasDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Result:
f g : ℝ → ℝ
f' g' x : ℝ
hf : HasDerivWithinAt f f' Set.univ x
hg : HasDerivWithinAt g g' Set.univ x
h : 0 < f x
⊢ HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) Set.univ x
-- Mathlib/Algebra/Ring/Parity.lean
lemma Odd.pow (ha : Odd a) : ∀ {n : ℕ}, Odd (a ^ n)
  | 0 => by
    rw [pow_zero]
    exact odd_one
  | n + 1 => by rw [pow_succ]; exact ha.pow.mul ha

Proof state:
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
⊢ Odd 1

Tactic:
exact odd_one

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
n : ℕ
⊢ Odd (a ^ n * a)

Tactic:
exact ha.pow.mul ha

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
n : ℕ
⊢ Odd (a ^ (n + 1))

Tactic:
rw [pow_succ]

Result:
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
n : ℕ
⊢ Odd (a ^ n * a)

Proof state:
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
⊢ Odd (a ^ 0)

Tactic:
rw [pow_zero]

Result:
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
⊢ Odd 1
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem singleton_subperm_iff {α} {l : List α} {a : α} : [a] <+~ l ↔ a ∈ l

Proof state:
α : Type u_1
l : List α
a : α
⊢ [a] <+~ l ↔ a ∈ l

Tactic:
refine ⟨fun ⟨s, hla, h⟩ => ?_, fun h => ⟨[a], .rfl, singleton_sublist.mpr h⟩⟩

Result:
α : Type u_1
l : List α
a : α
x✝ : [a] <+~ l
s : List α
hla : s ~ [a]
h : s <+ l
⊢ a ∈ l

Proof state:
α : Type u_1
l : List α
a : α
x✝ : [a] <+~ l
s : List α
hla : s ~ [a]
h : s <+ l
⊢ a ∈ l

Tactic:
rwa [perm_singleton.mp hla, singleton_sublist] at h

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp]
lemma expect_image [DecidableEq ι] {m : κ → ι} (hm : (t : Set κ).InjOn m) :
    𝔼 i ∈ t.image m, f i = 𝔼 i ∈ t, f (m i)

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
f : ι → M
t : Finset κ
inst✝ : DecidableEq ι
m : κ → ι
hm : Set.InjOn m ↑t
⊢ 𝔼 i ∈ image m t, f i = 𝔼 i ∈ t, f (m i)

Tactic:
simp_rw [expect, card_image_of_injOn hm, sum_image hm]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Equiv.lean
theorem ofSubmodule'_toLinearMap [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂)
    (U : Submodule R₂ M₂) :
    (f.ofSubmodule' U).toLinearMap = (f.toLinearMap.domRestrict _).codRestrict _ Subtype.prop

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
f : M ≃ₛₗ[σ₁₂] M₂
U : Submodule R₂ M₂
⊢ ↑(f.ofSubmodule' U) = LinearMap.codRestrict U ((↑f).domRestrict (Submodule.comap (↑f) U)) ⋯

Tactic:
ext

Result:
case h.a
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
f : M ≃ₛₗ[σ₁₂] M₂
U : Submodule R₂ M₂
x✝ : ↥(Submodule.comap (↑f) U)
⊢ ↑(↑(f.ofSubmodule' U) x✝) = ↑((LinearMap.codRestrict U ((↑f).domRestrict (Submodule.comap (↑f) U)) ⋯) x✝)

Proof state:
case h.a
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
f : M ≃ₛₗ[σ₁₂] M₂
U : Submodule R₂ M₂
x✝ : ↥(Submodule.comap (↑f) U)
⊢ ↑(↑(f.ofSubmodule' U) x✝) = ↑((LinearMap.codRestrict U ((↑f).domRestrict (Submodule.comap (↑f) U)) ⋯) x✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem not_mem_adicCompletionIntegers {x : v.adicCompletion K} :
    x ∉ v.adicCompletionIntegers K ↔ 1 < Valued.v x

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : adicCompletion K v
⊢ ¬Valued.v x ≤ 1 ↔ 1 < Valued.v x

Tactic:
exact not_le

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : adicCompletion K v
⊢ x ∉ adicCompletionIntegers K v ↔ 1 < Valued.v x

Tactic:
rw [not_congr <| mem_adicCompletionIntegers R K v]

Result:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : adicCompletion K v
⊢ ¬Valued.v x ≤ 1 ↔ 1 < Valued.v x
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem mulDysonETransform.card :
    (mulDysonETransform e x).1.card + (mulDysonETransform e x).2.card = x.1.card + x.2.card

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ #(x.1 ∪ e • x.2) + #(x.2 ∩ e⁻¹ • x.1) = #x.1 + #x.2

Tactic:
rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm,
  card_union_add_card_inter, card_smul_finset]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ #(mulDysonETransform e x).1 + #(mulDysonETransform e x).2 = #x.1 + #x.2

Tactic:
dsimp

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ #(x.1 ∪ e • x.2) + #(x.2 ∩ e⁻¹ • x.1) = #x.1 + #x.2
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_map_inv : (m.map fun i => (f i)⁻¹).prod = (m.map f).prod⁻¹

Proof state:
ι : Type u_2
α : Type u_3
inst✝ : DivisionCommMonoid α
m : Multiset ι
f : ι → α
⊢ (map (fun i => (f i)⁻¹) m).prod = (map f m).prod⁻¹

Tactic:
rw [← (m.map f).prod_map_inv', map_map, Function.comp_def]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem pi_if {p : ι → Prop} [h : DecidablePred p] (s : Set ι) (t₁ t₂ : ∀ i, Set (α i)) :
    (pi s fun i => if p i then t₁ i else t₂ i) =
      pi ({ i ∈ s | p i }) t₁ ∩ pi ({ i ∈ s | ¬p i }) t₂

Proof state:
case h.refine_1.right.intro
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i => if p i then t₁ i else t₂ i
i : ι
his : i ∈ s
hpi : ¬p i
⊢ f i ∈ t₂ i

Tactic:
simpa [*] using h i

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ (s.pi fun i => if p i then t₁ i else t₂ i) = {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂

Tactic:
ext f

Result:
case h
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ (f ∈ s.pi fun i => if p i then t₁ i else t₂ i) ↔ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂

Proof state:
case h.refine_1.right
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i => if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂

Tactic:
rintro i ⟨his, hpi⟩

Result:
case h.refine_1.right.intro
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i => if p i then t₁ i else t₂ i
i : ι
his : i ∈ s
hpi : ¬p i
⊢ f i ∈ t₂ i

Proof state:
case h.refine_2.intro
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ {i | i ∈ s ∧ p i}.pi t₁
ht₂ : f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂
i : ι
his : i ∈ s
⊢ f i ∈ (fun i => if p i then t₁ i else t₂ i) i

Tactic:
by_cases p i <;> simp_all

Result:
no goals

Proof state:
case h.refine_2
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂ → f ∈ s.pi fun i => if p i then t₁ i else t₂ i

Tactic:
rintro ⟨ht₁, ht₂⟩ i his

Result:
case h.refine_2.intro
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ {i | i ∈ s ∧ p i}.pi t₁
ht₂ : f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂
i : ι
his : i ∈ s
⊢ f i ∈ (fun i => if p i then t₁ i else t₂ i) i

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ (f ∈ s.pi fun i => if p i then t₁ i else t₂ i) ↔ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂

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

Result:
case h.refine_1
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i => if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂

case h.refine_2
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂ → f ∈ s.pi fun i => if p i then t₁ i else t₂ i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_filter_ne_empty [DecidablePred fun l : Array α => l ≠ #[]] {L : Array (Array α)} :
    flatten (L.filter fun l => l ≠ #[]) = L.flatten

Proof state:
α : Type u_1
inst✝ : DecidablePred fun l => l ≠ #[]
L : Array (Array α)
⊢ (filter (fun l => decide (l ≠ #[])) L).flatten = L.flatten

Tactic:
simp only [ne_eq, ← isEmpty_iff, Bool.not_eq_true, Bool.decide_eq_false,
  flatten_filter_not_isEmpty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_cons_of_neg (l) (pa : ¬p a) : countP p (a :: l) = countP p l

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ countP p (a :: l) = countP p l

Tactic:
simp [countP, countP.go, pa]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_C_mul_X_pow (n : ℕ) {c : R} (h : c ≠ 0) :
    Polynomial.support (C c * X ^ n) = singleton n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
c : R
h : c ≠ 0
⊢ (C c * X ^ n).support = {n}

Tactic:
rw [C_mul_X_pow_eq_monomial, support_monomial n h]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Grp_.lean
theorem lift_inv_comp_left {A B : Grp_ C} (f : A ⟶ B) :
    lift (A.inv ≫ f.hom) f.hom ≫ B.mul = toUnit _ ≫ B.one

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A B : Grp_ C
f : A ⟶ B
this : (lift A.inv (𝟙 A.X) ≫ A.mul) ≫ f.hom = (toUnit A.X ≫ A.one) ≫ f.hom
⊢ lift (A.inv ≫ f.hom) f.hom ≫ B.mul = toUnit A.X ≫ B.one

Tactic:
rwa [assoc, f.mul_hom, assoc, f.one_hom, lift_map_assoc, id_comp] at this

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A B : Grp_ C
f : A ⟶ B
⊢ lift (A.inv ≫ f.hom) f.hom ≫ B.mul = toUnit A.X ≫ B.one

Tactic:
have := A.left_inv =≫ f.hom

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A B : Grp_ C
f : A ⟶ B
this : (lift A.inv (𝟙 A.X) ≫ A.mul) ≫ f.hom = (toUnit A.X ≫ A.one) ≫ f.hom
⊢ lift (A.inv ≫ f.hom) f.hom ≫ B.mul = toUnit A.X ≫ B.one
-- Mathlib/Algebra/Module/Injective.lean
theorem chain_linearPMap_of_chain_extensionOf {c : Set (ExtensionOf i f)}
    (hchain : IsChain (· ≤ ·) c) :
    IsChain (· ≤ ·) <| (fun x : ExtensionOf i f => x.toLinearPMap) '' c

Proof state:
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
⊢ IsChain (fun x1 x2 => x1 ≤ x2) ((fun x => x.toLinearPMap) '' c)

Tactic:
rintro _ ⟨a, a_mem, rfl⟩ _ ⟨b, b_mem, rfl⟩ neq

Result:
case intro.intro.intro.intro
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
a : ExtensionOf i f
a_mem : a ∈ c
b : ExtensionOf i f
b_mem : b ∈ c
neq : (fun x => x.toLinearPMap) a ≠ (fun x => x.toLinearPMap) b
⊢ (fun x1 x2 => x1 ≤ x2) ((fun x => x.toLinearPMap) a) ((fun x => x.toLinearPMap) b) ∨
    (fun x1 x2 => x1 ≤ x2) ((fun x => x.toLinearPMap) b) ((fun x => x.toLinearPMap) a)

Proof state:
case intro.intro.intro.intro
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
a : ExtensionOf i f
a_mem : a ∈ c
b : ExtensionOf i f
b_mem : b ∈ c
neq : (fun x => x.toLinearPMap) a ≠ (fun x => x.toLinearPMap) b
⊢ (fun x1 x2 => x1 ≤ x2) ((fun x => x.toLinearPMap) a) ((fun x => x.toLinearPMap) b) ∨
    (fun x1 x2 => x1 ≤ x2) ((fun x => x.toLinearPMap) b) ((fun x => x.toLinearPMap) a)

Tactic:
exact hchain a_mem b_mem (ne_of_apply_ne _ neq)

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Subcategory.lean
lemma zero [S.P.IsClosedUnderIsomorphisms] : S.P 0

Proof state:
case intro.intro
C : Type u_1
inst✝⁶ : Category.{u_2, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
S : Subcategory C
inst✝ : S.P.IsClosedUnderIsomorphisms
X : C
hX : IsZero X
mem : S.P X
⊢ S.P 0

Tactic:
exact S.P.prop_of_iso hX.isoZero mem

Result:
no goals

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_2, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
S : Subcategory C
inst✝ : S.P.IsClosedUnderIsomorphisms
⊢ S.P 0

Tactic:
obtain ⟨X, hX, mem⟩ := S.zero'

Result:
case intro.intro
C : Type u_1
inst✝⁶ : Category.{u_2, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
S : Subcategory C
inst✝ : S.P.IsClosedUnderIsomorphisms
X : C
hX : IsZero X
mem : S.P X
⊢ S.P 0
-- Mathlib/Data/Fintype/Card.lean
theorem Finset.card_eq_iff_eq_univ [Fintype α] (s : Finset α) : #s = Fintype.card α ↔ s = univ :=
  ⟨s.eq_univ_of_card, by
    rintro rfl
    exact Finset.card_univ⟩

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ #univ = Fintype.card α

Tactic:
exact Finset.card_univ

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s = univ → #s = Fintype.card α

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : Fintype α
⊢ #univ = Fintype.card α
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_setIfInBounds (a : Vector α n) (i : Nat) (x : α) (j : Nat)
    (hj : j < n) : (a.setIfInBounds i x)[j] = if i = j then x else a[j]

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
x : α
j : Nat
hj : j < n
⊢ (a.setIfInBounds i x)[j] = if i = j then x else a[j]

Tactic:
cases a

Result:
case mk
α : Type u_1
n i : Nat
x : α
j : Nat
hj : j < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.setIfInBounds i x)[j] =
    if i = j then x else { toArray := toArray✝, size_toArray := size_toArray✝ }[j]

Proof state:
case mk
α : Type u_1
n i : Nat
x : α
j : Nat
hj : j < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.setIfInBounds i x)[j] =
    if i = j then x else { toArray := toArray✝, size_toArray := size_toArray✝ }[j]

Tactic:
split <;> simp_all [Array.getElem_setIfInBounds]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_pos_iff {p} : 0 < countP p l ↔ ∃ a ∈ l, p a

Proof state:
case mk
α✝ : Type u_1
n✝ : Nat
p : α✝ → Bool
toArray✝ : Array α✝
size_toArray✝ : toArray✝.size = n✝
⊢ 0 < countP p { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    ∃ a, a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∧ p a = true

Tactic:
simp

Result:
no goals

Proof state:
α✝ : Type u_1
n✝ : Nat
l : Vector α✝ n✝
p : α✝ → Bool
⊢ 0 < countP p l ↔ ∃ a, a ∈ l ∧ p a = true

Tactic:
cases l

Result:
case mk
α✝ : Type u_1
n✝ : Nat
p : α✝ → Bool
toArray✝ : Array α✝
size_toArray✝ : toArray✝.size = n✝
⊢ 0 < countP p { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    ∃ a, a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∧ p a = true
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Raised.dist_le' {n m} (H : Raised n m) : Nat.dist m n ≤ 1

Proof state:
n m : ℕ
H : Raised n m
⊢ m.dist n ≤ 1

Tactic:
rw [Nat.dist_comm]

Result:
n m : ℕ
H : Raised n m
⊢ n.dist m ≤ 1

Proof state:
n m : ℕ
H : Raised n m
⊢ n.dist m ≤ 1

Tactic:
exact H.dist_le

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem toNNReal_add {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :
    Real.toNNReal (r + p) = Real.toNNReal r + Real.toNNReal p :=
  NNReal.eq <| by simp [hr, hp, add_nonneg]

Proof state:
r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ ↑(r + p).toNNReal = ↑(r.toNNReal + p.toNNReal)

Tactic:
simp [hr, hp, add_nonneg]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_three_add_inv_three : (3 : ℝ≥0∞)⁻¹ + 3⁻¹ + 3⁻¹ = 1

Proof state:
⊢ 3⁻¹ + 3⁻¹ + 3⁻¹ = 3 * 3⁻¹

Tactic:
ring

Result:
no goals

Proof state:
⊢ 3⁻¹ + 3⁻¹ + 3⁻¹ = 1

Tactic:
rw [← ENNReal.mul_inv_cancel three_ne_zero ofNat_ne_top]

Result:
⊢ 3⁻¹ + 3⁻¹ + 3⁻¹ = 3 * 3⁻¹
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
lemma lowerSet_le_lower {t₁ t₂ : TopologicalSpace α} [@Topology.IsLowerSet α t₁ _]
    [@IsLower α t₂ _] : t₁ ≤ t₂ := fun s hs => by
  rw [@isOpen_iff_isLowerSet α _ t₁]
  exact IsLower.isLowerSet_of_isOpen hs

Proof state:
α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsLowerSet α
inst✝ : IsLower α
s : Set α
hs : IsOpen s
⊢ IsOpen s

Tactic:
rw [@isOpen_iff_isLowerSet α _ t₁]

Result:
α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsLowerSet α
inst✝ : IsLower α
s : Set α
hs : IsOpen s
⊢ IsLowerSet s

Proof state:
α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsLowerSet α
inst✝ : IsLower α
s : Set α
hs : IsOpen s
⊢ IsLowerSet s

Tactic:
exact IsLower.isLowerSet_of_isOpen hs

Result:
no goals
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_drop_append (l : List α) (l₁ : List β) (l₂ : List β) (h : Forall₂ R l (l₁ ++ l₂)) :
    Forall₂ R (List.drop (length l₁) l) l₂

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (drop l₁.length l) (drop l₁.length (l₁ ++ l₂))
⊢ Forall₂ R (drop l₁.length l) l₂

Tactic:
rwa [drop_left] at h'

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (drop l₁.length l) l₂

Tactic:
have h' : Forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂)) :=
  forall₂_drop (length l₁) h

Result:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (drop l₁.length l) (drop l₁.length (l₁ ++ l₂))
⊢ Forall₂ R (drop l₁.length l) l₂
-- Mathlib/Data/Num/Lemmas.lean
theorem of_to_int' : ∀ n : ZNum, ZNum.ofInt' n = n
  | 0 => by dsimp [ofInt', cast_zero]; erw [Num.ofNat'_zero, Num.toZNum]
  | pos a => by rw [cast_pos, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]; rfl
  | neg a => by
    rw [cast_neg, ofInt'_neg, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]; rfl

Proof state:
a : PosNum
⊢ ofInt' ↑(pos a) = pos a

Tactic:
rw [cast_pos, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]

Result:
a : PosNum
⊢ (Num.pos a).toZNum = pos a

Proof state:
⊢ (Num.ofNat' 0).toZNum = 0

Tactic:
erw [Num.ofNat'_zero, Num.toZNum]

Result:
no goals

Proof state:
a : PosNum
⊢ (Num.pos a).toZNum = pos a

Tactic:
rfl

Result:
no goals

Proof state:
⊢ ofInt' ↑0 = 0

Tactic:
dsimp [ofInt', cast_zero]

Result:
⊢ (Num.ofNat' 0).toZNum = 0

Proof state:
a : PosNum
⊢ ofInt' ↑(neg a) = neg a

Tactic:
rw [cast_neg, ofInt'_neg, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]

Result:
a : PosNum
⊢ -(Num.pos a).toZNum = neg a

Proof state:
a : PosNum
⊢ -(Num.pos a).toZNum = neg a

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem tprod_eq_mul_tprod_ite [DecidableEq β] (hf : Multipliable f) (b : β) :
    ∏' n, f n = f b * ∏' n, ite (n = b) 1 (f n)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
inst✝¹ : T2Space α
inst✝ : DecidableEq β
hf : Multipliable f
b : β
⊢ ∏' (n : β), f n = f b * ∏' (n : β), if n = b then 1 else f n

Tactic:
rw [(hasProd_ite_div_hasProd hf.hasProd b).tprod_eq]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
inst✝¹ : T2Space α
inst✝ : DecidableEq β
hf : Multipliable f
b : β
⊢ ∏' (n : β), f n = f b * ((∏' (b : β), f b) / f b)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
inst✝¹ : T2Space α
inst✝ : DecidableEq β
hf : Multipliable f
b : β
⊢ ∏' (n : β), f n = f b * ((∏' (b : β), f b) / f b)

Tactic:
exact (mul_div_cancel _ _).symm

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
lemma integral_preCDF_fst (ρ : Measure (α × ℝ)) (r : ℚ) [IsFiniteMeasure ρ] :
    ∫ x, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd r univ).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
inst✝ : IsFiniteMeasure ρ
⊢ ∫ (x : α), (preCDF ρ r x).toReal ∂ρ.fst = ((ρ.IicSnd ↑r) univ).toReal

Tactic:
rw [← setIntegral_univ, setIntegral_preCDF_fst ρ _ MeasurableSet.univ]

Result:
no goals
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem ramificationIdx_eq_find [DecidablePred fun n ↦ ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n]
    (h : ∃ n, ∀ k, map f p ≤ P ^ k → k ≤ n) :
    ramificationIdx f p P = Nat.find h

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝ : DecidablePred fun n => ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
h : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ ramificationIdx f p P = Nat.find h

Tactic:
convert Nat.sSup_def h

Result:
no goals