harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem ClosedComplemented.isClosed [IsTopologicalAddGroup M] [T1Space M]
    {p : Submodule R M} (h : ClosedComplemented p) : IsClosed (p : Set M)

Proof state:
case intro
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalAddGroup M
inst✝ : T1Space M
p : Submodule R M
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
this : LinearMap.ker (ContinuousLinearMap.id R M - p.subtypeL.comp f) = p
⊢ IsClosed ↑p

Tactic:
exact this ▸ isClosed_ker _

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalAddGroup M
inst✝ : T1Space M
p : Submodule R M
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ IsClosed ↑p

Tactic:
have : ker (id R M - p.subtypeL.comp f) = p := LinearMap.ker_id_sub_eq_of_proj hf

Result:
case intro
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalAddGroup M
inst✝ : T1Space M
p : Submodule R M
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
this : LinearMap.ker (ContinuousLinearMap.id R M - p.subtypeL.comp f) = p
⊢ IsClosed ↑p

Proof state:
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalAddGroup M
inst✝ : T1Space M
p : Submodule R M
h : p.ClosedComplemented
⊢ IsClosed ↑p

Tactic:
rcases h with ⟨f, hf⟩

Result:
case intro
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalAddGroup M
inst✝ : T1Space M
p : Submodule R M
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ IsClosed ↑p
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem ordered_iff {t : RBNode α} :
    t.Ordered cmp ↔ t.toList.Pairwise (cmpLT cmp)

Proof state:
α : Type u_1
cmp : α → α → Ordering
t : RBNode α
⊢ Ordered cmp t ↔ List.Pairwise (cmpLT cmp) t.toList

Tactic:
induction t with
| nil => simp
| node c l v r ihl ihr =>
  simp [*, List.pairwise_append, Ordered, All_def,
    and_assoc, and_left_comm, and_comm, imp_and, forall_and]
  exact fun _ _ hl hr a ha b hb => (hl _ ha).trans (hr _ hb)

Result:
no goals

Proof state:
case node
α : Type u_1
cmp : α → α → Ordering
c : RBColor
l : RBNode α
v : α
r : RBNode α
ihl : Ordered cmp l ↔ List.Pairwise (cmpLT cmp) l.toList
ihr : Ordered cmp r ↔ List.Pairwise (cmpLT cmp) r.toList
⊢ List.Pairwise (cmpLT cmp) l.toList →
    List.Pairwise (cmpLT cmp) r.toList →
      (∀ (x : α), x ∈ l → cmpLT cmp x v) →
        (∀ (a' : α), a' ∈ r → cmpLT cmp v a') → ∀ (x : α), x ∈ l → ∀ (a : α), a ∈ r → cmpLT cmp x a

Tactic:
exact fun _ _ hl hr a ha b hb => (hl _ ha).trans (hr _ hb)

Result:
no goals

Proof state:
case nil
α : Type u_1
cmp : α → α → Ordering
⊢ Ordered cmp nil ↔ List.Pairwise (cmpLT cmp) nil.toList

Tactic:
simp

Result:
no goals

Proof state:
case node
α : Type u_1
cmp : α → α → Ordering
c : RBColor
l : RBNode α
v : α
r : RBNode α
ihl : Ordered cmp l ↔ List.Pairwise (cmpLT cmp) l.toList
ihr : Ordered cmp r ↔ List.Pairwise (cmpLT cmp) r.toList
⊢ Ordered cmp (node c l v r) ↔ List.Pairwise (cmpLT cmp) (node c l v r).toList

Tactic:
simp [*, List.pairwise_append, Ordered, All_def,
  and_assoc, and_left_comm, and_comm, imp_and, forall_and]

Result:
case node
α : Type u_1
cmp : α → α → Ordering
c : RBColor
l : RBNode α
v : α
r : RBNode α
ihl : Ordered cmp l ↔ List.Pairwise (cmpLT cmp) l.toList
ihr : Ordered cmp r ↔ List.Pairwise (cmpLT cmp) r.toList
⊢ List.Pairwise (cmpLT cmp) l.toList →
    List.Pairwise (cmpLT cmp) r.toList →
      (∀ (x : α), x ∈ l → cmpLT cmp x v) →
        (∀ (a' : α), a' ∈ r → cmpLT cmp v a') → ∀ (x : α), x ∈ l → ∀ (a : α), a ∈ r → cmpLT cmp x a
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem hasDerivAt_mul_const (c : 𝕜) : HasDerivAt (fun x => x * c) c x

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x c : 𝕜
⊢ HasDerivAt (fun x => x * c) c x

Tactic:
simpa only [one_mul] using (hasDerivAt_id' x).mul_const c

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem succ_pos (a : Fin n) : (0 : Fin (n + 1)) < a.succ

Proof state:
n : Nat
a : Fin n
⊢ 0 < a.succ

Tactic:
simp [Fin.lt_def, Nat.succ_pos]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma preimage_zeroLocus {X Y : Scheme.{u}} (f : X ⟶ Y) {U : Y.Opens} (s : Set Γ(Y, U)) :
    f.base ⁻¹' Y.zeroLocus s = X.zeroLocus ((f.app U).hom '' s)

Proof state:
case h
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
s : Set ↑Γ(Y, U)
x✝ : ↑↑X.toPresheafedSpace
⊢ (∀ f_1 ∈ s, (ConcreteCategory.hom f.base) x✝ ∉ Y.basicOpen f_1) ↔ ∀ a ∈ s, x✝ ∉ f ⁻¹ᵁ Y.basicOpen a

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
s : Set ↑Γ(Y, U)
⊢ ⇑(ConcreteCategory.hom f.base) ⁻¹' Y.zeroLocus s = X.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.app f U)) '' s)

Tactic:
ext

Result:
case h
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
s : Set ↑Γ(Y, U)
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Y.zeroLocus s ↔ x✝ ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.app f U)) '' s)

Proof state:
case h
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
s : Set ↑Γ(Y, U)
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Y.zeroLocus s ↔ x✝ ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.app f U)) '' s)

