harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem isHermitian_transpose_mul_self [Fintype m] (A : Matrix m n α) : (Aᴴ * A).IsHermitian

Proof state:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝² : NonUnitalSemiring α
inst✝¹ : StarRing α
inst✝ : Fintype m
A : Matrix m n α
⊢ (Aᴴ * A).IsHermitian

Tactic:
rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderivWithin_comp_add_right (a : E) :
    fderivWithin 𝕜 (fun x ↦ f (x + a)) s x = fderivWithin 𝕜 f (a +ᵥ s) (x + a)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
a : E
⊢ fderivWithin 𝕜 (fun x => f (x + a)) s x = fderivWithin 𝕜 f (a +ᵥ s) (x + a)

Tactic:
simp only [add_comm _ a, fderivWithin_comp_add_left]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_of_gt {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSucc j < i) :
    X.σ (Fin.castSucc j) ≫ X.δ i.succ = X.δ i ≫ X.σ j

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.σ j.castSucc ≫ X.δ i.succ = X.δ i ≫ X.σ j

Tactic:
dsimp [δ, σ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.map (SimplexCategory.σ j.castSucc).op ≫ X.map (SimplexCategory.δ i.succ).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ X.map (SimplexCategory.σ j.castSucc).op ≫ X.map (SimplexCategory.δ i.succ).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt H]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
lemma op_distinguished (T : Triangle C) (hT : T ∈ distTriang C) :
    ((triangleOpEquivalence C).functor.obj (Opposite.op T)) ∈ distTriang Cᵒᵖ

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ (triangleOpEquivalence C).functor.obj (Opposite.op T) ∈ distinguishedTriangles

