harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.size_combine (le) (s : Heap α) :
    (s.combine le).size = s.size

Proof state:
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a₁ : α
c₁ : Heap α
a₂ : α
c₂ s : Heap α
⊢ (merge le (merge le (node a₁ c₁ (node a₂ c₂ s)) (node a₂ c₂ s)) (combine le s)).size =
    (node a₁ c₁ (node a₂ c₂ s)).size

Tactic:
rw [size_merge le (noSibling_merge _ _ _) (noSibling_combine _ _),
  size_merge_node, size_combine le s]

Result:
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a₁ : α
c₁ : Heap α
a₂ : α
c₂ s : Heap α
⊢ c₁.size + c₂.size + 2 + s.size = (node a₁ c₁ (node a₂ c₂ s)).size

Proof state:
case h_2
α : Type u_1
le : α → α → Bool
s x✝¹ : Heap α
x✝ : ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α), s = node a child (node a_1 child_1 s_1) → False
⊢ s.size = s.size

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ (match s with
      | h₁@h_1:(node a child h₂@h:(node a_1 child_1 s)) => merge le (merge le h₁ h₂) (combine le s)
      | h => h).size =
    s.size

Tactic:
split

Result:
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s✝ : Heap α
⊢ (merge le (merge le (node a✝¹ child✝¹ (node a✝ child✝ s✝)) (node a✝ child✝ s✝)) (combine le s✝)).size =
    (node a✝¹ child✝¹ (node a✝ child✝ s✝)).size

case h_2
α : Type u_1
le : α → α → Bool
s x✝¹ : Heap α
x✝ : ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α), s = node a child (node a_1 child_1 s_1) → False
⊢ s.size = s.size

Proof state:
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s✝ : Heap α
⊢ (merge le (merge le (node a✝¹ child✝¹ (node a✝ child✝ s✝)) (node a✝ child✝ s✝)) (combine le s✝)).size =
    (node a✝¹ child✝¹ (node a✝ child✝ s✝)).size

Tactic:
rename_i a₁ c₁ a₂ c₂ s

Result:
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a₁ : α
c₁ : Heap α
a₂ : α
c₂ s : Heap α
⊢ (merge le (merge le (node a₁ c₁ (node a₂ c₂ s)) (node a₂ c₂ s)) (combine le s)).size =
    (node a₁ c₁ (node a₂ c₂ s)).size

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ (combine le s).size = s.size

Tactic:
unfold combine

Result:
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ (match s with
      | h₁@h_1:(node a child h₂@h:(node a_1 child_1 s)) => merge le (merge le h₁ h₂) (combine le s)
      | h => h).size =
    s.size

Proof state:
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a₁ : α
c₁ : Heap α
a₂ : α
c₂ s : Heap α
⊢ c₁.size + c₂.size + 2 + s.size = (node a₁ c₁ (node a₂ c₂ s)).size

Tactic:
simp_arith [size]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
lemma GeneralizingMap.comp {f : X → Y} {g : Y → Z}
    (hf : GeneralizingMap f) (hg : GeneralizingMap g) :
    GeneralizingMap (g ∘ f)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : GeneralizingMap f
hg : GeneralizingMap g
⊢ GeneralizingMap (g ∘ f)

Tactic:
simp only [GeneralizingMap_iff_stableUnderGeneralization_image, Set.image_comp] at *

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (f '' s)
hg : ∀ (s : Set Y), StableUnderGeneralization s → StableUnderGeneralization (g '' s)
⊢ ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (g '' (f '' s))

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (f '' s)
hg : ∀ (s : Set Y), StableUnderGeneralization s → StableUnderGeneralization (g '' s)
⊢ ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (g '' (f '' s))

Tactic:
exact fun s h ↦ hg _ (hf  _ h)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem basis_toMatrix_basisFun_mul (b : Basis ι R (ι → R)) (A : Matrix ι ι R) :
    b.toMatrix (Pi.basisFun R ι) * A = of fun i j => b.repr (Aᵀ j) i