Tactic:
simp [← Scheme.preimage_basicOpen]

Result:
case h
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
s : Set ↑Γ(Y, U)
x✝ : ↑↑X.toPresheafedSpace
⊢ (∀ f_1 ∈ s, (ConcreteCategory.hom f.base) x✝ ∉ Y.basicOpen f_1) ↔ ∀ a ∈ s, x✝ ∉ f ⁻¹ᵁ Y.basicOpen a
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_le_one : a⁻¹ ≤ 1 ↔ 1 ≤ a

Proof state:
a : ℝ≥0∞
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
rw [inv_le_iff_inv_le, inv_one]

Result:
no goals
-- Mathlib/Analysis/SumIntegralComparisons.lean
theorem AntitoneOn.integral_le_sum_Ico (hab : a ≤ b) (hf : AntitoneOn f (Set.Icc a b)) :
    (∫ x in a..b, f x) ≤ ∑ x ∈ Finset.Ico a b, f x

Proof state:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x ∈ Finset.range (b - a), f (↑a + ↑x)

Tactic:
apply AntitoneOn.integral_le_sum

Result:
case hf
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ AntitoneOn f (Icc (↑a) (↑a + ↑(b - a)))

Proof state:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x ∈ Finset.Ico (0 + a) (b - a + a), f ↑x

Tactic:
rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range]

Result:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x ∈ Finset.range (b - a), f ↑(a + x)

Proof state:
case hf
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ AntitoneOn f (Icc (↑a) (↑a + ↑(b - a)))

Tactic:
simp only [hf, hab, Nat.cast_sub, add_sub_cancel]

Result:
no goals

Proof state:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ x ∈ Finset.Ico a b, f ↑x

Tactic:
rw [(Nat.sub_add_cancel hab).symm, Nat.cast_add]

Result:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x ≤ ∑ x ∈ Finset.Ico a (b - a + a), f ↑x
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma sUnion_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
    ⋃₀ hC.disjointOfDiff hs ht = s \ t

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ⋃₀ ↑(hC.disjointOfDiff hs ht) = ⋃₀ ↑⋯.choose

