harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma liftCochain_descCochain :
    (liftCochain φ α β h).comp (descCochain φ α' β' h') hp =
      α.comp α' (by omega) + β.comp β' (by omega)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.248067, u_1} C
inst✝³ : Category.{?u.248071, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K L : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
⊢ m + m' = p

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K L : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
⊢ m + -1 + n' = ?m.250612

Tactic:
linarith

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.248067, u_1} C
inst✝³ : Category.{?u.248071, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K L : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
⊢ n + n' = p

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K L : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
⊢ -1 + n' = m'

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K L : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
⊢ (liftCochain φ α β h).comp (descCochain φ α' β' h') hp = α.comp α' ⋯ + β.comp β' ⋯

Tactic:
simp [liftCochain, descCochain,
  Cochain.comp_assoc α (inl φ) _ _ (show -1 + n' = m' by omega) (by linarith)]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem sum_rpow_le_norm_rpow (hp : 0 < p.toReal) (f : lp E p) (s : Finset α) :
    ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ∑' (i : α), ‖↑f i‖ ^ p.toReal

Tactic:
have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i => Real.rpow_nonneg (norm_nonneg _) _

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ∑' (i : α), ‖↑f i‖ ^ p.toReal

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ∑' (i : α), ‖↑f i‖ ^ p.toReal

Tactic:
refine sum_le_tsum _ (fun i _ => this i) ?_

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ Summable fun i => ‖↑f i‖ ^ p.toReal

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ Summable fun i => ‖↑f i‖ ^ p.toReal

Tactic:
exact (lp.memℓp f).summable hp

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal

Tactic:
rw [lp.norm_rpow_eq_tsum hp f]

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ∑' (i : α), ‖↑f i‖ ^ p.toReal
-- Mathlib/Order/Interval/Finset/Box.lean
lemma eq_zero_iff_eq_zero_of_mem_box  {x : α} (hx : x ∈ box n) : x = 0 ↔ n = 0 :=
  ⟨zero_mem_box.mp ∘ (· ▸ hx), fun hn ↦ by rwa [hn, box_zero, mem_singleton] at hx⟩

Proof state:
α : Type u_1
inst✝² : OrderedRing α
inst✝¹ : LocallyFiniteOrder α
n : ℕ
inst✝ : DecidableEq α
x : α
hx : x ∈ box n
hn : n = 0
⊢ x = 0

Tactic:
rwa [hn, box_zero, mem_singleton] at hx

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem l_iSup (gc : GaloisConnection l u) {f : ι → α} : l (iSup f) = ⨆ i, l (f i) :=
  Eq.symm <|
    IsLUB.iSup_eq <|
      show IsLUB (range (l ∘ f)) (l (iSup f)) by
        rw [range_comp, ← sSup_range]; exact gc.isLUB_l_image (isLUB_sSup _)

Proof state:
α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (range (l ∘ f)) (l (iSup f))

Tactic:
rw [range_comp, ← sSup_range]

Result:
α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (l '' range f) (l (sSup (range f)))

Proof state:
α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (l '' range f) (l (sSup (range f)))

Tactic:
exact gc.isLUB_l_image (isLUB_sSup _)

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma setIntegral_densityProcess_of_mem (hκν : fst κ ≤ ν) [hν : IsFiniteKernel ν]
    (n : ℕ) (a : α) {s : Set β} (hs : MeasurableSet s) {u : Set γ}
    (hu : u ∈ countablePartition γ n) :
    ∫ x in u, densityProcess κ ν n a x s ∂(ν a) = (κ a (u ×ˢ s)).toReal

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
x : γ
h0 : (ν a) (countablePartitionSet n x) = 0
h0' : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ s) = 0

Tactic:
refine measure_mono_null (fun x ↦ ?_) h0'

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
x✝ : γ
h0 : (ν a) (countablePartitionSet n x✝) = 0
h0' : (κ a) {p | p.1 ∈ countablePartitionSet n x✝} = 0
x : γ × β
⊢ x ∈ countablePartitionSet n x✝ ×ˢ s → x ∈ {p | p.1 ∈ countablePartitionSet n x✝}

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
x : γ
h0 : (ν a) (countablePartitionSet n x) = 0
h0' : (κ.fst a) (countablePartitionSet n x) = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ s) = 0

Tactic:
rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)] at h0'

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
x : γ
h0 : (ν a) (countablePartitionSet n x) = 0
h0' : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ s) = 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this✝ : IsFiniteKernel κ
hu_meas : MeasurableSet u
x : γ
h0 : (ν a) (countablePartitionSet n x) = 0
this : (κ a) (countablePartitionSet n x ×ˢ s) = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) < ⊤