Proof state:
case a
ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
⊢ (toMatrix (Pi.basisFun R ι) b) (toLin' A) i j = of (fun i j => (b.repr (Aᵀ j)) i) i j

Tactic:
rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
  Matrix.mulVec_single_one, Matrix.of_apply]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
⊢ (toMatrix (Pi.basisFun R ι) b) (toLin' A) = of fun i j => (b.repr (Aᵀ j)) i

Tactic:
ext i j

Result:
case a
ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
⊢ (toMatrix (Pi.basisFun R ι) b) (toLin' A) i j = of (fun i j => (b.repr (Aᵀ j)) i) i j

Proof state:
ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
⊢ b.toMatrix ⇑(Pi.basisFun R ι) * A = of fun i j => (b.repr (Aᵀ j)) i

Tactic:
classical
simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']
ext i j
rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
  Matrix.mulVec_single_one, Matrix.of_apply]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
⊢ b.toMatrix ⇑(Pi.basisFun R ι) * A = of fun i j => (b.repr (Aᵀ j)) i

Tactic:
simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']

Result:
ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
⊢ (toMatrix (Pi.basisFun R ι) b) (toLin' A) = of fun i j => (b.repr (Aᵀ j)) i
-- Mathlib/Data/Fin/Rev.lean
lemma predAbove_rev_left (p : Fin n) (i : Fin (n + 1)) :
    p.rev.predAbove i = (p.predAbove i.rev).rev

Proof state:
case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
rw [predAbove_of_le_castSucc _ _ h, rev_castPred,
  predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), pred_inj, rev_rev]

Result:
no goals

Proof state:
n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
obtain h | h := (rev i).succ_le_or_le_castSucc p

Result:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Proof state:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
rw [predAbove_of_succ_le _ _ h, rev_pred,
  predAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), castPred_inj, rev_rev]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_le_mul_of_nonpos_left [ExistsAddOfLE α] [PosMulMono α]
    [AddRightMono α] [AddRightReflectLE α]
    (h : b ≤ a) (hc : c ≤ 0) : c * a ≤ c * b

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
⊢ c * a ≤ c * b

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc

Result:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
d : α
hcd : 0 = c + d
⊢ c * a ≤ c * b

Proof state:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
d : α
hcd : 0 = c + d
⊢ c * a ≤ c * b

Tactic:
refine le_of_add_le_add_right (a := d * b + d * a) ?_

Result:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
d : α
hcd : 0 = c + d
⊢ c * a + (d * b + d * a) ≤ c * b + (d * b + d * a)

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
d : α
hcd : 0 = c + d
⊢ c * a + (d * b + d * a) = d * b

Tactic:
rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]

Result:
no goals

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
d : α
hcd : 0 = c + d
⊢ d * a = c * b + (d * b + d * a)

Tactic:
rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

Result:
no goals

Proof state:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
h : b ≤ a
hc : c ≤ 0
d : α
hcd : 0 = c + d
⊢ c * a + (d * b + d * a) ≤ c * b + (d * b + d * a)

Tactic:
calc
  _ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
  _ ≤ d * a := mul_le_mul_of_nonneg_left h <| hcd.trans_le <| add_le_of_nonpos_left hc
  _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

Result:
no goals
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem ramificationIdx_eq_normalizedFactors_count [DecidableEq (Ideal S)]
    (hp0 : map f p ≠ ⊥) (hP : P.IsPrime)
    (hP0 : P ≠ ⊥) : ramificationIdx f p P = (normalizedFactors (map f p)).count P

Proof state:
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : DecidableEq (Ideal S)
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
⊢ ramificationIdx f p P = Multiset.count P (normalizedFactors (map f p))

Tactic:
have hPirr := (Ideal.prime_of_isPrime hP0 hP).irreducible

Result:
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : DecidableEq (Ideal S)
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ramificationIdx f p P = Multiset.count P (normalizedFactors (map f p))

Proof state:
case refine_2
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : DecidableEq (Ideal S)
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ¬Multiset.count P (normalizedFactors (map f p)) + 1 ≤ Multiset.count P (normalizedFactors (map f p))

