harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncate_comp_lift : (WittVector.truncate n).comp (lift _ f_compat) = f n

Proof state:
case a
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
x✝ : S
⊢ ((truncate n).comp (lift f f_compat)) x✝ = (f n) x✝

Tactic:
rw [RingHom.comp_apply, truncate_lift]

Result:
no goals

Proof state:
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ (truncate n).comp (lift f f_compat) = f n

Tactic:
ext1

Result:
case a
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
x✝ : S
⊢ ((truncate n).comp (lift f f_compat)) x✝ = (f n) x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem?_eq_getElem {l : BitVec w} {n} (h : n < w) : l[n]? = some l[n]

Proof state:
w : Nat
l : BitVec w
n : Nat
h : n < w
⊢ l[n]? = some l[n]

Tactic:
simp only [getElem?_def, h, ↓reduceDIte]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toArray_eraseIdx! (a : Vector α n) (i) (hi : i < n) :
    (a.eraseIdx! i).toArray = a.toArray.eraseIdx! i

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
hi : i < n
⊢ (a.eraseIdx! i).toArray = a.eraseIdx! i

Tactic:
cases a

Result:
case mk
α : Type u_1
n i : Nat
hi : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.eraseIdx! i).toArray =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.eraseIdx! i

Proof state:
case mk
α : Type u_1
n i : Nat
hi : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.eraseIdx! i).toArray =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.eraseIdx! i

Tactic:
simp_all [Array.eraseIdx!]

Result:
no goals
-- Mathlib/Data/Vector/Defs.lean
lemma getElem_def (v : Vector α n) (i : ℕ) {hi : i < n} :
    v[i] = v.toList[i]'(by simpa) := rfl

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
hi : i < n
⊢ i < v.toList.length

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem isSymmetric_iff_isSelfAdjoint (A : E →ₗ[𝕜] E) : IsSymmetric A ↔ IsSelfAdjoint A

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
A : E →ₗ[𝕜] E
⊢ A.IsSymmetric ↔ IsSelfAdjoint A

Tactic:
rw [isSelfAdjoint_iff', IsSymmetric, ← LinearMap.eq_adjoint_iff]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
A : E →ₗ[𝕜] E
⊢ A = adjoint A ↔ adjoint A = A

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
A : E →ₗ[𝕜] E
⊢ A = adjoint A ↔ adjoint A = A

Tactic:
exact eq_comm

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem revzip_powersetAux' {l : List α} ⦃x⦄ (h : x ∈ revzip (powersetAux' l)) :
    x.1 + x.2 = ↑l

Proof state:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a ∈ l.sublists'.revzip, Prod.map ofList ofList a = x
⊢ x.1 + x.2 = ↑l

Tactic:
simp only [Prod.map_apply, Prod.exists] at h

Result:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a b, (a, b) ∈ l.sublists'.revzip ∧ (↑a, ↑b) = x
⊢ x.1 + x.2 = ↑l

Proof state:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a b, (a, b) ∈ l.sublists'.revzip ∧ (↑a, ↑b) = x
⊢ x.1 + x.2 = ↑l

Tactic:
rcases h with ⟨l₁, l₂, h, rfl, rfl⟩

Result:
case intro.intro.intro.refl
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.revzip
⊢ (↑l₁, ↑l₂).1 + (↑l₁, ↑l₂).2 = ↑l

Proof state:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux' l).revzip
⊢ x.1 + x.2 = ↑l

Tactic:
rw [revzip, powersetAux', ← map_reverse, zip_map, ← revzip, List.mem_map] at h

Result:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a ∈ l.sublists'.revzip, Prod.map ofList ofList a = x
⊢ x.1 + x.2 = ↑l

Proof state:
case intro.intro.intro.refl
α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.revzip
⊢ (↑l₁, ↑l₂).1 + (↑l₁, ↑l₂).2 = ↑l

Tactic:
exact Quot.sound (revzip_sublists' _ _ _ h)

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCoseparating_op_iff (𝒢 : Set C) : IsCoseparating 𝒢.op ↔ IsSeparating 𝒢

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢.op, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

Tactic:
refine Quiver.Hom.unop_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.op_inj ?_)

Result:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢.op, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : C
hG : G ∈ 𝒢
h : G ⟶ unop Y
⊢ (h ≫ f.unop).op = (h ≫ g.unop).op

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
⊢ IsCoseparating 𝒢.op ↔ IsSeparating 𝒢

Tactic:
refine ⟨fun h𝒢 X Y f g hfg => ?_, fun h𝒢 X Y f g hfg => ?_⟩

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢.op
X Y : C
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢.op, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢.op
X Y : C
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Tactic:
refine Quiver.Hom.op_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.unop_inj ?_)

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢.op
X Y : C
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : Cᵒᵖ
hG : G ∈ 𝒢.op
h : op X ⟶ G
⊢ (f.op ≫ h).unop = (g.op ≫ h).unop

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢.op
X Y : C
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : Cᵒᵖ
hG : G ∈ 𝒢.op
h : op X ⟶ G
⊢ (f.op ≫ h).unop = (g.op ≫ h).unop

