harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem inf_factors {A B : C} {X Y : Subobject B} (f : A ⟶ B) :
    (X ⊓ Y).Factors f ↔ X.Factors f ∧ Y.Factors f :=
  ⟨fun h => ⟨factors_left_of_inf_factors h, factors_right_of_inf_factors h⟩, by
    revert X Y
    apply Quotient.ind₂'
    rintro X Y ⟨⟨g₁, rfl⟩, ⟨g₂, hg₂⟩⟩
    exact ⟨_, pullback.lift_snd_assoc _ _ hg₂ _⟩⟩

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
⊢ ∀ (a₁ a₂ : MonoOver B),
    Factors (Quotient.mk'' a₁) f ∧ Factors (Quotient.mk'' a₂) f → (Quotient.mk'' a₁ ⊓ Quotient.mk'' a₂).Factors f

Tactic:
rintro X Y ⟨⟨g₁, rfl⟩, ⟨g₂, hg₂⟩⟩

Result:
case h.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A B : C
X Y : MonoOver B
g₁ : A ⟶ X.obj.left
g₂ : A ⟶ Y.obj.left
hg₂ : g₂ ≫ Y.arrow = g₁ ≫ X.arrow
⊢ (Quotient.mk'' X ⊓ Quotient.mk'' Y).Factors (g₁ ≫ X.arrow)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
⊢ ∀ {X Y : Subobject B}, X.Factors f ∧ Y.Factors f → (X ⊓ Y).Factors f

Tactic:
apply Quotient.ind₂'

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
⊢ ∀ (a₁ a₂ : MonoOver B),
    Factors (Quotient.mk'' a₁) f ∧ Factors (Quotient.mk'' a₂) f → (Quotient.mk'' a₁ ⊓ Quotient.mk'' a₂).Factors f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A B : C
X Y : Subobject B
f : A ⟶ B
⊢ X.Factors f ∧ Y.Factors f → (X ⊓ Y).Factors f

Tactic:
revert X Y

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
⊢ ∀ {X Y : Subobject B}, X.Factors f ∧ Y.Factors f → (X ⊓ Y).Factors f

Proof state:
case h.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A B : C
X Y : MonoOver B
g₁ : A ⟶ X.obj.left
g₂ : A ⟶ Y.obj.left
hg₂ : g₂ ≫ Y.arrow = g₁ ≫ X.arrow
⊢ (Quotient.mk'' X ⊓ Quotient.mk'' Y).Factors (g₁ ≫ X.arrow)

Tactic:
exact ⟨_, pullback.lift_snd_assoc _ _ hg₂ _⟩

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_star : birthday star = 1

Proof state:
⊢ ((lsub fun i => (star.moveLeft i).birthday) ⊔ lsub fun i => (star.moveRight i).birthday) = 1

Tactic:
simp

Result:
no goals

Proof state:
⊢ star.birthday = 1

Tactic:
rw [birthday_def]