Tactic:
exact (Nat.lt_succ_self _).not_le

Result:
no goals

Proof state:
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : DecidableEq (Ideal S)
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ramificationIdx f p P = Multiset.count P (normalizedFactors (map f p))

Tactic:
refine ramificationIdx_spec (Ideal.le_of_dvd ?_) (mt Ideal.dvd_iff_le.mpr ?_) <;>
  rw [dvd_iff_normalizedFactors_le_normalizedFactors (pow_ne_zero _ hP0) hp0,
    normalizedFactors_pow, normalizedFactors_irreducible hPirr, normalize_eq,
    Multiset.nsmul_singleton, ← Multiset.le_count_iff_replicate_le]

Result:
case refine_2
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : DecidableEq (Ideal S)
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ ¬Multiset.count P (normalizedFactors (map f p)) + 1 ≤ Multiset.count P (normalizedFactors (map f p))
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem Homeomorph.mulLeft_symm (a : G) : (Homeomorph.mulLeft a).symm = Homeomorph.mulLeft a⁻¹

Proof state:
case H
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a x✝ : G
⊢ (Homeomorph.mulLeft a).symm x✝ = (Homeomorph.mulLeft a⁻¹) x✝

Tactic:
rfl

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a : G
⊢ (Homeomorph.mulLeft a).symm = Homeomorph.mulLeft a⁻¹

Tactic:
ext

Result:
case H
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a x✝ : G
⊢ (Homeomorph.mulLeft a).symm x✝ = (Homeomorph.mulLeft a⁻¹) x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mkArray_inj : mkArray n a = mkArray m b ↔ n = m ∧ (n = 0 ∨ a = b)

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
b : α✝
⊢ mkArray n a = mkArray m b ↔ n = m ∧ (n = 0 ∨ a = b)

Tactic:
rw [← toList_inj]

Result:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
b : α✝
⊢ (mkArray n a).toList = (mkArray m b).toList ↔ n = m ∧ (n = 0 ∨ a = b)

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
b : α✝
⊢ (mkArray n a).toList = (mkArray m b).toList ↔ n = m ∧ (n = 0 ∨ a = b)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem zero_right (X : C) : IsPushout (0 : X ⟶ 0) (𝟙 X) (0 : (0 : C) ⟶ 0) (0 : X ⟶ 0) :=
  { w

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ PushoutCocone.inr s ≫ 0 = PushoutCocone.inr s ≫ 𝟙 s.pt

Tactic:
simpa using PushoutCocone.condition s

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 ⋯).ι.app j ≫ (fun x => 0) s = s.ι.app j

Tactic:
have c :=
  @PushoutCocone.coequalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _)
    (by simp [eq_iff_true_of_subsingleton]) (by simpa using PushoutCocone.condition s)

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
c : ∀ (j : WalkingSpan), s.ι.app j ≫ 0 = s.ι.app j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 ⋯).ι.app j ≫ (fun x => 0) s = s.ι.app j

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ PushoutCocone.inl s ≫ 0 = PushoutCocone.inl s ≫ 𝟙 s.pt

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
c : ∀ (j : WalkingSpan), s.ι.app j ≫ 0 = s.ι.app j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 ⋯).ι.app j ≫ (fun x => 0) s = s.ι.app j

Tactic:
simpa using c

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ 0 = 𝟙 X ≫ 0

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem alternatingGroup.index_eq_two [Nontrivial α] :
    (alternatingGroup α).index = 2

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ Nat.card ↥⊤ = 2

Tactic:
simp_rw [mem_top, Nat.card_eq_fintype_card, card_subtype_true, card_units_int]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ (alternatingGroup α).index = 2

Tactic:
rw [alternatingGroup, index_ker, MonoidHom.range_eq_top.mpr (sign_surjective α)]

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ Nat.card ↥⊤ = 2
-- Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean
lemma rieszContentAux_union {K₁ K₂ : TopologicalSpace.Compacts X}
    (disj : Disjoint (K₁ : Set X) K₂) :
    rieszContentAux Λ (K₁ ⊔ K₂) = rieszContentAux Λ K₁ + rieszContentAux Λ K₂