Tactic:
simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ (Set.mem_op.1 hG) _

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢.op, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : C
hG : G ∈ 𝒢
h : G ⟶ unop Y
⊢ (h ≫ f.unop).op = (h ≫ g.unop).op

Tactic:
simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ (Set.op_mem_op.2 hG) _

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Defs.lean
theorem pow_eq_zero_iff' [MonoidWithZero R] [IsReduced R] [Nontrivial R] {n : ℕ} :
    x ^ n = 0 ↔ x = 0 ∧ n ≠ 0

Proof state:
R : Type u_1
x : R
inst✝² : MonoidWithZero R
inst✝¹ : IsReduced R
inst✝ : Nontrivial R
n : ℕ
⊢ x ^ n = 0 ↔ x = 0 ∧ n ≠ 0

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean
lemma hasProjectiveDimensionLT_of_ge (m : ℕ) (h : n ≤ m)
    [HasProjectiveDimensionLT X n] :
    HasProjectiveDimensionLT X m

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
⊢ HasProjectiveDimensionLT X m

Tactic:
letI := HasExt.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
⊢ HasProjectiveDimensionLT X m

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
⊢ HasProjectiveDimensionLT X m

Tactic:
rw [hasProjectiveDimensionLT_iff]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), m ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
i : ℕ
hi : m ≤ i
Y : C
e : Ext X Y i
⊢ n ≤ i

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), m ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0

Tactic:
intro i hi Y e

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
i : ℕ
hi : m ≤ i
Y : C
e : Ext X Y i
⊢ e = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
i : ℕ
hi : m ≤ i
Y : C
e : Ext X Y i
⊢ e = 0

Tactic:
exact e.eq_zero_of_hasProjectiveDimensionLT n (by omega)

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem isRotated_append : (l ++ l') ~r (l' ++ l) :=
  ⟨l.length, by simp⟩