Tactic:
simp [h0, this]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
/-- The multiplicity of `a` as root of a nonzero polynomial `p` is at least `n` iff
`(X - a) ^ n` divides `p`. -/
lemma le_rootMultiplicity_iff (p0 : p ≠ 0) {a : R} {n : ℕ} :
    n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ m < n, ¬¬(X - C a) ^ (m + 1) ∣ p) ↔ (X - C a) ^ n ∣ p

Tactic:
simp_rw [Classical.not_not]

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ m < n, (X - C a) ^ (m + 1) ∣ p) ↔ (X - C a) ^ n ∣ p

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ m < n, (X - C a) ^ (m + 1) ∣ p) ↔ (X - C a) ^ n ∣ p

Tactic:
refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ n ∣ p

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p

Tactic:
rw [rootMultiplicity_eq_nat_find_of_nonzero p0, @Nat.le_find_iff _ (_)]

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ m < n, ¬¬(X - C a) ^ (m + 1) ∣ p) ↔ (X - C a) ^ n ∣ p

Proof state:
case succ
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n + 1, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ (n + 1) ∣ p

Tactic:
exact h n n.lt_succ_self

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ n ∣ p

Tactic:
rcases n with - | n

Result:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ m < 0, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ 0 ∣ p

case succ
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n + 1, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ (n + 1) ∣ p

Proof state:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ m < 0, (X - C a) ^ (m + 1) ∣ p
⊢ 1 ∣ p

Tactic:
apply one_dvd

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ m < 0, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ 0 ∣ p

Tactic:
rw [pow_zero]

Result:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ m < 0, (X - C a) ^ (m + 1) ∣ p
⊢ 1 ∣ p
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem one [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] :
    PosDef (1 : Matrix n n R) :=
  ⟨isHermitian_one, fun x hx => by simpa only [one_mulVec, dotProduct_star_self_pos_iff]⟩

Proof state:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
x : n → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ 1 *ᵥ x