Result:
⊢ ((lsub fun i => (star.moveLeft i).birthday) ⊔ lsub fun i => (star.moveRight i).birthday) = 1
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrixAlgEquiv_apply (f : M₁ →ₗ[R] M₁) (i j : n) :
    LinearMap.toMatrixAlgEquiv v₁ f i j = v₁.repr (f (v₁ j)) i

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
i j : n
⊢ (toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i

Tactic:
simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Sub.lean
@[simp]
protected lemma add_sub_cancel [IsFiniteMeasure ν] : μ + ν - ν = μ

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ (μ + ν - ν) s = μ s

Tactic:
rw [sub_apply hs (Measure.le_add_left (le_refl _)), add_apply,
  ENNReal.add_sub_cancel_right (measure_ne_top ν s)]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ μ + ν - ν = μ

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ (μ + ν - ν) s = μ s
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem IsNormal.apply_lt_nfp (H : IsNormal f) {a b} : f b < nfp f a ↔ b < nfp f a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfpFamily (fun x => f) a ↔ Unit → f b < nfpFamily (fun x => f) a

Tactic:
exact ⟨fun h _ => h, fun h => h Unit.unit⟩

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfp f a ↔ b < nfp f a

Tactic:
unfold nfp

Result:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfpFamily (fun x => f) a ↔ b < nfpFamily (fun x => f) a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfpFamily (fun x => f) a ↔ b < nfpFamily (fun x => f) a

Tactic:
rw [← @apply_lt_nfpFamily_iff Unit (fun _ => f) _ _ (fun _ => H) a b]

Result:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfpFamily (fun x => f) a ↔ Unit → f b < nfpFamily (fun x => f) a
-- Mathlib/Data/List/SplitLengths.lean
@[simp]
lemma splitLengths_cons (n : ℕ) :
    (n :: sz).splitLengths l = l.take n :: sz.splitLengths (l.drop n)

Proof state:
α : Type u_1
l : List α
sz : List ℕ
n : ℕ
⊢ (n :: sz).splitLengths l = take n l :: sz.splitLengths (drop n l)

Tactic:
simp [splitLengths]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
lemma arg_exp_mul_I (θ : ℝ) :
    arg (exp (θ * I)) = toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ

Proof state:
θ : ℝ
⊢ toIocMod ⋯ (-π) θ ∈ Ioc (-π) π

Tactic:
convert toIocMod_mem_Ioc _ _ _

Result:
case h.e'_4.h.e'_4
θ : ℝ
⊢ π = -π + 2 * π

Proof state:
θ : ℝ
⊢ (cexp (↑θ * I)).arg = toIocMod ⋯ (-π) θ

Tactic:
convert arg_cos_add_sin_mul_I (θ := toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ) _ using 2

Result:
case h.e'_2.h.e'_1
θ : ℝ
⊢ cexp (↑θ * I) = cos ↑(toIocMod ⋯ (-π) θ) + sin ↑(toIocMod ⋯ (-π) θ) * I

θ : ℝ
⊢ toIocMod ⋯ (-π) θ ∈ Ioc (-π) π

Proof state:
case h.e'_4.h.e'_4
θ : ℝ
⊢ π = -π + 2 * π

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_2.h.e'_1
θ : ℝ
⊢ cexp (↑θ * I) = cos ↑(toIocMod ⋯ (-π) θ) + sin ↑(toIocMod ⋯ (-π) θ) * I

Tactic:
rw [← exp_mul_I, eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
  ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_intCast (x : ℂ) (n : ℤ) : x ^ (n : ℂ) = x ^ n

Proof state:
x : ℂ
n : ℤ
⊢ x ^ ↑n = x ^ n

Tactic:
simpa using cpow_int_mul x n 1

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem X_ne_zero [Nontrivial R] : (X : R⟦X⟧) ≠ 0 := fun H => by
  simpa only [coeff_one_X, one_ne_zero, map_zero] using congr_arg (coeff R 1) H

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
H : X = 0
⊢ False

Tactic:
simpa only [coeff_one_X, one_ne_zero, map_zero] using congr_arg (coeff R 1) H

Result:
no goals
-- Mathlib/Algebra/Algebra/Tower.lean
theorem smul_mem_span_smul' {s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S} {x : A}
    (hx : x ∈ span R (s • t)) : k • x ∈ span R (s • t)

Proof state:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ restrictScalars R (span S t)
⊢ k • x ∈ restrictScalars R (span S t)

Tactic:
exact (span S t).smul_mem k hx

Result:
no goals

Proof state:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ span R (s • t)
⊢ k • x ∈ span R (s • t)

Tactic:
rw [span_smul_of_span_eq_top hs] at hx ⊢

Result:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ restrictScalars R (span S t)
⊢ k • x ∈ restrictScalars R (span S t)
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bddAbove_range {ι : Type u} (f : ι → Ordinal.{max u v}) : BddAbove (Set.range f) :=
  ⟨(iSup (succ ∘ card ∘ f)).ord, by
    rintro a ⟨i, rfl⟩
    exact le_of_lt (Cardinal.lt_ord.2 ((lt_succ _).trans_le
      (le_ciSup (Cardinal.bddAbove_range _) _)))⟩

Proof state:
case intro
ι : Type u
f : ι → Ordinal.{max u v}
i : ι
⊢ f i ≤ (iSup (succ ∘ card ∘ f)).ord

Tactic:
exact le_of_lt (Cardinal.lt_ord.2 ((lt_succ _).trans_le
  (le_ciSup (Cardinal.bddAbove_range _) _)))

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (iSup (succ ∘ card ∘ f)).ord ∈ upperBounds (range f)

Tactic:
rintro a ⟨i, rfl⟩

Result:
case intro
ι : Type u
f : ι → Ordinal.{max u v}
i : ι
⊢ f i ≤ (iSup (succ ∘ card ∘ f)).ord
-- Mathlib/Algebra/Lie/SkewAdjoint.lean
theorem skewAdjointMatricesLieSubalgebraEquiv_apply (P : Matrix n n R) (h : Invertible P)
    (A : skewAdjointMatricesLieSubalgebra J) :
    ↑(skewAdjointMatricesLieSubalgebraEquiv J P h A) = P⁻¹ * A * P

Proof state:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
A : ↥(skewAdjointMatricesLieSubalgebra J)
⊢ ↑((skewAdjointMatricesLieSubalgebraEquiv J P h) A) = P⁻¹ * ↑A * P

Tactic:
simp [skewAdjointMatricesLieSubalgebraEquiv]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem neg_pi_lt_log_im (x : ℂ) : -π < (log x).im

Proof state:
x : ℂ
⊢ -π < (log x).im

Tactic:
simp only [log_im, neg_pi_lt_arg]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean
lemma map_top_submodule {R : Type*} [Semiring R] [AddCommGroup E] [Module R E] :
    (⊤ : Submodule R E).map (linearEquiv R E).symm = ⊤

Proof state:
case h
E : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
x : C⋆ᵐᵒᵈ E
⊢ x ∈ Submodule.map (linearEquiv R E).symm ⊤ ↔ x ∈ ⊤

Tactic:
refine ⟨fun _  => trivial, fun _ => ?_⟩

Result:
case h
E : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
x : C⋆ᵐᵒᵈ E
x✝ : x ∈ ⊤
⊢ x ∈ Submodule.map (linearEquiv R E).symm ⊤

Proof state:
case h
E : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
x : C⋆ᵐᵒᵈ E
x✝ : x ∈ ⊤
⊢ ∃ y ∈ ⊤, (linearEquiv R E).symm y = x

Tactic:
exact ⟨linearEquiv R E x, by simp⟩

Result:
no goals

Proof state:
case h
E : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
x : C⋆ᵐᵒᵈ E
x✝ : x ∈ ⊤
⊢ x ∈ Submodule.map (linearEquiv R E).symm ⊤

Tactic:
rw [Submodule.mem_map]

Result:
case h
E : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
x : C⋆ᵐᵒᵈ E
x✝ : x ∈ ⊤
⊢ ∃ y ∈ ⊤, (linearEquiv R E).symm y = x

Proof state:
E : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
⊢ Submodule.map (linearEquiv R E).symm ⊤ = ⊤

Tactic:
ext x

Result:
case h
E : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
x : C⋆ᵐᵒᵈ E
⊢ x ∈ Submodule.map (linearEquiv R E).symm ⊤ ↔ x ∈ ⊤

Proof state:
E : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
x : C⋆ᵐᵒᵈ E
x✝ : x ∈ ⊤
⊢ (linearEquiv R E) x ∈ ⊤ ∧ (linearEquiv R E).symm ((linearEquiv R E) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma InjOn.prodMap (h₁ : s₁.InjOn f₁) (h₂ : s₂.InjOn f₂) :
    (s₁ ×ˢ s₂).InjOn fun x ↦ (f₁ x.1, f₂ x.2) :=
  fun x hx y hy ↦ by simp_rw [Prod.ext_iff]; exact And.imp (h₁ hx.1 hy.1) (h₂ hx.2 hy.2)

Proof state:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ (fun x => (f₁ x.1, f₂ x.2)) x = (fun x => (f₁ x.1, f₂ x.2)) y → x = y

Tactic:
simp_rw [Prod.ext_iff]

Result:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ f₁ x.1 = f₁ y.1 ∧ f₂ x.2 = f₂ y.2 → x.1 = y.1 ∧ x.2 = y.2

Proof state:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ f₁ x.1 = f₁ y.1 ∧ f₂ x.2 = f₂ y.2 → x.1 = y.1 ∧ x.2 = y.2

Tactic:
exact And.imp (h₁ hx.1 hy.1) (h₂ hx.2 hy.2)

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem interior_frontier (h : IsClosed s) : interior (frontier s) = ∅

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (frontier s) = ∅

Tactic:
have B : interior (frontier s) ⊆ interior s := by rw [A]; exact interior_mono diff_subset

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
⊢ interior (frontier s) = ∅

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (s \ interior s) ⊆ interior s

Tactic:
exact interior_mono diff_subset

Result:
no goals

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
⊢ interior (frontier s) = ∅

Tactic:
have A : frontier s = s \ interior s := h.frontier_eq

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (frontier s) = ∅

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (frontier s) ⊆ interior s

Tactic:
rw [A]

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (s \ interior s) ⊆ interior s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
⊢ interior (frontier s) ⊆ s \ interior s

Tactic:
simpa [A] using C

Result:
no goals

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
⊢ interior (frontier s) = ∅

Tactic:
have : interior (frontier s) ⊆ interior s ∩ (s \ interior s) :=
  subset_inter B (by simpa [A] using C)

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
this : interior (frontier s) ⊆ interior s ∩ (s \ interior s)
⊢ interior (frontier s) = ∅

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
⊢ interior (frontier s) = ∅

Tactic:
have C : interior (frontier s) ⊆ frontier s := interior_subset

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
⊢ interior (frontier s) = ∅

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
this : interior (frontier s) ⊆ interior s ∩ (s \ interior s)
⊢ interior (frontier s) = ∅

Tactic:
rwa [inter_diff_self, subset_empty_iff] at this

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean
@[simp]
lemma CategoryTheory.LocallyDiscrete.eqToHom_toLoc {C : Type u} [Category.{v} C] {a b : C}
    (h : a = b) : (eqToHom h).toLoc = eqToHom (congrArg LocallyDiscrete.mk h)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
a b : C
h : a = b
⊢ (eqToHom h).toLoc = eqToHom ⋯

Tactic:
subst h

Result:
C : Type u
inst✝ : Category.{v, u} C
a : C
⊢ (eqToHom ⋯).toLoc = eqToHom ⋯

Proof state:
C : Type u
inst✝ : Category.{v, u} C
a : C
⊢ (eqToHom ⋯).toLoc = eqToHom ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
lemma dynEntourage_comp_subset (T : X → X) (U V : Set (X × X)) (n : ℕ) :
    (dynEntourage T U n) ○ (dynEntourage T V n) ⊆ dynEntourage T (U ○ V) n

Proof state:
case intro.intro
X : Type u_1
T : X → X
U V : Set (X × X)
n k : ℕ
k_n : k < n
xy : X × X
z : X
hz1 : ∀ i < n, (T^[i] xy.1, T^[i] z) ∈ U
hz2 : ∀ i < n, (T^[i] z, T^[i] xy.2) ∈ V
⊢ ∃ z, ((map T^[k] T^[k] xy).1, z) ∈ U ∧ (z, (map T^[k] T^[k] xy).2) ∈ V

Tactic:
exact mem_ball_comp (hz1 k k_n) (hz2 k k_n)

Result:
no goals

Proof state:
X : Type u_1
T : X → X
U V : Set (X × X)
n : ℕ
⊢ dynEntourage T U n ○ dynEntourage T V n ⊆ dynEntourage T (U ○ V) n

Tactic:
simp only [dynEntourage, map_iterate, subset_iInter_iff]

Result:
X : Type u_1
T : X → X
U V : Set (X × X)
n : ℕ
⊢ ∀ i < n,
    (⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U) ○ ⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V ⊆
      map T^[i] T^[i] ⁻¹' (U ○ V)

Proof state:
X : Type u_1
T : X → X
U V : Set (X × X)
n k : ℕ
k_n : k < n
xy : X × X
xy_comp : xy ∈ (⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U) ○ ⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V
⊢ xy ∈ map T^[k] T^[k] ⁻¹' (U ○ V)

Tactic:
simp only [compRel, mem_iInter, mem_preimage, map_apply, mem_setOf_eq] at xy_comp ⊢

Result:
X : Type u_1
T : X → X
U V : Set (X × X)
n k : ℕ
k_n : k < n
xy : X × X
xy_comp : ∃ z, (∀ i < n, (T^[i] xy.1, T^[i] z) ∈ U) ∧ ∀ i < n, (T^[i] z, T^[i] xy.2) ∈ V
⊢ ∃ z, ((map T^[k] T^[k] xy).1, z) ∈ U ∧ (z, (map T^[k] T^[k] xy).2) ∈ V

Proof state:
X : Type u_1
T : X → X
U V : Set (X × X)
n k : ℕ
k_n : k < n
xy : X × X
xy_comp : ∃ z, (∀ i < n, (T^[i] xy.1, T^[i] z) ∈ U) ∧ ∀ i < n, (T^[i] z, T^[i] xy.2) ∈ V
⊢ ∃ z, ((map T^[k] T^[k] xy).1, z) ∈ U ∧ (z, (map T^[k] T^[k] xy).2) ∈ V

Tactic:
rcases xy_comp with ⟨z, hz1, hz2⟩

Result:
case intro.intro
X : Type u_1
T : X → X
U V : Set (X × X)
n k : ℕ
k_n : k < n
xy : X × X
z : X
hz1 : ∀ i < n, (T^[i] xy.1, T^[i] z) ∈ U
hz2 : ∀ i < n, (T^[i] z, T^[i] xy.2) ∈ V
⊢ ∃ z, ((map T^[k] T^[k] xy).1, z) ∈ U ∧ (z, (map T^[k] T^[k] xy).2) ∈ V

Proof state:
X : Type u_1
T : X → X
U V : Set (X × X)
n : ℕ
⊢ ∀ i < n,
    (⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U) ○ ⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V ⊆
      map T^[i] T^[i] ⁻¹' (U ○ V)

Tactic:
intro k k_n xy xy_comp

Result:
X : Type u_1
T : X → X
U V : Set (X × X)
n k : ℕ
k_n : k < n
xy : X × X
xy_comp : xy ∈ (⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U) ○ ⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' V
⊢ xy ∈ map T^[k] T^[k] ⁻¹' (U ○ V)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/HashMap/Lemmas.lean
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k ∈ m.insert k v

Proof state:
α : Type u
β : Type v
x✝¹ : BEq α
x✝ : Hashable α
m : HashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
v : β
⊢ k ∈ m.insert k v

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lex_asymm {r : α → α → Prop}
    (h : ∀ {x y : α}, r x y → ¬ r y x) : ∀ {l₁ l₂ : List α}, Lex r l₁ l₂ → ¬ Lex r l₂ l₁
  | nil, _, .nil => by simp
  | x :: l₁, y :: l₂, .rel h₁ =>
    fun
    | .rel h₂ => h h₁ h₂
    | .cons h₂ => h h₁ h₁
  | x :: l₁, _ :: l₂, .cons h₁ =>
    fun
    | .rel h₂ => h h₂ h₂
    | .cons h₂ => lex_asymm h h₁ h₂

Proof state:
α : Type u_1
r : α → α → Prop
h : ∀ {x y : α}, r x y → ¬r y x
a✝ : α
l✝ : List α
⊢ ¬Lex r (a✝ :: l✝) []

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l : Vector α n) (H) :
    pmap f l H = l.attach.map fun x => f x.1 (H _ x.2)

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
⊢ pmap f { toArray := l, size_toArray := ⋯ } H = map (fun x => f x.val ⋯) { toArray := l, size_toArray := ⋯ }.attach

Tactic:
simp only [pmap_mk, Array.pmap_eq_map_attach, attach_mk, map_mk, eq_mk]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
⊢ Array.map (fun x => f x.val ⋯) l.attach =
    Array.map (fun x => f x.val ⋯) (l.attachWith (fun x => x ∈ { toArray := l, size_toArray := ⋯ }) ⋯)

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
⊢ Array.pmap (fun a h => f ⟨a, h⟩.val ⋯) l ⋯ = Array.pmap (fun a h => f ⟨a, ⋯⟩.val ⋯) l ⋯

Tactic:
ext i hi₁ hi₂ <;> simp

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
⊢ Array.map (fun x => f x.val ⋯) l.attach =
    Array.map (fun x => f x.val ⋯) (l.attachWith (fun x => x ∈ { toArray := l, size_toArray := ⋯ }) ⋯)

Tactic:
rw [Array.map_attach, Array.map_attachWith]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
⊢ Array.pmap (fun a h => f ⟨a, h⟩.val ⋯) l ⋯ = Array.pmap (fun a h => f ⟨a, ⋯⟩.val ⋯) l ⋯

Proof state:
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : (a : α) → p a → β
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
⊢ pmap f l H = map (fun x => f x.val ⋯) l.attach

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
⊢ pmap f { toArray := l, size_toArray := ⋯ } H = map (fun x => f x.val ⋯) { toArray := l, size_toArray := ⋯ }.attach
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo
    {p : Submodule R M} (f g : End R M) (hf : MapsTo f p p) (hg : MapsTo g p p) {μ₁ μ₂ : R}
    (h : MapsTo f (g.maxGenEigenspace μ₁) (g.maxGenEigenspace μ₂)) :
    MapsTo (f.restrict hf)
      (maxGenEigenspace (g.restrict hg) μ₁)
      (maxGenEigenspace (g.restrict hg) μ₂)

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
x : ↥p
hx : x ∈ ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₁)
⊢ (LinearMap.restrict f hf) x ∈ ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₂)

Tactic:
simp_rw [SetLike.mem_coe, mem_maxGenEigenspace, ← LinearMap.restrict_smul_one _,
  LinearMap.restrict_sub _, LinearMap.pow_restrict _, LinearMap.restrict_apply,
  Submodule.mk_eq_zero, ← mem_maxGenEigenspace] at hx ⊢

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
x : ↥p
hx : ↑x ∈ g.maxGenEigenspace μ₁
⊢ f ↑x ∈ g.maxGenEigenspace μ₂

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
x : ↥p
hx : ↑x ∈ g.maxGenEigenspace μ₁
⊢ f ↑x ∈ g.maxGenEigenspace μ₂

Tactic:
exact h hx

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
⊢ MapsTo ⇑(LinearMap.restrict f hf) ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₁)
    ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₂)

Tactic:
intro x hx

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
x : ↥p
hx : x ∈ ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₁)
⊢ (LinearMap.restrict f hf) x ∈ ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₂)