Tactic:
rw [mem_distTriang_op_iff']

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ∃ T',
    ∃ (_ : T' ∈ distinguishedTriangles),
      Nonempty
        ((triangleOpEquivalence C).functor.obj (Opposite.op T) ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ∃ T',
    ∃ (_ : T' ∈ distinguishedTriangles),
      Nonempty
        ((triangleOpEquivalence C).functor.obj (Opposite.op T) ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Tactic:
exact ⟨T, hT, ⟨Iso.refl _⟩⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatMap_toArray (l : Vector α n) (f : α → Vector β m) :
    l.toArray.flatMap (fun a => (f a).toArray) = (l.flatMap f).toArray

Proof state:
case mk
α : Type u_1
β : Type u_2
m : Nat
f : α → Vector β m
l : Array α
⊢ Array.flatMap (fun a => (f a).toArray) { toArray := l, size_toArray := ⋯ }.toArray =
    ({ toArray := l, size_toArray := ⋯ }.flatMap f).toArray

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
m : Nat
l : Vector α n
f : α → Vector β m
⊢ Array.flatMap (fun a => (f a).toArray) l.toArray = (l.flatMap f).toArray

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
m : Nat
f : α → Vector β m
l : Array α
⊢ Array.flatMap (fun a => (f a).toArray) { toArray := l, size_toArray := ⋯ }.toArray =
    ({ toArray := l, size_toArray := ⋯ }.flatMap f).toArray
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_eq_empty [Fintype s] : s.toFinset = ∅ ↔ s = ∅

Proof state:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
A : Fintype ↑∅ := Fintype.ofIsEmpty
⊢ s.toFinset = ∅ ↔ s = ∅

Tactic:
rw [← toFinset_empty, toFinset_inj]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset = ∅ ↔ s = ∅

Tactic:
let A : Fintype (∅ : Set α) := Fintype.ofIsEmpty

Result:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
A : Fintype ↑∅ := Fintype.ofIsEmpty
⊢ s.toFinset = ∅ ↔ s = ∅
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem IsIntegral.tower_top [Algebra A B] [IsScalarTower R A B] {x : B}
    (hx : IsIntegral R x) : IsIntegral A x :=
  let ⟨p, hp, hpx⟩ := hx
  ⟨p.map <| algebraMap R A, hp.map _, by rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]⟩

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : B
hx : IsIntegral R x
p : R[X]
hp : p.Monic
hpx : eval₂ (algebraMap R B) x p = 0
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap R A) p) = 0

Tactic:
rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexHull_union (hs : s.Nonempty) (ht : t.Nonempty) :
    convexHull 𝕜 (s ∪ t) = convexJoin 𝕜 (convexHull 𝕜 s) (convexHull 𝕜 t)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ (convexHull 𝕜) ((convexHull 𝕜) s ∪ (convexHull 𝕜) t) = convexJoin 𝕜 ((convexHull 𝕜) s) ((convexHull 𝕜) t)

Tactic:
exact (convex_convexHull 𝕜 s).convexHull_union (convex_convexHull 𝕜 t) hs.convexHull ht.convexHull

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ (convexHull 𝕜) (s ∪ t) = convexJoin 𝕜 ((convexHull 𝕜) s) ((convexHull 𝕜) t)

Tactic:
rw [← convexHull_convexHull_union_left, ← convexHull_convexHull_union_right]

Result:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ (convexHull 𝕜) ((convexHull 𝕜) s ∪ (convexHull 𝕜) t) = convexJoin 𝕜 ((convexHull 𝕜) s) ((convexHull 𝕜) t)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.add_const_left (a b c : BitVec w) : a + (b + c) = (a + b) + c

Proof state:
w : Nat
a b c : BitVec w
⊢ a + (b + c) = a + b + c

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coverage.lean
lemma factorsThru_of_le {X : C} (S T : Presieve X) (h : S ≤ T) :
    S.FactorsThru T :=
  fun Y g hg => ⟨Y, 𝟙 _, g, h _ hg, by simp⟩

Proof state:
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
h : S ≤ T
Y : C
g : Y ⟶ X
hg : S g
⊢ 𝟙 Y ≫ g = g

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem isCompl_range_inl_range_inr : IsCompl (range <| @Sum.inl α β) (range Sum.inr) :=
  IsCompl.of_le
    (by
      rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, h⟩⟩
      exact Sum.noConfusion h)
    (by rintro (x | y) - <;> [left; right] <;> exact mem_range_self _)

Proof state:
α : Type u_1
β : Type u_2
⊢ ⊤ ≤ range Sum.inl ⊔ range Sum.inr

Tactic:
rintro (x | y) - <;> [left; right] <;> exact mem_range_self _

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
x₁ : α
x₂ : β
h : Sum.inr x₂ = Sum.inl x₁
⊢ Sum.inl x₁ ∈ ⊥

Tactic:
exact Sum.noConfusion h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
⊢ range Sum.inl ⊓ range Sum.inr ≤ ⊥

Tactic:
rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, h⟩⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
x₁ : α
x₂ : β
h : Sum.inr x₂ = Sum.inl x₁
⊢ Sum.inl x₁ ∈ ⊥
-- Mathlib/Order/Hom/CompleteLattice.lean
theorem map_iSup [SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : ι → α) :
    f (⨆ i, g i) = ⨆ i, f (g i)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Sort u_6
inst✝³ : FunLike F α β
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : sSupHomClass F α β
f : F
g : ι → α
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
simp [iSup, ← Set.range_comp, Function.comp_def]

Result:
no goals
-- Mathlib/Data/List/GetD.lean
theorem getD_eq_getD_getElem? (n : ℕ) : l.getD n d = l[n]?.getD d

Proof state:
case inl
α : Type u
l : List α
d : α
n : ℕ
h : n < l.length
⊢ l.getD n d = l[n]?.getD d

Tactic:
rw [getD_eq_getElem _ _ h, getElem?_eq_getElem h, Option.getD_some]

Result:
no goals

Proof state:
case inr
α : Type u
l : List α
d : α
n : ℕ
h : n ≥ l.length
⊢ l.getD n d = l[n]?.getD d

Tactic:
rw [getD_eq_default _ _ h, getElem?_eq_none_iff.mpr h, Option.getD_none]

Result:
no goals

Proof state:
α : Type u
l : List α
d : α
n : ℕ
⊢ l.getD n d = l[n]?.getD d

Tactic:
cases Nat.lt_or_ge n l.length with
| inl h => rw [getD_eq_getElem _ _ h, getElem?_eq_getElem h, Option.getD_some]
| inr h => rw [getD_eq_default _ _ h, getElem?_eq_none_iff.mpr h, Option.getD_none]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem lineMap_lt_lineMap_iff_of_lt (h : r < r') : lineMap a b r < lineMap a b r' ↔ a < b

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : r < r'
⊢ (lineMap a b) r < (lineMap a b) r' ↔ a < b

Tactic:
simp only [lineMap_apply_module]

Result:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : r < r'
⊢ (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : r < r'
⊢ (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b

Tactic:
rw [← lt_sub_iff_add_lt, add_sub_assoc, ← sub_lt_iff_lt_add', ← sub_smul, ← sub_smul,
  sub_sub_sub_cancel_left, smul_lt_smul_iff_of_pos_left (sub_pos.2 h)]

Result:
no goals
-- Mathlib/Data/List/ProdSigma.lean
theorem mem_sigma {l₁ : List α} {l₂ : ∀ a, List (σ a)} {a : α} {b : σ a} :
    Sigma.mk a b ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a

Proof state:
α : Type u_1
σ : α → Type u_3
l₁ : List α
l₂ : (a : α) → List (σ a)
a : α
b : σ a
⊢ ⟨a, b⟩ ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a

Tactic:
simp [List.sigma, mem_flatMap, mem_map, exists_prop, exists_and_left, and_left_comm,
  exists_eq_left, heq_iff_eq, exists_eq_right]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem univ_pi_update [DecidableEq ι] {β : ι → Type*} (i : ι) (f : ∀ j, α j) (a : α i)
    (t : ∀ j, α j → Set (β j)) :
    (pi univ fun j => t j (update f i a j)) = { x | x i ∈ t i a } ∩ pi {i}ᶜ fun j => t j (f j)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
β : ι → Type u_4
i : ι
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (univ.pi fun j => t j (update f i a j)) = {x | x i ∈ t i a} ∩ {i}ᶜ.pi fun j => t j (f j)

Tactic:
rw [compl_eq_univ_diff, ← pi_update_of_mem (mem_univ _)]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem filter_product_left (p : α → Prop) [DecidablePred p] :
    ((s ×ˢ t).filter fun x : α × β => p x.1) = s.filter p ×ˢ t

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
inst✝ : DecidablePred p
⊢ filter (fun x => p x.1) (s ×ˢ t) = filter p s ×ˢ t

Tactic:
simpa using filter_product p fun _ => true

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsTopologicalGroup.t1Space (h : @IsClosed G _ {1}) : T1Space G :=
  ⟨fun x => by simpa using isClosedMap_mul_right x _ h⟩

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsClosed {1}
x : G
⊢ IsClosed {x}

Tactic:
simpa using isClosedMap_mul_right x _ h

Result:
no goals
-- Mathlib/Analysis/Asymptotics/TVS.lean
lemma isLittleOTVS_iff_tendsto_inv_smul [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E} {l : Filter α}
    (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) :
    g =o[𝕜;l] f ↔ Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0)

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto (fun x => (f x)⁻¹ • g x) l (𝓝 0)
x : α
hx : f x = 0 → g x = 0
⊢ (fun x => f x • (f x)⁻¹ • g x) x = g x

Tactic:
by_cases h : f x = 0 <;> simp [h, hx]

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
⊢ g =o[𝕜;l] f ↔ Tendsto (fun x => (f x)⁻¹ • g x) l (𝓝 0)

Tactic:
refine ⟨IsLittleOTVS.tendsto_inv_smul, fun h ↦ ?_⟩

Result:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto (fun x => (f x)⁻¹ • g x) l (𝓝 0)
⊢ g =o[𝕜;l] f

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto (fun x => (f x)⁻¹ • g x) l (𝓝 0)
⊢ (fun x => f x • 1 x) =ᶠ[l] f

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto (fun x => (f x)⁻¹ • g x) l (𝓝 0)
⊢ g =o[𝕜;l] f

Tactic:
refine (((isLittleOTVS_one (𝕜 := 𝕜)).mpr h).smul_left f).congr' (h₀.mono fun x hx ↦ ?_) (by simp)

Result:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto (fun x => (f x)⁻¹ • g x) l (𝓝 0)
x : α
hx : f x = 0 → g x = 0
⊢ (fun x => f x • (f x)⁻¹ • g x) x = g x
-- Mathlib/Data/Int/Init.lean
protected lemma lt_asymm : a < b → ¬ b < a

Proof state:
a b : ℤ
⊢ a < b → ¬b < a

Tactic:
rw [Int.not_lt]

Result:
a b : ℤ
⊢ a < b → a ≤ b

Proof state:
a b : ℤ
⊢ a < b → a ≤ b

Tactic:
exact Int.le_of_lt

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem comp_compQuasiMeasurePreserving
    {β : Type*} [MeasurableSpace β] {ν} (g : γ → δ) (hg : Continuous g)
    (f : β →ₘ[ν] γ) {φ : α → β} (hφ : Measure.QuasiMeasurePreserving φ μ ν) :
    (comp g hg f).compQuasiMeasurePreserving φ hφ =
      comp g hg (f.compQuasiMeasurePreserving φ hφ)

Proof state:
case mk
α : Type u_1
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
ν : Measure β
g : γ → δ
hg : Continuous g
f : β →ₘ[ν] γ
φ : α → β
hφ : Measure.QuasiMeasurePreserving φ μ ν
a✝ : { f // AEStronglyMeasurable f ν }
⊢ (comp g hg (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝)).compQuasiMeasurePreserving φ hφ =
    comp g hg (compQuasiMeasurePreserving (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝) φ hφ)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
ν : Measure β
g : γ → δ
hg : Continuous g
f : β →ₘ[ν] γ
φ : α → β
hφ : Measure.QuasiMeasurePreserving φ μ ν
⊢ (comp g hg f).compQuasiMeasurePreserving φ hφ = comp g hg (f.compQuasiMeasurePreserving φ hφ)

Tactic:
rcases f

Result:
case mk
α : Type u_1
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
ν : Measure β
g : γ → δ
hg : Continuous g
f : β →ₘ[ν] γ
φ : α → β
hφ : Measure.QuasiMeasurePreserving φ μ ν
a✝ : { f // AEStronglyMeasurable f ν }
⊢ (comp g hg (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝)).compQuasiMeasurePreserving φ hφ =
    comp g hg (compQuasiMeasurePreserving (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝) φ hφ)
-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem aeval_zeta [IsDomain B] [NeZero ((n : ℕ) : B)] :
    aeval (zeta n A B) (cyclotomic n A) = 0

Proof state:
n : ℕ+
A : Type w
B : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsCyclotomicExtension {n} A B
inst✝¹ : IsDomain B
inst✝ : NeZero ↑↑n
⊢ IsPrimitiveRoot (zeta n A B) ↑n

Tactic:
exact zeta_spec n A B

Result:
no goals

Proof state:
n : ℕ+
A : Type w
B : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsCyclotomicExtension {n} A B
inst✝¹ : IsDomain B
inst✝ : NeZero ↑↑n
⊢ (aeval (zeta n A B)) (cyclotomic (↑n) A) = 0

Tactic:
rw [aeval_def, ← eval_map, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff]

Result:
n : ℕ+
A : Type w
B : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsCyclotomicExtension {n} A B
inst✝¹ : IsDomain B
inst✝ : NeZero ↑↑n
⊢ IsPrimitiveRoot (zeta n A B) ↑n
-- Mathlib/Topology/Order/Basic.lean
theorem nhdsGE_eq_iInf_inf_principal [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
    𝓝[≥] a = (⨅ (u) (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) = (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)

Tactic:
refine le_antisymm (inf_le_inf_right _ inf_le_right) (le_inf (le_inf ?_ inf_le_left) inf_le_right)

Result:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) ≤ ⨅ b ∈ Iio a, 𝓟 (Ioi b)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝[≥] a = (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)

Tactic:
rw [nhdsWithin, nhds_eq_order]

Result:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) = (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ (⨅ u, ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) ≤ ⨅ b ∈ Iio a, 𝓟 (Ioi b)

Tactic:
exact inf_le_right.trans (le_iInf₂ fun l hl => principal_mono.2 <| Ici_subset_Ioi.2 hl)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
lemma neg_modByMonic (p q : R[X]) : (-p) %ₘ q = - (p %ₘ q)

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
⊢ -p %ₘ q = -(p %ₘ q)

Tactic:
rw [eq_neg_iff_add_eq_zero, ← add_modByMonic, neg_add_cancel, zero_modByMonic]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem le_trans : ∀ {x y z : Bool}, x ≤ y → y ≤ z → x ≤ z

Proof state:
⊢ ∀ {x y z : Bool}, x ≤ y → y ≤ z → x ≤ z

Tactic:
decide

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem map_isCycle_iff_of_injective {p : G.Walk u u} (hinj : Function.Injective f) :
    (p.map f).IsCycle ↔ p.IsCycle

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective ⇑f
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle

Tactic:
rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, Ne, map_eq_nil_iff,
  support_map, ← List.map_tail, List.nodup_map_iff hinj]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem quotientEquivAlgOfEq_symm {I J : Ideal A} [I.IsTwoSided] [J.IsTwoSided] (h : I = J) :
    (quotientEquivAlgOfEq R₁ h).symm = quotientEquivAlgOfEq R₁ h.symm

Proof state:
case h
R₁ : Type u_1
A : Type u_3
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
I J : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
a✝ : A ⧸ J
⊢ (quotientEquivAlgOfEq R₁ h).symm a✝ = (quotientEquivAlgOfEq R₁ ⋯) a✝

Tactic:
rfl

Result:
no goals

Proof state:
R₁ : Type u_1
A : Type u_3
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
I J : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
⊢ (quotientEquivAlgOfEq R₁ h).symm = quotientEquivAlgOfEq R₁ ⋯

Tactic:
ext

Result:
case h
R₁ : Type u_1
A : Type u_3
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
I J : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
a✝ : A ⧸ J
⊢ (quotientEquivAlgOfEq R₁ h).symm a✝ = (quotientEquivAlgOfEq R₁ ⋯) a✝
-- Mathlib/Computability/Ackermann.lean
theorem not_nat_primrec_ack_self : ¬Nat.Primrec fun n => ack n n := fun h => by
  obtain ⟨m, hm⟩ := exists_lt_ack_of_nat_primrec h
  exact (hm m).false

Proof state:
case intro
h : Nat.Primrec fun n => ack n n
m : ℕ
hm : ∀ (n : ℕ), ack n n < ack m n
⊢ False

Tactic:
exact (hm m).false

Result:
no goals

Proof state:
h : Nat.Primrec fun n => ack n n
⊢ False

Tactic:
obtain ⟨m, hm⟩ := exists_lt_ack_of_nat_primrec h

Result:
case intro
h : Nat.Primrec fun n => ack n n
m : ℕ
hm : ∀ (n : ℕ), ack n n < ack m n
⊢ False
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma vanishingIdeal_irreducibleComponents :
    vanishingIdeal '' (irreducibleComponents <| PrimeSpectrum R) =
    minimalPrimes R

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ {x | Minimal (fun x => ∃ x₀, (IsClosed x₀ ∧ IsIrreducible x₀) ∧ vanishingIdeal x₀ = x) x} =
    {x | Minimal (Membership.mem (vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s})) x}

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_not_iff_right_iff_imp : ∀ {a b : Bool}, ((a || !b) = b) ↔ a ∧ b

Proof state:
⊢ ∀ {a b : Bool}, (a || !b) = b ↔ a = true ∧ b = true

Tactic:
decide

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_eq_aleph0 {c : Cardinal.{u}} : lift.{v} c = ℵ₀ ↔ c = ℵ₀

Proof state:
c : Cardinal.{u}
⊢ lift.{v, u} c = ℵ₀ ↔ c = ℵ₀

Tactic:
simpa using lift_inj (b := ℵ₀)

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyBijective.lean
lemma isLocallySurjective_presheafToSheaf_map_iff :
    Sheaf.IsLocallySurjective ((presheafToSheaf J A).map φ) ↔ IsLocallySurjective J φ

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : HasWeakSheafify J A
inst✝ : J.WEqualsLocallyBijective A
P Q : Cᵒᵖ ⥤ A
φ : P ⟶ Q
⊢ Sheaf.IsLocallySurjective ((presheafToSheaf J A).map φ) ↔ IsLocallySurjective J φ

Tactic:
rw [← Sheaf.isLocallySurjective_sheafToPresheaf_map_iff,
  ← isLocallySurjective_comp_iff J _ (toSheafify J Q),
  ← comp_isLocallySurjective_iff J (toSheafify J P),
  toSheafify_naturality, sheafToPresheaf_map]

Result:
no goals
-- Mathlib/Topology/UrysohnsLemma.lean
theorem lim_of_mem_C (c : CU P) (x : X) (h : x ∈ c.C) : c.lim x = 0

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
x : X
h : x ∈ c.C
⊢ c.lim x = 0

Tactic:
simp only [CU.lim, approx_of_mem_C, h, ciSup_const]

Result:
no goals