Proof state:
α : Type u
l l' : List α
⊢ (l ++ l').rotate l.length = l' ++ l

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem inv_whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
    inv (X ◁ f) = X ◁ inv f

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ inv (X ◁ f) = X ◁ inv f

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lift_lt {a b : Ordinal} : lift.{u, v} a < lift.{u, v} b ↔ a < b

Proof state:
a b : Ordinal.{v}
⊢ lift.{u, v} a < lift.{u, v} b ↔ a < b

Tactic:
simp_rw [lt_iff_le_not_le, lift_le]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
protected lemma add [AddLeftMono R] {A : Matrix m m R} {B : Matrix m m R}
    (hA : A.PosSemidef) (hB : B.PosSemidef) : (A + B).PosSemidef :=
  ⟨hA.isHermitian.add hB.isHermitian, fun x => by
    rw [add_mulVec, dotProduct_add]
    exact add_nonneg (hA.2 x) (hB.2 x)⟩

Proof state:
m : Type u_1
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : AddLeftMono R
A B : Matrix m m R
hA : A.PosSemidef
hB : B.PosSemidef
x : m → R
⊢ 0 ≤ star x ⬝ᵥ (A + B) *ᵥ x

Tactic:
rw [add_mulVec, dotProduct_add]

Result:
m : Type u_1
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : AddLeftMono R
A B : Matrix m m R
hA : A.PosSemidef
hB : B.PosSemidef
x : m → R
⊢ 0 ≤ star x ⬝ᵥ A *ᵥ x + star x ⬝ᵥ B *ᵥ x

Proof state:
m : Type u_1
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : AddLeftMono R
A B : Matrix m m R
hA : A.PosSemidef
hB : B.PosSemidef
x : m → R
⊢ 0 ≤ star x ⬝ᵥ A *ᵥ x + star x ⬝ᵥ B *ᵥ x

Tactic:
exact add_nonneg (hA.2 x) (hB.2 x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem replaceEntry_of_perm [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k}
    (hl : DistinctKeys l) (h : Perm l l') : Perm (replaceEntry k v l) (replaceEntry k v l')

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l l' : List ((a : α) × β a)
k : α
v : β k
hl : DistinctKeys l
h : l.Perm l'
⊢ ∀ (a : α), getEntry? a (replaceEntry k v l) = getEntry? a (replaceEntry k v l')

Tactic:
simp [getEntry?_replaceEntry, getEntry?_of_perm hl h, containsKey_of_perm h]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l l' : List ((a : α) × β a)
k : α
v : β k
hl : DistinctKeys l
h : l.Perm l'
⊢ (replaceEntry k v l).Perm (replaceEntry k v l')

Tactic:
apply getEntry?_ext hl.replaceEntry (hl.perm h.symm).replaceEntry

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l l' : List ((a : α) × β a)
k : α
v : β k
hl : DistinctKeys l
h : l.Perm l'
⊢ ∀ (a : α), getEntry? a (replaceEntry k v l) = getEntry? a (replaceEntry k v l')
-- Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
theorem Integrable.exists_hasCompactSupport_integral_sub_le
    [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular]
    {f : α → E} (hf : Integrable f μ) {ε : ℝ} (hε : 0 < ε) :
    ∃ g : α → E, HasCompactSupport g ∧ (∫ x, ‖f x - g x‖ ∂μ) ≤ ε ∧
      Continuous g ∧ Integrable g μ

Proof state:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
f : α → E
ε : ℝ
hε : 0 < ε
hf : MemLp f (ENNReal.ofReal 1) μ
⊢ ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ MemLp g (ENNReal.ofReal 1) μ

Tactic:
simpa using hf.exists_hasCompactSupport_integral_rpow_sub_le zero_lt_one hε

Result:
no goals

Proof state:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
f : α → E
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ Integrable g μ

Tactic:
simp only [← memLp_one_iff_integrable, ← eLpNorm_one_eq_lintegral_enorm, ← ENNReal.ofReal_one]
  at hf ⊢

Result:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
f : α → E
ε : ℝ
hε : 0 < ε
hf : MemLp f (ENNReal.ofReal 1) μ
⊢ ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ MemLp g (ENNReal.ofReal 1) μ
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_withDensity_eq_setIntegral_smul {f : X → ℝ≥0} (f_meas : Measurable f)
    (g : X → E) {s : Set X} (hs : MeasurableSet s) :
    ∫ x in s, g x ∂μ.withDensity (fun x => f x) = ∫ x in s, f x • g x ∂μ

Proof state:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
s : Set X
hs : MeasurableSet s
⊢ (∫ (x : X) in s, g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ

Tactic:
rw [restrict_withDensity hs, integral_withDensity_eq_integral_smul f_meas]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
lemma inf_not_iff_bot :
    φ ⊓ ∼φ ⇔[T] ⊥ := fun M v xs => by
  simp only [realize_iff, realize_inf, realize_not, and_not_self, realize_bot]

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⊓ ∼φ ⇔ ⊥).Realize v xs

Tactic:
simp only [realize_iff, realize_inf, realize_not, and_not_self, realize_bot]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem dotProduct_adjMatrix [NonAssocSemiring α] (v : V) (vec : V → α) :
    dotProduct vec (G.adjMatrix α v) = ∑ u ∈ G.neighborFinset v, vec u

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ vec ⬝ᵥ adjMatrix α G v = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
simp [neighborFinset_eq_filter, dotProduct, sum_filter, Finset.sum_apply]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjectionFn_norm_sq (v : E) :
    ‖v‖ * ‖v‖ =
      ‖v - orthogonalProjectionFn K v‖ * ‖v - orthogonalProjectionFn K v‖ +
        ‖orthogonalProjectionFn K v‖ * ‖orthogonalProjectionFn K v‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
p : E := orthogonalProjectionFn K v
h' : ⟪v - p, p⟫_𝕜 = 0
⊢ ‖v‖ * ‖v‖ = ‖v - p‖ * ‖v - p‖ + ‖p‖ * ‖p‖

Tactic:
convert norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (v - p) p h' using 2 <;> simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
p : E := orthogonalProjectionFn K v
⊢ ‖v‖ * ‖v‖ = ‖v - p‖ * ‖v - p‖ + ‖p‖ * ‖p‖

Tactic:
have h' : ⟪v - p, p⟫ = 0 :=
  orthogonalProjectionFn_inner_eq_zero _ _ (orthogonalProjectionFn_mem v)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
p : E := orthogonalProjectionFn K v
h' : ⟪v - p, p⟫_𝕜 = 0
⊢ ‖v‖ * ‖v‖ = ‖v - p‖ * ‖v - p‖ + ‖p‖ * ‖p‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
⊢ ‖v‖ * ‖v‖ =
    ‖v - orthogonalProjectionFn K v‖ * ‖v - orthogonalProjectionFn K v‖ +
      ‖orthogonalProjectionFn K v‖ * ‖orthogonalProjectionFn K v‖

Tactic:
set p := orthogonalProjectionFn K v

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
p : E := orthogonalProjectionFn K v
⊢ ‖v‖ * ‖v‖ = ‖v - p‖ * ‖v - p‖ + ‖p‖ * ‖p‖
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem lineMap_apply_one (p₀ p₁ : P1) : lineMap p₀ p₁ (1 : k) = p₁

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
⊢ (lineMap p₀ p₁) 1 = p₁

Tactic:
simp [lineMap_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem Bool.or_to_or (a b : Bool) : ((a = true) ∨ (b = true)) = ((a || b) = true)

Proof state:
a b : Bool
⊢ (a = true ∨ b = true) = ((a || b) = true)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem aeval_U [Algebra R R'] (x : R') (n : ℤ) : aeval x (U R n) = (U R' n).eval x

Proof state:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R'
n : ℤ
⊢ (aeval x) (U R n) = eval x (U R' n)

Tactic:
rw [aeval_def, eval₂_eq_eval_map, map_U]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem prev_lt_of_pos (s : String) (i : Pos) (h : i ≠ 0) : (s.prev i).1 < i.1

Proof state:
s : String
i : Pos
h : i ≠ 0
⊢ (s.prev i).byteIdx < i.byteIdx

Tactic:
simp [prev, h]

Result:
s : String
i : Pos
h : i ≠ 0
⊢ (utf8PrevAux s.data 0 i).byteIdx < i.byteIdx

Proof state:
s : String
i : Pos
h : i ≠ 0
⊢ (utf8PrevAux s.data 0 i).byteIdx < i.byteIdx

Tactic:
exact utf8PrevAux_lt_of_pos _ _ _ h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/EpiMono.lean
theorem preserves_epi_of_preservesColimit {X Y : C} (f : X ⟶ Y) [PreservesColimit (span f f) F]
    [Epi f] : Epi (F.map f)

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)
⊢ Epi (F.map f)

Tactic:
apply PushoutCocone.epi_of_isColimitMkIdId _ this

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)
⊢ Epi (F.map f)

Tactic:
simp_rw [F.map_id] at this

Result:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)
⊢ Epi (F.map f)

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
⊢ Epi (F.map f)

Tactic:
have := isColimitPushoutCoconeMapOfIsColimit F _ (PushoutCocone.isColimitMkIdId f)

Result:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)
⊢ Epi (F.map f)
-- Mathlib/Computability/RegularExpressions.lean
theorem zero_rmatch (x : List α) : rmatch 0 x = false

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x : List α
⊢ rmatch 0 x = false

Tactic:
induction x <;> simp [rmatch, matchEpsilon, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem false_imp_eq (p : Prop) : (False → p) = True

Proof state:
p : Prop
⊢ (False → p) = True

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_succ_column {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (j : Fin n.succ) :
    det A =
      ∑ i : Fin n.succ, (-1) ^ (i + j : ℕ) * A i j * det (A.submatrix i.succAbove j.succAbove)

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j : Fin n.succ
⊢ A.det = ∑ i : Fin n.succ, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
rw [← det_transpose, det_succ_row _ j]

Result:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j : Fin n.succ
⊢ ∑ j_1 : Fin n.succ, (-1) ^ (↑j + ↑j_1) * Aᵀ j j_1 * (Aᵀ.submatrix j.succAbove j_1.succAbove).det =
    ∑ i : Fin n.succ, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j : Fin n.succ
⊢ ∑ j_1 : Fin n.succ, (-1) ^ (↑j + ↑j_1) * Aᵀ j j_1 * (Aᵀ.submatrix j.succAbove j_1.succAbove).det =
    ∑ i : Fin n.succ, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
refine Finset.sum_congr rfl fun i _ => ?_

Result:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ (↑j + ↑i) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ (↑j + ↑i) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
rw [add_comm, ← det_transpose, transpose_apply, transpose_submatrix, transpose_transpose]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem isCoprime_of_isMaximal [I.IsMaximal] [J.IsMaximal] (ne : I ≠ J) : IsCoprime I J

Proof state:
R : Type u
inst✝² : CommSemiring R
I J : Ideal R
inst✝¹ : IsCoatom I
inst✝ : IsCoatom J
ne : I ≠ J
⊢ Codisjoint I J

Tactic:
exact IsCoatom.codisjoint_of_ne ‹_› ‹_› ne

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
I J : Ideal R
inst✝¹ : I.IsMaximal
inst✝ : J.IsMaximal
ne : I ≠ J
⊢ IsCoprime I J

Tactic:
rw [isCoprime_iff_codisjoint, isMaximal_def] at *

Result:
R : Type u
inst✝² : CommSemiring R
I J : Ideal R
inst✝¹ : IsCoatom I
inst✝ : IsCoatom J
ne : I ≠ J
⊢ Codisjoint I J
-- Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
lemma norm_cfcₙ_one_sub_one_add_inv_lt_one (a : A) :
    ‖cfcₙ (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹) a‖ < 1 :=
  nnnorm_cfcₙ_nnreal_lt fun x _ ↦ tsub_lt_self zero_lt_one (by positivity)

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
x : ℝ≥0
x✝ : x ∈ σₙ ℝ≥0 a
⊢ 0 < (1 + x)⁻¹

Tactic:
positivity

Result:
no goals