Proof state:
case neg
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
x : X
h : ¬f x = 0
⊢ ↑(f x) = ↑((⇑g₁ + ⇑g₂) x) * ↑(f x)

Tactic:
push_neg at h

Result:
case neg
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
x : X
h : f x ≠ 0
⊢ ↑(f x) = ↑((⇑g₁ + ⇑g₂) x) * ↑(f x)
-- Mathlib/Data/Nat/Digits.lean
/-- Interpreting as a base `p` number and dividing by `p` is the same as interpreting the tail.
-/
lemma ofDigits_div_eq_ofDigits_tail {p : ℕ} (hpos : 0 < p) (digits : List ℕ)
    (w₁ : ∀ l ∈ digits, l < p) : ofDigits p digits / p = ofDigits p digits.tail

Proof state:
case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd / p + ofDigits p tl = ofDigits p (hd :: tl).tail

Tactic:
rw [Nat.div_eq_of_lt <| w₁ _ <| List.mem_cons_self _ _, zero_add]

Result:
case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p tl = ofDigits p (hd :: tl).tail

Proof state:
case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p (hd :: tl) / p = ofDigits p (hd :: tl).tail

Tactic:
refine Eq.trans (add_mul_div_left hd _ hpos) ?_

Result:
case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd / p + ofDigits p tl = ofDigits p (hd :: tl).tail

Proof state:
case nil
p : ℕ
hpos : 0 < p
w₁ : ∀ l ∈ [], l < p
⊢ ofDigits p [] / p = ofDigits p [].tail

Tactic:
simp [ofDigits]

Result:
no goals

Proof state:
case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p tl = ofDigits p (hd :: tl).tail

Tactic:
rfl

Result:
no goals

Proof state:
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits / p = ofDigits p digits.tail

Tactic:
induction' digits with hd tl

Result:
case nil
p : ℕ
hpos : 0 < p
w₁ : ∀ l ∈ [], l < p
⊢ ofDigits p [] / p = ofDigits p [].tail

case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p (hd :: tl) / p = ofDigits p (hd :: tl).tail
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem inv_logb_div_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :
    (logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹

Proof state:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a / b) = logb c a - logb c b

Tactic:
exact logb_div h₁ h₂

Result:
no goals

Proof state:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹

Tactic:
simp_rw [inv_logb]

Result:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a / b) = logb c a - logb c b
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma factorization_floorRoot (n a : ℕ) :
    (floorRoot n a).factorization = a.factorization ⌊/⌋ n

Proof state:
case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌊/⌋ n

Tactic:
obtain rfl | rfl := h <;> simp

Result:
no goals

Proof state:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌊/⌋ n).support
⊢ Prime p

Tactic:
have : p.Prime ∧ p ∣ a ∧ ¬a = 0 := by simpa using support_floorDiv_subset hp

Result:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌊/⌋ n).support
this : Prime p ∧ p ∣ a ∧ ¬a = 0
⊢ Prime p

Proof state:
n a : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 => x1 ^ x2).factorization = a.factorization ⌊/⌋ n

Tactic:
split_ifs with h

Result:
case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌊/⌋ n

case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ ((a.factorization ⌊/⌋ n).prod fun x1 x2 => x1 ^ x2).factorization = a.factorization ⌊/⌋ n

Proof state:
n a : ℕ
⊢ (n.floorRoot a).factorization = a.factorization ⌊/⌋ n

Tactic:
rw [floorRoot_def]

Result:
n a : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 => x1 ^ x2).factorization = a.factorization ⌊/⌋ n

Proof state:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌊/⌋ n).support
this : Prime p ∧ p ∣ a ∧ ¬a = 0
⊢ Prime p

Tactic:
exact this.1

Result:
no goals

Proof state:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ ((a.factorization ⌊/⌋ n).prod fun x1 x2 => x1 ^ x2).factorization = a.factorization ⌊/⌋ n

Tactic:
refine prod_pow_factorization_eq_self fun p hp ↦ ?_

Result:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌊/⌋ n).support
⊢ Prime p