Tactic:
simp only [disjointOfDiff, coe_sdiff, coe_singleton, diff_singleton_subset_iff]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ⋃₀ (↑⋯.choose \ {∅}) = ⋃₀ ↑⋯.choose

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ⋃₀ (↑⋯.choose \ {∅}) = ⋃₀ ↑⋯.choose

Tactic:
rw [sUnion_diff_singleton_empty]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ⋃₀ ↑(hC.disjointOfDiff hs ht) = s \ t

Tactic:
rw [(hC.diff_eq_sUnion' s hs t ht).choose_spec.2.2]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ⋃₀ ↑(hC.disjointOfDiff hs ht) = ⋃₀ ↑⋯.choose

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ⋃₀ ↑(hC.disjointOfDiff hs ht) = s \ t

Tactic:
classical
rw [(hC.diff_eq_sUnion' s hs t ht).choose_spec.2.2]
simp only [disjointOfDiff, coe_sdiff, coe_singleton, diff_singleton_subset_iff]
rw [sUnion_diff_singleton_empty]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Opposite.lean
theorem image_ι_op_comp_imageUnopOp_hom :
    (image.ι g.unop).op ≫ (imageUnopOp g).hom = factorThruImage g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ (image.ι g.unop).op ≫ (imageUnopOp g).hom = factorThruImage g

Tactic:
simp only [imageUnopOp, Iso.trans, Iso.symm, Iso.op, cokernelOpOp_inv, cokernelEpiComp_hom,
  cokernelCompIsIso_hom, Abelian.coimageIsoImage'_hom, ← Category.assoc, ← op_comp]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ (((((kernel.lift (cokernel.π g.unop) (cokernel.π (cokernel.π g.unop).op).unop ⋯ ≫
                  (Abelian.imageIsoImage g.unop).hom) ≫
                image.ι g.unop).op ≫
            (cokernelIsoOfEq ⋯).hom) ≫
          cokernel.desc ((cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom ⋯) (cokernel.π (kernel.ι g ≫ eqToHom ⋯)) ⋯) ≫
        cokernel.desc (kernel.ι g ≫ eqToHom ⋯) (inv (eqToHom ⋯) ≫ cokernel.π (kernel.ι g)) ⋯) ≫
      cokernel.desc (kernel.ι g) (factorThruImage g) ⋯ =
    factorThruImage g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (𝟙 A) ≫ factorThruImage g = factorThruImage g

Tactic:
rw [IsIso.inv_id, Category.id_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ (((((kernel.lift (cokernel.π g.unop) (cokernel.π (cokernel.π g.unop).op).unop ⋯ ≫
                  (Abelian.imageIsoImage g.unop).hom) ≫
                image.ι g.unop).op ≫
            (cokernelIsoOfEq ⋯).hom) ≫
          cokernel.desc ((cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom ⋯) (cokernel.π (kernel.ι g ≫ eqToHom ⋯)) ⋯) ≫
        cokernel.desc (kernel.ι g ≫ eqToHom ⋯) (inv (eqToHom ⋯) ≫ cokernel.π (kernel.ι g)) ⋯) ≫
      cokernel.desc (kernel.ι g) (factorThruImage g) ⋯ =
    factorThruImage g

Tactic:
simp only [Category.assoc, Abelian.imageIsoImage_hom_comp_image_ι, kernel.lift_ι,
  Quiver.Hom.op_unop, cokernelIsoOfEq_hom_comp_desc_assoc, cokernel.π_desc_assoc,
  cokernel.π_desc]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (eqToHom ⋯) ≫ factorThruImage g = factorThruImage g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (eqToHom ⋯) ≫ factorThruImage g = factorThruImage g

Tactic:
simp only [eqToHom_refl]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (𝟙 A) ≫ factorThruImage g = factorThruImage g
-- Mathlib/Data/Fin/Tuple/Basic.lean
lemma snoc_zero {α : Sort*} (p : Fin 0 → α) (x : α) :
    Fin.snoc p x = fun _ ↦ x

Proof state:
case h
α : Sort u_2
p : Fin 0 → α
x : α
y : Fin (0 + 1)
⊢ snoc p x y = x

Tactic:
have : Subsingleton (Fin (0 + 1)) := Fin.subsingleton_one

Result:
case h
α : Sort u_2
p : Fin 0 → α
x : α
y : Fin (0 + 1)
this : Subsingleton (Fin (0 + 1))
⊢ snoc p x y = x

Proof state:
α : Sort u_2
p : Fin 0 → α
x : α
⊢ snoc p x = fun x_1 => x

Tactic:
ext y

Result:
case h
α : Sort u_2
p : Fin 0 → α
x : α
y : Fin (0 + 1)
⊢ snoc p x y = x

Proof state:
case h
α : Sort u_2
p : Fin 0 → α
x : α
y : Fin (0 + 1)
this : Subsingleton (Fin (0 + 1))
⊢ snoc p x y = x

Tactic:
simp only [Subsingleton.elim y (Fin.last 0), snoc_last]

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem StrictConvexOn.sup (hf : StrictConvexOn 𝕜 s f) (hg : StrictConvexOn 𝕜 s g) :
    StrictConvexOn 𝕜 s (f ⊔ g) :=
  ⟨hf.left, fun x hx y hy hxy a b ha hb hab =>
    max_lt
      (calc
        f (a • x + b • y) < a • f x + b • f y := hf.2 hx hy hxy ha hb hab
        _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • g x + b • g y ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y)

Tactic:
gcongr <;> apply le_sup_right

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y)

Tactic:
gcongr <;> apply le_sup_left

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Tor.lean
/-- The higher `Tor` groups for `X` and `Y` are zero if `Y` is projective. -/
lemma isZero_Tor_succ_of_projective (X Y : C) [Projective Y] (n : ℕ) :
    IsZero (((Tor C (n + 1)).obj X).obj Y)

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : MonoidalCategory C
inst✝³ : Abelian C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasProjectiveResolutions C
X Y : C
inst✝ : Projective Y
n : ℕ
⊢ IsZero (((Tor C (n + 1)).obj X).obj Y)

Tactic:
apply Functor.isZero_leftDerived_obj_projective_succ

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean
theorem IsLimit.pushout_zero_ext [HasZeroMorphisms C] [HasPushouts C] [HasLimitsOfShape J C]
    [HasExactLimitsOfShape J C] {F : J ⥤ C} {c : Cone F} (hc : IsLimit c) {X Y : C}
    {g : Y ⟶ c.pt} {f : c.pt ⟶ X} (hf : ∀ j, g ≫ f ≫ pushout.inr (c.π.app j) f = 0) :
    g ≫ f = 0

Proof state:
J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = 0
⊢ g ≫ f = 0

Tactic:
suffices g ≫ f = 0 ≫ f by simpa

Result:
J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = 0
⊢ g ≫ f = 0 ≫ f

Proof state:
J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = 0
this : g ≫ f = 0 ≫ f
⊢ g ≫ f = 0

Tactic:
simpa

Result:
no goals

Proof state:
J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = 0
⊢ ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = 0 ≫ f ≫ pushout.inr (c.π.app j) f

Tactic:
simpa using hf

Result:
no goals

Proof state:
J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = 0
⊢ g ≫ f = 0 ≫ f

Tactic:
exact hc.pushout_hom_ext (by simpa using hf)

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem units_pow_card_sub_one_eq_one (p : ℕ) [Fact p.Prime] (a : (ZMod p)ˣ) : a ^ (p - 1) = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : (ZMod p)ˣ
⊢ a ^ (p - 1) = 1

Tactic:
rw [← card_units p, pow_card_eq_one]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.comp_linearIsometry {v : ι → E} (hv : Orthonormal 𝕜 v) (f : E →ₗᵢ[𝕜] E') :
    Orthonormal 𝕜 (f ∘ v)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
v : ι → E
hv : Orthonormal 𝕜 v
f : E →ₗᵢ[𝕜] E'
⊢ Orthonormal 𝕜 (⇑f ∘ v)

Tactic:
rwa [f.orthonormal_comp_iff]

Result:
no goals
-- Mathlib/Algebra/DirectSum/LinearMap.lean
/-- If `f` and `g` are commuting endomorphisms of a finite, free `R`-module `M`, such that `f`
is triangularizable, then to prove that the trace of `g ∘ f` vanishes, it is sufficient to prove
that the trace of `g` vanishes on each generalized eigenspace of `f`. -/
lemma trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero
    [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M]
    {f g : Module.End R M}
    (h_comm : Commute f g)
    (hf : ⨆ μ, f.maxGenEigenspace μ = ⊤)
    (hg : ∀ μ, trace R _ (g.restrict (f.mapsTo_maxGenEigenspace_of_comm h_comm μ)) = 0) :
    trace R _ (g ∘ₗ f) = 0

Proof state:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
this : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
⊢ (trace R M) (g ∘ₗ f) = 0

Tactic:
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
  f.independent_maxGenEigenspace hf

Result:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
this : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
hds : IsInternal f.maxGenEigenspace
⊢ (trace R M) (g ∘ₗ f) = 0

Proof state:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
⊢ (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0

Tactic:
replace h_comm : Commute (g.restrict (f.mapsTo_maxGenEigenspace_of_comm h_comm μ))
    (f.restrict (f.mapsTo_maxGenEigenspace_of_comm rfl μ)) :=
  restrict_commute h_comm.symm _ _

Result:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f g : Module.End R M
h_comm✝ : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
⊢ (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
-- Mathlib/Data/Complex/Basic.lean
theorem re_eq_add_conj (z : ℂ) : (z.re : ℂ) = (z + conj z) / 2

Proof state:
z : ℂ
⊢ ↑z.re = (z + (starRingEnd ℂ) z) / 2

Tactic:
simp only [add_conj, ofReal_mul, ofReal_ofNat, mul_div_cancel_left₀ (z.re : ℂ) two_ne_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem measurableSet_eq_fun {m : MeasurableSpace α} {E} [MeasurableSpace E] [AddGroup E]
    [MeasurableSingletonClass E] [MeasurableSub₂ E] {f g : α → E} (hf : Measurable f)
    (hg : Measurable g) : MeasurableSet { x | f x = g x }

Proof state:
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
h_set_eq : {x | f x = g x} = {x | (f - g) x = 0}
⊢ MeasurableSet {x | f x = g x}

Tactic:
rw [h_set_eq]

Result:
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
h_set_eq : {x | f x = g x} = {x | (f - g) x = 0}
⊢ MeasurableSet {x | (f - g) x = 0}

Proof state:
case h
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
x✝ : α
⊢ x✝ ∈ {x | f x = g x} ↔ x✝ ∈ {x | (f - g) x = 0}

Tactic:
simp_rw [Set.mem_setOf_eq, Pi.sub_apply, sub_eq_zero]

Result:
no goals

Proof state:
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
⊢ MeasurableSet {x | f x = g x}

Tactic:
suffices h_set_eq : { x : α | f x = g x } = { x | (f - g) x = (0 : E) } by
  rw [h_set_eq]
  exact (hf.sub hg) measurableSet_eq

Result:
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
⊢ {x | f x = g x} = {x | (f - g) x = 0}

Proof state:
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
h_set_eq : {x | f x = g x} = {x | (f - g) x = 0}
⊢ MeasurableSet {x | (f - g) x = 0}

Tactic:
exact (hf.sub hg) measurableSet_eq

Result:
no goals

Proof state:
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
⊢ {x | f x = g x} = {x | (f - g) x = 0}

Tactic:
ext

Result:
case h
α : Type u_3
m : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
x✝ : α
⊢ x✝ ∈ {x | f x = g x} ↔ x✝ ∈ {x | (f - g) x = 0}
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mod_lt (a) {b : Ordinal} (h : b ≠ 0) : a % b < b :=
  (add_lt_add_iff_left (b * (a / b))).1 <| by rw [div_add_mod]; exact lt_mul_div_add a h

Proof state:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ b * (a / b) + a % b < b * (a / b) + b

Tactic:
rw [div_add_mod]

Result:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * (a / b) + b

Proof state:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * (a / b) + b

Tactic:
exact lt_mul_div_add a h

Result:
no goals