Tactic:
simpa only [one_mulVec, dotProduct_star_self_pos_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_filter {l : Array α} (h : p a) : count a (filter p l) = count a l

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
a : α
h : p a = true
toList✝ : List α
⊢ count a (filter p { toList := toList✝ }) = count a { toList := toList✝ }

Tactic:
simp [List.count_filter, h]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
a : α
l : Array α
h : p a = true
⊢ count a (filter p l) = count a l

Tactic:
cases l

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
a : α
h : p a = true
toList✝ : List α
⊢ count a (filter p { toList := toList✝ }) = count a { toList := toList✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sub_left_le_of_le_add {a b c : Int} (h : a ≤ b + c) : a - b ≤ c

Proof state:
a b c : Int
h : a ≤ b + c
⊢ a - b ≤ c

Tactic:
have h := Int.add_le_add_right h (-b)

Result:
a b c : Int
h✝ : a ≤ b + c
h : a + -b ≤ b + c + -b
⊢ a - b ≤ c

Proof state:
a b c : Int
h✝ : a ≤ b + c
h : a + -b ≤ b + c + -b
⊢ a - b ≤ c

Tactic:
rwa [Int.add_comm b c, Int.add_neg_cancel_right] at h

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean
theorem LinearMap.continuousAt_zero_of_locally_bounded (f : E →ₛₗ[σ] F)
    (hf : ∀ s, IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (f '' s)) : ContinuousAt f 0

Proof state:
case refine_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : RCLike 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
h : ¬ContinuousAt (⇑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ∀ t ∈ 𝓝 0, ∃ i, True ∧ Set.MapsTo (fun x => ↑n • x) (b i) t
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n

Tactic:
rcases hcont (b n) (bE1 n).1 with ⟨i, _, hi⟩

Result:
case refine_2.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : RCLike 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
h : ¬ContinuousAt (⇑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ∀ t ∈ 𝓝 0, ∃ i, True ∧ Set.MapsTo (fun x => ↑n • x) (b i) t
i : ℕ
left✝ : True
hi : Set.MapsTo (fun x => ↑n • x) (b i) (b n)
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma singularPart_eq_zero_of_ac (h : μ ≪ ν) : μ.singularPart ν = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
⊢ μ.singularPart ν ⟂ₘ μ.singularPart ν

Tactic:
exact MutuallySingular.mono_ac (mutuallySingular_singularPart _ _)
  AbsolutelyContinuous.rfl ((absolutelyContinuous_of_le (singularPart_le _ _)).trans h)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
⊢ μ.singularPart ν = 0

Tactic:
rw [← MutuallySingular.self_iff]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
⊢ μ.singularPart ν ⟂ₘ μ.singularPart ν
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem filter_eq_some {o : Option α} {p : α → Bool} :
    o.filter p = some a ↔ a ∈ o ∧ p a

Proof state:
case some
α : Type u_1
a✝ : α
p : α → Bool
a : α
⊢ (if p a = true then some a else none) = some a✝ ↔ a = a✝ ∧ p a✝ = true

Tactic:
split <;> rename_i h

Result:
case some.isTrue
α : Type u_1
a✝ : α
p : α → Bool
a : α
h : p a = true
⊢ some a = some a✝ ↔ a = a✝ ∧ p a✝ = true

case some.isFalse
α : Type u_1
a✝ : α
p : α → Bool
a : α
h : ¬p a = true
⊢ none = some a✝ ↔ a = a✝ ∧ p a✝ = true

Proof state:
case none
α : Type u_1
a : α
p : α → Bool
⊢ Option.filter p none = some a ↔ a ∈ none ∧ p a = true

Tactic:
simp

Result:
no goals

Proof state:
case some.isFalse
α : Type u_1
a✝ : α
p : α → Bool
a : α
h : ¬p a = true
⊢ none = some a✝ ↔ a = a✝ ∧ p a✝ = true

Tactic:
simp only [reduceCtorEq, false_iff, not_and, Bool.not_eq_true]

Result:
case some.isFalse
α : Type u_1
a✝ : α
p : α → Bool
a : α
h : ¬p a = true
⊢ a = a✝ → p a✝ = false

Proof state:
case some.isTrue
α : Type u_1
a✝ : α
p : α → Bool
a : α
h : p a = true
⊢ some a = some a✝ ↔ a = a✝ ∧ p a✝ = true

Tactic:
simp only [some.injEq, iff_self_and]

Result:
case some.isTrue
α : Type u_1
a✝ : α
p : α → Bool
a : α
h : p a = true
⊢ a = a✝ → p a✝ = true

Proof state:
case some.isFalse
α : Type u_1
a✝ : α
p : α → Bool
a : α
h : ¬p a = true
⊢ a = a✝ → p a✝ = false

Tactic:
rintro rfl

Result:
case some.isFalse
α : Type u_1
p : α → Bool
a : α
h : ¬p a = true
⊢ p a = false

Proof state:
case some.isTrue
α : Type u_1
p : α → Bool
a : α
h : p a = true
⊢ p a = true

Tactic:
exact h

Result:
no goals

Proof state:
case some
α : Type u_1
a✝ : α
p : α → Bool
a : α
⊢ Option.filter p (some a) = some a✝ ↔ a✝ ∈ some a ∧ p a✝ = true

Tactic:
simp [filter_some]

Result:
case some
α : Type u_1
a✝ : α
p : α → Bool
a : α
⊢ (if p a = true then some a else none) = some a✝ ↔ a = a✝ ∧ p a✝ = true

Proof state:
case some.isTrue
α : Type u_1
a✝ : α
p : α → Bool
a : α
h : p a = true
⊢ a = a✝ → p a✝ = true

Tactic:
rintro rfl

Result:
case some.isTrue
α : Type u_1
p : α → Bool
a : α
h : p a = true
⊢ p a = true

Proof state:
case some.isFalse
α : Type u_1
p : α → Bool
a : α
h : ¬p a = true
⊢ p a = false

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
lemma posPart_smul_of_nonpos {r : ℝ} (hr : r ≤ 0) {a : A} : (r • a)⁺ = -r • a⁻

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ (- -r • a)⁺ = -r • a⁻

Tactic:
rw [neg_smul, ← smul_neg, posPart_smul_of_nonneg (neg_nonneg.mpr hr), posPart_neg]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ (r • a)⁺ = -r • a⁻

Tactic:
nth_rw 1 [← neg_neg r]

Result:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ (- -r • a)⁺ = -r • a⁻
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem transvection_mul_apply_of_ne (a b : n) (ha : a ≠ i) (c : R) (M : Matrix n n R) :
    (transvection i j c * M) a b = M a b

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
a b : n
ha : a ≠ i
c : R
M : Matrix n n R
⊢ (transvection i j c * M) a b = M a b

Tactic:
simp [transvection, Matrix.add_mul, ha]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem findIdx_eq_findIdx? (p : α → Bool) (l : List α) :
    l.findIdx p = (match l.findIdx? p with | some i => i | none => l.length)

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx p xs =
    match findIdx? p xs with
    | some i => i
    | none => xs.length
h : ¬p x = true
⊢ (bif p x then 0 else findIdx p xs + 1) =
    match if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | some i => i
    | none => (x :: xs).length

Tactic:
cases h' : findIdx? p xs <;> simp [h, h', ih]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx p xs =
    match findIdx? p xs with
    | some i => i
    | none => xs.length
h : p x = true
⊢ (bif p x then 0 else findIdx p xs + 1) =
    match if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | some i => i
    | none => (x :: xs).length

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ findIdx p l =
    match findIdx? p l with
    | some i => i
    | none => l.length

Tactic:
induction l with
| nil => rfl
| cons x xs ih =>
  rw [findIdx_cons, findIdx?_cons]
  if h : p x then
    simp [h]
  else
    cases h' : findIdx? p xs <;> simp [h, h', ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx p xs =
    match findIdx? p xs with
    | some i => i
    | none => xs.length
⊢ findIdx p (x :: xs) =
    match findIdx? p (x :: xs) with
    | some i => i
    | none => (x :: xs).length

Tactic:
rw [findIdx_cons, findIdx?_cons]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx p xs =
    match findIdx? p xs with
    | some i => i
    | none => xs.length
⊢ (bif p x then 0 else findIdx p xs + 1) =
    match if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | some i => i
    | none => (x :: xs).length

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx p xs =
    match findIdx? p xs with
    | some i => i
    | none => xs.length
⊢ (bif p x then 0 else findIdx p xs + 1) =
    match if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | some i => i
    | none => (x :: xs).length

Tactic:
if h : p x then
  simp [h]
else
  cases h' : findIdx? p xs <;> simp [h, h', ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ findIdx p [] =
    match findIdx? p [] with
    | some i => i
    | none => [].length

Tactic:
rfl

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
theorem LeftInverse.iterate {g : α → α} (hg : LeftInverse g f) (n : ℕ) :
    LeftInverse g^[n] f^[n] :=
  Nat.recOn n (fun _ ↦ rfl) fun n ihn ↦ by
    rw [iterate_succ', iterate_succ]
    exact ihn.comp hg

Proof state:
α : Type u
f g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse g^[n.succ] f^[n.succ]

Tactic:
rw [iterate_succ', iterate_succ]

Result:
α : Type u
f g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)

Proof state:
α : Type u
f g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)

Tactic:
exact ihn.comp hg

Result:
no goals