Proof state:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌊/⌋ n).support
⊢ Prime p ∧ p ∣ a ∧ ¬a = 0

Tactic:
simpa using support_floorDiv_subset hp

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_subsingleton {s : Set X} (h : s.Subsingleton) : dimH s = 0

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
s : Set X
h : s.Subsingleton
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH s ≤ 0

Tactic:
refine dimH_le_of_hausdorffMeasure_ne_top ?_

Result:
X : Type u_2
inst✝ : EMetricSpace X
s : Set X
h : s.Subsingleton
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ μH[↑0] s ≠ ⊤

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
s : Set X
h : s.Subsingleton
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ μH[↑0] s ≠ ⊤

Tactic:
exact ((hausdorffMeasure_le_one_of_subsingleton h le_rfl).trans_lt ENNReal.one_lt_top).ne

Result:
no goals

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
s : Set X
h : s.Subsingleton
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH s = 0

Tactic:
apply le_antisymm _ (zero_le _)

Result:
X : Type u_2
inst✝ : EMetricSpace X
s : Set X
h : s.Subsingleton
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH s ≤ 0

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
s : Set X
h : s.Subsingleton
⊢ dimH s = 0

Tactic:
borelize X

Result:
X : Type u_2
inst✝ : EMetricSpace X
s : Set X
h : s.Subsingleton
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH s = 0
-- Mathlib/Data/Real/EReal.lean
lemma inv_neg_of_neg_ne_bot {a : EReal} (h : a < 0) (h' : a ≠ ⊥) : a⁻¹ < 0

Proof state:
a : EReal
h : a < 0
h' : a ≠ ⊥
⊢ a⁻¹ < 0

Tactic:
cases a with
| h_bot => exact (h' (Eq.refl ⊥)).rec
| h_real a => rw [← coe_inv a]; norm_cast at *; exact inv_lt_zero.2 h
| h_top => exact (not_top_lt h).rec

Result:
no goals

Proof state:
case h_top
h : ⊤ < 0
h' : ⊤ ≠ ⊥
⊢ ⊤⁻¹ < 0

Tactic:
exact (not_top_lt h).rec

Result:
no goals

Proof state:
case h_real
a : ℝ
h' : ¬↑a = ⊥
h : a < 0
⊢ a⁻¹ < 0

Tactic:
exact inv_lt_zero.2 h

Result:
no goals

Proof state:
case h_real
a : ℝ
h : ↑a < 0
h' : ↑a ≠ ⊥
⊢ ↑a⁻¹ < 0

Tactic:
norm_cast at *

Result:
case h_real
a : ℝ
h' : ¬↑a = ⊥
h : a < 0
⊢ a⁻¹ < 0

Proof state:
case h_bot
h : ⊥ < 0
h' : ⊥ ≠ ⊥
⊢ ⊥⁻¹ < 0

Tactic:
exact (h' (Eq.refl ⊥)).rec

Result:
no goals

Proof state:
case h_real
a : ℝ
h : ↑a < 0
h' : ↑a ≠ ⊥
⊢ (↑a)⁻¹ < 0

Tactic:
rw [← coe_inv a]

Result:
case h_real
a : ℝ
h : ↑a < 0
h' : ↑a ≠ ⊥
⊢ ↑a⁻¹ < 0
-- Mathlib/Data/Matroid/Rank/Finite.lean
lemma IsRkFinite.insert (hX : M.IsRkFinite X) (e : α) : M.IsRkFinite (insert e X)

Proof state:
α : Type u_1
M : Matroid α
X : Set α
hX : M.IsRkFinite X
e : α
⊢ M.IsRkFinite (X ∪ {e})

Tactic:
exact hX.union M.isRkFinite_singleton

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X : Set α
hX : M.IsRkFinite X
e : α
⊢ M.IsRkFinite (Insert.insert e X)

Tactic:
rw [← union_singleton]

Result:
α : Type u_1
M : Matroid α
X : Set α
hX : M.IsRkFinite X
e : α
⊢ M.IsRkFinite (X ∪ {e})